Theory Term_Impl
section‹Extensions for Existing AFP Entries›
subsection‹First Order Terms›
theory Term_Impl
imports
First_Order_Terms.Term_More
Certification_Monads.Check_Monad
Deriving.Compare_Order_Instances
Show.Shows_Literal
FOR_Preliminaries
begin
derive compare_order "term"
subsubsection‹Positions›
fun poss_list :: "('f, 'v) term ⇒ pos list"
where
"poss_list (Var x) = [[]]" |
"poss_list (Fun f ss) = ([] # concat (map (λ (i, ps).
map ((#) i) ps) (zip [0 ..< length ss] (map poss_list ss))))"
lemma poss_list_sound [simp]:
"set (poss_list s) = poss s"
proof (induct s)
case (Fun f ss)
let ?z = "zip [0..<length ss] (map poss_list ss)"
have "(⋃a∈set ?z. set (case_prod (λi. map ((#) i)) a)) =
{i # p |i p. i < length ss ∧ p ∈ poss (ss ! i)}" (is "?l = ?r")
proof (rule set_eqI)
fix ip
show "(ip ∈ ?l) = (ip ∈ ?r)"
proof
assume "ip ∈ ?l"
from this obtain ipI where
z: "ipI ∈ set ?z" and
ip: "ip ∈ set (case_prod (λ i. map ((#) i)) ipI)"
by auto
from z obtain i where i: "i < length ?z" and zi: "?z ! i = ipI"
by (force simp: set_conv_nth)
with ip Fun show "ip ∈ ?r" by auto
next
assume "ip ∈ ?r"
from this obtain i p where i: "i < length ss" and "p ∈ poss (ss ! i)"
and ip: "ip = i # p" by auto
with Fun have p: "p ∈ set (poss_list (ss ! i))" and iz: "i < length ?z" by auto
from i have id: "?z ! i = (i, poss_list (ss ! i))" (is "_ = ?ipI") by auto
from iz have "?z ! i ∈ set ?z" by (rule nth_mem)
with id have inZ: "?ipI ∈ set ?z" by auto
from p have "i # p ∈ set (case_prod (λ i. map ((#) i)) ?ipI)" by auto
with inZ ip show "ip ∈ ?l" by force
qed
qed
with Fun show ?case by simp
qed simp
declare poss_list.simps [simp del]
fun var_poss_list :: "('f, 'v) term ⇒ pos list"
where
"var_poss_list (Var x) = [[]]" |
"var_poss_list (Fun f ss) = (concat (map (λ (i, ps).
map ((#) i) ps) (zip [0 ..< length ss] (map var_poss_list ss))))"
lemma var_poss_list_sound [simp]:
"set (var_poss_list s) = var_poss s"
proof (induct s)
case (Fun f ss)
let ?z = "zip [0..<length ss] (map var_poss_list ss)"
have "(⋃a∈set ?z. set (case_prod (λi. map ((#) i)) a)) =
(⋃i<length ss. {i # p |p. p ∈ var_poss (ss ! i)})" (is "?l = ?r")
proof (rule set_eqI)
fix ip
show "(ip ∈ ?l) = (ip ∈ ?r)"
proof
assume "ip ∈ ?l"
from this obtain ipI where
z: "ipI ∈ set ?z" and
ip: "ip ∈ set (case_prod (λ i. map ((#) i)) ipI)"
by auto
from z obtain i where i: "i < length ?z" and zi: "?z ! i = ipI"
by (force simp: set_conv_nth)
with ip Fun show "ip ∈ ?r" by auto
next
assume "ip ∈ ?r"
from this obtain i p where i: "i < length ss" and "p ∈ var_poss (ss ! i)"
and ip: "ip = i # p" by auto
with Fun have p: "p ∈ set (var_poss_list (ss ! i))" and iz: "i < length ?z" by auto
from i have id: "?z ! i = (i, var_poss_list (ss ! i))" (is "_ = ?ipI") by auto
from iz have "?z ! i ∈ set ?z" by (rule nth_mem)
with id have inZ: "?ipI ∈ set ?z" by auto
from p have "i # p ∈ set (case_prod (λ i. map ((#) i)) ?ipI)" by auto
with inZ ip show "ip ∈ ?l" by force
qed
qed
with Fun show ?case unfolding var_poss_list.simps by simp
qed simp
lemma length_var_poss_list: "length (var_poss_list t) = length (vars_term_list t)"
proof(induct t)
case (Var x)
then show ?case unfolding var_poss_list.simps vars_term_list.simps by simp
next
case (Fun f ts)
let ?xs="map2 (λx. map ((#) x)) [0..<length ts] (map var_poss_list ts)"
let ?ys="map vars_term_list ts"
have l1:"length ?xs = length ts"
by simp
have l2:"length ?ys = length ts"
by simp
{fix i assume i:"i < length ts"
then have "(zip [0..<length ts] (map var_poss_list ts)) ! i = (i, var_poss_list (ts!i))" by simp
with i have "?xs!i = (map ((#) i)) (var_poss_list (ts!i))" by simp
then have "length (?xs!i) = length (var_poss_list (ts!i))" by simp
with i have "length (?xs!i) = length (?ys!i)" using Fun.hyps by simp
}
then show ?case
unfolding var_poss_list.simps vars_term_list.simps using eq_length_concat_nth[of ?xs ?ys] l1 l2 by presburger
qed
lemma vars_term_list_var_poss_list:
assumes "i < length (vars_term_list t)"
shows "Var ((vars_term_list t)!i) = t|_((var_poss_list t)!i)"
using assms proof(induct t arbitrary:i)
case (Var x)
then have i:"i = 0"
unfolding vars_term_list.simps by simp
then show ?case unfolding i vars_term_list.simps poss_list.simps var_poss.simps by simp
next
case (Fun f ts)
let ?xs="(map vars_term_list ts)"
let ?ys="(map2 (λi. map ((#) i)) [0..<length ts] (map var_poss_list ts))"
from Fun(2) have 1:"i < length (concat ?xs)" unfolding vars_term_list.simps by simp
have 2:"length ?ys = length ?xs" unfolding length_map by simp
{fix i assume i:"i < length ?xs"
then have *:"(map2 (λx. map ((#) x)) [0..<length ts] (map var_poss_list ts) ! i) = map ((#) i) (var_poss_list (ts!i))"
unfolding length_map by simp
with i have "length (?ys ! i) = length (?xs ! i)"
unfolding * length_map length_var_poss_list by simp
}note l=this
then obtain j k where j:"j < length ?xs" and k:"k < length (?xs ! j)"
and concat:"concat ?xs ! i = ?xs ! j ! k" "concat ?ys ! i = ?ys ! j ! k"
using nth_concat_two_lists[OF 1 2] by blast
from Fun(1) j k have "Var (vars_term_list (ts!j) ! k) = (ts!j) |_ var_poss_list (ts!j) ! k"
unfolding length_map by force
then have "Var (vars_term_list (Fun f ts) ! i) = (Fun f ts)|_(j#(var_poss_list (ts!j) ! k))"
unfolding vars_term_list.simps concat(1) using j by auto
moreover have "j#(var_poss_list (ts!j) ! k) = ((var_poss_list (Fun f ts))!i)" proof-
from k have "k < length (map2 (λi. map ((#) i)) [0..<length ts] (map var_poss_list ts) ! j)"
using l j by presburger
then show ?thesis
unfolding var_poss_list.simps concat(2) using j unfolding length_map by simp
qed
ultimately show ?case
by presburger
qed
lemma var_poss_list_map_vars_term:
shows "var_poss_list (map_vars_term f t) = var_poss_list t"
proof(induct t)
case (Fun g ts)
then have IH:"map var_poss_list ts = map var_poss_list (map (map_vars_term f) ts)"
by fastforce
then show ?case unfolding map_vars_term_eq eval_term.simps IH var_poss_list.simps
by force
qed simp
lemma distinct_var_poss_list:
shows "distinct (var_poss_list t)"
proof(induct t)
case (Fun f ts)
let ?xs="(map2 (λi. map ((#) i)) [0..<length ts] (map var_poss_list ts))"
have l:"length ?xs = length ts"
by force
have d1:"distinct (removeAll [] ?xs)" proof-
have xs':"removeAll [] ?xs = filter (λx. x ≠ []) ?xs"
by (metis (mono_tags, lifting) filter_cong removeAll_filter_not_eq)
{fix i j assume i:"i < length ?xs" "?xs!i ≠ []" and j:"j < length ?xs" "?xs!j ≠ []" and ij:"i ≠ j"
from i l obtain p where p:"i#p ∈ set (?xs!i)" using nth_mem
by (smt (z3) add.left_neutral diff_zero length_greater_0_conv length_map length_upt nth_map nth_upt nth_zip prod.simps(2))
from l j(1) have "?xs ! j = map ((#) j) ((map var_poss_list ts)!j)"
by simp
with p have "?xs!i ≠ ?xs!j" using ij by force
}
then show ?thesis using distinct_filter2 xs' by (smt (verit))
qed
{fix x assume "x ∈ set ?xs"
with l obtain i where i:"i < length ts" and "x = ?xs!i" by (metis in_set_idx)
then have x:"x = map ((#) i) (var_poss_list (ts!i))" by simp
from Fun i have "distinct (var_poss_list (ts!i))" by auto
then have "distinct x"
unfolding x by (simp add: distinct_map)
}note d2=this
{fix x y assume "x ∈ set ?xs" "y ∈ set ?xs" "x ≠ y"
then obtain i j where i:"i < length ?xs" "x = ?xs!i" and j:"j < length ?xs" "y = ?xs!j" and ij:"i ≠ j"
by (metis in_set_idx)
from i have x:"x = map ((#) i) (var_poss_list (ts!i))" by simp
from j have y:"y = map ((#) j) (var_poss_list (ts!j))" by simp
{fix p q assume p:"p ∈ set x" and q:"q ∈ set y"
from x p obtain p' where p':"p = i#p'" and "p' ∈ set (var_poss_list (ts!i))"
by auto
from y q obtain q' where q':"q = j#q'" and "q' ∈ set (var_poss_list (ts!j))"
by auto
from q' p' have "p ≠ q" by (simp add: ij)
}
then have "set x ∩ set y = {}" by auto
}note d3=this
from d1 d2 d3 show ?case unfolding var_poss_list.simps using distinct_concat_iff by blast
qed simp
fun fun_poss_list :: "('f, 'v) term ⇒ pos list"
where
"fun_poss_list (Var x) = []" |
"fun_poss_list (Fun f ss) = ([] # concat (map (λ (i, ps).
map ((#) i) ps) (zip [0 ..< length ss] (map fun_poss_list ss))))"
lemma set_fun_poss_list [simp]:
"set (fun_poss_list t) = fun_poss t"
by (induct t; auto simp: UNION_set_zip)
context
begin
private fun in_poss :: "pos ⇒ ('f, 'v) term ⇒ bool"
where
"in_poss [] _ ⟷ True" |
"in_poss (Cons i p) (Fun f ts) ⟷ i < length ts ∧ in_poss p (ts ! i)" |
"in_poss (Cons i p) (Var _) ⟷ False"
lemma poss_code[code_unfold]:
"p ∈ poss t = in_poss p t" by (induct rule: in_poss.induct) auto
end
subsubsection‹List of Distinct Variables›
text‹We introduce a duplicate free version of @{const vars_term_list} that preserves order of
appearance of variables. This is used for the theory on proof terms.›
abbreviation vars_distinct :: "('f, 'v) term ⇒ 'v list" where "vars_distinct t ≡ (rev ∘ remdups ∘ rev) (vars_term_list t)"
lemma single_var[simp]: "vars_distinct (Var x) = [x]"
by (simp add: vars_term_list.simps(1))
lemma vars_term_list_vars_distinct:
assumes "i < length (vars_term_list t)"
shows "∃j < length (vars_distinct t). (vars_term_list t)!i = (vars_distinct t)!j"
by (metis assms in_set_idx nth_mem o_apply set_remdups set_rev)
subsubsection ‹Useful abstractions›
text ‹Given that we perform the same operations on terms in order to get
a list of the variables and a list of the functions, we define functions
that run through the term and perform these actions.›
context
begin
private fun contains_var_term :: "'v ⇒ ('f, 'v) term ⇒ bool" where
"contains_var_term x (Var y) = (x = y)"
| "contains_var_term x (Fun _ ts) = Bex (set ts) (contains_var_term x)"
lemma contains_var_term_sound[simp]:
"contains_var_term x t ⟷ x ∈ vars_term t"
by (induct t) auto
lemma in_vars_term_code[code_unfold]: "x ∈ vars_term t = contains_var_term x t" by simp
end
subsubsection‹Linear Terms›
lemma distinct_vars_linear_term:
assumes "distinct (vars_term_list t)"
shows "linear_term t"
using assms proof(induct t)
case (Fun f ts)
{fix t' assume t':"t' ∈ set ts"
with Fun(2) have "distinct (vars_term_list t')"
unfolding vars_term_list.simps by (simp add: distinct_concat_iff)
with Fun(1) t' have "linear_term t'" by auto
}note IH=this
have "is_partition (map (set ∘ vars_term_list) ts)"
using distinct_is_partitition_sets vars_term_list.simps(2) Fun(2) by force
then have "is_partition (map vars_term ts)" by (simp add: comp_def)
with IH show ?case by simp
qed simp
fun
linear_term_impl :: "'v set ⇒ ('f, 'v) term ⇒ ('v set) option"
where
"linear_term_impl xs (Var x) = (if x ∈ xs then None else Some (insert x xs))" |
"linear_term_impl xs (Fun _ []) = Some xs" |
"linear_term_impl xs (Fun f (t # ts)) = (case linear_term_impl xs t of
None ⇒ None
| Some ys ⇒ linear_term_impl ys (Fun f ts))"
lemma linear_term_code[code]: "linear_term t = (linear_term_impl {} t ≠ None)"
proof -
{
note [simp] = is_partition_Nil is_partition_Cons
fix xs ys
let ?P = "λ ys xs t. (linear_term_impl xs t = None ⟶ (xs ∩ vars_term t ≠ {} ∨ ¬ linear_term t)) ∧
(linear_term_impl xs t = Some ys ⟶ (ys = (xs ∪ vars_term t)) ∧ xs ∩ vars_term t = {} ∧ linear_term t)"
have "?P ys xs t"
proof (induct rule: linear_term_impl.induct[of "λ xs t. ∀ ys. ?P ys xs t", rule_format])
case (3 xs f t ts zs)
show ?case
proof (cases "linear_term_impl xs t")
case None
with 3 show ?thesis by auto
next
case (Some ys)
note some = this
with 3 have rec1: "ys = xs ∪ vars_term t ∧ xs ∩ vars_term t = {} ∧ linear_term t" by auto
show ?thesis
proof (cases "linear_term_impl ys (Fun f ts)")
case None
with rec1 Some have res: "linear_term_impl xs (Fun f (t # ts)) = None" by simp
from None 3(2) Some have rec2: "ys ∩ vars_term (Fun f ts) ≠ {} ∨ ¬ linear_term (Fun f ts)" by simp
then have "xs ∩ vars_term (Fun f (t # ts)) ≠ {} ∨ ¬ linear_term (Fun f (t # ts))"
proof
assume "ys ∩ vars_term (Fun f ts) ≠ {}"
then obtain x where x1: "x ∈ ys" and x2: "x ∈ vars_term (Fun f ts)" by auto
show ?thesis
proof (cases "x ∈ xs")
case True
with x2 show ?thesis by auto
next
case False
with x1 rec1 have "x ∈ vars_term t" by auto
with x2 have "¬ linear_term (Fun f (t # ts))" by auto
then show ?thesis ..
qed
next
assume "¬ linear_term (Fun f ts)" then have "¬ linear_term (Fun f (t # ts))" by auto
then show ?thesis ..
qed
with res show ?thesis by auto
next
case (Some us)
with some have res: "linear_term_impl xs (Fun f (t # ts)) = Some us" by auto
{
assume us: "us = zs"
from Some[simplified us] 3(2) some
have rec2: "zs = ys ∪ vars_term (Fun f ts) ∧ ys ∩ vars_term (Fun f ts) = {} ∧ linear_term (Fun f ts)" by auto
from rec1 rec2
have part1: "zs = xs ∪ vars_term (Fun f (t # ts)) ∧ xs ∩ vars_term (Fun f (t # ts)) = {}" (is ?part1) by auto
from rec1 rec2 have "vars_term t ∩ vars_term (Fun f ts) = {}" and "linear_term t" and "linear_term (Fun f ts)" by auto
then have "linear_term (Fun f (t # ts))" (is ?part2) by auto
with part1 have "?part1 ∧ ?part2" ..
}
with res show ?thesis by auto
qed
qed
qed auto
} note main = this
from main[of "{}"] show ?thesis by (cases "linear_term_impl {} t", auto)
qed
definition check_linear_term :: "('f :: showl, 'v :: showl) term ⇒ showsl check"
where
"check_linear_term s = check (linear_term s)
(showsl (STR ''the term '') ∘ showsl s ∘ showsl (STR '' is not linear⏎''))"
lemma check_linear_term [simp]:
"isOK (check_linear_term s) = linear_term s"
by (simp add: check_linear_term_def)
subsubsection‹Subterms›
fun supteq_list :: "('f, 'v) term ⇒ ('f, 'v) term list"
where
"supteq_list (Var x) = [Var x]" |
"supteq_list (Fun f ts) = Fun f ts # concat (map supteq_list ts)"
fun supt_list :: "('f, 'v) term ⇒ ('f, 'v) term list"
where
"supt_list (Var x) = []" |
"supt_list (Fun f ts) = concat (map supteq_list ts)"
lemma supteq_list [simp]:
"set (supteq_list t) = {s. t ⊵ s}"
proof (rule set_eqI, unfold mem_Collect_eq)
fix s
show "s ∈ set(supteq_list t) = (t ⊵ s)"
proof (induct t)
case (Fun f ss)
show ?case
proof (cases "Fun f ss = s")
case False
show ?thesis
proof
assume "Fun f ss ⊵ s"
with False have sup: "Fun f ss ⊳ s" using supteq_supt_conv by auto
obtain C where "C ≠ □" and "Fun f ss = C⟨s⟩" using sup by auto
then obtain b D a where "Fun f ss = Fun f (b @ D⟨s⟩ # a)" by (cases C, auto)
then have D: "D⟨s⟩ ∈ set ss" by auto
with Fun[OF D] ctxt_imp_supteq[of D s] obtain t where "t ∈ set ss" and "s ∈ set (supteq_list t)" by auto
then show "s ∈ set (supteq_list (Fun f ss))" by auto
next
assume "s ∈ set (supteq_list (Fun f ss))"
with False obtain t where t: "t ∈ set ss" and "s ∈ set (supteq_list t)" by auto
with Fun[OF t] have "t ⊵ s" by auto
with t show "Fun f ss ⊵ s" by auto
qed
qed auto
qed (simp add: supteq_var_imp_eq)
qed
lemma supt_list_sound [simp]:
"set (supt_list t) = {s. t ⊳ s}"
by (cases t) auto
fun supt_impl :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool"
where
"supt_impl (Var x) t ⟷ False" |
"supt_impl (Fun f ss) t ⟷ t ∈ set ss ∨ Bex (set ss) (λs. supt_impl s t)"
lemma supt_impl [code_unfold]:
"s ⊳ t ⟷ supt_impl s t"
proof
assume "s ⊳ t" then show "supt_impl s t"
proof (induct s)
case (Var x) then show ?case by auto
next
case (Fun f ss) then show ?case
proof (cases "t ∈ set ss")
case True then show ?thesis by (simp)
next
case False
assume "⋀s. ⟦s ∈ set ss; s ⊳ t⟧ ⟹ supt_impl s t"
and "Fun f ss ⊳ t" and "t ∉ set ss"
moreover from ‹Fun f ss ⊳ t› obtain s where "s ∈ set ss" and "s ⊳ t"
by (cases rule: supt.cases) (simp_all add: ‹t ∉ set ss›)
ultimately have "supt_impl s t" by simp
with ‹s ∈ set ss› show ?thesis by auto
qed
qed
next
assume "supt_impl s t"
then show "s ⊳ t"
proof (induct s)
case (Var x) then show ?case by simp
next
case (Fun f ss)
then have "t ∈ set ss ∨ (∃s∈set ss. supt_impl s t)" by simp
then show ?case
proof
assume "t ∈ set ss" then show ?case by auto
next
assume "∃s∈set ss. supt_impl s t"
then obtain s where "s ∈ set ss" and "supt_impl s t" by auto
with Fun have "s ⊳ t" by auto
with ‹s ∈ set ss› show ?thesis by auto
qed
qed
qed
lemma supteq_impl[code_unfold]: "s ⊵ t ⟷ s = t ∨ supt_impl s t"
unfolding supteq_supt_set_conv
by (auto simp: supt_impl)
definition check_no_var :: "('f::showl, 'v::showl) term ⇒ showsl check" where
"check_no_var t ≡ check (is_Fun t) (showsl (STR ''variable found⏎''))"
lemma check_no_var_sound[simp]:
"isOK (check_no_var t) ⟷ is_Fun t"
unfolding check_no_var_def by simp
definition
check_supt :: "('f::showl, 'v::showl) term ⇒ ('f, 'v) term ⇒ showsl check"
where
"check_supt s t ≡ check (s ⊳ t) (showsl t ∘ showsl (STR '' is not a proper subterm of '') ∘ showsl s)"
definition
check_supteq :: "('f::showl, 'v::showl) term ⇒ ('f, 'v) term ⇒ showsl check"
where
"check_supteq s t ≡ check (s ⊵ t) (showsl t ∘ showsl (STR '' is not a subterm of '') ∘ showsl s)"
lemma isOK_check_supt [simp]:
"isOK (check_supt s t) ⟷ s ⊳ t"
by (auto simp: check_supt_def)
lemma isOK_check_supteq [simp]:
"isOK (check_supteq s t) ⟷ s ⊵ t"
by (auto simp: check_supteq_def)
subsubsection ‹Additional Functions on Terms›
fun with_arity :: "('f, 'v) term ⇒ ('f × nat, 'v) term" where
"with_arity (Var x) = Var x"
| "with_arity (Fun f ts) = Fun (f, length ts) (map with_arity ts)"
fun add_vars_term :: "('f, 'v) term ⇒ 'v list ⇒ 'v list"
where
"add_vars_term (Var x) xs = x # xs" |
"add_vars_term (Fun _ ts) xs = foldr add_vars_term ts xs"
fun add_funs_term :: "('f, 'v) term ⇒ 'f list ⇒ 'f list"
where
"add_funs_term (Var _) fs = fs" |
"add_funs_term (Fun f ts) fs = f # foldr add_funs_term ts fs"
fun add_funas_term :: "('f, 'v) term ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
"add_funas_term (Var _) fs = fs" |
"add_funas_term (Fun f ts) fs = (f, length ts) # foldr add_funas_term ts fs"
definition add_funas_args_term :: "('f, 'v) term ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
"add_funas_args_term t fs = foldr add_funas_term (args t) fs"
lemma add_vars_term_vars_term_list_conv [simp]:
"add_vars_term t xs = vars_term_list t @ xs"
proof (induct t arbitrary: xs)
case (Fun f ts)
then show ?case by (induct ts) (simp_all add: vars_term_list.simps)
qed (simp add: vars_term_list.simps)
lemma add_funs_term_funs_term_list_conv [simp]:
"add_funs_term t fs = funs_term_list t @ fs"
proof (induct t arbitrary: fs)
case (Fun f ts)
then show ?case by (induct ts) (simp_all add: funs_term_list.simps)
qed (simp add: funs_term_list.simps)
lemma add_funas_term_funas_term_list_conv [simp]:
"add_funas_term t fs = funas_term_list t @ fs"
proof (induct t arbitrary: fs)
case (Fun f ts)
then show ?case by (induct ts) (simp_all add: funas_term_list.simps)
qed (simp add: funas_term_list.simps)
lemma add_vars_term_vars_term_list_abs_conv [simp]:
"add_vars_term = (@) ∘ vars_term_list"
by (intro ext) simp
lemma add_funs_term_funs_term_list_abs_conv [simp]:
"add_funs_term = (@) ∘ funs_term_list"
by (intro ext) simp
lemma add_funas_term_funas_term_list_abs_conv [simp]:
"add_funas_term = (@) ∘ funas_term_list"
by (intro ext) simp
lemma add_funas_args_term_funas_args_term_list_conv [simp]:
"add_funas_args_term t fs = funas_args_term_list t @ fs"
by (simp add: add_funas_args_term_def funas_args_term_list_def concat_conv_foldr foldr_map)
fun insert_vars_term :: "('f, 'v) term ⇒ 'v list ⇒ 'v list"
where
"insert_vars_term (Var x) xs = List.insert x xs" |
"insert_vars_term (Fun f ts) xs = foldr insert_vars_term ts xs"
fun insert_funs_term :: "('f, 'v) term ⇒ 'f list ⇒ 'f list"
where
"insert_funs_term (Var x) fs = fs" |
"insert_funs_term (Fun f ts) fs = List.insert f (foldr insert_funs_term ts fs)"
fun insert_funas_term :: "('f, 'v) term ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
"insert_funas_term (Var x) fs = fs" |
"insert_funas_term (Fun f ts) fs = List.insert (f, length ts) (foldr insert_funas_term ts fs)"
definition insert_funas_args_term :: "('f, 'v) term ⇒ ('f × nat) list ⇒ ('f × nat) list"
where
"insert_funas_args_term t fs = foldr insert_funas_term (args t) fs"
lemma set_insert_vars_term_vars_term [simp]:
"set (insert_vars_term t xs) = vars_term t ∪ set xs"
proof (induct t arbitrary: xs)
case (Fun f ts)
then show ?case by (induct ts) auto
qed simp
lemma set_insert_funs_term_funs_term [simp]:
"set (insert_funs_term t fs) = funs_term t ∪ set fs"
proof (induct t arbitrary: fs)
case (Fun f ts)
then show ?case by (induct ts) auto
qed simp
lemma set_insert_funas_term_funas_term [simp]:
"set (insert_funas_term t fs) = funas_term t ∪ set fs"
proof (induct t arbitrary: fs)
case (Fun f ts)
then have "set (foldr insert_funas_term ts fs) = ⋃ (funas_term ` set ts) ∪ set fs"
by (induct ts) auto
then show ?case by simp
qed simp
lemma set_insert_funas_args_term [simp]:
"set (insert_funas_args_term t fs) = ⋃ (funas_term ` set (args t)) ∪ set fs"
proof (induct t arbitrary: fs)
case (Fun f ts)
then show ?case by (induct ts) (auto simp: insert_funas_args_term_def)
qed (simp add: insert_funas_args_term_def)
text ‹Implementations of corresponding set-based functions.›
abbreviation "vars_term_impl t ≡ insert_vars_term t []"
abbreviation "funs_term_impl t ≡ insert_funs_term t []"
abbreviation "funas_term_impl t ≡ insert_funas_term t []"
lemma vars_funs_term_list_code[code]:
"vars_term_list t = add_vars_term t []"
"funs_term_list t = add_funs_term t []"
by simp_all
lemma with_arity_term_fold [code]:
"with_arity = Term_More.fold Var (λf ts. Fun (f, length ts) ts)"
proof
fix t :: "('f, 'v) term"
show "with_arity t = Term_More.fold Var (λf ts. Fun (f, length ts) ts) t"
by (induct t) simp_all
qed
fun flatten_term_enum :: "('f list, 'v) term ⇒ ('f, 'v) term list"
where
"flatten_term_enum (Var x) = [Var x]" |
"flatten_term_enum (Fun fs ts) =
(let
lts = map flatten_term_enum ts;
ss = concat_lists lts
in concat (map (λ f. map (Fun f) ss) fs))"
lemma flatten_term_enum:
"set (flatten_term_enum t) = {u. instance_term u (map_funs_term set t)}"
proof (induct t)
case (Var x)
show ?case (is "_ = ?R")
proof -
{
fix t
assume "t ∈ ?R"
then have "t = Var x" by (cases t, auto)
}
then show ?thesis by auto
qed
next
case (Fun fs ts)
show ?case (is "?L = ?R")
proof -
{
fix i
assume "i < length ts"
then have "ts ! i ∈ set ts" by auto
note Fun[OF this]
} note ind = this
have idL: "?L = {Fun g ss | g ss. g ∈ set fs ∧ length ss = length ts ∧ (∀i<length ts. ss ! i ∈ set (flatten_term_enum (ts ! i)))}" (is "_ = ?M1") by auto
let ?R1 = "{Fun f ss | f ss. f ∈ set fs ∧ length ss = length ts ∧ (∀ i<length ss. instance_term (ss ! i) (map_funs_term set (ts ! i)))}"
{
fix u
assume "u ∈ ?R"
then have "u ∈ ?R1" by (cases u, auto)
}
then have idR: "?R = ?R1" by auto
show ?case unfolding idL idR using ind by auto
qed
qed
definition check_ground_term :: "('f :: showl, 'v :: showl) term ⇒ showsl check"
where
"check_ground_term s = check (ground s)
(showsl (STR ''the term '') ∘ showsl s ∘ showsl (STR '' is not a ground term⏎''))"
lemma check_ground_term [simp]:
"isOK (check_ground_term s) ⟷ ground s"
by (simp add: check_ground_term_def)
type_synonym 'f sig_list = "('f × nat)list"
fun check_funas_term :: "'f :: showl sig ⇒ ('f,'v :: showl)term ⇒ showsl check" where
"check_funas_term F (Fun f ts) = do {
check ((f, length ts) ∈ F) (showsl (Fun f ts)
o showsl_lit (STR ''problem: root of subterm '') o showsl f o showsl_lit (STR '' not in signature⏎''));
check_allm (check_funas_term F) ts
}"
| "check_funas_term F (Var _) = return ()"
lemma check_funas_term[simp]: "isOK(check_funas_term F t) = (funas_term t ⊆ F)"
by (induct t, auto)
subsubsection‹Substitutions›
definition mk_subst_domain :: "('f, 'v) substL ⇒ ('v × ('f, 'v) term) list" where
"mk_subst_domain σ ≡
let τ = mk_subst Var σ in
(filter (λ(x, t). Var x ≠ t) (map (λ x. (x, τ x)) (remdups (map fst σ))))"
lemma mk_subst_domain:
"set (mk_subst_domain σ) = (λ x. (x, mk_subst Var σ x)) ` subst_domain (mk_subst Var σ)"
(is "?I = ?R")
proof -
have "?I ⊆ ?R" unfolding mk_subst_domain_def Let_def subst_domain_def by auto
moreover
{
fix xt
assume mem: "xt ∈ ?R"
obtain x t where xt: "xt = (x, t)" by force
from mem [unfolded xt]
have x: "x ∈ subst_domain (mk_subst Var σ)" and t: "t = mk_subst Var σ x" by auto
then have "mk_subst Var σ x ≠ Var x" unfolding subst_domain_def by simp
with t have l: "map_of σ x = Some t" and tx: "t ≠ Var x"
unfolding mk_subst_def by (cases "map_of σ x", auto)
from map_of_SomeD[OF l] l t tx have "(x,t) ∈ ?I" unfolding mk_subst_domain_def Let_def
by force
then have "xt ∈ ?I" unfolding xt .
}
ultimately show ?thesis by blast
qed
lemma finite_mk_subst: "finite (subst_domain (mk_subst Var σ))"
proof -
have "subst_domain (mk_subst Var σ) = fst ` set (mk_subst_domain σ)"
unfolding mk_subst_domain Let_def by force
moreover have "finite ..."
using finite_set by auto
ultimately show ?thesis by simp
qed
definition subst_eq :: "('f, 'v) substL ⇒ ('f, 'v) substL ⇒ bool" where
"subst_eq σ τ = (let σ' = mk_subst_domain σ; τ' = mk_subst_domain τ in set σ' = set τ')"
lemma subst_eq [simp]:
"subst_eq σ τ = (mk_subst Var σ = mk_subst Var τ)"
proof -
let ?σ = "mk_subst Var σ"
let ?τ = "mk_subst Var τ"
{
assume id: "((λ x. (x, ?σ x)) ` subst_domain ?σ) = ((λ x. (x, ?τ x)) ` subst_domain ?τ)" (is "?l = ?r")
from arg_cong[OF id, of "(`) fst"] have idd: "subst_domain ?σ = subst_domain ?τ" by force
have "?σ = ?τ"
proof (rule ext)
fix x
show "?σ x = ?τ x"
proof (cases "x ∈ subst_domain ?σ")
case False
then show ?thesis using idd unfolding subst_domain_def by auto
next
case True
with idd have x: "(x,?σ x) ∈ ?l" "(x,?τ x) ∈ ?r" by auto
with id have x: "(x,?τ x) ∈ ?l" "(x,?σ x) ∈ ?l" by auto
then show ?thesis by auto
qed
qed
}
then show ?thesis
unfolding subst_eq_def Let_def
unfolding mk_subst_domain by auto
qed
definition range_vars_impl :: "('f, 'v) substL ⇒ 'v list"
where
"range_vars_impl σ =
(let σ' = mk_subst_domain σ in
concat (map (vars_term_list o snd) σ'))"
definition vars_subst_impl :: "('f, 'v) substL ⇒ 'v list"
where
"vars_subst_impl σ =
(let σ' = mk_subst_domain σ in
map fst σ' @ concat (map (vars_term_list o snd) σ'))"
lemma vars_subst_impl [simp]:
"set (vars_subst_impl σ) = vars_subst (mk_subst Var σ)"
unfolding vars_subst_def vars_subst_impl_def Let_def
by (auto simp: mk_subst_domain, force)
lemma range_vars_impl [simp]:
"set (range_vars_impl σ) = range_vars (mk_subst Var σ)"
unfolding range_vars_def range_vars_impl_def Let_def
by (auto simp: mk_subst_domain)
lemma mk_subst_one [simp]: "mk_subst Var [(x, t)] = subst x t"
unfolding mk_subst_def subst_def by auto
lemma fst_image [simp]: "fst ` (λ x. (x,g x)) ` a = a" by force
definition
subst_compose_impl :: "('f, 'v) substL ⇒ ('f, 'v) substL ⇒ ('f, 'v) substL"
where
"subst_compose_impl σ τ ≡
let
σ' = mk_subst_domain σ;
τ' = mk_subst_domain τ;
dσ = map fst σ'
in map (λ (x, t). (x, t ⋅ mk_subst Var τ')) σ' @ filter (λ (x, t). x ∉ set dσ) τ'"
lemma mk_subst_mk_subst_domain [simp]:
"mk_subst Var (mk_subst_domain σ) = mk_subst Var σ"
proof (intro ext)
fix x
{
assume x: "x ∉ subst_domain (mk_subst Var σ)"
then have σ: "mk_subst Var σ x = Var x" unfolding subst_domain_def by auto
from x have "x ∉ fst ` set (mk_subst_domain σ)" unfolding mk_subst_domain by auto
then have look: "map_of (mk_subst_domain σ) x = None" by (cases "map_of (mk_subst_domain σ) x", insert map_of_SomeD[of "mk_subst_domain σ" x], force+)
then have "mk_subst Var (mk_subst_domain σ) x = mk_subst Var σ x" unfolding σ
unfolding mk_subst_def by auto
} note ndom = this
{
assume "x ∈ subst_domain (mk_subst Var σ)"
then have "x ∈ fst ` set (mk_subst_domain σ)" unfolding mk_subst_domain by auto
then obtain t where look: "map_of (mk_subst_domain σ) x = Some t" by (cases "map_of (mk_subst_domain σ) x", (force simp: map_of_eq_None_iff)+)
from map_of_SomeD[OF look, unfolded mk_subst_domain] have t: "t = mk_subst Var σ x" by auto
from look t have res: "mk_subst Var (mk_subst_domain σ) x = mk_subst Var σ x" unfolding mk_subst_def by auto
} note dom = this
from ndom dom
show "mk_subst Var (mk_subst_domain σ) x = mk_subst Var σ x" by auto
qed
lemma subst_compose_impl [simp]:
"mk_subst Var (subst_compose_impl σ τ) = mk_subst Var σ ∘⇩s mk_subst Var τ" (is "?l = ?r")
proof (rule ext)
fix x
let ?σ = "mk_subst Var σ"
let ?τ = "mk_subst Var τ"
let ?s = "map (λ (x, t). (x, t ⋅ mk_subst Var (mk_subst_domain τ))) (mk_subst_domain σ)"
let ?t = "[(x,t) ← mk_subst_domain τ. x ∉ set (map fst (mk_subst_domain σ))]"
note d = subst_compose_impl_def[unfolded Let_def]
show "?l x = ?r x"
proof (cases "x ∈ subst_domain (mk_subst Var σ)")
case True
then have "?σ x ≠ Var x" unfolding subst_domain_def by auto
then obtain t where look: "map_of σ x = Some t" and σ: "?σ x = t"
unfolding mk_subst_def by (cases "map_of σ x", auto)
from σ have r: "?r x = t ⋅ ?τ" unfolding subst_compose_def by simp
from True have "x ∈ subst_domain (mk_subst Var (mk_subst_domain σ))"
by simp
from σ True have mem: "(x,t ⋅ ?τ) ∈ set ?s" by (auto simp: mk_subst_domain)
with map_of_eq_None_iff[of "?s" x]
obtain u where look2: "map_of ?s x = Some u"
by (cases "map_of ?s x", force+)
from map_of_SomeD[OF this] σ have u: "u = t ⋅ ?τ"
by (auto simp: mk_subst_domain)
note look2 = map_of_append_Some[OF look2, of ?t]
have l: "?l x = t ⋅ ?τ" unfolding d mk_subst_def[of Var "?s @ ?t"] look2 u
by simp
from l r show ?thesis by simp
next
case False
then have σ: "?σ x = Var x" unfolding subst_domain_def by auto
from σ have r: "?r x = ?τ x" unfolding subst_compose_def by simp
from False have "x ∉ subst_domain (mk_subst Var (mk_subst_domain σ))"
by simp
from False have mem: "⋀ y. (x,y) ∉ set ?s" by (auto simp: mk_subst_domain)
with map_of_SomeD[of ?s x] have look2: "map_of ?s x = None"
by (cases "map_of ?s x", auto)
note look2 = map_of_append_None[OF look2, of ?t]
have l: "?l x = (case map_of ?t x of None ⇒ Var x | Some t ⇒ t)" unfolding d mk_subst_def[of Var "?s @ ?t"] look2 by simp
also have "... = ?τ x"
proof (cases "x ∈ subst_domain ?τ")
case True
then have "?τ x ≠ Var x" unfolding subst_domain_def by auto
then obtain t where look: "map_of τ x = Some t" and τ: "?τ x = t"
unfolding mk_subst_def by (cases "map_of τ x", auto)
from True have "x ∈ subst_domain (mk_subst Var (mk_subst_domain τ))"
by simp
from τ True have mem: "(x,?τ x) ∈ set ?t" using False by (auto simp: mk_subst_domain)
with map_of_eq_None_iff[of ?t x] obtain u where look2: "map_of ?t x = Some u"
by (cases "map_of ?t x", force+)
from map_of_SomeD[OF this] τ have u: "u = ?τ x"
by (auto simp: mk_subst_domain)
show ?thesis using look2 u by simp
next
case False
then have τ: "?τ x = Var x" unfolding subst_domain_def by auto
from False have "x ∉ subst_domain (mk_subst Var (mk_subst_domain τ))"
by simp
from False have mem: "⋀ y. (x,y) ∉ set ?t" by (auto simp: mk_subst_domain)
with map_of_SomeD[of ?t x] have look2: "map_of ?t x = None"
by (cases "map_of ?t x", auto)
show ?thesis unfolding τ look2 by simp
qed
finally show ?thesis unfolding r by simp
qed
qed
fun subst_power_impl :: "('f, 'v) substL ⇒ nat ⇒ ('f, 'v) substL" where
"subst_power_impl σ 0 = []"
| "subst_power_impl σ (Suc n) = subst_compose_impl σ (subst_power_impl σ n)"
lemma subst_power_impl [simp]:
"mk_subst Var (subst_power_impl σ n) = (mk_subst Var σ)^^n"
by (induct n, auto)
definition commutes_impl :: "('f, 'v) substL ⇒ ('f, 'v) substL ⇒ bool" where
"commutes_impl σ μ ≡ subst_eq (subst_compose_impl σ μ) (subst_compose_impl μ σ)"
lemma commutes_impl [simp]:
"commutes_impl σ μ = ((mk_subst Var σ ∘⇩s mk_subst Var μ) = (mk_subst Var μ ∘⇩s mk_subst Var σ))"
unfolding commutes_impl_def by simp
definition
subst_compose'_impl :: "('f, 'v) substL ⇒ ('f, 'v) subst ⇒ ('f, 'v) substL"
where
"subst_compose'_impl σ ρ ≡ map (λ (x, s). (x, s ⋅ ρ)) (mk_subst_domain σ)"
lemma subst_compose'_impl [simp]:
"mk_subst Var (subst_compose'_impl σ ρ) = subst_compose' (mk_subst Var σ) ρ" (is "?l = ?r")
proof (rule ext)
fix x
note d = subst_compose'_def subst_compose'_impl_def
let ?σ = "mk_subst Var σ"
let ?s = "subst_compose'_impl σ ρ"
show "?l x = ?r x"
proof (cases "x ∈ subst_domain (mk_subst Var σ)")
case True
then have r: "?r x = ?σ x ⋅ ρ" unfolding d by simp
from True have "(x, ?σ x) ∈ set (mk_subst_domain σ)" unfolding mk_subst_domain by auto
then have "(x, ?σ x ⋅ ρ) ∈ set ?s" unfolding d by auto
with map_of_eq_None_iff[of ?s x] obtain u where look: "map_of ?s x = Some u"
by (cases "map_of ?s x", force+)
from map_of_SomeD[OF this] have u: "u = ?σ x ⋅ ρ" unfolding d using mk_subst_domain[of σ] by auto
then have l: "?l x = ?σ x ⋅ ρ" using look u unfolding mk_subst_def by auto
from l r show ?thesis by simp
next
case False
then have r: "?r x = Var x" unfolding d by simp
from False have "⋀ y. (x,y) ∉ set ?s" unfolding d
by (auto simp: mk_subst_domain)
with map_of_SomeD[of ?s x] have look: "map_of ?s x = None"
by (cases "map_of ?s x", auto)
then have l: "?l x = Var x" unfolding mk_subst_def by simp
from l r show ?thesis by simp
qed
qed
definition
subst_replace_impl :: "('f, 'v) substL ⇒ 'v ⇒ ('f, 'v) term ⇒ ('f, 'v) substL"
where
"subst_replace_impl σ x t ≡ (x, t) # filter (λ (y, t). y ≠ x) σ"
lemma subst_replace_impl [simp]:
"mk_subst Var (subst_replace_impl σ x t) = (λ y. if x = y then t else mk_subst Var σ y)" (is "?l = ?r")
proof (rule ext)
fix y
note d = subst_replace_impl_def
show "?l y = ?r y"
proof (cases "y = x")
case True
then show ?thesis unfolding d mk_subst_def by auto
next
case False
let ?σ = "mk_subst Var σ"
from False have r: "?r y = ?σ y" by auto
from False have l: "?l y = mk_subst Var ([(y, t)←σ . y ≠ x]) y" unfolding mk_subst_def d
by simp
also have "... = ?σ y" unfolding mk_subst_def
using map_of_filter[of "λ y. y ≠ x" y σ, OF False] by simp
finally show ?thesis using r by simp
qed
qed
lemma mk_subst_domain_distinct: "distinct (map fst (mk_subst_domain σ))"
unfolding mk_subst_domain_def Let_def distinct_map
by (rule conjI[OF distinct_filter], auto simp: distinct_map inj_on_def)
definition is_renaming_impl :: "('f,'v) substL ⇒ bool" where
"is_renaming_impl σ ≡
let σ' = map snd (mk_subst_domain σ) in
(∀ t ∈ set σ'. is_Var t) ∧ distinct σ'"
lemma is_renaming_impl [simp]:
"is_renaming_impl σ = is_renaming (mk_subst Var σ)" (is "?l = ?r")
proof -
let ?σ = "mk_subst Var σ"
let ?d = "mk_subst_domain σ"
let ?m = "map snd ?d"
let ?k = "map fst ?d"
have "?l = ((∀ t ∈ set ?m. is_Var t) ∧ distinct ?m)" unfolding is_renaming_impl_def Let_def by auto
also have "(∀ t ∈ set ?m. is_Var t) = (∀ x. is_Var (?σ x))"
by (force simp: mk_subst_domain subst_domain_def)
also have "distinct ?m = inj_on ?σ (subst_domain ?σ)"
proof
assume inj: "inj_on ?σ (subst_domain ?σ)"
show "distinct ?m" unfolding distinct_conv_nth
proof (intro allI impI)
fix i j
assume i: "i < length ?m" and j: "j < length ?m" and ij: "i ≠ j"
obtain x t where di: "?d ! i = (x,t)" by (cases "?d ! i", auto)
obtain y s where dj: "?d ! j = (y,s)" by (cases "?d ! j", auto)
from di i have mi: "?m ! i = t" and ki: "?k ! i = x" by auto
from dj j have mj: "?m ! j = s" and kj: "?k ! j = y" by auto
from di i have xt: "(x,t) ∈ set ?d" unfolding set_conv_nth by force
from dj j have ys: "(y,s) ∈ set ?d" unfolding set_conv_nth by force
from xt ys have d: "x ∈ subst_domain ?σ" "y ∈ subst_domain ?σ" unfolding mk_subst_domain by auto
have dist: "distinct ?k" by (rule mk_subst_domain_distinct)
from ij i j have xy: "x ≠ y" unfolding ki[symmetric] kj[symmetric]
using dist[unfolded distinct_conv_nth] by auto
from xt ys have m: "?σ x = t" "?σ y = s" unfolding mk_subst_domain by auto
from inj[unfolded inj_on_def, rule_format, OF d]
show "?m ! i ≠ ?m ! j" unfolding m mi mj using xy by auto
qed
next
assume dist: "distinct ?m"
show "inj_on ?σ (subst_domain ?σ)" unfolding inj_on_def
proof (intro ballI impI)
fix x y
assume x: "x ∈ subst_domain ?σ" and y: "y ∈ subst_domain ?σ"
and id: "?σ x = ?σ y"
from x y have x: "(x,?σ x) ∈ set ?d" and y: "(y,?σ y) ∈ set ?d"
unfolding mk_subst_domain by auto
from x obtain i where di: "?d ! i = (x,?σ x)" and i: "i < length ?d" unfolding set_conv_nth by auto
from y obtain j where dj: "?d ! j = (y,?σ y)" and j: "j < length ?d" unfolding set_conv_nth by auto
from di i have mi: "?m ! i = ?σ x" by simp
from dj j have mj: "?m ! j = ?σ x" unfolding id by simp
from mi mj have id: "?m ! i = ?m ! j" by simp
from dist[unfolded distinct_conv_nth] i j id have id: "i = j" by auto
with di dj
show "x = y" by auto
qed
qed
finally
show ?thesis unfolding is_renaming_def by simp
qed
definition is_inverse_renaming_impl :: "('f, 'v) substL ⇒ ('f, 'v) substL" where
"is_inverse_renaming_impl σ ≡
let σ' = mk_subst_domain σ in
map (λ (x, y). (the_Var y, Var x)) σ'"
lemma is_inverse_renaming_impl [simp]:
fixes σ :: "('f, 'v) substL"
assumes var: "is_renaming (mk_subst Var σ)"
shows "mk_subst Var (is_inverse_renaming_impl σ) = is_inverse_renaming (mk_subst Var σ)" (is "?l = ?r")
proof (rule ext)
fix x
let ?σ = "mk_subst Var σ"
let ?σ' = "mk_subst_domain σ"
let ?m = "map (λ (x, y). (the_Var y, Var x :: ('f, 'v) term)) ?σ'"
let ?ran = "subst_range ?σ"
note d = is_inverse_renaming_impl_def is_inverse_renaming_def
{
fix t
assume "(x,t) ∈ set ?m"
then obtain u z where id: "(x,t) = (the_Var u,Var z)" and mem: "(z,u) ∈ set ?σ'" by auto
from var[unfolded is_renaming_def] mem obtain zz where u: "u = Var zz"
unfolding mk_subst_domain by auto
from id[unfolded u] have id: "zz = x" "t = Var z" by auto
with mem u have "(z,Var x) ∈ set ?σ'" by auto
then have "?σ z = Var x" "z ∈ subst_domain ?σ" unfolding mk_subst_domain by auto
with id have "∃ z. t = Var z ∧ ?σ z = Var x ∧ z ∈ subst_domain ?σ" by auto
} note one = this
have "?l x = mk_subst Var ?m x" unfolding d by simp
also have "... = ?r x"
proof (cases "Var x ∈ ?ran")
case False
{
fix t
assume "(x,t) ∈ set ?m"
from one[OF this] obtain z where t: "t = Var z" and z: "?σ z = Var x"
and dom: "z ∈ subst_domain ?σ" by auto
from z dom False have False by force
}
from this[OF map_of_SomeD[of ?m x]] have look: "map_of ?m x = None"
by (cases "map_of ?m x", auto)
then have "mk_subst Var ?m x = Var x" unfolding mk_subst_def by auto
also have "... = ?r x" using False unfolding d by simp
finally show ?thesis .
next
case True
then obtain y where y: "y ∈ subst_domain ?σ" and x: "?σ y = Var x" by auto
then have "(y,Var x) ∈ set ?σ'" unfolding mk_subst_domain by auto
then have "(x,Var y) ∈ set ?m" by force
then obtain u where look: "map_of ?m x = Some u" using map_of_eq_None_iff[of ?m x]
by (cases "map_of ?m x", force+)
from map_of_SomeD[OF this] have xu: "(x,u) ∈ set ?m" by auto
from one[OF this] obtain z where u: "u = Var z" and z: "?σ z = Var x" and dom: "z ∈ subst_domain ?σ" by auto
have "mk_subst Var ?m x = Var z" unfolding mk_subst_def look u by simp
also have "... = ?r x" using is_renaming_inverse_domain[OF var dom] z by auto
finally show ?thesis .
qed
finally show "?l x = ?r x" .
qed
definition
mk_subst_case :: "'v list ⇒ ('f, 'v) subst ⇒ ('f, 'v) substL ⇒ ('f, 'v) substL"
where
"mk_subst_case xs σ τ = subst_compose_impl (map (λ x. (x, σ x)) xs) τ"
lemma mk_subst_case [simp]:
"mk_subst Var (mk_subst_case xs σ τ) =
(λ x. if x ∈ set xs then σ x ⋅ mk_subst Var τ else mk_subst Var τ x)"
proof -
let ?m = "map (λ x. (x, σ x)) xs"
have id: "mk_subst Var ?m = (λ x. if x ∈ set xs then σ x else Var x)" (is "?l = ?r")
proof (rule ext)
fix x
show "?l x = ?r x"
proof (cases "x ∈ set xs")
case True
then have "(x,σ x) ∈ set ?m" by auto
with map_of_eq_None_iff[of ?m x] obtain u where look: "map_of ?m x = Some u" by auto
from map_of_SomeD[OF look] have u: "u = σ x" by auto
show ?thesis unfolding mk_subst_def look u using True by auto
next
case False
with map_of_SomeD[of ?m x]
have look: "map_of ?m x = None" by (cases "map_of ?m x", auto)
show ?thesis unfolding mk_subst_def look using False by auto
qed
qed
show ?thesis unfolding mk_subst_case_def subst_compose_impl id
unfolding subst_compose_def by auto
qed
end