# Theory Term_Utils

theory Term_Utils
imports
"HOL-Library.Finite_Map"
begin

fun map2 where
"map2 f (x # xs) (y # ys) = f x y # map2 f xs ys" |
"map2 _ _ _ = []"

lemma map2_elemE:
assumes "z ∈ set (map2 f xs ys)"
obtains x y where "x ∈ set xs" "y ∈ set ys" "z = f x y"
using assms by (induct f xs ys rule: map2.induct) auto

lemma map2_elemE1:
assumes "length xs = length ys" "x ∈ set xs"
obtains y where "y ∈ set ys" "f x y ∈ set (map2 f xs ys)"
using assms by (induct xs ys rule: list_induct2) auto

lemma map2_elemE2:
assumes "length xs = length ys" "y ∈ set ys"
obtains x where "x ∈ set xs" "f x y ∈ set (map2 f xs ys)"
using assms by (induct xs ys rule: list_induct2) auto

lemma map2_cong[fundef_cong]:
assumes "xs1 = xs2" "ys1 = ys2"
assumes fg: "⋀x y. x ∈ set xs1 ⟹ y ∈ set ys1 ⟹ f x y = g x y"
shows "map2 f xs1 ys1 = map2 g xs2 ys2"
proof -
have "map2 f xs1 ys1 = map2 g xs1 ys1"
using fg
by (induction f xs1 ys1 rule: map2.induct) auto
with assms show ?thesis
by simp
qed

lemma option_bindE:
assumes "x ⤜ f = Some a"
obtains x' where "x = Some x'"  "f x' = Some a"
using assms
by (cases x) auto

lemma rel_option_bind[intro]:
assumes "rel_option R x y" "⋀a b. R a b ⟹ rel_option R (f a) (g b)"
shows "rel_option R (x ⤜ f) (y ⤜ g)"
using assms(1) proof (cases rule: option.rel_cases)
case None
thus ?thesis
by simp
next
case (Some a b)
thus ?thesis
using assms(2) by simp
qed

lemma list_split:
assumes "n < length xs"
obtains xs⇩1 xs⇩2 where "xs = xs⇩1 @ xs⇩2" "n = length xs⇩2" "0 < length xs⇩1"
proof
let ?xs⇩1 = "take (length xs - n) xs"
let ?xs⇩2 = "drop (length xs - n) xs"

show "xs = ?xs⇩1 @ ?xs⇩2"
by simp
show "n = length ?xs⇩2" "0 < length ?xs⇩1"
using assms by auto
qed

context
includes fset.lifting
begin

lemma ffUnion_alt_def: "x |∈| ffUnion A ⟷ fBex A (λX. x |∈| X)"
by transfer blast

lemma funion_image_bind_eq: "ffUnion (f || M) = fbind M f"
by transfer auto

lemma fbind_funion: "fbind (M |∪| N) f = fbind M f |∪| fbind N f"
by transfer' auto

lemma ffUnion_least: "fBall A (λX. X |⊆| C) ⟹ ffUnion A |⊆| C"
by transfer blast

lemma fbind_iff: "x |∈| fbind S f ⟷ (∃s. x |∈| f s ∧ s |∈| S)"
by transfer' auto

lemma fBall_pred_weaken: "(⋀x. x |∈| M ⟹ P x ⟹ Q x) ⟹ fBall M P ⟹ fBall M Q"
by auto

end

lemma fmmap_fmupd[simp]:
"fmmap f (fmupd k v m) = fmupd k (f v) (fmmap f m)"
apply (rule fmap_ext)
by auto

definition fmlookup_default :: "('a, 'b) fmap ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" where
"fmlookup_default m f x = (case fmlookup m x of None ⇒ f x | Some b ⇒ b)"

end


# Theory Find_First

theory Find_First
imports
"HOL-Library.Finite_Map"
"List-Index.List_Index"
begin

fun find_first :: "'a ⇒ 'a list ⇒ nat option" where
"find_first _ [] = None" |
"find_first x (y # ys) = (if x = y then Some 0 else map_option Suc (find_first x ys))"

lemma find_first_correct:
assumes "find_first x xs = Some i"
shows "i < length xs" "xs ! i = x" "x ∉ set (take i xs)"
using assms
proof (induction xs arbitrary: i)
case (Cons y ys)
{ case 1 with Cons show ?case by (cases "x = y") auto }
{ case 2 with Cons show ?case by (cases "x = y") auto }
{ case 3 with Cons show ?case by (cases "x = y") auto }
qed auto

lemma find_first_none: "x ∉ set xs ⟹ find_first x xs = None"
by (induct xs) auto

lemma find_first_some_strong:
assumes "x ∈ set (take n xs)" "n ≤ length xs"
obtains i where "find_first x xs = Some i" "i < n"
using assms
proof (induction xs arbitrary: thesis n)
case (Cons y ys)
show ?case
proof (cases "x = y")
case True
show ?thesis
proof (rule Cons.prems)
show "find_first x (y # ys) = Some 0"
unfolding ‹x = y› by simp
next
show "0 < n"
using Cons by (metis length_pos_if_in_set length_take min.absorb2)
qed
next
case False
show ?thesis
proof (rule Cons.IH)
fix i
assume "find_first x ys = Some i" "i < n - 1"
with False have "find_first x (y # ys) = Some (Suc i)" "Suc i < n"
using False by auto
thus thesis
using Cons by metis
next
show "x ∈ set (take (n - 1) ys)"
using Cons False by (metis empty_iff list.set(1) set_ConsD take_Cons')
next
show "n - 1 ≤ length ys"
using Cons by (metis One_nat_def le_diff_conv list.size(4))
qed
qed
qed simp

lemma find_first_some:
assumes "x ∈ set xs"
obtains i where "find_first x xs = Some i" "i < length xs"
using assms
by (metis order_refl take_all find_first_some_strong)

lemma find_first_some_index: "i < length xs ⟹ distinct xs ⟹ find_first (xs ! i) xs = Some i"
proof (induction xs arbitrary: i)
case (Cons x xs)
show ?case
proof (cases "i = 0")
case False
have "find_first ((x # xs) ! i) (x # xs) = map_option Suc (Some (i - 1))"
using Cons False by auto
also have "… = Some i"
using False by auto
finally show ?thesis .
qed simp
qed auto

lemma find_first_append:
"find_first x (ys @ zs) =
(case find_first x ys of None ⇒ map_option (λi. i + length ys) (find_first x zs) | Some a ⇒ Some a)"
by (induct ys) (auto simp: option.map_comp comp_def map_option.identity split: option.splits)

lemma find_first_first:
assumes "i < length xs" "x ∉ set (take i xs)" "xs ! i = x"
shows "find_first x xs = Some i"
proof -
let ?ys = "take i xs"
let ?zs = "drop i xs"

have "?zs ! 0 = x"
using assms by simp
hence "find_first x ?zs = Some 0"
using assms by (cases ?zs) auto
moreover have "find_first x ?ys = None"
using assms by (simp add: find_first_none)
ultimately have "find_first x (?ys @ ?zs) = Some i"
unfolding find_first_append
using assms by simp
thus ?thesis
using assms by simp
qed

lemma find_first_prefix:
assumes "find_first x xs = Some i" "i < n"
shows "find_first x (take n xs) = Some i"
proof (rule find_first_first)
show "i < length (take n xs)"
using assms by (simp add: find_first_correct)
next
have "x ∉ set (take i xs)"
using assms by (simp add: find_first_correct)
with assms show "x ∉ set (take i (take n xs))"
by (simp add: min.absorb1)
next
show "take n xs ! i = x"
using assms by (simp add: find_first_correct)
qed

lemma find_first_later:
assumes "i < length xs" "j < length xs" "i < j"
assumes "xs ! i = x" "xs ! j = x"
shows "find_first x xs ≠ Some j"
proof (cases "x ∈ set (take i xs)")
case True
then obtain k where "find_first x xs = Some k" "k < i"
using assms by (auto elim: find_first_some_strong)
thus ?thesis
using assms by simp
next
case False
hence "find_first x xs = Some i"
using assms by (simp add: find_first_first)
thus ?thesis
using assms by simp
qed

lemma find_first_in_map:
assumes "length xs ≤ length ys" "find_first n xs = Some i"
shows "fmlookup (fmap_of_list (zip xs ys)) n = Some (ys ! i)"
using assms proof (induction xs arbitrary: ys i)
case (Cons x xs)
then obtain y ys' where "ys = y # ys'"
by (metis Skolem_list_nth le_0_eq length_greater_0_conv less_nat_zero_code list.set_cases listrel_Cons1 listrel_iff_nth nth_mem)
with Cons show ?case
by (cases "x = n") auto
qed auto

fun common_prefix where
"common_prefix (x # xs) (y # ys) = (if x = y then x # common_prefix xs ys else [])" |
"common_prefix _ _ = []"

lemma common_prefix_find:
assumes "z ∈ set (common_prefix xs ys)"
shows "find_first z xs = find_first z ys"
using assms
by (induct xs ys rule: common_prefix.induct) auto

lemma find_first_insert_nth_eq:
assumes "n ≤ length xs" "x ∉ set (take n xs)"
shows "find_first x (insert_nth n x xs) = Some n"
using assms
by (auto simp: find_first_append find_first_none split: option.splits)

lemma insert_nth_induct:
fixes P :: "nat ⇒ 'a ⇒ 'a list ⇒ bool"
and a0 :: "nat"
and a1 :: "'a"
and a2 :: "'a list"
assumes "⋀x xs. P 0 x xs"
and "⋀n x y ys. P n x ys ⟹ P (Suc n) x (y # ys)"
and "⋀n x. P (Suc n) x []"
shows "P a0 a1 a2"
using assms
apply induction_schema
apply pat_completeness
apply lexicographic_order
done

lemma find_first_insert_nth_neq:
assumes "x ≠ y"
shows "find_first x (insert_nth n y xs) = map_option (λi. if i < n then i else Suc i) (find_first x xs)"
using assms
proof (induction n y xs rule: insert_nth_induct)
case 2
note insert_nth_take_drop[simp del]
show ?case
apply auto
apply (subst 2)
apply (rule 2)
unfolding option.map_comp
apply (rule option.map_cong0)
by auto
qed auto

end

# Theory Name

chapter ‹Names as a unique datatype›

theory Name
imports Main
begin

text ‹
I would like to model names as @{typ string}s. Unfortunately, there is no default order on lists,
as there could be multiple reasonable implementations: e.g.\ lexicographic and point-wise.
For both choices, users can import the corresponding instantiation.

In Isabelle, only at most one implementation of a given type class for a given type may be present
in the same theory. Consequently, I avoided importing a list ordering from the library, because it
may cause conflicts with users who use another ordering. The general approach for these situations
is to introduce a type copy.

The full flexibility of strings (i.e.\ string manipulations) is only required where fresh names
are being produced. Otherwise, only a linear order on terms is needed. Conveniently, Sternagel and
Thiemann @{cite sternagel2015deriving} provide tooling to automatically generate such a
lexicographic order.
›

datatype name = Name (as_string: string)

― ‹Mostly copied from ‹List_Lexorder››

instantiation name :: ord
begin

definition less_name where
"xs < ys ⟷ (as_string xs, as_string ys) ∈ lexord {(u, v). (of_char u :: nat) < of_char v}"

definition less_eq_name where
"(xs :: name) ≤ ys ⟷ xs < ys ∨ xs = ys"

instance ..

end

instance name :: order
proof
fix xs :: "name"
show "xs ≤ xs" by (simp add: less_eq_name_def)
next
fix xs ys zs :: "name"
assume "xs ≤ ys" and "ys ≤ zs"
then show "xs ≤ zs"
apply (auto simp add: less_eq_name_def less_name_def)
apply (rule lexord_trans)
apply (auto intro: transI)
done
next
fix xs ys :: "name"
assume "xs ≤ ys" and "ys ≤ xs"
then show "xs = ys"
apply (auto simp add: less_eq_name_def less_name_def)
apply (rule lexord_irreflexive [THEN notE])
defer
apply (rule lexord_trans)
apply (auto intro: transI)
done
next
fix xs ys :: "name"
show "xs < ys ⟷ xs ≤ ys ∧ ¬ ys ≤ xs"
apply (auto simp add: less_name_def less_eq_name_def)
defer
apply (rule lexord_irreflexive [THEN notE])
apply auto
apply (rule lexord_irreflexive [THEN notE])
defer
apply (rule lexord_trans)
apply (auto intro: transI)
done
qed

instance name :: linorder
proof
fix xs ys :: "name"
have "(as_string xs, as_string ys) ∈ lexord {(u, v). (of_char u::nat) < of_char v} ∨ xs = ys ∨ (as_string ys, as_string xs) ∈ lexord {(u, v). (of_char u::nat) < of_char v}"
by (metis (no_types, lifting) case_prodI lexord_linear linorder_neqE_nat mem_Collect_eq name.expand of_char_eq_iff)
then show "xs ≤ ys ∨ ys ≤ xs"
by (auto simp add: less_eq_name_def less_name_def)
qed

lemma less_name_code[code]:
"Name xs < Name [] ⟷ False"
"Name [] < Name (x # xs) ⟷ True"
"Name (x # xs) < Name (y # ys) ⟷ (of_char x::nat) < of_char y ∨ x = y ∧ Name xs < Name ys"
unfolding less_name_def by auto

lemma le_name_code[code]:
"Name (x # xs) ≤ Name [] ⟷ False"
"Name [] ≤ Name (x # xs) ⟷ True"
"Name (x # xs) ≤ Name (y # ys) ⟷ (of_char x::nat) < of_char y ∨ x = y ∧ Name xs ≤ Name ys"
unfolding less_eq_name_def less_name_def by auto

context begin

qualified definition append :: "name ⇒ name ⇒ name" where
"append v1 v2 = Name (as_string v1 @ as_string v2)"

lemma name_append_less:
assumes "xs ≠ Name []"
shows "append ys xs > ys"
proof -
have "Name (ys @ xs) > Name ys" if "xs ≠ []" for xs ys
using that
proof (induction ys)
case Nil
thus ?case
unfolding less_name_def
by (cases xs) auto
next
case (Cons y ys)
thus ?case
unfolding less_name_def
by auto
qed
with assms show ?thesis
unfolding append_def
by (cases xs, cases ys) auto
qed

end

end

chapter ‹A monad for generating fresh names›

imports
Term_Utils
begin

text ‹
Generation of fresh names in general can be thought of as picking a string that is not an element
of a (finite) set of already existing names. For Isabelle, the ∗‹Nominal› framework
@{cite urban2008nominal and urban2013nominal} provides support for reasoning over fresh names, but
unfortunately, its definitions are not executable.

Instead, I chose to model generation of fresh names as a monad based on @{type state}. With this,
it becomes possible to write programs using ‹do›-notation. This is implemented abstractly as a
@{command locale} that expects two operations:

▪ ‹next› expects a value and generates a larger value, according to @{class linorder}
▪ ‹arb› produces any value, similarly to @{const undefined}, but executable
›

locale fresh =
fixes "next" :: "'a::linorder ⇒ 'a" and arb :: 'a
assumes next_ge: "next x > x"
begin

abbreviation update_next :: "('a, unit) state" where
"update_next ≡ State_Monad.update next"

lemma update_next_strict_mono[simp, intro]: "strict_mono_state update_next"
using next_ge by (auto intro: update_strict_mono)

lemma update_next_mono[simp, intro]: "mono_state update_next"
by (rule strict_mono_implies_mono) (rule update_next_strict_mono)

definition create :: "('a, 'a) state" where
"create = update_next ⤜ (λ_. State_Monad.get)"

lemma create_alt_def[code]: "create = State (λa. (next a, next a))"
by simp

abbreviation fresh_in :: "'a set ⇒ 'a ⇒ bool" where
"fresh_in S s ≡ Ball S ((≥) s)"

lemma next_ge_all: "finite S ⟹ fresh_in S s ⟹ next s ∉ S"
by (metis antisym less_imp_le less_irrefl next_ge)

definition Next :: "'a set ⇒ 'a" where
"Next S = (if S = {} then arb else next (Max S))"

lemma Next_ge_max: "finite S ⟹ S ≠ {} ⟹ Next S > Max S"
unfolding Next_def using next_ge by simp

lemma Next_not_member_subset: "finite S' ⟹ S ⊆ S' ⟹ Next S' ∉ S"
unfolding Next_def using next_ge
by (metis Max_ge Max_mono empty_iff finite_subset leD less_le_trans subset_empty)

lemma Next_not_member: "finite S ⟹ Next S ∉ S"
by (rule Next_not_member_subset) auto

lemma Next_geq_not_member: "finite S ⟹ s ≥ Next S ⟹ s ∉ S"
unfolding Next_def using next_ge
by (metis (full_types) Max_ge all_not_in_conv leD le_less_trans)

lemma next_not_member: "finite S ⟹ s ≥ Next S ⟹ next s ∉ S"
by (meson Next_geq_not_member less_imp_le next_ge order_trans)

lemma create_mono[simp, intro]: "mono_state create"
unfolding create_def
by (auto intro: bind_mono_strong)

lemma create_strict_mono[simp, intro]: "strict_mono_state create"
unfolding create_def
by (rule bind_strict_mono_strong2) auto

abbreviation run_fresh where
"run_fresh m S ≡ fst (run_state m (Next S))"

abbreviation fresh_fin :: "'a fset ⇒ 'a ⇒ bool" where
"fresh_fin S s ≡ fBall S ((≥) s)"

context includes fset.lifting begin

lemma next_ge_fall: "fresh_fin S s ⟹ next s |∉| S"
by (transfer fixing: "next") (rule next_ge_all)

lift_definition fNext :: "'a fset ⇒ 'a" is Next .

lemma fNext_ge_max: "S ≠ {||} ⟹ fNext S > fMax S"
by transfer (rule Next_ge_max)

lemma next_not_fmember: "s ≥ fNext S ⟹ next s |∉| S"
by transfer (rule next_not_member)

lemma fNext_geq_not_member: "s ≥ fNext S ⟹ s |∉| S"
by transfer (rule Next_geq_not_member)

lemma fNext_not_member: "fNext S |∉| S"
by transfer (rule Next_not_member)

lemma fNext_not_member_subset: "S |⊆| S' ⟹ fNext S' |∉| S"
by transfer (rule Next_not_member_subset)

abbreviation frun_fresh where
"frun_fresh m S ≡ fst (run_state m (fNext S))"

end

end

end

# Theory Fresh_Class

section ‹Fresh monad operations as class operations›

theory Fresh_Class
imports
Name
begin

text ‹
The @{const fresh} locale allows arbitrary instantiations. However, this may be inconvenient to
use. The following class serves as a global instantiation that can be used without interpretation.
The ‹arb› parameter of the locale redirects to @{const default}.

Some instantiations are provided. For @{typ name}s, underscores are appended to generate a fresh
name.
›

class fresh = linorder + default +
fixes "next" :: "'a ⇒ 'a"
assumes next_ge: "next x > x"

global_interpretation Fresh_Monad.fresh "next" default
defines fresh_create = create
and fresh_Next = Next
and fresh_fNext = fNext
and fresh_frun = frun_fresh
and fresh_run = run_fresh
proof
show "x < next x" for x by (rule next_ge)
qed

lemma [code]: "fresh_frun m S = fst (run_state m (fresh_fNext S))"
by (simp add: fresh_fNext_def fresh_frun_def)

lemma [code]: "fresh_run m S = fst (run_state m (fresh_Next S))"
by (simp add: fresh_Next_def fresh_run_def)

instantiation nat :: fresh begin

definition default_nat :: nat where
"default_nat = 0"

definition next_nat where
"next_nat = Suc"

instance
by intro_classes (auto simp: next_nat_def)

end

instantiation char :: default
begin

definition default_char :: char where
"default_char = CHR ''_''"

instance ..

end

instantiation name :: fresh begin

definition default_name where
"default_name = Name ''_''"

definition next_name where
"next_name xs = Name.append xs default"

instance proof
fix v :: name
show "v < next v"
unfolding next_name_def default_name_def
by (rule name_append_less) simp
qed

end

export_code
fresh_create fresh_Next fresh_fNext fresh_frun fresh_run
checking Scala? SML?

end

# Theory Term_Class

chapter ‹Terms›

theory Term_Class
imports
Datatype_Order_Generator.Order_Generator
Name
Term_Utils
"HOL-Library.Disjoint_FSets"
begin

hide_type (open) "term"

section ‹A simple term type, modelled after Pure's ‹term› type›

datatype "term" =
Const name |
Free name |
Abs "term" ("Λ _"  71) |
Bound nat |
App "term" "term" (infixl "$" 70) derive linorder "term" section ‹A type class describing terms› text ‹ The type class is split into two parts, ∗‹pre-terms› and ∗‹terms›. The only difference is that terms assume more axioms about substitution (see below). A term must provide the following generic constructors that behave like regular free constructors: ▪ ‹const :: name ⇒ τ› ▪ ‹free :: name ⇒ τ› ▪ ‹app :: τ ⇒ τ ⇒ τ› › text ‹ Conversely, there are also three corresponding destructors that could be defined in terms of Hilbert's choice operator. However, I have instead opted to let instances define destructors directly, which is simpler for execution purposes. Besides the generic constructors, terms may also contain other constructors. Those are abstractly called ∗‹abstractions›, even though that name is not entirely accurate (bound variables may also fall under this). Additionally, there must be operations that compute the list of all free variables (‹frees›), constants (‹consts›), and substitutions (‹subst›). Pre-terms only assume some basic properties of substitution on the generic constructors. Most importantly, substitution is not specified for environments containing terms with free variables. Term types are not required to implement ‹α›-renaming to prevent capturing of variables. › class pre_term = size + fixes frees :: "'a ⇒ name fset" and subst :: "'a ⇒ (name, 'a) fmap ⇒ 'a" and "consts" :: "'a ⇒ name fset" fixes app :: "'a ⇒ 'a ⇒ 'a" and unapp :: "'a ⇒ ('a × 'a) option" fixes const :: "name ⇒ 'a" and unconst :: "'a ⇒ name option" fixes free :: "name ⇒ 'a" and unfree :: "'a ⇒ name option" assumes unapp_app[simp]: "unapp (app u⇩1 u⇩2) = Some (u⇩1, u⇩2)" assumes app_unapp[dest]: "unapp u = Some (u⇩1, u⇩2) ⟹ u = app u⇩1 u⇩2" assumes app_size[simp]: "size (app u⇩1 u⇩2) = size u⇩1 + size u⇩2 + 1" assumes unconst_const[simp]: "unconst (const name) = Some name" assumes const_unconst[dest]: "unconst u = Some name ⟹ u = const name" assumes unfree_free[simp]: "unfree (free name) = Some name" assumes free_unfree[dest]: "unfree u = Some name ⟹ u = free name" assumes app_const_distinct: "app u⇩1 u⇩2 ≠ const name" assumes app_free_distinct: "app u⇩1 u⇩2 ≠ free name" assumes free_const_distinct: "free name⇩1 ≠ const name⇩2" assumes frees_const[simp]: "frees (const name) = fempty" assumes frees_free[simp]: "frees (free name) = {| name |}" assumes frees_app[simp]: "frees (app u⇩1 u⇩2) = frees u⇩1 |∪| frees u⇩2" assumes consts_free[simp]: "consts (free name) = fempty" assumes consts_const[simp]: "consts (const name) = {| name |}" assumes consts_app[simp]: "consts (app u⇩1 u⇩2) = consts u⇩1 |∪| consts u⇩2" assumes subst_app[simp]: "subst (app u⇩1 u⇩2) env = app (subst u⇩1 env) (subst u⇩2 env)" assumes subst_const[simp]: "subst (const name) env = const name" assumes subst_free[simp]: "subst (free name) env = (case fmlookup env name of Some t ⇒ t | _ ⇒ free name)" assumes free_inject: "free name⇩1 = free name⇩2 ⟹ name⇩1 = name⇩2" assumes const_inject: "const name⇩1 = const name⇩2 ⟹ name⇩1 = name⇩2" assumes app_inject: "app u⇩1 u⇩2 = app u⇩3 u⇩4 ⟹ u⇩1 = u⇩3 ∧ u⇩2 = u⇩4" instantiation "term" :: pre_term begin definition app_term where "app_term t u = t$ u"

fun unapp_term where
"unapp_term (t $u) = Some (t, u)" | "unapp_term _ = None" definition const_term where "const_term = Const" fun unconst_term where "unconst_term (Const name) = Some name" | "unconst_term _ = None" definition free_term where "free_term = Free" fun unfree_term where "unfree_term (Free name) = Some name" | "unfree_term _ = None" fun frees_term :: "term ⇒ name fset" where "frees_term (Free x) = {| x |}" | "frees_term (t⇩1$ t⇩2) = frees_term t⇩1 |∪| frees_term t⇩2" |
"frees_term (Λ t) = frees_term t" |
"frees_term _ = {||}"

fun subst_term :: "term ⇒ (name, term) fmap ⇒ term" where
"subst_term (Free s) env = (case fmlookup env s of Some t ⇒ t | None ⇒ Free s)" |
"subst_term (t⇩1 $t⇩2) env = subst_term t⇩1 env$ subst_term t⇩2 env" |
"subst_term (Λ t) env = Λ subst_term t env" |
"subst_term t env = t"

fun consts_term :: "term ⇒ name fset" where
"consts_term (Const x) = {| x |}" |
"consts_term (t⇩1 $t⇩2) = consts_term t⇩1 |∪| consts_term t⇩2" | "consts_term (Λ t) = consts_term t" | "consts_term _ = {||}" instance by standard (auto simp: app_term_def const_term_def free_term_def elim: unapp_term.elims unconst_term.elims unfree_term.elims split: option.splits) end context pre_term begin definition freess :: "'a list ⇒ name fset" where "freess = ffUnion ∘ fset_of_list ∘ map frees" lemma freess_cons[simp]: "freess (x # xs) = frees x |∪| freess xs" unfolding freess_def by simp lemma freess_single: "freess [x] = frees x" unfolding freess_def by simp lemma freess_empty[simp]: "freess [] = {||}" unfolding freess_def by simp lemma freess_app[simp]: "freess (xs @ ys) = freess xs |∪| freess ys" unfolding freess_def by simp lemma freess_subset: "set xs ⊆ set ys ⟹ freess xs |⊆| freess ys" unfolding freess_def comp_apply by (intro ffunion_mono fset_of_list_subset) auto abbreviation id_env :: "(name, 'a) fmap ⇒ bool" where "id_env ≡ fmpred (λx y. y = free x)" definition closed_except :: "'a ⇒ name fset ⇒ bool" where "closed_except t S ⟷ frees t |⊆| S" abbreviation closed :: "'a ⇒ bool" where "closed t ≡ closed_except t {||}" lemmas term_inject = free_inject const_inject app_inject lemmas term_distinct[simp] = app_const_distinct app_const_distinct[symmetric] app_free_distinct app_free_distinct[symmetric] free_const_distinct free_const_distinct[symmetric] lemma app_size1: "size u⇩1 < size (app u⇩1 u⇩2)" by simp lemma app_size2: "size u⇩2 < size (app u⇩1 u⇩2)" by simp lemma unx_some_lemmas: "unapp u = Some x ⟹ unconst u = None" "unapp u = Some x ⟹ unfree u = None" "unconst u = Some y ⟹ unapp u = None" "unconst u = Some y ⟹ unfree u = None" "unfree u = Some z ⟹ unconst u = None" "unfree u = Some z ⟹ unapp u = None" subgoal by (metis app_unapp const_unconst app_const_distinct not_None_eq surj_pair) subgoal by (metis app_free_distinct app_unapp free_unfree option.exhaust surj_pair) subgoal by (metis app_unapp const_unconst app_const_distinct old.prod.exhaust option.distinct(1) option.expand option.sel) subgoal by (metis const_unconst free_const_distinct free_unfree option.exhaust) subgoal by (metis const_unconst free_const_distinct free_unfree option.exhaust) subgoal by (metis app_free_distinct app_unapp free_unfree not_Some_eq surj_pair) done lemma unx_none_simps[simp]: "unapp (const name) = None" "unapp (free name) = None" "unconst (app t u) = None" "unconst (free name) = None" "unfree (const name) = None" "unfree (app t u) = None" subgoal by (metis app_unapp app_const_distinct not_None_eq surj_pair) subgoal by (metis app_free_distinct app_unapp option.exhaust surj_pair) subgoal by (metis const_unconst app_const_distinct option.distinct(1) option.expand option.sel) subgoal by (metis const_unconst free_const_distinct option.exhaust) subgoal by (metis free_const_distinct free_unfree option.exhaust) subgoal by (metis app_free_distinct free_unfree not_Some_eq) done lemma term_cases: obtains (free) name where "t = free name" | (const) name where "t = const name" | (app) u⇩1 u⇩2 where "t = app u⇩1 u⇩2" | (other) "unfree t = None" "unapp t = None" "unconst t = None" apply (cases "unfree t") apply (cases "unconst t") apply (cases "unapp t") subgoal by auto subgoal for x by (cases x) auto subgoal by auto subgoal by auto done definition is_const where "is_const t ⟷ (unconst t ≠ None)" definition const_name where "const_name t = (case unconst t of Some name ⇒ name)" lemma is_const_simps[simp]: "is_const (const name)" "¬ is_const (app t u)" "¬ is_const (free name)" unfolding is_const_def by simp+ lemma const_name_simps[simp]: "const_name (const name) = name" "is_const t ⟹ const (const_name t) = t" unfolding const_name_def is_const_def by auto definition is_free where "is_free t ⟷ (unfree t ≠ None)" definition free_name where "free_name t = (case unfree t of Some name ⇒ name)" lemma is_free_simps[simp]: "is_free (free name)" "¬ is_free (const name)" "¬ is_free (app t u)" unfolding is_free_def by simp+ lemma free_name_simps[simp]: "free_name (free name) = name" "is_free t ⟹ free (free_name t) = t" unfolding free_name_def is_free_def by auto definition is_app where "is_app t ⟷ (unapp t ≠ None)" definition left where "left t = (case unapp t of Some (l, _) ⇒ l)" definition right where "right t = (case unapp t of Some (_, r) ⇒ r)" lemma app_simps[simp]: "¬ is_app (const name)" "¬ is_app (free name)" "is_app (app t u)" unfolding is_app_def by simp+ lemma left_right_simps[simp]: "left (app l r) = l" "right (app l r) = r" "is_app t ⟹ app (left t) (right t) = t" unfolding is_app_def left_def right_def by auto definition ids :: "'a ⇒ name fset" where "ids t = frees t |∪| consts t" lemma closed_except_const[simp]: "closed_except (const name) S" unfolding closed_except_def by auto abbreviation closed_env :: "(name, 'a) fmap ⇒ bool" where "closed_env ≡ fmpred (λ_. closed)" lemma closed_except_self: "closed_except t (frees t)" unfolding closed_except_def by simp end class "term" = pre_term + size + fixes abs_pred :: "('a ⇒ bool) ⇒ 'a ⇒ bool" assumes raw_induct[case_names const free app abs]: "(⋀name. P (const name)) ⟹ (⋀name. P (free name)) ⟹ (⋀t⇩1 t⇩2. P t⇩1 ⟹ P t⇩2 ⟹ P (app t⇩1 t⇩2)) ⟹ (⋀t. abs_pred P t) ⟹ P t" assumes raw_subst_id: "abs_pred (λt. ∀env. id_env env ⟶ subst t env = t) t" and raw_subst_drop: "abs_pred (λt. x |∉| frees t ⟶ (∀env. subst t (fmdrop x env) = subst t env)) t" and raw_subst_indep: "abs_pred (λt. ∀env⇩1 env⇩2. closed_env env⇩2 ⟶ fdisjnt (fmdom env⇩1) (fmdom env⇩2) ⟶ subst t (env⇩1 ++⇩f env⇩2) = subst (subst t env⇩2) env⇩1) t" and raw_subst_frees: "abs_pred (λt. ∀env. closed_env env ⟶ frees (subst t env) = frees t |-| fmdom env) t" and raw_subst_consts': "abs_pred (λa. ∀x. consts (subst a x) = consts a |∪| ffUnion (consts || fmimage x (frees a))) t" and abs_pred_trivI: "P t ⟹ abs_pred P t" begin lemma subst_id: "id_env env ⟹ subst t env = t" proof (induction t arbitrary: env rule: raw_induct) case (abs t) show ?case by (rule raw_subst_id) qed (auto split: option.splits) lemma subst_drop: "x |∉| frees t ⟹ subst t (fmdrop x env) = subst t env" proof (induction t arbitrary: env rule: raw_induct) case (abs t) show ?case by (rule raw_subst_drop) qed (auto split: option.splits) lemma subst_frees: "fmpred (λ_. closed) env ⟹ frees (subst t env) = frees t |-| fmdom env" proof (induction t arbitrary: env rule: raw_induct) case (abs t) show ?case by (rule raw_subst_frees) qed (auto split: option.splits simp: closed_except_def) lemma subst_consts': "consts (subst t env) = consts t |∪| ffUnion (consts || fmimage env (frees t))" proof (induction t arbitrary: env rule: raw_induct) case (free name) then show ?case by (auto split: option.splits simp: ffUnion_alt_def fmlookup_ran_iff fmlookup_image_iff fmlookup_dom_iff intro!: fBexI) next case (abs t) show ?case by (rule raw_subst_consts') qed (auto simp: funion_image_bind_eq finter_funion_distrib fbind_funion) fun match :: "term ⇒ 'a ⇒ (name, 'a) fmap option" where "match (t⇩1$ t⇩2) u = do {
(u⇩1, u⇩2) ← unapp u;
env⇩1 ← match t⇩1 u⇩1;
env⇩2 ← match t⇩2 u⇩2;
Some (env⇩1 ++⇩f env⇩2)
}" |
"match (Const name) u =
(case unconst u of
None ⇒ None
| Some name' ⇒ if name = name' then Some fmempty else None)" |
"match (Free name) u = Some (fmap_of_list [(name, u)])" |
"match (Bound n) u = None" |
"match (Abs t) u = None"

lemma match_simps[simp]:
"match (t⇩1 $t⇩2) (app u⇩1 u⇩2) = do { env⇩1 ← match t⇩1 u⇩1; env⇩2 ← match t⇩2 u⇩2; Some (env⇩1 ++⇩f env⇩2) }" "match (Const name) (const name') = (if name = name' then Some fmempty else None)" by auto lemma match_some_induct[consumes 1, case_names app const free]: assumes "match t u = Some env" assumes "⋀t⇩1 t⇩2 u⇩1 u⇩2 env⇩1 env⇩2. P t⇩1 u⇩1 env⇩1 ⟹ match t⇩1 u⇩1 = Some env⇩1 ⟹ P t⇩2 u⇩2 env⇩2 ⟹ match t⇩2 u⇩2 = Some env⇩2 ⟹ P (t⇩1$ t⇩2) (app u⇩1 u⇩2) (env⇩1 ++⇩f env⇩2)"
assumes "⋀name. P (Const name) (const name) fmempty"
assumes "⋀name u. P (Free name) u (fmupd name u fmempty)"
shows "P t u env"
using assms
by (induction t u arbitrary: env rule: match.induct)
(auto split: option.splits if_splits elim!: option_bindE)

lemma match_dom: "match p t = Some env ⟹ fmdom env = frees p"
by (induction p arbitrary: t env)
(fastforce split: option.splits if_splits elim: option_bindE)+

lemma match_vars: "match p t = Some env ⟹ fmpred (λ_ u. frees u |⊆| frees t) env"
proof (induction p t env rule: match_some_induct)
case (app t⇩1 t⇩2 u⇩1 u⇩2 env⇩1 env⇩2)
show ?case
apply rule
using app
by (fastforce intro: fmpred_mono_strong)+
qed auto

lemma match_appE_split:
assumes "match (t⇩1 $t⇩2) u = Some env" obtains u⇩1 u⇩2 env⇩1 env⇩2 where "u = app u⇩1 u⇩2" "match t⇩1 u⇩1 = Some env⇩1" "match t⇩2 u⇩2 = Some env⇩2" "env = env⇩1 ++⇩f env⇩2" using assms by (auto split: option.splits elim!: option_bindE) lemma subst_consts: assumes "consts t |⊆| S" "fmpred (λ_ u. consts u |⊆| S) env" shows "consts (subst t env) |⊆| S" apply (subst subst_consts') using assms by (auto intro!: ffUnion_least) lemma subst_empty[simp]: "subst t fmempty = t" by (auto simp: subst_id) lemma subst_drop_fset: "fdisjnt S (frees t) ⟹ subst t (fmdrop_fset S env) = subst t env" by (induct S) (auto simp: subst_drop fdisjnt_alt_def) lemma subst_restrict: assumes "frees t |⊆| M" shows "subst t (fmrestrict_fset M env) = subst t env" proof - have *: "fmrestrict_fset M env = fmdrop_fset (fmdom env - M) env" by (rule fmap_ext) auto show ?thesis apply (subst *) apply (subst subst_drop_fset) unfolding fdisjnt_alt_def using assms by auto qed corollary subst_restrict'[simp]: "subst t (fmrestrict_fset (frees t) env) = subst t env" by (simp add: subst_restrict) corollary subst_cong: assumes "⋀x. x |∈| frees t ⟹ fmlookup Γ⇩1 x = fmlookup Γ⇩2 x" shows "subst t Γ⇩1 = subst t Γ⇩2" proof - have "fmrestrict_fset (frees t) Γ⇩1 = fmrestrict_fset (frees t) Γ⇩2" apply (rule fmap_ext) using assms by simp thus ?thesis by (metis subst_restrict') qed corollary subst_add_disjnt: assumes "fdisjnt (frees t) (fmdom env⇩1)" shows "subst t (env⇩1 ++⇩f env⇩2) = subst t env⇩2" proof - have "subst t (env⇩1 ++⇩f env⇩2) = subst t (fmrestrict_fset (frees t) (env⇩1 ++⇩f env⇩2))" by (metis subst_restrict') also have "… = subst t (fmrestrict_fset (frees t) env⇩1 ++⇩f fmrestrict_fset (frees t) env⇩2)" by simp also have "… = subst t (fmempty ++⇩f fmrestrict_fset (frees t) env⇩2)" unfolding fmfilter_alt_defs apply (subst fmfilter_false) using assms by (auto simp: fdisjnt_alt_def intro: fmdomI) also have "… = subst t (fmrestrict_fset (frees t) env⇩2)" by simp also have "… = subst t env⇩2" by simp finally show ?thesis . qed corollary subst_add_shadowed_env: assumes "frees t |⊆| fmdom env⇩2" shows "subst t (env⇩1 ++⇩f env⇩2) = subst t env⇩2" proof - have "subst t (env⇩1 ++⇩f env⇩2) = subst t (fmdrop_fset (fmdom env⇩2) env⇩1 ++⇩f env⇩2)" by (subst fmadd_drop_left_dom) rule also have "… = subst t (fmrestrict_fset (frees t) (fmdrop_fset (fmdom env⇩2) env⇩1 ++⇩f env⇩2))" by (metis subst_restrict') also have "… = subst t (fmrestrict_fset (frees t) (fmdrop_fset (fmdom env⇩2) env⇩1) ++⇩f fmrestrict_fset (frees t) env⇩2)" by simp also have "… = subst t (fmempty ++⇩f fmrestrict_fset (frees t) env⇩2)" unfolding fmfilter_alt_defs using fsubsetD[OF assms] by auto also have "… = subst t env⇩2" by simp finally show ?thesis . qed corollary subst_restrict_closed: "closed_except t S ⟹ subst t (fmrestrict_fset S env) = subst t env" by (metis subst_restrict closed_except_def) lemma subst_closed_except_id: assumes "closed_except t S" "fdisjnt (fmdom env) S" shows "subst t env = t" using assms by (metis fdisjnt_subset_right fmdom_drop_fset fminus_cancel fmrestrict_fset_dom fmrestrict_fset_null closed_except_def subst_drop_fset subst_empty) lemma subst_closed_except_preserved: assumes "closed_except t S" "fdisjnt (fmdom env) S" shows "closed_except (subst t env) S" using assms by (metis subst_closed_except_id) corollary subst_closed_id: "closed t ⟹ subst t env = t" by (simp add: subst_closed_except_id fdisjnt_alt_def) corollary subst_closed_preserved: "closed t ⟹ closed (subst t env)" by (simp add: subst_closed_except_preserved fdisjnt_alt_def) context begin private lemma subst_indep0: assumes "closed_env env⇩2" "fdisjnt (fmdom env⇩1) (fmdom env⇩2)" shows "subst t (env⇩1 ++⇩f env⇩2) = subst (subst t env⇩2) env⇩1" using assms proof (induction t arbitrary: env⇩1 env⇩2 rule: raw_induct) case (free name) show ?case using ‹closed_env env⇩2› by (cases rule: fmpred_cases[where x = name]) (auto simp: subst_closed_id) next case (abs t) show ?case by (rule raw_subst_indep) qed auto lemma subst_indep: assumes "closed_env Γ'" shows "subst t (Γ ++⇩f Γ') = subst (subst t Γ') Γ" proof - have "subst t (Γ ++⇩f Γ') = subst t (fmrestrict_fset (frees t) (Γ ++⇩f Γ'))" by (metis subst_restrict') also have "… = subst t (fmrestrict_fset (frees t) Γ ++⇩f Γ')" by (smt fmlookup_add fmlookup_restrict_fset subst_cong) also have "… = subst t (fmrestrict_fset (frees t |-| fmdom Γ') Γ ++⇩f Γ')" by (rule subst_cong) (simp add: fmfilter_alt_defs(5)) also have "… = subst (subst t Γ') (fmrestrict_fset (frees t |-| fmdom Γ') Γ)" apply (rule subst_indep0[OF assms]) using fmdom_restrict_fset unfolding fdisjnt_alt_def by auto also have "… = subst (subst t Γ') (fmrestrict_fset (frees (subst t Γ')) Γ)" using assms by (auto simp: subst_frees) also have "… = subst (subst t Γ') Γ" by simp finally show ?thesis . qed lemma subst_indep': assumes "closed_env Γ'" "fdisjnt (fmdom Γ') (fmdom Γ)" shows "subst t (Γ' ++⇩f Γ) = subst (subst t Γ') Γ" using assms by (metis subst_indep fmadd_disjnt) lemma subst_twice: assumes "Γ' ⊆⇩f Γ" "closed_env Γ'" shows "subst (subst t Γ') Γ = subst t Γ" proof - have "subst (subst t Γ') Γ = subst t (Γ ++⇩f Γ')" apply (rule subst_indep[symmetric]) apply fact done also have "… = subst t Γ" apply (rule subst_cong) using ‹Γ' ⊆⇩f Γ› unfolding fmsubset_alt_def by fastforce finally show ?thesis . qed end fun matchs :: "term list ⇒ 'a list ⇒ (name, 'a) fmap option" where "matchs [] [] = Some fmempty" | "matchs (t # ts) (u # us) = do { env⇩1 ← match t u; env⇩2 ← matchs ts us; Some (env⇩1 ++⇩f env⇩2) }" | "matchs _ _ = None" lemmas matchs_induct = matchs.induct[case_names empty cons] context begin private lemma matchs_alt_def0: assumes "length ps = length vs" shows "map_option (λenv. m ++⇩f env) (matchs ps vs) = map_option (foldl (++⇩f) m) (those (map2 match ps vs))" using assms proof (induction arbitrary: m rule: list_induct2) case (Cons x xs y ys) show ?case proof (cases "match x y") case x_y: Some show ?thesis proof (cases "matchs xs ys") case None with x_y Cons show ?thesis by simp next case Some with x_y show ?thesis apply simp using Cons(2) apply simp apply (subst option.map_comp) by (auto cong: map_option_cong) qed qed simp qed simp lemma matchs_alt_def: assumes "length ps = length vs" shows "matchs ps vs = map_option (foldl (++⇩f) fmempty) (those (map2 match ps vs))" by (subst matchs_alt_def0[where m = fmempty, simplified, symmetric, OF assms]) (simp add: option.map_ident) end lemma matchs_neq_length_none[simp]: "length xs ≠ length ys ⟹ matchs xs ys = None" by (induct xs ys rule: matchs.induct) fastforce+ corollary matchs_some_eq_length: "matchs xs ys = Some env ⟹ length xs = length ys" by (metis option.distinct(1) matchs_neq_length_none) lemma matchs_app[simp]: assumes "length xs⇩2 = length ys⇩2" shows "matchs (xs⇩1 @ xs⇩2) (ys⇩1 @ ys⇩2) = matchs xs⇩1 ys⇩1 ⤜ (λenv⇩1. matchs xs⇩2 ys⇩2 ⤜ (λenv⇩2. Some (env⇩1 ++⇩f env⇩2)))" using assms by (induct xs⇩1 ys⇩1 rule: matchs.induct) fastforce+ corollary matchs_appI: assumes "matchs xs ys = Some env⇩1" "matchs xs' ys' = Some env⇩2" shows "matchs (xs @ xs') (ys @ ys') = Some (env⇩1 ++⇩f env⇩2)" using assms by (metis (no_types, lifting) Option.bind_lunit matchs_app matchs_some_eq_length) corollary matchs_dom: assumes "matchs ps ts = Some env" shows "fmdom env = freess ps" using assms by (induction ps ts arbitrary: env rule: matchs_induct) (auto simp: match_dom elim!: option_bindE) fun find_match :: "(term × 'a) list ⇒ 'a ⇒ ((name, 'a) fmap × term × 'a) option" where "find_match [] _ = None" | "find_match ((pat, rhs) # cs) t = (case match pat t of Some env ⇒ Some (env, pat, rhs) | None ⇒ find_match cs t)" lemma find_match_map: "find_match (map (λ(pat, t). (pat, f pat t)) cs) t = map_option (λ(env, pat, rhs). (env, pat, f pat rhs)) (find_match cs t)" by (induct cs) (auto split: option.splits) lemma find_match_elem: assumes "find_match cs t = Some (env, pat, rhs)" shows "(pat, rhs) ∈ set cs" "match pat t = Some env" using assms by (induct cs) (auto split: option.splits) lemma match_subst_closed: assumes "match pat t = Some env" "closed_except rhs (frees pat)" "closed t" shows "closed (subst rhs env)" using assms by (smt fminusE fmpred_iff fset_mp fsubsetI closed_except_def match_vars match_dom subst_frees) fun rewrite_step :: "(term × 'a) ⇒ 'a ⇒ 'a option" where "rewrite_step (t⇩1, t⇩2) u = map_option (subst t⇩2) (match t⇩1 u)" abbreviation rewrite_step' :: "(term × 'a) ⇒ 'a ⇒ 'a ⇒ bool" ("_/ ⊢/ _ →/ _" [50,0,50] 50) where "r ⊢ t → u ≡ rewrite_step r t = Some u" lemma rewrite_step_closed: assumes "frees t⇩2 |⊆| frees t⇩1" "(t⇩1, t⇩2) ⊢ u → u'" "closed u" shows "closed u'" proof - from assms obtain env where *: "match t⇩1 u = Some env" by auto then have "closed (subst t⇩2 env)" apply (rule match_subst_closed[where pat = t⇩1 and t = u]) using assms unfolding closed_except_def by auto with * show ?thesis using assms by auto qed definition matches :: "'a ⇒ 'a ⇒ bool" (infix "≲" 50) where "t ≲ u ⟷ (∃env. subst t env = u)" lemma matchesI[intro]: "subst t env = u ⟹ t ≲ u" unfolding matches_def by auto lemma matchesE[elim]: assumes "t ≲ u" obtains env where "subst t env = u" using assms unfolding matches_def by blast definition overlapping :: "'a ⇒ 'a ⇒ bool" where "overlapping s t ⟷ (∃u. s ≲ u ∧ t ≲ u)" lemma overlapping_refl: "overlapping t t" unfolding overlapping_def matches_def by blast lemma overlapping_sym: "overlapping t u ⟹ overlapping u t" unfolding overlapping_def by auto lemma overlappingI[intro]: "s ≲ u ⟹ t ≲ u ⟹ overlapping s t" unfolding overlapping_def by auto lemma overlappingE[elim]: assumes "overlapping s t" obtains u where "s ≲ u" "t ≲ u" using assms unfolding overlapping_def by blast abbreviation "non_overlapping s t ≡ ¬ overlapping s t" corollary non_overlapping_implies_neq: "non_overlapping t u ⟹ t ≠ u" by (metis overlapping_refl) end inductive rewrite_first :: "(term × 'a::term) list ⇒ 'a ⇒ 'a ⇒ bool" where match: "match pat t = Some env ⟹ rewrite_first ((pat, rhs) # _) t (subst rhs env)" | nomatch: "match pat t = None ⟹ rewrite_first cs t t' ⟹ rewrite_first ((pat, _) # cs) t t'" code_pred (modes: i ⇒ i ⇒ o ⇒ bool) rewrite_first . lemma rewrite_firstE: assumes "rewrite_first cs t t'" obtains pat rhs env where "(pat, rhs) ∈ set cs" "match pat t = Some env" "t' = subst rhs env" using assms by induction auto text ‹ This doesn't follow from @{thm [source] find_match_elem}, because @{const rewrite_first} requires the first match, not just any. › lemma find_match_rewrite_first: assumes "find_match cs t = Some (env, pat, rhs)" shows "rewrite_first cs t (subst rhs env)" using assms proof (induction cs) case (Cons c cs) obtain pat0 rhs0 where "c = (pat0, rhs0)" by fastforce thus ?case using Cons by (cases "match pat0 t") (auto intro: rewrite_first.intros) qed simp definition term_cases :: "(name ⇒ 'b) ⇒ (name ⇒ 'b) ⇒ ('a ⇒ 'a ⇒ 'b) ⇒ 'b ⇒ 'a::term ⇒ 'b" where "term_cases if_const if_free if_app otherwise t = (case unconst t of Some name ⇒ if_const name | None ⇒ (case unfree t of Some name ⇒ if_free name | None ⇒ (case unapp t of Some (t, u) ⇒ if_app t u | None ⇒ otherwise)))" lemma term_cases_cong[fundef_cong]: assumes "t = u" "otherwise1 = otherwise2" assumes "(⋀name. t = const name ⟹ if_const1 name = if_const2 name)" assumes "(⋀name. t = free name ⟹ if_free1 name = if_free2 name)" assumes "(⋀u⇩1 u⇩2. t = app u⇩1 u⇩2 ⟹ if_app1 u⇩1 u⇩2 = if_app2 u⇩1 u⇩2)" shows "term_cases if_const1 if_free1 if_app1 otherwise1 t = term_cases if_const2 if_free2 if_app2 otherwise2 u" using assms unfolding term_cases_def by (auto split: option.splits) lemma term_cases[simp]: "term_cases if_const if_free if_app otherwise (const name) = if_const name" "term_cases if_const if_free if_app otherwise (free name) = if_free name" "term_cases if_const if_free if_app otherwise (app t u) = if_app t u" unfolding term_cases_def by (auto split: option.splits) lemma term_cases_template: assumes "⋀x. f x = term_cases if_const if_free if_app otherwise x" shows "f (const name) = if_const name" and "f (free name) = if_free name" and "f (app t u) = if_app t u" unfolding assms by (rule term_cases)+ context "term" begin function (sequential) strip_comb :: "'a ⇒ 'a × 'a list" where [simp del]: "strip_comb t = (case unapp t of Some (t, u) ⇒ (let (f, args) = strip_comb t in (f, args @ [u])) | None ⇒ (t, []))" by pat_completeness auto (* FIXME why is this not automatic? *) termination apply (relation "measure size") apply rule apply auto done lemma strip_comb_simps[simp]: "strip_comb (app t u) = (let (f, args) = strip_comb t in (f, args @ [u]))" "unapp t = None ⟹ strip_comb t = (t, [])" by (subst strip_comb.simps; auto)+ lemma strip_comb_induct[case_names app no_app]: assumes "⋀x y. P x ⟹ P (app x y)" assumes "⋀t. unapp t = None ⟹ P t" shows "P t" proof (rule strip_comb.induct, goal_cases) case (1 t) show ?case proof (cases "unapp t") case None with assms show ?thesis by metis next case (Some a) then show ?thesis apply (cases a) using 1 assms by auto qed qed lemma strip_comb_size: "t' ∈ set (snd (strip_comb t)) ⟹ size t' < size t" by (induction t rule: strip_comb_induct) (auto split: prod.splits) lemma sstrip_comb_termination[termination_simp]: "(f, ts) = strip_comb t ⟹ t' ∈ set ts ⟹ size t' < size t" by (metis snd_conv strip_comb_size) lemma strip_comb_empty: "snd (strip_comb t) = [] ⟹ fst (strip_comb t) = t" by (induction t rule: strip_comb_induct) (auto split: prod.splits) lemma strip_comb_app: "fst (strip_comb (app t u)) = fst (strip_comb t)" by (simp split: prod.splits) primrec list_comb :: "'a ⇒ 'a list ⇒ 'a" where "list_comb f [] = f" | "list_comb f (t # ts) = list_comb (app f t) ts" lemma list_comb_app[simp]: "list_comb f (xs @ ys) = list_comb (list_comb f xs) ys" by (induct xs arbitrary: f) auto corollary list_comb_snoc: "app (list_comb f xs) y = list_comb f (xs @ [y])" by simp lemma list_comb_size[simp]: "size (list_comb f xs) = size f + size_list size xs" by (induct xs arbitrary: f) auto lemma subst_list_comb: "subst (list_comb f xs) env = list_comb (subst f env) (map (λt. subst t env) xs)" by (induct xs arbitrary: f) auto abbreviation const_list_comb :: "name ⇒ 'a list ⇒ 'a" (infixl "$$" 70) where "const_list_comb name ≡ list_comb (const name)" lemma list_strip_comb[simp]: "list_comb (fst (strip_comb t)) (snd (strip_comb t)) = t" by (induction t rule: strip_comb_induct) (auto split: prod.splits) lemma strip_list_comb: "strip_comb (list_comb f ys) = (fst (strip_comb f), snd (strip_comb f) @ ys)" by (induct ys arbitrary: f) (auto simp: split_beta) lemma strip_list_comb_const: "strip_comb (name$$ xs) = (const name, xs)" by (simp add: strip_list_comb) lemma frees_list_comb[simp]: "frees (list_comb t xs) = frees t |∪| freess xs" by (induct xs arbitrary: t) (auto simp: freess_def) lemma consts_list_comb: "consts (list_comb f xs) = consts f |∪| ffUnion (fset_of_list (map consts xs))" by (induct xs arbitrary: f) auto lemma ids_list_comb: "ids (list_comb f xs) = ids f |∪| ffUnion (fset_of_list (map ids xs))" unfolding ids_def frees_list_comb consts_list_comb freess_def apply auto apply (smt fbind_iff finsert_absorb finsert_fsubset funion_image_bind_eq inf_sup_ord(3)) apply (metis fbind_iff funionCI funion_image_bind_eq) by (smt fbind_iff funionE funion_image_bind_eq) lemma frees_strip_comb: "frees t = frees (fst (strip_comb t)) |∪| freess (snd (strip_comb t))" by (metis list_strip_comb frees_list_comb) lemma list_comb_cases': obtains (app) "is_app (list_comb f xs)" | (empty) "list_comb f xs = f" "xs = []" by (induction xs arbitrary: f) auto (* FIXME case names? *) lemma list_comb_cases[consumes 1]: assumes "t = list_comb f xs" obtains (head) "t = f" "xs = []" | (app) u v where "t = app u v" using assms by (metis list_comb_cases' left_right_simps(3)) end fun left_nesting :: "'a::term ⇒ nat" where [simp del]: "left_nesting t = term_cases (λ_. 0) (λ_. 0) (λt u. Suc (left_nesting t)) 0 t" lemmas left_nesting_simps[simp] = term_cases_template[OF left_nesting.simps] lemma list_comb_nesting[simp]: "left_nesting (list_comb f xs) = left_nesting f + length xs" by (induct xs arbitrary: f) auto lemma list_comb_cond_inj: assumes "list_comb f xs = list_comb g ys" "left_nesting f = left_nesting g" shows "xs = ys" "f = g" using assms proof (induction xs arbitrary: f g ys) case Nil fix f g :: 'a fix ys assume prems: "list_comb f [] = list_comb g ys" "left_nesting f = left_nesting g" hence "left_nesting f = left_nesting g + length ys" by simp with prems show "[] = ys" "f = g" by simp+ next case (Cons x xs) fix f g ys assume prems: "list_comb f (x # xs) = list_comb g ys" "left_nesting f = left_nesting g" hence "left_nesting (list_comb f (x # xs)) = left_nesting (list_comb g ys)" by simp hence "Suc (left_nesting f + length xs) = left_nesting g + length ys" by simp with prems have "length ys = Suc (length xs)" by linarith then obtain z zs where "ys = z # zs" by (metis length_Suc_conv) thus "x # xs = ys" "f = g" using prems Cons[where ys = zs and f = "app f x" and g = "app g z"] by (auto dest: app_inject) qed lemma list_comb_inj_second: "inj (list_comb f)" by (metis injI list_comb_cond_inj) lemma list_comb_semi_inj: assumes "length xs = length ys" assumes "list_comb f xs = list_comb g ys" shows "xs = ys" "f = g" proof - from assms have "left_nesting (list_comb f xs) = left_nesting (list_comb g ys)" by simp with assms have "left_nesting f = left_nesting g" unfolding list_comb_nesting by simp with assms show "xs = ys" "f = g" by (metis list_comb_cond_inj)+ qed fun no_abs :: "'a::term ⇒ bool" where [simp del]: "no_abs t = term_cases (λ_. True) (λ_. True) (λt u. no_abs t ∧ no_abs u) False t" lemmas no_abs_simps[simp] = term_cases_template[OF no_abs.simps] lemma no_abs_induct[consumes 1, case_names free const app, induct pred: no_abs]: assumes "no_abs t" assumes "⋀name. P (free name)" assumes "⋀name. P (const name)" assumes "⋀t⇩1 t⇩2. P t⇩1 ⟹ no_abs t⇩1 ⟹ P t⇩2 ⟹ no_abs t⇩2 ⟹ P (app t⇩1 t⇩2)" shows "P t" using assms(1) proof (induction rule: no_abs.induct) case (1 t) show ?case proof (cases rule: pre_term_class.term_cases[where t = t]) case (free name) then show ?thesis using assms by auto next case (const name) then show ?thesis using assms by auto next case (app u⇩1 u⇩2) with assms have "P u⇩1" "P u⇩2" using 1 by auto with assms ‹no_abs t› show ?thesis unfolding ‹t = _› by auto next case other then show ?thesis using ‹no_abs t› apply (subst (asm) no_abs.simps) apply (subst (asm) term_cases_def) by simp qed qed lemma no_abs_cases[consumes 1, cases pred: no_abs]: assumes "no_abs t" obtains (free) name where "t = free name" | (const) name where "t = const name" | (app) t⇩1 t⇩2 where "t = app t⇩1 t⇩2" "no_abs t⇩1" "no_abs t⇩2" proof (cases rule: pre_term_class.term_cases[where t = t]) case (app u⇩1 u⇩2) show ?thesis apply (rule that(3)) apply fact using ‹no_abs t› unfolding ‹t = _› by auto next case other then have False using ‹no_abs t› apply (subst (asm) no_abs.simps) by (auto simp: term_cases_def) then show ?thesis .. qed definition is_abs :: "'a::term ⇒ bool" where "is_abs t = term_cases (λ_. False) (λ_. False) (λ_ _. False) True t" lemmas is_abs_simps[simp] = term_cases_template[OF is_abs_def] definition abs_ish :: "term list ⇒ 'a::term ⇒ bool" where "abs_ish pats rhs ⟷ pats ≠ [] ∨ is_abs rhs" locale simple_syntactic_and = fixes P :: "'a::term ⇒ bool" assumes app: "P (app t u) ⟷ P t ∧ P u" begin context notes app[simp] begin lemma list_comb: "P (list_comb f xs) ⟷ P f ∧ list_all P xs" by (induction xs arbitrary: f) auto corollary list_combE: assumes "P (list_comb f xs)" shows "P f" "x ∈ set xs ⟹ P x" using assms by (auto simp: list_comb list_all_iff) lemma match: assumes "match pat t = Some env" "P t" shows "fmpred (λ_. P) env" using assms by (induction pat t env rule: match_some_induct) auto lemma matchs: assumes "matchs pats ts = Some env" "list_all P ts" shows "fmpred (λ_. P) env" using assms by (induction pats ts arbitrary: env rule: matchs.induct) (auto elim!: option_bindE intro: match) end end locale subst_syntactic_and = simple_syntactic_and + assumes subst: "P t ⟹ fmpred (λ_. P) env ⟹ P (subst t env)" begin lemma rewrite_step: assumes "(lhs, rhs) ⊢ t → t'" "P t" "P rhs" shows "P t'" using assms by (auto intro: match subst) end locale simple_syntactic_or = fixes P :: "'a::term ⇒ bool" assumes app: "P (app t u) ⟷ P t ∨ P u" begin context notes app[simp] begin lemma list_comb: "P (list_comb f xs) ⟷ P f ∨ list_ex P xs" by (induction xs arbitrary: f) auto lemma match: assumes "match pat t = Some env" "¬ P t" shows "fmpred (λ_ t. ¬ P t) env" using assms by (induction pat t env rule: match_some_induct) auto end sublocale neg: simple_syntactic_and "λt. ¬ P t" by standard (auto simp: app) end global_interpretation no_abs: simple_syntactic_and no_abs by standard simp global_interpretation closed: simple_syntactic_and "λt. closed_except t S" for S by standard (simp add: closed_except_def) global_interpretation closed: subst_syntactic_and closed by standard (rule subst_closed_preserved) corollary closed_list_comb: "closed (name $$args) ⟷ list_all closed args" by (simp add: closed.list_comb) locale term_struct_rel = fixes P :: "'a::term ⇒ 'b::term ⇒ bool" assumes P_t_const: "P t (const name) ⟹ t = const name" assumes P_const_const: "P (const name) (const name)" assumes P_t_app: "P t (app u⇩1 u⇩2) ⟹ ∃t⇩1 t⇩2. t = app t⇩1 t⇩2 ∧ P t⇩1 u⇩1 ∧ P t⇩2 u⇩2" assumes P_app_app: "P t⇩1 u⇩1 ⟹ P t⇩2 u⇩2 ⟹ P (app t⇩1 t⇩2) (app u⇩1 u⇩2)" begin abbreviation P_env :: "('k, 'a) fmap ⇒ ('k, 'b) fmap ⇒ bool" where "P_env ≡ fmrel P" lemma related_match: assumes "match x u = Some env" "P t u" obtains env' where "match x t = Some env'" "P_env env' env" using assms proof (induction x u env arbitrary: t thesis rule: match_some_induct) case (app v⇩1 v⇩2 w⇩1 w⇩2 env⇩1 env⇩2) obtain u⇩1 u⇩2 where "t = app u⇩1 u⇩2" "P u⇩1 w⇩1" "P u⇩2 w⇩2" using P_t_app[OF ‹P t (app w⇩1 w⇩2)›] by auto with app obtain env⇩1' env⇩2' where "match v⇩1 u⇩1 = Some env⇩1'" "P_env env⇩1' env⇩1" and "match v⇩2 u⇩2 = Some env⇩2'" "P_env env⇩2' env⇩2" by metis hence "match (v⇩1 v⇩2) (app u⇩1 u⇩2) = Some (env⇩1' ++⇩f env⇩2')" by simp show ?case proof (rule app.prems) show "match (v⇩1 v⇩2) t = Some (env⇩1' ++⇩f env⇩2')" unfolding ‹t = _› by fact next show "P_env (env⇩1' ++⇩f env⇩2') (env⇩1 ++⇩f env⇩2)" by rule fact+ qed qed (auto split: option.splits if_splits dest: P_t_const) lemma list_combI: assumes "list_all2 P us⇩1 us⇩2" "P t⇩1 t⇩2" shows "P (list_comb t⇩1 us⇩1) (list_comb t⇩2 us⇩2)" using assms by (induction arbitrary: t⇩1 t⇩2 rule: list.rel_induct) (auto intro: P_app_app) lemma list_combE: assumes "P t (name$$ args)" obtains args' where "t = name $$args'" "list_all2 P args' args" using assms proof (induction args arbitrary: t thesis rule: rev_induct) case Nil hence "P t (const name)" by simp hence "t = const name" using P_t_const by auto with Nil show ?case by simp next case (snoc x xs) hence "P t (app (name$$ xs) x)" by simp obtain t' y where "t = app t' y" "P t' (name $$xs)" "P y x" using P_t_app[OF ‹P t (app (name$$ xs) x)›] by auto with snoc obtain ys where "t' = name $$ys" "list_all2 P ys xs" by blast show ?case proof (rule snoc.prems) show "t = name$$ (ys @ [y])" unfolding ‹t = app t' y› ‹t' = name $$ys› by simp next have "list_all2 P [y] [x]" using ‹P y x› by simp thus "list_all2 P (ys @ [y]) (xs @ [x])" using ‹list_all2 P ys xs› by (metis list_all2_appendI) qed qed end locale term_struct_rel_strong = term_struct_rel + assumes P_const_t: "P (const name) t ⟹ t = const name" assumes P_app_t: "P (app u⇩1 u⇩2) t ⟹ ∃t⇩1 t⇩2. t = app t⇩1 t⇩2 ∧ P u⇩1 t⇩1 ∧ P u⇩2 t⇩2" begin lemma unconst_rel: "P t u ⟹ unconst t = unconst u" by (metis P_const_t P_t_const const_name_simps(2) is_const_def unconst_const) lemma unapp_rel: "P t u ⟹ rel_option (rel_prod P P) (unapp t) (unapp u)" by (smt P_app_t P_t_app is_app_def left_right_simps(3) option.rel_sel option.sel option.simps(3) rel_prod_inject unapp_app) lemma match_rel: assumes "P t u" shows "rel_option P_env (match p t) (match p u)" using assms proof (induction p arbitrary: t u) case (Const name) thus ?case by (auto split: option.splits simp: unconst_rel) next case (App p1 p2) hence "rel_option (rel_prod P P) (unapp t) (unapp u)" by (metis unapp_rel) thus ?case using App by cases (auto split: option.splits intro!: rel_option_bind) qed auto lemma find_match_rel: assumes "list_all2 (rel_prod (=) P) cs cs'" "P t t'" shows "rel_option (rel_prod P_env (rel_prod (=) P)) (find_match cs t) (find_match cs' t')" using assms proof induction case (Cons x xs y ys) moreover obtain px tx py ty where "x = (px, tx)" "y = (py, ty)" by (cases x, cases y) auto moreover note match_rel[OF Cons(4), where p = px] ultimately show ?case by (auto elim: option.rel_cases) qed auto end fun convert_term :: "'a::term ⇒ 'b::term" where [simp del]: "convert_term t = term_cases const free (λt u. app (convert_term t) (convert_term u)) undefined t" lemmas convert_term_simps[simp] = term_cases_template[OF convert_term.simps] lemma convert_term_id: assumes "no_abs t" shows "convert_term t = t" using assms by induction auto lemma convert_term_no_abs: assumes "no_abs t" shows "no_abs (convert_term t)" using assms by induction auto lemma convert_term_inj: assumes "no_abs t" "no_abs t'" "convert_term t = convert_term t'" shows "t = t'" using assms proof (induction t arbitrary: t') case (free name) then show ?case by cases (auto dest: term_inject) next case (const name) then show ?case by cases (auto dest: term_inject) next case (app t⇩1 t⇩2) from ‹no_abs t'› show ?case apply cases using app by (auto dest: term_inject) qed lemma convert_term_idem: assumes "no_abs t" shows "convert_term (convert_term t) = convert_term t" using assms by (induction t) auto lemma convert_term_frees[simp]: assumes "no_abs t" shows "frees (convert_term t) = frees t" using assms by induction auto lemma convert_term_consts[simp]: assumes "no_abs t" shows "consts (convert_term t) = consts t" using assms by induction auto text ‹ The following lemma does not generalize to when @{prop ‹match t u = None›}. Assume matching return @{const None}, because the pattern is an application and the object is a term satisfying @{const is_abs}. Now, @{const convert_term} applied to the object will produce @{const undefined}. Of course we don't know anything about that and whether or not that matches. A workaround would be to require implementations of @{class term} to prove @{prop ‹∃t. is_abs t›}, such that @{const convert_term} could use that instead of @{const undefined}. This seems to be too much of a special case in order to be useful. › lemma convert_term_match: assumes "match t u = Some env" shows "match t (convert_term u) = Some (fmmap convert_term env)" using assms by (induction t u env rule: match_some_induct) auto section ‹Related work› text ‹ Schmidt-Schau{\ss} and Siekmann @{cite schmidt1988unification} discuss the concept of ∗‹unification algebras›. They generalize terms to ∗‹objects› and substitutions to ∗‹mappings›. A unification problem can be rephrased to finding a mapping such that a set of objects are mapped to the same object. The advantage of this generalization is that other -- superficially unrelated -- problems like solving algebraic equations or querying logic programs can be seen as unification problems. In particular, the authors note that among the similarities of such problems are that objects [have] variables'' whose names do not matter'' and there exists an operation like substituting objects into variables''. The major difference between this formalization and their work is that I use concrete types for variables and mappings. Otherwise, some similarities to here can be found. Eder @{cite eder1985properties} discusses properties of substitutions with a special focus on a partial ordering between substitutions. However, Eder constructs and uses a concrete type of first-order terms, similarly to Sternagel and Thiemann @{cite sternagel2018terms}. Williams @{cite williams1991instantiation} defines substitutions as elements in a monoid. In this setting, instantiations can be represented as ∗‹monoid actions›. Williams then proceeds to define -- for arbitrary sets of terms and variables -- the notion of ∗‹instantiation systems,› heavily drawing on notation from Schmidt-Schau{\ss} and Siekmann. Some of the presented axioms are also present in this formalization, as are some theorems that have a direct correspondence. › end # Theory Term section ‹Instantiation of class ‹term› for type ‹term›› theory Term imports Term_Class begin instantiation "term" :: "term" begin text ‹ All of these definitions need to be marked as ‹code del›; otherwise the code generator will attempt to generate these, which will fail because they are not executable. › definition abs_pred_term :: "(term ⇒ bool) ⇒ term ⇒ bool" where [code del]: "abs_pred P t ⟷ (∀x. t = Bound x ⟶ P t) ∧ (∀t'. t = Λ t' ⟶ P t' ⟶ P t)" instance proof (standard, goal_cases) case (1 P t) then show ?case by (induction t) (auto simp: abs_pred_term_def const_term_def free_term_def app_term_def) qed (auto simp: abs_pred_term_def) end lemma is_const_free[simp]: "¬ is_const (Free name)" unfolding is_const_def by simp lemma is_free_app[simp]: "¬ is_free (t u)" unfolding is_free_def by simp lemma is_free_free[simp]: "is_free (Free name)" unfolding is_free_def by simp lemma is_const_const[simp]: "is_const (Const name)" unfolding is_const_def by simp lemma list_comb_free: "is_free (list_comb f xs) ⟹ is_free f" apply (induction xs arbitrary: f) apply auto subgoal premises prems apply (insert prems(1)[OF prems(2)]) unfolding app_term_def by simp done lemma const_list_comb_free[simp]: "¬ is_free (name$$ args)" by (fastforce dest: list_comb_free simp: const_term_def) corollary const_list_comb_neq_free[simp]: "name $$args ≠ free name'" by (metis const_list_comb_free is_free_simps(1)) declare const_list_comb_neq_free[symmetric, simp] lemma match_list_comb_list_comb_eq_lengths[simp]: assumes "length ps = length vs" shows "match (list_comb f ps) (list_comb g vs) = (case match f g of Some env ⇒ (case those (map2 match ps vs) of Some envs ⇒ Some (foldl (++⇩f) env envs) | None ⇒ None) | None ⇒ None)" using assms by (induction ps vs arbitrary: f g rule: list_induct2) (auto split: option.splits simp: app_term_def) lemma matchs_match_list_comb[simp]: "match (name$$ xs) (name $$ys) = matchs xs ys" proof (induction xs arbitrary: ys rule: rev_induct) case Nil show ?case by (cases ys rule: rev_cases) (auto simp: const_term_def) next case (snoc x xs) note snoc0 = snoc have "match (name$$ xs$ x) (name $$ys) = matchs (xs @ [x]) ys" proof (cases ys rule: rev_cases) case (snoc zs z) show ?thesis unfolding snoc using snoc0 by simp qed auto thus ?case by (simp add: app_term_def) qed fun bounds :: "term ⇒ nat fset" where "bounds (Bound i) = {| i |}" | "bounds (t⇩1  t⇩2) = bounds t⇩1 |∪| bounds t⇩2" | "bounds (Λ t) = (λi. i - 1) || (bounds t - {| 0 |})" | "bounds _ = {||}" definition shift_nat :: "nat ⇒ int ⇒ nat" where [simp]: "shift_nat n k = (if k ≥ 0 then n + nat k else n - nat ¦k¦)" fun incr_bounds :: "int ⇒ nat ⇒ term ⇒ term" where "incr_bounds inc lev (Bound i) = (if i ≥ lev then Bound (shift_nat i inc) else Bound i)" | "incr_bounds inc lev (Λ u) = Λ incr_bounds inc (lev + 1) u" | "incr_bounds inc lev (t⇩1  t⇩2) = incr_bounds inc lev t⇩1  incr_bounds inc lev t⇩2" | "incr_bounds _ _ t = t" lemma incr_bounds_frees[simp]: "frees (incr_bounds n k t) = frees t" by (induction n k t rule: incr_bounds.induct) auto lemma incr_bounds_zero[simp]: "incr_bounds 0 i t = t" by (induct t arbitrary: i) auto fun replace_bound :: "nat ⇒ term ⇒ term ⇒ term" where "replace_bound lev (Bound i) t = (if i < lev then Bound i else if i = lev then incr_bounds (int lev) 0 t else Bound (i - 1))" | "replace_bound lev (t⇩1  t⇩2) t = replace_bound lev t⇩1 t  replace_bound lev t⇩2 t" | "replace_bound lev (Λ u) t = Λ replace_bound (lev + 1) u t" | "replace_bound _ t _ = t" abbreviation β_reduce :: "term ⇒ term ⇒ term" ("_ [_]⇩β") where "t [u]⇩β ≡ replace_bound 0 t u" lemma replace_bound_frees: "frees (replace_bound n t t') |⊆| frees t |∪| frees t'" by (induction n t t' rule: replace_bound.induct) auto lemma replace_bound_eq: assumes "i |∉| bounds t" shows "replace_bound i t t' = incr_bounds (-1) (i + 1) t" using assms by (induct t arbitrary: i) force+ fun wellformed' :: "nat ⇒ term ⇒ bool" where "wellformed' n (t⇩1  t⇩2) ⟷ wellformed' n t⇩1 ∧ wellformed' n t⇩2" | "wellformed' n (Bound n') ⟷ n' < n" | "wellformed' n (Λ t) ⟷ wellformed' (n + 1) t" | "wellformed' _ _ ⟷ True" lemma wellformed_inc: assumes "wellformed' k t" "k ≤ n" shows "wellformed' n t" using assms by (induct t arbitrary: k n) auto abbreviation wellformed :: "term ⇒ bool" where "wellformed ≡ wellformed' 0" lemma wellformed'_replace_bound_eq: assumes "wellformed' n t" "k ≥ n" shows "replace_bound k t u = t" using assms by (induction t arbitrary: n k) auto lemma wellformed_replace_bound_eq: "wellformed t ⟹ replace_bound k t u = t" by (rule wellformed'_replace_bound_eq) simp+ lemma incr_bounds_eq: "n ≥ k ⟹ wellformed' k t ⟹ incr_bounds i n t = t" by (induct t arbitrary: k n) force+ lemma incr_bounds_subst: assumes "⋀t. t ∈ fmran' env ⟹ wellformed t" shows "incr_bounds i n (subst t env) = subst (incr_bounds i n t) env" proof (induction t arbitrary: n) case (Free name) show ?case proof (cases "fmlookup env name") case (Some t) hence "wellformed t" using assms by (auto intro: fmran'I) hence "incr_bounds i n t = t" by (subst incr_bounds_eq) auto with Some show ?thesis by simp qed auto qed auto lemma incr_bounds_wellformed: assumes "wellformed' m u" shows "wellformed' (k + m) (incr_bounds (int k) n u)" using assms by (induct u arbitrary: n m) force+ lemma replace_bound_wellformed: assumes "wellformed u" "wellformed' (Suc k) t" "i ≤ k" shows "wellformed' k (replace_bound i t u)" using assms apply (induction t arbitrary: i k) apply auto using incr_bounds_wellformed[where m = 0, simplified] using wellformed_inc by blast lemma subst_wellformed: assumes "wellformed' n t" "fmpred (λ_. wellformed) env" shows "wellformed' n (subst t env)" using assms by (induction t arbitrary: n) (auto split: option.splits intro: wellformed_inc) global_interpretation wellformed: simple_syntactic_and "wellformed' n" for n by standard (auto simp: app_term_def) global_interpretation wellformed: subst_syntactic_and wellformed by standard (auto intro: subst_wellformed) lemma match_list_combE: assumes "match (name$$ xs) t = Some env"
obtains ys where "t = name $$ys" "matchs xs ys = Some env" proof - from assms that show thesis proof (induction xs arbitrary: t env thesis rule: rev_induct) case Nil from Nil(1) show ?case apply (auto simp: const_term_def split: option.splits if_splits) using Nil(2)[where ys = "[]"] by auto next case (snoc x xs) obtain t' y where "t = app t' y" using ‹match _ t = Some env› by (auto simp: app_term_def elim!: option_bindE) from snoc(2) obtain env⇩1 env⇩2 where "match (name$$ xs) t' = Some env⇩1" "match x y = Some env⇩2" "env = env⇩1 ++⇩f env⇩2"
unfolding ‹t = _› by (fastforce simp: app_term_def elim: option_bindE)

with snoc obtain ys where "t' = name $$ys" "matchs xs ys = Some env⇩1" by blast show ?case proof (rule snoc(3)) show "t = name$$ (ys @ [y])"
unfolding ‹t = _› ‹t' = _›
by simp
next
have "matchs [x] [y] = Some env⇩2"
using ‹match x y = _› by simp
thus "matchs (xs @ [x]) (ys @ [y]) = Some env"
unfolding ‹env = _› using ‹matchs xs ys = _›
by simp
qed
qed
qed

lemma left_nesting_neq_match:
"left_nesting f ≠ left_nesting g ⟹ is_const (fst (strip_comb f)) ⟹ match f g = None"
proof (induction f arbitrary: g)
case (Const x)
then show ?case
apply (auto split: option.splits)
apply (fold const_term_def)
apply auto
done
next
case (App f1 f2)
then have f1_g: "Suc (left_nesting f1) ≠ left_nesting g" and f1: "is_const (fst (strip_comb f1))"
apply (fold app_term_def)
by (auto split: prod.splits)
show ?case
proof (cases "unapp g")
case (Some g')
obtain g1 g2 where "g' = (g1, g2)"
by (cases g') auto
with Some have "g = app g1 g2"
by auto
with f1_g have "left_nesting f1 ≠ left_nesting g1"
by simp
with f1 App have "match f1 g1 = None"
by simp
then show ?thesis
unfolding ‹g' = _› ‹g = _›
by simp
qed simp
qed auto

context begin

private lemma match_list_comb_list_comb_none_structure:
assumes "length ps = length vs" "left_nesting f ≠ left_nesting g"
assumes "is_const (fst (strip_comb f))"
shows "match (list_comb f ps) (list_comb g vs) = None"
using assms
by (induction ps vs arbitrary: f g rule: list_induct2) (auto simp: split_beta left_nesting_neq_match)

lemma match_list_comb_list_comb_some:
assumes "match (list_comb f ps) (list_comb g vs) = Some env" "left_nesting f = left_nesting g"
assumes "is_const (fst (strip_comb f))"
shows "match f g ≠ None" "length ps = length vs"
proof -
have "match f g ≠ None ∧ length ps = length vs"
proof (cases rule: linorder_cases[where y = "length vs" and x = "length ps"])
assume "length ps = length vs"
thus ?thesis
using assms
proof (induction ps vs arbitrary: f g env rule: list_induct2)
case (Cons p ps v vs)
have "match (app f p) (app g v) ≠ None ∧ length ps = length vs"
proof (rule Cons)
show "is_const (fst (strip_comb (app f p)))"
using Cons by (simp add: split_beta)
next
show "left_nesting (app f p) = left_nesting (app g v)"
using Cons by simp
next
show "match (list_comb (app f p) ps) (list_comb (app g v) vs) = Some env"
using Cons by simp
qed
thus ?case
unfolding app_term_def
by (auto elim: match.elims option_bindE)
qed auto
next
assume "length ps < length vs"
then obtain vs⇩1 vs⇩2 where "vs = vs⇩1 @ vs⇩2" "length ps = length vs⇩2" "0 < length vs⇩1"
by (auto elim: list_split)

have "match (list_comb f ps) (list_comb (list_comb g vs⇩1) vs⇩2) = None"
proof (rule match_list_comb_list_comb_none_structure)
show "left_nesting f ≠ left_nesting (list_comb g vs⇩1)"
using assms(2) ‹0 < length vs⇩1› by simp
qed fact+
hence "match (list_comb f ps) (list_comb g vs) = None"
unfolding ‹vs = _› by simp
hence False
using assms by auto
thus ?thesis ..
next
assume "length vs < length ps"
then obtain ps⇩1 ps⇩2 where "ps = ps⇩1 @ ps⇩2" "length ps⇩2 = length vs" "0 < length ps⇩1"
by (auto elim: list_split)

have "match (list_comb (list_comb f ps⇩1) ps⇩2) (list_comb g vs) = None"
proof (rule match_list_comb_list_comb_none_structure)
show "left_nesting (list_comb f ps⇩1) ≠ left_nesting g"
using assms ‹0 < length ps⇩1› by simp
next
show "is_const (fst (strip_comb (list_comb f ps⇩1)))"
using assms by (simp add: strip_list_comb)
qed fact
hence "match (list_comb f ps) (list_comb g vs) = None"
unfolding ‹ps = _› by simp
hence False
using assms by auto
thus ?thesis ..
qed
thus "match f g ≠ None" "length ps = length vs"
by simp+
qed

end

lemma match_list_comb_list_comb_none_name[simp]:
assumes "name ≠ name'"
shows "match (name $$ps) (name'$$ vs) = None"
proof (rule ccontr)
assume "match (name $$ps) (name'$$ vs) ≠ None"
then obtain env where *: "match (name $$ps) (name'$$ vs) = Some env"
by blast
hence "match (const name) (const name' :: 'a) ≠ None"
by (rule match_list_comb_list_comb_some) (simp add: is_const_def)+
hence "name = name'"
unfolding const_term_def
by (simp split: if_splits)
thus False
using assms by blast
qed

lemma match_list_comb_list_comb_none_length[simp]:
assumes "length ps ≠ length vs"
shows "match (name $$ps) (name'$$ vs) = None"
proof (rule ccontr)
assume "match (name $$ps) (name'$$ vs) ≠ None"
then obtain env where "match (name $$ps) (name'$$ vs) = Some env"
by blast
hence "length ps = length vs"
by (rule match_list_comb_list_comb_some) (simp add: is_const_def)+
thus False
using assms by blast
qed

context term_struct_rel begin

corollary related_matchs:
assumes "matchs ps ts⇩2 = Some env⇩2" "list_all2 P ts⇩1 ts⇩2"
obtains env⇩1 where "matchs ps ts⇩1 = Some env⇩1" "P_env env⇩1 env⇩2"
proof -
fix name ― ‹dummy›

from assms have "match (name $$ps) (name$$ ts⇩2) = Some env⇩2"
by simp
moreover have "P (name $$ts⇩1) (name$$ ts⇩2)"
using assms by (auto intro: P_const_const list_combI)
ultimately obtain env⇩1 where "match (name $$ps) (name$$ ts⇩1) = Some env⇩1" "P_env env⇩1 env⇩2"
by (metis related_match)
hence "matchs ps ts⇩1 = Some env⇩1"
by simp

show thesis
by (rule that) fact+
qed

end

end

# Theory Pats

chapter ‹Wellformedness of patterns›

theory Pats
imports Term
begin

text ‹
The @{class term} class already defines a generic definition of ∗‹matching› a ∗‹pattern› with a
term. Importantly, the type of patterns is neither generic, nor a dedicated pattern type; instead,
it is @{typ term} itself.

Patterns are a proper subset of terms, with the restriction that no abstractions may occur and
there must be at most a single occurrence of any variable (usually known as ∗‹linearity›).
The first restriction can be modelled in a datatype, the second cannot. Consequently, I define a
predicate that captures both properties.

Using linearity, many more generic properties can be proved, for example that substituting the
environment produced by matching yields the matched term.
›

fun linear :: "term ⇒ bool" where
"linear (Free _) ⟷ True" |
"linear (Const _) ⟷ True" |
"linear (t⇩1 $t⇩2) ⟷ linear t⇩1 ∧ linear t⇩2 ∧ ¬ is_free t⇩1 ∧ fdisjnt (frees t⇩1) (frees t⇩2)" | "linear _ ⟷ False" lemmas linear_simps[simp] = linear.simps(2)[folded const_term_def] linear.simps(3)[folded app_term_def] lemma linear_implies_no_abs: "linear t ⟹ no_abs t" proof induction case Const then show ?case by (fold const_term_def free_term_def app_term_def) auto next case Free then show ?case by (fold const_term_def free_term_def app_term_def) auto next case App then show ?case by (fold const_term_def free_term_def app_term_def) auto qed auto fun linears :: "term list ⇒ bool" where "linears [] ⟷ True" | "linears (t # ts) ⟷ linear t ∧ fdisjnt (frees t) (freess ts) ∧ linears ts" lemma linears_butlastI[intro]: "linears ts ⟹ linears (butlast ts)" proof (induction ts) case (Cons t ts) hence "linear t" "linears (butlast ts)" by simp+ moreover have " fdisjnt (frees t) (freess (butlast ts))" proof (rule fdisjnt_subset_right) show "freess (butlast ts) |⊆| freess ts" by (rule freess_subset) (auto dest: in_set_butlastD) next show "fdisjnt (frees t) (freess ts)" using Cons by simp qed ultimately show ?case by simp qed simp lemma linears_appI[intro]: assumes "linears xs" "linears ys" "fdisjnt (freess xs) (freess ys)" shows "linears (xs @ ys)" using assms proof (induction xs) case (Cons z zs) hence "linears zs" by simp+ have "fdisjnt (frees z) (freess zs |∪| freess ys)" proof (rule fdisjnt_union_right) show "fdisjnt (frees z) (freess zs)" using ‹linears (z # zs)› by simp next have "frees z |⊆| freess (z # zs)" unfolding freess_def by simp thus "fdisjnt (frees z) (freess ys)" by (rule fdisjnt_subset_left) fact qed moreover have "linears (zs @ ys)" proof (rule Cons) show "fdisjnt (freess zs) (freess ys)" using Cons by (auto intro: freess_subset fdisjnt_subset_left) qed fact+ ultimately show ?case using Cons by auto qed simp lemma linears_linear: "linears ts ⟹ t ∈ set ts ⟹ linear t" by (induct ts) auto lemma linears_singleI[intro]: "linear t ⟹ linears [t]" by (simp add: freess_def fdisjnt_alt_def) lemma linear_strip_comb: "linear t ⟹ linear (fst (strip_comb t))" by (induction t rule: strip_comb_induct) (auto simp: split_beta) lemma linears_strip_comb: "linear t ⟹ linears (snd (strip_comb t))" proof (induction t rule: strip_comb_induct) case (app t⇩1 t⇩2) have "linears (snd (strip_comb t⇩1) @ [t⇩2])" proof (intro linears_appI linears_singleI) have "freess (snd (strip_comb t⇩1)) |⊆| frees t⇩1" by (subst frees_strip_comb) auto moreover have "fdisjnt (frees t⇩1) (frees t⇩2)" using app by auto ultimately have "fdisjnt (freess (snd (strip_comb t⇩1))) (frees t⇩2)" by (rule fdisjnt_subset_left) thus "fdisjnt (freess (snd (strip_comb t⇩1))) (freess [t⇩2])" by simp next show "linear t⇩2" "linears (snd (strip_comb t⇩1))" using app by auto qed thus ?case by (simp add: split_beta) qed auto lemma linears_appendD: assumes "linears (xs @ ys)" shows "linears xs" "linears ys" "fdisjnt (freess xs) (freess ys)" using assms proof (induction xs) case (Cons x xs) assume "linears ((x # xs) @ ys)" hence "linears (x # (xs @ ys))" by simp hence "linears (xs @ ys)" "linear x" "fdisjnt (frees x) (freess (xs @ ys))" by auto hence "linears xs" using Cons by simp moreover have "fdisjnt (frees x) (freess xs)" proof (rule fdisjnt_subset_right) show "freess xs |⊆| freess (xs @ ys)" by simp qed fact ultimately show "linears (x # xs)" using ‹linear x› by auto have "fdisjnt (freess xs) (freess ys)" by (rule Cons) fact moreover have "fdisjnt (frees x) (freess ys)" proof (rule fdisjnt_subset_right) show "freess ys |⊆| freess (xs @ ys)" by simp qed fact ultimately show "fdisjnt (freess (x # xs)) (freess ys)" unfolding fdisjnt_alt_def by auto qed (auto simp: fdisjnt_alt_def) lemma linear_list_comb: assumes "linear f" "linears xs" "fdisjnt (frees f) (freess xs)" "¬ is_free f" shows "linear (list_comb f xs)" using assms proof (induction xs arbitrary: f) case (Cons x xs) hence *: "fdisjnt (frees f) (frees x |∪| freess xs)" by simp have "linear (list_comb (f$ x) xs)"
proof (rule Cons)
have "linear x"
using Cons by simp
moreover have "fdisjnt (frees f) (frees x)"
using * by (auto intro: fdisjnt_subset_right)
ultimately show "linear (f $x)" using assms Cons by simp next show "linears xs" using Cons by simp next have "fdisjnt (frees f) (freess xs)" using * by (auto intro: fdisjnt_subset_right) moreover have "fdisjnt (frees x) (freess xs)" using Cons by simp ultimately show "fdisjnt (frees (f$ x)) (freess xs)"
by (auto intro: fdisjnt_union_left)
qed auto
thus ?case
by (simp add: app_term_def)
qed auto

corollary linear_list_comb': "linears xs ⟹ linear (name $$xs)" by (auto intro: linear_list_comb simp: fdisjnt_alt_def) lemma linear_strip_comb_cases[consumes 1]: assumes "linear pat" obtains (comb) s args where "strip_comb pat = (Const s, args)" "pat = s$$ args"
| (free) s where "strip_comb pat = (Free s, [])" "pat = Free s"
using assms
proof (induction pat rule: strip_comb_induct)
case (app t⇩1 t⇩2)
show ?case
proof (rule "app.IH")
show "linear t⇩1"
using app by simp
next
fix s
assume "strip_comb t⇩1 = (Free s, [])"
hence "t⇩1 = Free s"
by (metis fst_conv snd_conv strip_comb_empty)
hence False
using app by simp
thus thesis
by simp
next
fix s args
assume "strip_comb t⇩1 = (Const s, args)"
with app show thesis
by (fastforce simp add: strip_comb_app)
qed
next
case (no_app t)
thus ?case
by (cases t) (auto simp: const_term_def)
qed

lemma wellformed_linearI: "linear t ⟹ wellformed' n t"
by (induct t) auto

lemma pat_cases:
obtains (free) s where "t = Free s"
| (comb) name args where "linears args" "t = name $$args" | (nonlinear) "¬ linear t" proof (cases t) case Free thus thesis using free by simp next case Bound thus thesis using nonlinear by simp next case Abs thus thesis using nonlinear by simp next case (Const name) have "linears []" by simp moreover have "t = name$$ []" unfolding Const by (simp add: const_term_def)
ultimately show thesis
by (rule comb)
next
case (App u v)
show thesis
proof (cases "linear t")
case False
thus thesis using nonlinear by simp
next
case True
thus thesis
proof (cases rule: linear_strip_comb_cases)
case free
thus thesis using that by simp
next
case (comb name args)
moreover hence "linears (snd (strip_comb t))"
using True by (blast intro: linears_strip_comb)
ultimately have "linears args"
by simp
thus thesis using that comb by simp
qed
qed
qed

corollary linear_pat_cases[consumes 1]:
assumes "linear t"
obtains (free) s where "t = Free s"
| (comb) name args where "linears args" "t = name $$args" using assms by (metis pat_cases) lemma linear_pat_induct[consumes 1, case_names free comb]: assumes "linear t" assumes "⋀s. P (Free s)" assumes "⋀name args. linears args ⟹ (⋀arg. arg ∈ set args ⟹ P arg) ⟹ P (name$$ args)"
shows "P t"
using wf_measure[of size] ‹linear t›
proof (induction t)
case (less t)

show ?case
using ‹linear t›
proof (cases rule: linear_pat_cases)
case (free name)
thus ?thesis
using assms by simp
next
case (comb name args)
show ?thesis
proof (cases "args = []")
case True
thus ?thesis
using assms comb by fastforce
next
case False
show ?thesis
unfolding ‹t = _›
proof (rule assms)
fix arg
assume "arg ∈ set args"

then have "(arg, t) ∈ measure size"
unfolding ‹t = _›
by (induction args) auto

moreover have "linear arg"
using ‹arg ∈ set args› ‹linears args›
by (auto dest: linears_linear)

ultimately show "P arg"
using less by auto
qed fact
qed
qed
qed

context begin

private lemma match_subst_correctness0:
assumes "linear t"
shows "case match t u of
None ⇒ (∀env. subst (convert_term t) env ≠ u) |
Some env ⇒ subst (convert_term t) env = u"
using assms proof (induction t arbitrary: u)
case Free
show ?case
unfolding match.simps
by (fold free_term_def) auto
next
case Const
show ?case
unfolding match.simps
by (fold const_term_def) (auto split: option.splits)
next
case (App t⇩1 t⇩2)
hence linear: "linear t⇩1" "linear t⇩2" "fdisjnt (frees t⇩1) (frees t⇩2)"
by simp+

show ?case
proof (cases "unapp u")
case None
then show ?thesis
apply simp
apply (fold app_term_def)
apply simp
using app_simps(3) is_app_def by blast
next
case (Some u')
then obtain u⇩1 u⇩2 where u: "unapp u = Some (u⇩1, u⇩2)" by (cases u') auto
hence "u = app u⇩1 u⇩2" by auto

note 1 = App(1)[OF ‹linear t⇩1›, of u⇩1]
note 2 = App(2)[OF ‹linear t⇩2›, of u⇩2]

show ?thesis
proof (cases "match t⇩1 u⇩1")
case None
then show ?thesis
using u
apply simp
apply (fold app_term_def)
using 1 by auto
next
case (Some env⇩1)
with 1 have s1: "subst (convert_term t⇩1) env⇩1 = u⇩1" by simp
show ?thesis
proof (cases "match t⇩2 u⇩2")
case None
then show ?thesis
using u
apply simp
apply (fold app_term_def)
using 2 by auto
next
case (Some env⇩2)
with 2 have s2: "subst (convert_term t⇩2) env⇩2 = u⇩2" by simp

note match = ‹match t⇩1 u⇩1 = Some env⇩1› ‹match t⇩2 u⇩2 = Some env⇩2›

let ?env = "env⇩1 ++⇩f env⇩2"
from match have "frees t⇩1 = fmdom env⇩1" "frees t⇩2 = fmdom env⇩2"
by (auto simp: match_dom)
with linear have "env⇩1 = fmrestrict_fset (frees t⇩1) ?env" "env⇩2 = fmrestrict_fset (frees t⇩2) ?env"
apply auto
apply (auto simp: fmfilter_alt_defs)
apply (subst fmfilter_false; auto simp: fdisjnt_alt_def intro: fmdomI)+
done
with s1 s2 have "subst (convert_term t⇩1) ?env = u⇩1" "subst (convert_term t⇩2) ?env = u⇩2"
using linear
by (metis subst_restrict' convert_term_frees linear_implies_no_abs)+

then show ?thesis
using match unfolding ‹u = _›
apply simp
apply (fold app_term_def)
by simp
qed
qed
qed
qed auto

lemma match_subst_some[simp]:
"match t u = Some env ⟹ linear t ⟹ subst (convert_term t) env = u"
by (metis (mono_tags) match_subst_correctness0 option.simps(5))

lemma match_subst_none:
"match t u = None ⟹ linear t ⟹ subst (convert_term t) env = u ⟹ False"
by (metis (mono_tags, lifting) match_subst_correctness0 option.simps(4))

end

(* FIXME inverse direction? *)

lemma match_matches: "match t u = Some env ⟹ linear t ⟹ t ≲ u"
by (metis match_subst_some linear_implies_no_abs convert_term_id matchesI)

lemma overlapping_var1I: "overlapping (Free name) t"
proof (intro overlappingI matchesI)
show "subst (Free name) (fmap_of_list [(name, t)]) = t"
by simp
next
show "subst t fmempty = t"
by simp
qed

lemma overlapping_var2I: "overlapping t (Free name)"
proof (intro overlappingI matchesI)
show "subst (Free name) (fmap_of_list [(name, t)]) = t"
by simp
next
show "subst t fmempty = t"
by simp
qed

lemma non_overlapping_appI1: "non_overlapping t⇩1 u⇩1 ⟹ non_overlapping (t⇩1 $t⇩2) (u⇩1$ u⇩2)"
unfolding overlapping_def matches_def by auto

lemma non_overlapping_appI2: "non_overlapping t⇩2 u⇩2 ⟹ non_overlapping (t⇩1 $t⇩2) (u⇩1$ u⇩2)"
unfolding overlapping_def matches_def by auto

lemma non_overlapping_app_constI: "non_overlapping (t⇩1 $t⇩2) (Const name)" unfolding overlapping_def matches_def by simp lemma non_overlapping_const_appI: "non_overlapping (Const name) (t⇩1$ t⇩2)"
unfolding overlapping_def matches_def by simp

lemma non_overlapping_const_constI: "x ≠ y ⟹ non_overlapping (Const x) (Const y)"
unfolding overlapping_def matches_def by simp

lemma match_overlapping:
assumes "linear t⇩1" "linear t⇩2"
assumes "match t⇩1 u = Some env⇩1" "match t⇩2 u = Some env⇩2"
shows "overlapping t⇩1 t⇩2"
proof -
define env⇩1' where "env⇩1' = (fmmap convert_term env⇩1 :: (name, term) fmap)"
define env⇩2' where "env⇩2' = (fmmap convert_term env⇩2 :: (name, term) fmap)"
from assms have "match t⇩1 (convert_term u :: term) = Some env⇩1'" "match t⇩2 (convert_term u :: term) = Some env⇩2'"
unfolding env⇩1'_def env⇩2'_def
by (metis convert_term_match)+
with assms show ?thesis
by (metis overlappingI match_matches)
qed

end

# Theory Nterm

chapter ‹Terms with explicit bound variable names›

theory Nterm
imports Term_Class
begin

text ‹
The ‹nterm› type is similar to @{typ term}, but removes the distinction between bound and free
variables. Instead, there are only named variables.
›

datatype nterm =
Nconst name |
Nvar name |
Nabs name nterm ("Λ⇩n _. _" [0, 50] 50) |
Napp nterm nterm (infixl "$⇩n" 70) derive linorder nterm instantiation nterm :: pre_term begin definition app_nterm where "app_nterm t u = t$⇩n u"

fun unapp_nterm where
"unapp_nterm (t $⇩n u) = Some (t, u)" | "unapp_nterm _ = None" definition const_nterm where "const_nterm = Nconst" fun unconst_nterm where "unconst_nterm (Nconst name) = Some name" | "unconst_nterm _ = None" definition free_nterm where "free_nterm = Nvar" fun unfree_nterm where "unfree_nterm (Nvar name) = Some name" | "unfree_nterm _ = None" fun frees_nterm :: "nterm ⇒ name fset" where "frees_nterm (Nvar x) = {| x |}" | "frees_nterm (t⇩1$⇩n t⇩2) = frees_nterm t⇩1 |∪| frees_nterm t⇩2" |
"frees_nterm (Λ⇩n x. t) = frees_nterm t - {| x |}" |
"frees_nterm (Nconst _) = {||}"

fun subst_nterm :: "nterm ⇒ (name, nterm) fmap ⇒ nterm" where
"subst_nterm (Nvar s) env = (case fmlookup env s of Some t ⇒ t | None ⇒ Nvar s)" |
"subst_nterm (t⇩1 $⇩n t⇩2) env = subst_nterm t⇩1 env$⇩n subst_nterm t⇩2 env" |
"subst_nterm (Λ⇩n x. t) env = (Λ⇩n x. subst_nterm t (fmdrop x env))" |
"subst_nterm t env = t"

fun consts_nterm :: "nterm ⇒ name fset" where
"consts_nterm (Nconst x) = {| x |}" |
"consts_nterm (t⇩1 $⇩n t⇩2) = consts_nterm t⇩1 |∪| consts_nterm t⇩2" | "consts_nterm (Nabs _ t) = consts_nterm t" | "consts_nterm (Nvar _) = {||}" instance by standard (auto simp: app_nterm_def const_nterm_def free_nterm_def elim: unapp_nterm.elims unconst_nterm.elims unfree_nterm.elims split: option.splits) end instantiation nterm :: "term" begin definition abs_pred_nterm :: "(nterm ⇒ bool) ⇒ nterm ⇒ bool" where [code del]: "abs_pred P t ⟷ (∀t' x. t = (Λ⇩n x. t') ⟶ P t' ⟶ P t)" instance proof (standard, goal_cases) case (1 P t) then show ?case by (induction t) (auto simp: abs_pred_nterm_def const_nterm_def free_nterm_def app_nterm_def) next case 3 show ?case unfolding abs_pred_nterm_def apply auto apply (subst fmdrop_comm) by auto next case 4 show ?case unfolding abs_pred_nterm_def apply auto apply (erule_tac x = "fmdrop x env⇩1" in allE) apply (erule_tac x = "fmdrop x env⇩2" in allE) by (auto simp: fdisjnt_alt_def) next case 5 show ?case unfolding abs_pred_nterm_def apply clarify subgoal for t' x env apply (erule allE[where x = "fmdrop x env"]) by auto done next case 6 show ?case unfolding abs_pred_nterm_def apply clarify subgoal premises prems[rule_format] for t x env unfolding consts_nterm.simps subst_nterm.simps frees_nterm.simps apply (subst prems) unfolding fmimage_drop fmdom_drop apply (rule arg_cong[where f = "(|∪|) (consts t)"]) apply (rule arg_cong[where f = ffUnion]) apply (rule arg_cong[where f = "λx. consts || fmimage env x"]) by auto done qed (auto simp: abs_pred_nterm_def) end lemma no_abs_abs[simp]: "¬ no_abs (Λ⇩n x. t)" by (subst no_abs.simps) (auto simp: term_cases_def) end # Theory Term_to_Nterm chapter ‹Converting between ‹term›s and ‹nterm›s› theory Term_to_Nterm imports Fresh_Class Find_First Term Nterm begin section ‹‹α›-equivalence› inductive alpha_equiv :: "(name, name) fmap ⇒ nterm ⇒ nterm ⇒ bool" where const: "alpha_equiv env (Nconst x) (Nconst x)" | var1: "x |∉| fmdom env ⟹ x |∉| fmran env ⟹ alpha_equiv env (Nvar x) (Nvar x)" | var2: "fmlookup env x = Some y ⟹ alpha_equiv env (Nvar x) (Nvar y)" | abs: "alpha_equiv (fmupd x y env) n1 n2 ⟹ alpha_equiv env (Λ⇩n x. n1) (Λ⇩n y. n2)" | app: "alpha_equiv env n1 n2 ⟹ alpha_equiv env m1 m2 ⟹ alpha_equiv env (n1$⇩n m1) (n2 $⇩n m2)" code_pred alpha_equiv . abbreviation alpha_eq :: "nterm ⇒ nterm ⇒ bool" (infixl "≈⇩α" 50) where "alpha_eq n1 n2 ≡ alpha_equiv fmempty n1 n2" lemma alpha_equiv_refl[intro?]: assumes "fmpred (=) Γ" shows "alpha_equiv Γ t t" using assms proof (induction t arbitrary: Γ) case Napp show ?case apply (rule alpha_equiv.app; rule Napp) using Napp.prems unfolding fdisjnt_alt_def by auto qed (auto simp: fdisjnt_alt_def intro: alpha_equiv.intros) corollary alpha_eq_refl: "alpha_eq t t" by (auto intro: alpha_equiv_refl) section ‹From @{typ term} to @{typ nterm}› fun term_to_nterm :: "name list ⇒ term ⇒ (name, nterm) state" where "term_to_nterm _ (Const name) = State_Monad.return (Nconst name)" | "term_to_nterm _ (Free name) = State_Monad.return (Nvar name)" | "term_to_nterm Γ (Bound n) = State_Monad.return (Nvar (Γ ! n))" | "term_to_nterm Γ (Λ t) = do { n ← fresh_create; e ← term_to_nterm (n # Γ) t; State_Monad.return (Λ⇩n n. e) }" | "term_to_nterm Γ (t⇩1$ t⇩2) = do {
e⇩1 ← term_to_nterm Γ t⇩1;
e⇩2 ← term_to_nterm Γ t⇩2;
State_Monad.return (e⇩1 $⇩n e⇩2) }" lemmas term_to_nterm_induct = term_to_nterm.induct[case_names const free bound abs app] lemma term_to_nterm: assumes "no_abs t" shows "fst (run_state (term_to_nterm Γ t) x) = convert_term t" using assms apply (induction arbitrary: x) apply auto by (auto simp: free_term_def free_nterm_def const_term_def const_nterm_def app_term_def app_nterm_def split_beta split: prod.splits) definition term_to_nterm' :: "term ⇒ nterm" where "term_to_nterm' t = frun_fresh (term_to_nterm [] t) (frees t)" lemma term_to_nterm_mono: "mono_state (term_to_nterm Γ x)" by (induction Γ x rule: term_to_nterm.induct) (auto intro: bind_mono_strong) lemma term_to_nterm_vars0: assumes "wellformed' (length Γ) t" shows "frees (fst (run_state (term_to_nterm Γ t) s)) |⊆| frees t |∪| fset_of_list Γ" using assms proof (induction Γ t arbitrary: s rule: term_to_nterm_induct) case (bound Γ i) hence "Γ ! i |∈| fset_of_list Γ" including fset.lifting by transfer auto thus ?case by (auto simp: State_Monad.return_def) next case (abs Γ t) let ?x = "next s" from abs have "frees (fst (run_state (term_to_nterm (?x # Γ) t) ?x)) |⊆| frees t |∪| {|?x|} |∪| fset_of_list Γ" by simp thus ?case by (auto simp: create_alt_def split_beta) qed (auto simp: split_beta) corollary term_to_nterm_vars: assumes "wellformed t" shows "frees (fresh_frun (term_to_nterm [] t) F) |⊆| frees t" proof - let ?Γ = "[]" from assms have "wellformed' (length ?Γ) t" by simp hence "frees (fst (run_state (term_to_nterm ?Γ t) (fNext F))) |⊆| (frees t |∪| fset_of_list ?Γ)" by (rule term_to_nterm_vars0) thus ?thesis by (simp add: fresh_fNext_def fresh_frun_def) qed corollary term_to_nterm_closed: "closed t ⟹ wellformed t ⟹ closed (term_to_nterm' t)" using term_to_nterm_vars[where F = "frees t" and t = t, simplified] unfolding closed_except_def term_to_nterm'_def by (simp add: fresh_frun_def) lemma term_to_nterm_consts: "pred_state (λt'. consts t' = consts t) (term_to_nterm Γ t)" apply (rule pred_stateI) apply (induction t arbitrary: Γ) apply (auto split: prod.splits) done section ‹From @{typ nterm} to @{typ term}› fun nterm_to_term :: "name list ⇒ nterm ⇒ term" where "nterm_to_term Γ (Nconst name) = Const name" | "nterm_to_term Γ (Nvar name) = (case find_first name Γ of Some n ⇒ Bound n | None ⇒ Free name)" | "nterm_to_term Γ (t$⇩n u) = nterm_to_term Γ t $nterm_to_term Γ u" | "nterm_to_term Γ (Λ⇩n x. t) = Λ nterm_to_term (x # Γ) t" lemma nterm_to_term: assumes "no_abs t" "fdisjnt (fset_of_list Γ) (frees t)" shows "nterm_to_term Γ t = convert_term t" using assms proof (induction arbitrary: Γ) case (free name) then show ?case apply simp apply (auto simp: free_nterm_def free_term_def fdisjnt_alt_def split: option.splits) apply (rule find_first_none) by (metis fset_of_list_elem) next case (const name) show ?case apply simp by (simp add: const_nterm_def const_term_def) next case (app t⇩1 t⇩2) then have "nterm_to_term Γ t⇩1 = convert_term t⇩1" "nterm_to_term Γ t⇩2 = convert_term t⇩2" by (auto simp: fdisjnt_alt_def finter_funion_distrib) then show ?case apply simp by (simp add: app_nterm_def app_term_def) qed abbreviation "nterm_to_term' ≡ nterm_to_term []" lemma nterm_to_term': "no_abs t ⟹ nterm_to_term' t = convert_term t" by (auto simp: fdisjnt_alt_def nterm_to_term) lemma nterm_to_term_frees[simp]: "frees (nterm_to_term Γ t) = frees t - fset_of_list Γ" proof (induction t arbitrary: Γ) case (Nvar name) show ?case proof (cases "find_first name Γ") case None hence "name |∉| fset_of_list Γ" including fset.lifting by transfer (metis find_first_some option.distinct(1)) with None show ?thesis by auto next case (Some u) hence "name |∈| fset_of_list Γ" including fset.lifting by transfer (metis find_first_none option.distinct(1)) with Some show ?thesis by auto qed qed (auto split: option.splits) section ‹Correctness› text ‹Some proofs in this section have been contributed by Yu Zhang.› lemma term_to_nterm_nterm_to_term0: assumes "wellformed' (length Γ) t" "fdisjnt (fset_of_list Γ) (frees t)" "distinct Γ" assumes "fBall (frees t |∪| fset_of_list Γ) (λx. x ≤ s)" shows "nterm_to_term Γ (fst (run_state (term_to_nterm Γ t) s)) = t" using assms proof (induction Γ t arbitrary: s rule: term_to_nterm_induct) case (free Γ name) hence "fdisjnt (fset_of_list Γ) {|name|}" by simp hence "name ∉ set Γ" including fset.lifting by transfer' (simp add: disjnt_def) hence "find_first name Γ = None" by (rule find_first_none) thus ?case by (simp add: State_Monad.return_def) next case (bound Γ i) thus ?case by (simp add: State_Monad.return_def find_first_some_index) next case (app Γ t⇩1 t⇩2) have "fdisjnt (fset_of_list Γ) (frees t⇩1)" apply (rule fdisjnt_subset_right[where N = "frees t⇩1 |∪| frees t⇩2"]) using app by auto have "fdisjnt (fset_of_list Γ) (frees t⇩2)" apply (rule fdisjnt_subset_right[where N = "frees t⇩1 |∪| frees t⇩2"]) using app by auto have s: "s ≤ snd (run_state (term_to_nterm Γ t⇩1) s)" apply (rule state_io_relD[OF term_to_nterm_mono]) apply (rule surjective_pairing) done show ?case apply (auto simp: split_beta) subgoal apply (rule app) subgoal using app by simp subgoal by fact subgoal by fact using app by auto subgoal apply (rule app) subgoal using app by simp subgoal by fact subgoal by fact using app s by force+ done next case (abs Γ t) have "next s |∉| frees t |∪| fset_of_list Γ" using abs(5)[simplified] by (rule next_ge_fall) have "nterm_to_term (next s # Γ) (fst (run_state (term_to_nterm (next s # Γ) t) (next s))) = t" proof (subst abs) show "wellformed' (length (next s # Γ)) t" using abs by auto show "fdisjnt (fset_of_list (next s # Γ)) (frees t)" apply simp apply (rule fdisjnt_insert) using ‹next s |∉| frees t |∪| fset_of_list Γ› abs by auto show "distinct (next s # Γ)" apply simp apply rule using ‹next s |∉| frees t |∪| fset_of_list Γ› apply (simp add: fset_of_list_elem) apply fact done show "fBall (frees t |∪| fset_of_list (next s # Γ)) (λx. x ≤ next s)" using abs(5) apply simp apply (rule fBall_pred_weaken[where P = "λx. x ≤ s"]) subgoal apply simp by (meson dual_order.strict_implies_order dual_order.strict_trans2 fresh_class.next_ge) subgoal by assumption done qed auto thus ?case by (auto simp: split_beta create_alt_def) qed (auto simp: State_Monad.return_def) lemma term_to_nterm_nterm_to_term: assumes "wellformed t" "frees t |⊆| S" shows "nterm_to_term' (frun_fresh (term_to_nterm [] t) (S |∪| Q)) = t" proof (rule term_to_nterm_nterm_to_term0) show "wellformed' (length []) t" using assms by simp next show "fdisjnt (fset_of_list []) (frees t)" unfolding fdisjnt_alt_def by simp next have "fBall (S |∪| Q) (λx. x < fresh.fNext next default (S |∪| Q))" by (metis fNext_geq_not_member fresh_fNext_def le_less_linear fBallI) hence "fBall (S |∪| Q) (λx. x ≤ fresh.fNext next default (S |∪| Q))" by (meson fBall_pred_weaken less_eq_name_def) thus "fBall (frees t |∪| fset_of_list []) (λx. x ≤ fresh.fNext next default (S |∪| Q))" using ‹frees t |⊆| S› by auto qed simp corollary term_to_nterm_nterm_to_term_simple: assumes "wellformed t" shows "nterm_to_term' (term_to_nterm' t) = t" unfolding term_to_nterm'_def using assms by (metis order_refl sup.idem term_to_nterm_nterm_to_term) lemma nterm_to_term_eq: assumes "frees u |⊆| fset_of_list (common_prefix Γ Γ')" shows "nterm_to_term Γ u = nterm_to_term Γ' u" using assms proof (induction u arbitrary: Γ Γ') case (Nvar name) hence "name ∈ set (common_prefix Γ Γ')" unfolding frees_nterm.simps including fset.lifting by transfer' simp thus ?case by (auto simp: common_prefix_find) next case (Nabs x t) hence *: "frees t - {|x|} |⊆| fset_of_list (common_prefix Γ Γ')" by simp show ?case apply simp apply (rule Nabs) using * Nabs by auto qed auto corollary nterm_to_term_eq_closed: "closed t ⟹ nterm_to_term Γ t = nterm_to_term Γ' t" by (rule nterm_to_term_eq) (auto simp: closed_except_def) lemma nterm_to_term_wellformed: "wellformed' (length Γ) (nterm_to_term Γ t)" proof (induction t arbitrary: Γ) case (Nabs x t) hence "wellformed' (Suc (length Γ)) (nterm_to_term (x # Γ) t)" by (metis length_Cons) thus ?case by auto qed (auto simp: find_first_correct split: option.splits) corollary nterm_to_term_closed_wellformed: "closed t ⟹ wellformed (nterm_to_term Γ t)" by (metis Ex_list_of_length nterm_to_term_eq_closed nterm_to_term_wellformed) lemma nterm_to_term_term_to_nterm: assumes "frees t |⊆| fset_of_list Γ" "length Γ = length Γ'" shows "alpha_equiv (fmap_of_list (zip Γ Γ')) t (fst (run_state (term_to_nterm Γ' (nterm_to_term Γ t)) s))" using assms proof (induction Γ t arbitrary: s Γ' rule:nterm_to_term.induct) case (4 Γ x t) show ?case apply (simp add: split_beta) apply (rule alpha_equiv.abs) using "4.IH"[where Γ' = "next s # Γ'"] "4.prems" by (fastforce simp: create_alt_def intro: alpha_equiv.intros) qed (force split: option.splits intro: find_first_some intro!: alpha_equiv.intros simp: fset_of_list_elem find_first_in_map split_beta fdisjnt_alt_def)+ corollary nterm_to_term_term_to_nterm': "closed t ⟹ t ≈⇩α term_to_nterm' (nterm_to_term' t)" unfolding term_to_nterm'_def closed_except_def apply (rule nterm_to_term_term_to_nterm[where Γ = "[]" and Γ' = "[]", simplified]) by auto context begin private lemma term_to_nterm_alpha_equiv0: "length Γ1 = length Γ2 ⟹ distinct Γ1 ⟹ distinct Γ2 ⟹ wellformed' (length Γ1) t1 ⟹ fresh_fin (frees t1 |∪| fset_of_list Γ1) s1 ⟹ fdisjnt (fset_of_list Γ1) (frees t1) ⟹ fresh_fin (frees t1 |∪| fset_of_list Γ2) s2 ⟹ fdisjnt (fset_of_list Γ2) (frees t1) ⟹ alpha_equiv (fmap_of_list (zip Γ1 Γ2)) (fst( run_state (term_to_nterm Γ1 t1) s1)) (fst ( run_state (term_to_nterm Γ2 t1) s2))" proof (induction Γ1 t1 arbitrary: Γ2 s1 s2 rule:term_to_nterm_induct) case (free Γ1 name) then have "name |∉| fmdom (fmap_of_list (zip Γ1 Γ2))" unfolding fdisjnt_alt_def by force moreover have "name |∉| fmran (fmap_of_list (zip Γ1 Γ2))" apply rule apply (subst (asm) fmran_of_list) apply (subst (asm) fset_of_list_map[symmetric]) apply (subst (asm) distinct_clearjunk_id) subgoal apply (subst map_fst_zip) apply fact apply fact done apply (subst (asm) map_snd_zip) apply fact using free unfolding fdisjnt_alt_def by fastforce ultimately show ?case by (force intro:alpha_equiv.intros) next case (abs Γ t) have *: "next s1 > s1" "next s2 > s2" using next_ge by force+ with abs have "next s1 ∉ set Γ" "next s2 ∉ set Γ2" by (metis fBall_funion fset_of_list_elem next_ge_fall)+ have "fresh_fin (frees t |∪| fset_of_list Γ) (next s1)" "fresh_fin (frees t |∪| fset_of_list Γ2) (next s2)" using * abs by (smt dual_order.trans fBall_pred_weaken frees_term.simps(3) less_imp_le)+ have "fdisjnt (finsert (next s1) (fset_of_list Γ)) (frees t)" "fdisjnt (finsert (next s2) (fset_of_list Γ2)) (frees t)" unfolding fdisjnt_alt_def using abs frees_term.simps by (metis fdisjnt_alt_def finter_finsert_right funionCI inf_commute next_ge_fall)+ have "wellformed' (Suc (length Γ2)) t" using wellformed'.simps abs by (metis Suc_eq_plus1) show ?case apply (auto simp: split_beta create_alt_def) apply rule apply (rule abs.IH[of _ "next s2 # Γ2", simplified]) by (fact | rule)+ next case (app Γ1 t⇩1 t⇩2) hence "wellformed' (length Γ1) t⇩1" "wellformed' (length Γ1) t⇩2" and "fresh_fin (frees t⇩1 |∪| fset_of_list Γ1) s1" "fresh_fin (frees t⇩1 |∪| fset_of_list Γ2) s2" and "fdisjnt (fset_of_list Γ1) (frees t⇩1)" "fdisjnt (fset_of_list Γ2) (frees t⇩1)" and "fdisjnt (fset_of_list Γ1) (frees t⇩2)" "fdisjnt (fset_of_list Γ2) (frees t⇩2)" using app unfolding fdisjnt_alt_def by (auto simp: inf_sup_distrib1) have "s1 ≤ snd (run_state (term_to_nterm Γ1 t⇩1) s1)" "s2 ≤ snd (run_state (term_to_nterm Γ2 t⇩1) s2)" using term_to_nterm_mono by (simp add: state_io_rel_def)+ hence "fresh_fin (frees t⇩2 |∪| fset_of_list Γ1) (snd (run_state (term_to_nterm Γ1 t⇩1) s1))" using ‹fresh_fin (frees (t⇩1$ t⇩2) |∪| fset_of_list Γ1) s1›
by force

have "fresh_fin (frees t⇩2 |∪| fset_of_list Γ2) (snd (run_state (term_to_nterm Γ2 t⇩1) s2))"
apply rule
using app frees_term.simps ‹s2 ≤ _› dual_order.trans
by (metis fbspec funion_iff)

show ?case
apply (auto simp: split_beta create_alt_def)
apply (rule alpha_equiv.app)
subgoal
apply (rule app)
apply (simp | fact)+
done
subgoal
apply (rule app)
apply (simp | fact)+
done
done
qed (force intro: alpha_equiv.intros simp: fmlookup_of_list in_set_zip)+

lemma term_to_nterm_alpha_equiv:
assumes "length Γ1 = length Γ2" "distinct Γ1" "distinct Γ2" "closed t"
assumes "wellformed' (length Γ1) t"
assumes "fresh_fin (fset_of_list Γ1) s1" "fresh_fin (fset_of_list Γ2) s2"
shows "alpha_equiv (fmap_of_list (zip Γ1 Γ2)) (fst (run_state (term_to_nterm Γ1 t) s1)) (fst (run_state (term_to_nterm Γ2 t) s2))"
― ‹An instantiated version of this lemma with @{prop ‹Γ1 = []›} and @{prop ‹Γ2 = []›}
would not make sense because then it would just be a special case of
@{thm [source=true] alpha_eq_refl}.›
using assms
by (simp add: fdisjnt_alt_def closed_except_def term_to_nterm_alpha_equiv0)

end

global_interpretation nrelated: term_struct_rel_strong "(λt n. t = nterm_to_term Γ n)" for Γ
proof (standard, goal_cases)
case (5 name t)
then show ?case by (cases t) (auto simp: const_term_def const_nterm_def split: option.splits)
next
case (6 u⇩1 u⇩2 t)
then show ?case by (cases t) (auto simp: app_term_def app_nterm_def split: option.splits)
qed (auto simp: const_term_def const_nterm_def app_term_def app_nterm_def)

lemma env_nrelated_closed:
assumes "nrelated.P_env Γ env nenv" "closed_env nenv"
shows "nrelated.P_env Γ' env nenv"
proof
fix x
from assms have "rel_option (λt n. t = nterm_to_term Γ n) (fmlookup env x) (fmlookup nenv x)"
by auto
thus "rel_option (λt n. t = nterm_to_term Γ' n) (fmlookup env x) (fmlookup nenv x)"
using assms
by (cases rule: option.rel_cases) (auto dest: fmdomI simp: nterm_to_term_eq_closed)
qed

lemma nrelated_subst:
assumes "nrelated.P_env Γ env nenv" "closed_env nenv" "fdisjnt (fset_of_list Γ) (fmdom nenv)"
shows "subst (nterm_to_term Γ t) env = nterm_to_term Γ (subst t nenv)"
using assms
proof (induction t arbitrary: Γ env nenv)
case (Nvar name)
thus ?case
proof (cases rule: fmrel_cases[where x = name])
case (some t⇩1 t⇩2)
with Nvar have "name |∉| fset_of_list Γ"
unfolding fdisjnt_alt_def by (auto dest: fmdomI)
hence "find_first name Γ = None"
including fset.lifting by transfer' (simp add: find_first_none)
with some show ?thesis
by auto
qed (auto split: option.splits)
next
case (Nabs x t)
show ?case
apply simp
apply (subst subst_drop[symmetric, where x = x])
subgoal by simp
apply (rule Nabs)
using Nabs unfolding fdisjnt_alt_def
by (auto intro: env_nrelated_closed)
qed auto

lemma nterm_to_term_insert_dupl:
assumes "y ∈ set (take n Γ)" "n ≤ length Γ"
shows "nterm_to_term Γ t = incr_bounds (- 1) (Suc n) (nterm_to_term (insert_nth n y Γ) t)"
using assms
proof (induction t arbitrary: n Γ)
case (Nvar name)
show ?case
proof (cases "y = name")
case True
with Nvar obtain i where "find_first name Γ = Some i" "i < n"
by (auto elim: find_first_some_strong)

hence "find_first name (take n Γ) = Some i"
by (rule find_first_prefix)

show ?thesis
apply simp
apply (subst ‹find_first name Γ = Some i›)
apply simp
apply (subst find_first_append)
apply (subst ‹find_first name (take n Γ) = Some i›)
apply simp
using ‹i < n› by simp
next
case False
show ?thesis
apply (simp del: insert_nth_take_drop)
apply (subst find_first_insert_nth_neq)
subgoal using False by simp
by (cases "find_first name Γ") auto
qed
next
case (Nabs x t)
show ?case
apply simp
apply (subst Nabs(1)[where n = "Suc n"])
using Nabs by auto
qed auto

lemma nterm_to_term_bounds_dupl:
assumes "i < length Γ" "j < length Γ" "i < j"
assumes "Γ ! i = Γ ! j"
shows "j |∉| bounds (nterm_to_term Γ t)"
using assms
proof (induction t arbitrary: Γ i j)
case (Nvar name)
show ?case
proof (cases "find_first name Γ")
case (Some k)
show ?thesis
proof
assume "j |∈| bounds (nterm_to_term Γ (Nvar name))"
with Some have "find_first name Γ = Some j"
by simp

moreover have "find_first name Γ ≠ Some j"
proof (rule find_first_later)
show "i < length Γ" "j < length Γ" "i < j"
by fact+
next
show "Γ ! j = name"
by (rule find_first_correct) fact
thus "Γ ! i = name"
using Nvar by simp
qed

ultimately show False
by blast
qed
qed simp
next
case (Nabs x t)
show ?case
proof
assume "j |∈| bounds (nterm_to_term Γ (Λ⇩n x. t))"
then obtain j' where "j' |∈| bounds (nterm_to_term (x # Γ) t)" "j' > 0" "j = j' - 1"
by auto
hence "Suc j |∈| bounds (nterm_to_term (x # Γ) t)"
by simp

moreover have "Suc j |∉| bounds (nterm_to_term (x # Γ) t)"
proof (rule Nabs)
show "Suc i < length (x # Γ)" "Suc j < length (x # Γ)" "Suc i < Suc j" "(x # Γ) ! Suc i = (x # Γ) ! Suc j"
using Nabs by simp+
qed

ultimately show False
by blast
qed
qed auto

fun subst_single :: "nterm ⇒ name ⇒ nterm ⇒ nterm" where
"subst_single (Nvar s) s' t' = (if s = s' then t' else Nvar s)" |
"subst_single (t⇩1 $⇩n t⇩2) s' t' = subst_single t⇩1 s' t'$⇩n subst_single t⇩2 s' t'" |
"subst_single (Λ⇩n x. t) s' t' = (Λ⇩n x. (if x = s' then t else subst_single t s' t'))" |
"subst_single t _ _ = t"

lemma subst_single_eq: "subst_single t s t' = subst t (fmap_of_list [(s, t')])"
proof (induction t)
case (Nabs x t)
then show ?case
by (cases "x = s") (simp add: fmfilter_alt_defs)+
qed auto

lemma nterm_to_term_subst_replace_bound:
assumes "closed u'" "n ≤ length Γ" "x ∉ set (take n Γ)"
shows "nterm_to_term Γ (subst_single u x u') = replace_bound n (nterm_to_term (insert_nth n x Γ) u) (nterm_to_term Γ u')"
using assms
proof (induction u arbitrary: n Γ)
case (Nvar name)
note insert_nth_take_drop[simp del]
show ?case
proof (cases "name = x")
case True
thus ?thesis
using Nvar
apply (simp add: find_first_insert_nth_eq)
apply (subst incr_bounds_eq[where k = 0])
subgoal by simp
apply (rule nterm_to_term_closed_wellformed)
by auto
next
case False
thus ?thesis
apply auto
apply (subst find_first_insert_nth_neq)
subgoal by simp
by (cases "find_first name Γ") auto
qed
next
case (Nabs y t)
note insert_nth_take_drop[simp del]
show ?case
proof (cases "x = y")
case True
have "nterm_to_term (y # Γ) t = replace_bound (Suc n) (nterm_to_term (y # insert_nth n y Γ) t) (nterm_to_term Γ u')"
proof (subst replace_bound_eq)
show "Suc n |∉| bounds (nterm_to_term (y # insert_nth n y Γ) t)"
apply (rule nterm_to_term_bounds_dupl[where i = 0])
subgoal by simp
subgoal using Nabs(3) by (simp add: insert_nth_take_drop)
subgoal by simp
apply simp
apply (subst nth_insert_nth_index_eq)
using Nabs by auto
show "nterm_to_term (y # Γ) t = incr_bounds (- 1) (Suc n + 1) (nterm_to_term (y # insert_nth n y Γ) t)"
apply (subst nterm_to_term_insert_dupl[where Γ = "y # Γ" and y = y and n = "Suc n"])
using Nabs by auto
qed
with True show ?thesis
by auto
next
case False
have "nterm_to_term (y # Γ) (subst_single t x u') = replace_bound (Suc n) (nterm_to_term (y # insert_nth n x Γ) t) (nterm_to_term Γ u')"
apply (subst Nabs(1)[of "Suc n"])
subgoal by fact
subgoal using Nabs by simp
subgoal using False Nabs by simp
apply (subst nterm_to_term_eq_closed[where t = u'])
using Nabs by auto
with False show ?thesis
by auto
qed
qed auto

corollary nterm_to_term_subst_β:
assumes "closed u'"
shows "nterm_to_term Γ (subst u (fmap_of_list [(x, u')])) = nterm_to_term (x # Γ) u [nterm_to_term Γ u']⇩β"
using assms
by (rule nterm_to_term_subst_replace_bound[where n = 0, simplified, unfolded subst_single_eq])

end

# Theory Unification_Compat

chapter ‹Instantiation for ‹HOL-ex.Unification› from session ‹HOL-ex››

theory Unification_Compat
imports
"HOL-ex.Unification"
Term_Class
begin

text ‹
The Isabelle library provides a unification algorithm on lambda-free terms. To illustrate
flexibility of the term algebra, I instantiate my class with that term type. The major issue is
that those terms are parameterized over the constant and variable type, which cannot easily be
supported by the classy approach, where those types are fixed to @{typ name}. As a workaround, I
introduce a class that requires the constant and variable type to be isomorphic to @{typ name}.
›

hide_const (open) Unification.subst

class is_name =
fixes of_name :: "name ⇒ 'a"
assumes bij: "bij of_name"
begin

definition to_name :: "'a ⇒ name" where
"to_name = inv of_name"

lemma to_of_name[simp]: "to_name (of_name a) = a"
unfolding to_name_def using bij by (metis bij_inv_eq_iff)

lemma of_to_name[simp]: "of_name (to_name a) = a"
unfolding to_name_def using bij by (meson bij_inv_eq_iff)

lemma of_name_inj: "of_name name⇩1 = of_name name⇩2 ⟹ name⇩1 = name⇩2"
using bij by (metis to_of_name)

end

instantiation name :: is_name begin

definition of_name_name :: "name ⇒ name" where
[code_unfold]: "of_name_name x = x"

instance by standard (auto simp: of_name_name_def bij_betw_def inj_on_def)

end

lemma [simp, code_unfold]: "(to_name :: name ⇒ name) = id"
unfolding to_name_def of_name_name_def by auto

instantiation trm :: (is_name) "pre_term" begin

definition app_trm where
"app_trm = Comb"

definition unapp_trm where
"unapp_trm t = (case t of Comb t u ⇒ Some (t, u) | _ ⇒ None)"

definition const_trm where
"const_trm n = trm.Const (of_name n)"

definition unconst_trm where
"unconst_trm t = (case t of trm.Const a ⇒ Some (to_name a) | _ ⇒ None)"

definition free_trm where
"free_trm n = Var (of_name n)"

definition unfree_trm where
"unfree_trm t = (case t of Var a ⇒ Some (to_name a) | _ ⇒ None)"

primrec consts_trm :: "'a trm ⇒ name fset" where
"consts_trm (Var _) = {||}" |
"consts_trm (trm.Const c) = {| to_name c |}" |
"consts_trm (M ⋅ N) = consts_trm M |∪| consts_trm N"

context
includes fset.lifting
begin

lift_definition frees_trm :: "'a trm ⇒ name fset" is "λt. to_name  vars_of t"
by auto

end

lemma frees_trm[code, simp]:
"frees (Var v) = {| to_name v |}"
"frees (trm.Const c) = {||}"
"frees (M ⋅ N) = frees M |∪| frees N"
including fset.lifting
by (transfer; auto)+

primrec subst_trm :: "'a trm ⇒ (name, 'a trm) fmap ⇒ 'a trm" where
"subst_trm (Var v) env = (case fmlookup env (to_name v) of Some v' ⇒ v' | _ ⇒ Var v)" |
"subst_trm (trm.Const c) _ = trm.Const c" |
"subst_trm (M ⋅ N) env = subst_trm M env ⋅ subst_trm N env"

instance
by standard
(auto
simp: app_trm_def unapp_trm_def const_trm_def unconst_trm_def free_trm_def unfree_trm_def of_name_inj
split: trm.splits option.splits)

end

instantiation trm :: (is_name) "term" begin

definition abs_pred_trm :: "('a trm ⇒ bool) ⇒ 'a trm ⇒ bool" where
"abs_pred_trm P t ⟷ True"

instance proof (standard, goal_cases)
case (1 P t)
then show ?case
proof (induction t)
case Var
then show ?case
unfolding free_trm_def
by (metis of_to_name)
next
case Const
then show ?case
unfolding const_trm_def
by (metis of_to_name)
qed (auto simp: app_trm_def)
qed (auto simp: abs_pred_trm_def)

end

lemma assoc_alt_def[simp]:
"assoc x y t = (case map_of t x of Some y' ⇒ y' | _ ⇒ y)"
by (induction t) auto

lemma subst_eq: "Unification.subst t s = subst t (fmap_of_list s)"
by (induction t) (auto split: option.splits simp: fmlookup_of_list)

end


# Theory Lambda_Free_Compat

chapter ‹Instantiation for ‹λ›-free terms according to Blanchette›

theory Lambda_Free_Compat
imports Unification_Compat "Lambda_Free_RPOs.Lambda_Free_Term"
begin

text ‹
Another instantiation of the algebra for Blanchette et al.'s term type
@{cite blanchette2016lambda}.
›

hide_const (open) Lambda_Free_Term.subst

instantiation tm :: (is_name, is_name) "pre_term" begin

definition app_tm where
"app_tm = tm.App"

definition unapp_tm where
"unapp_tm t = (case t of App t u ⇒ Some (t, u) | _ ⇒ None)"

definition const_tm where
"const_tm n = Hd (Sym (of_name n))"

definition unconst_tm where
"unconst_tm t = (case t of Hd (Sym a) ⇒ Some (to_name a) | _ ⇒ None)"

definition free_tm where
"free_tm n = Hd (Var (of_name n))"

definition unfree_tm where
"unfree_tm t = (case t of Hd (Var a) ⇒ Some (to_name a) | _ ⇒ None)"

context
includes fset.lifting
begin

lift_definition frees_tm :: "('a, 'b) tm ⇒ name fset" is "λt. to_name  vars t"
by auto

lift_definition consts_tm :: "('a, 'b) tm ⇒ name fset" is "λt. to_name  syms t"
by auto

end

lemma frees_tm[code, simp]:
"frees (App f x) = frees f |∪| frees x"
"frees (Hd h) = (case h of Sym _ ⇒ fempty | Var v ⇒ {| to_name v |})"
including fset.lifting
by (transfer; auto split: hd.splits)+

lemma consts_tm[code, simp]:
"consts (App f x) = consts f |∪| consts x"
"consts (Hd h) = (case h of Var _ ⇒ fempty | Sym v ⇒ {| to_name v |})"
including fset.lifting
by (transfer; auto split: hd.splits)+

definition subst_tm :: "('a, 'b) tm ⇒ (name, ('a, 'b) tm) fmap ⇒ ('a, 'b) tm" where
"subst_tm t env =
Lambda_Free_Term.subst (fmlookup_default env (Hd ∘ Var ∘ of_name) ∘ to_name) t"

lemma subst_tm[code, simp]:
"subst (App t u) env = App (subst t env) (subst u env)"
"subst (Hd h) env = (case h of
Sym s ⇒ Hd (Sym s) |
Var x ⇒ (case fmlookup env (to_name x) of
Some t' ⇒ t'
| None ⇒ Hd (Var x)))"
unfolding subst_tm_def
by (auto simp: fmlookup_default_def split: hd.splits option.splits)

instance
by standard
(auto
simp: app_tm_def unapp_tm_def const_tm_def unconst_tm_def free_tm_def unfree_tm_def of_name_inj
split: tm.splits hd.splits option.splits)

end

instantiation tm :: (is_name, is_name) "term" begin

definition abs_pred_tm :: "(('a, 'b) tm ⇒ bool) ⇒ ('a, 'b) tm ⇒ bool" where
"abs_pred_tm P t ⟷ True"

instance proof (standard, goal_cases)
case (1 P t)
then show ?case
proof (induction t)
case (Hd h)
then show ?case
apply (cases h)
apply (auto simp: free_tm_def const_tm_def)
apply (metis of_to_name)+
done
qed (auto simp: app_tm_def)
qed (auto simp: abs_pred_tm_def)

end

lemma apps_list_comb: "apps f xs = list_comb f xs"
by (induction xs arbitrary: f) (auto simp: app_tm_def)

end