Theory Term_More
section ‹More Results on Terms›
text ‹In this theory we introduce many more concepts of terms,
we provide several results that link various notions, e.g., positions,
subterms, contexts, substitutions, etc.›
theory Term_More
imports
Position
Subterm_and_Context
Polynomial_Factorization.Missing_List
begin
text ‹@{text "showl"}-Instance for Terms›
fun showsl_term' :: "('f ⇒ showsl) ⇒ ('v ⇒ showsl) ⇒ ('f, 'v) term ⇒ showsl"
where
"showsl_term' fun var (Var x) = var x" |
"showsl_term' fun var (Fun f ts) =
fun f ∘ showsl_list_gen id (STR '''') (STR ''('') (STR '', '') (STR '')'') (map (showsl_term' fun var) ts)"
abbreviation showsl_nat_var :: "nat ⇒ showsl"
where
"showsl_nat_var i ≡ showsl_lit (STR ''x'') ∘ showsl i"
abbreviation showsl_nat_term :: "('f::showl, nat) term ⇒ showsl"
where
"showsl_nat_term ≡ showsl_term' showsl showsl_nat_var"
instantiation "term" :: (showl,showl)showl
begin
definition "showsl (t :: ('a,'b)term) = showsl_term' showsl showsl t"
definition "showsl_list (xs :: ('a,'b)term list) = default_showsl_list showsl xs"
instance ..
end
text ‹@{class "showl"}-Instance for Contexts›
fun showsl_ctxt' :: "('f ⇒ showsl) ⇒ ('v ⇒ showsl) ⇒ ('f, 'v) ctxt ⇒ showsl" where
"showsl_ctxt' fun var (Hole) = showsl_lit (STR ''[]'')"
| "showsl_ctxt' fun var (More f ss1 D ss2) = (
fun f ∘ showsl (STR ''('') ∘
showsl_list_gen (showsl_term' fun var) (STR '''') (STR '''') (STR '', '') (STR '', '') ss1 ∘
showsl_ctxt' fun var D ∘
showsl_list_gen (showsl_term' fun var) (STR '')'') (STR '', '') (STR '', '') (STR '')'') ss2
)"
instantiation ctxt :: (showl,showl)showl
begin
definition "showsl (t :: ('a,'b)ctxt) = showsl_ctxt' showsl showsl t"
definition "showsl_list (xs :: ('a,'b)ctxt list) = default_showsl_list showsl xs"
instance ..
end
text ‹General Folds on Terms›
context
begin
qualified fun
fold :: "('v ⇒ 'a) ⇒ ('f ⇒ 'a list ⇒ 'a) ⇒ ('f, 'v) term ⇒ 'a"
where
"fold var fun (Var x) = var x" |
"fold var fun (Fun f ts) = fun f (map (fold var fun) ts)"
end
declare term.disc [intro]
abbreviation "num_args t ≡ length (args t)"
definition funas_args_term :: "('f, 'v) term ⇒ 'f sig"
where
"funas_args_term t = ⋃(set (map funas_term (args t)))"
fun eroot :: "('f, 'v) term ⇒ ('f × nat) + 'v"
where
"eroot (Fun f ts) = Inl (f, length ts)" |
"eroot (Var x) = Inr x"
abbreviation "root_set ≡ set_option ∘ root"
lemma funas_term_conv:
"funas_term t = set_option (root t) ∪ funas_args_term t"
by (cases t) (simp_all add: funas_args_term_def)
text ‹The \emph{depth} of a term is defined as follows:›
fun depth :: "('f, 'v) term ⇒ nat"
where
"depth (Var _) = 0" |
"depth (Fun _ []) = 0" |
"depth (Fun _ ts) = 1 + Max (set (map depth ts))"
declare conj_cong [fundef_cong]
text ‹The positions of a term›
fun poss :: "('f, 'v) term ⇒ pos set" where
"poss (Var x) = {[]}" |
"poss (Fun f ss) = {[]} ∪ {i # p | i p. i < length ss ∧ p ∈ poss (ss ! i)}"
declare conj_cong [fundef_cong del]
lemma Cons_poss_Var [simp]:
"i # p ∈ poss (Var x) ⟷ False"
by simp
lemma elem_size_size_list_size [termination_simp]:
"x ∈ set xs ⟹ size x < size_list size xs"
by (induct xs) auto
text ‹The set of function positions of a term›
fun fun_poss :: "('f, 'v) term ⇒ pos set"
where
"fun_poss (Var x) = {}" |
"fun_poss (Fun f ts) = {[]} ∪ (⋃i<length ts. {i # p | p. p ∈ fun_poss (ts ! i)})"
lemma fun_poss_imp_poss:
assumes "p ∈ fun_poss t"
shows "p ∈ poss t"
using assms by (induct t arbitrary: p) auto
lemma finite_fun_poss:
"finite (fun_poss t)"
by (induct t) auto
text ‹The set of variable positions of a term›
fun var_poss :: "('f, 'v) term ⇒ pos set"
where
"var_poss (Var x) = {[]}" |
"var_poss (Fun f ts) = (⋃i<length ts. {i # p | p. p ∈ var_poss (ts ! i)})"
lemma var_poss_imp_poss:
assumes "p ∈ var_poss t"
shows "p ∈ poss t"
using assms by (induct t arbitrary: p) auto
lemma finite_var_poss:
"finite (var_poss t)"
by (induct t) auto
lemma poss_simps [symmetric, simp]:
"poss t = fun_poss t ∪ var_poss t"
"poss t = var_poss t ∪ fun_poss t"
"fun_poss t = poss t - var_poss t"
"var_poss t = poss t - fun_poss t"
by (induct_tac [!] t) auto
lemma finite_poss [simp]:
"finite (poss t)"
by (subst poss_simps [symmetric]) (metis finite_Un finite_fun_poss finite_var_poss)
text ‹The subterm of a term~@{text s} at position~@{text p} is defined as follows:›
fun subt_at :: "('f, 'v) term ⇒ pos ⇒ ('f, 'v) term" (infixl "|'_" 67)
where
"s |_ [] = s" |
"Fun f ss |_ (i # p) = (ss ! i) |_ p"
lemma var_poss_iff:
"p ∈ var_poss t ⟷ (∃x. p ∈ poss t ∧ t |_ p = Var x)"
by (induct t arbitrary: p) auto
lemma fun_poss_fun_conv:
assumes "p ∈ fun_poss t"
shows "∃ f ts. t |_ p = Fun f ts"
proof (cases "t |_ p")
case (Var x)
have p_in_t: "p ∈ poss t" using fun_poss_imp_poss[OF assms].
then have "p ∈ poss t - fun_poss t" using Var(1) var_poss_iff by auto
then show ?thesis using assms by blast
next
case (Fun f ts) then show ?thesis by auto
qed
lemma pos_append_poss:
"p ∈ poss t ⟹ q ∈ poss (t |_ p) ⟹ p @ q ∈ poss t"
proof (induct t arbitrary: p q)
case (Fun f ts p q)
show ?case
proof (cases p)
case Nil then show ?thesis using Fun by auto
next
case (Cons i p')
with Fun have i: "i < length ts" and p': "p' ∈ poss (ts ! i)" by auto
then have mem: "ts ! i ∈ set ts" by auto
from Fun(3) have "q ∈ poss (ts ! i |_ p')" by (auto simp: Cons)
from Fun(1) [OF mem p' this]
show ?thesis by (auto simp: Cons i)
qed
qed simp
text ‹Creating a context from a term by adding a hole at a specific position.›
fun
ctxt_of_pos_term :: "pos ⇒ ('f, 'v) term ⇒ ('f, 'v) ctxt"
where
"ctxt_of_pos_term [] t = □" |
"ctxt_of_pos_term (i # ps) (Fun f ts) =
More f (take i ts) (ctxt_of_pos_term ps (ts!i)) (drop (Suc i) ts)"
lemma ctxt_supt_id:
assumes "p ∈ poss t"
shows "(ctxt_of_pos_term p t)⟨t |_ p⟩ = t"
using assms by (induct t arbitrary: p) (auto simp: id_take_nth_drop [symmetric])
text ‹
Let @{text s} and @{text t} be terms. The following three statements are equivalent:
\begin{enumerate}
\item \label{A}@{text "s ⊵ t"}
\item \label{B}@{text "∃p∈poss s. s|_p = t"}
\item \label{C}@{text "∃C. s = C⟨t⟩"}
\end{enumerate}
›
text ‹The position of the hole in a context is uniquely determined.›
fun
hole_pos :: "('f, 'v) ctxt ⇒ pos"
where
"hole_pos □ = []" |
"hole_pos (More f ss D ts) = length ss # hole_pos D"
lemma hole_pos_ctxt_of_pos_term [simp]:
assumes "p ∈ poss t"
shows "hole_pos (ctxt_of_pos_term p t) = p"
using assms
proof (induct t arbitrary: p)
case (Fun f ts)
show ?case
proof (cases p)
case Nil
then show ?thesis using Fun by auto
next
case (Cons i q)
with Fun(2) have i: "i < length ts" and q: "q ∈ poss (ts ! i)" by auto
then have "ts ! i ∈ set ts" by auto
from Fun(1)[OF this q] Cons i show ?thesis by simp
qed
qed simp
lemma hole_pos_id_ctxt:
assumes "C⟨s⟩ = t"
shows "ctxt_of_pos_term (hole_pos C) t = C"
using assms
proof (induct C arbitrary: t)
case (More f bef C aft)
then show ?case
proof (cases t)
case (Fun g ts)
with More have [simp]: "g = f" by simp
from Fun More have bef: "take (length bef) ts = bef" by auto
from Fun More have aft: "drop (Suc (length bef)) ts = aft" by auto
from Fun More have Cs: "C⟨s⟩ = ts ! length bef" by auto
from Fun More show ?thesis by (simp add: bef aft More(1)[OF Cs])
qed simp
qed simp
lemma supteq_imp_subt_at:
assumes "s ⊵ t"
shows "∃p∈poss s. s|_p = t"
using assms proof (induct s t rule: supteq.induct)
case (refl s)
have "[] ∈ poss s" by (induct s rule: term.induct) auto
have "s|_[] = s" by simp
from ‹[] ∈ poss s› and ‹s|_[] = s› show ?case by best
next
case (subt u ss t f)
then obtain p where "p ∈ poss u" and "u|_p = t" by best
from ‹u ∈ set ss› obtain i
where "i < length ss" and "u = ss!i" by (auto simp: in_set_conv_nth)
from ‹i < length ss› and ‹p ∈ poss u›
have "i#p ∈ poss (Fun f ss)" unfolding ‹u = ss!i› by simp
have "Fun f ss|_ (i#p) = t"
unfolding subt_at.simps unfolding ‹u = ss!i›[symmetric] by (rule ‹u|_p = t›)
with ‹i#p ∈ poss (Fun f ss)› show ?case by best
qed
lemma subt_at_imp_ctxt:
assumes "p ∈ poss s"
shows "∃C. C⟨s|_p⟩ = s"
using assms proof (induct p arbitrary: s)
case (Nil s)
have "□⟨s|_[]⟩ = s" by simp
then show ?case by best
next
case (Cons i p s)
then obtain f ss where "s = Fun f ss" by (cases s) auto
with ‹i#p ∈ poss s› obtain u :: "('a,'b) term"
where "u = ss!i" and "p ∈ poss u" and "i < length ss" by auto
from Cons and ‹p∈poss u› obtain D where "D⟨u|_p⟩ = u" by auto
let ?ss1 = "take i ss" and ?ss2 = "drop (Suc i) ss"
let ?E = "More f ?ss1 D ?ss2"
have "?ss1@D⟨u|_p⟩#?ss2 = ss" (is "?ss = ss") unfolding ‹D⟨u|_p⟩ = u› unfolding ‹u = ss!i›
unfolding id_take_nth_drop[OF ‹i < length ss›, symmetric] ..
have "s|_ (i#p) = u|_p" unfolding ‹s = Fun f ss› using ‹u = ss!i› by simp
have "?E⟨s|_(i#p)⟩ = s"
unfolding ctxt_apply_term.simps ‹s|_(i#p) = u|_p› ‹?ss = ss› unfolding ‹s = Fun f ss› ..
then show ?case by best
qed
lemma subt_at_imp_supteq':
assumes "p ∈ poss s" and "s|_p = t"
shows "s ⊵ t"
proof -
from ‹p ∈ poss s› obtain C where "C⟨s|_p⟩ = s" using subt_at_imp_ctxt by best
then show ?thesis unfolding ‹s|_p = t› using ctxt_imp_supteq by auto
qed
lemma subt_at_imp_supteq: "p ∈ poss s ⟹ s ⊵ s|_p"
by (simp add: subt_at_imp_supteq')
lemma fun_poss_ctxt_apply_term:
assumes "p ∈ fun_poss C⟨s⟩"
shows "(∀t. p ∈ fun_poss C⟨t⟩) ∨ (∃q. p = (hole_pos C) @ q ∧ q ∈ fun_poss s)"
using assms
proof (induct p arbitrary: C)
case Nil then show ?case by (cases C) auto
next
case (Cons i p)
then show ?case
proof (cases C)
case (More f bef C' aft)
with Cons(2) have "i < length (bef @ C'⟨s⟩ # aft)" by auto
consider "i < length bef" | (C') "i = length bef" | "i > length bef"
by (cases "i < length bef", auto, cases "i = length bef", auto)
then show ?thesis
proof (cases)
case C'
then have "p ∈ fun_poss C'⟨s⟩" using More Cons by auto
from Cons(1)[OF this] More C' show ?thesis by auto
qed (insert More Cons, auto simp: nth_append)
qed auto
qed
text ‹Conversions between contexts and proper subterms.›
text ‹
By adding \emph{non-empty} to statements \ref{B} and \ref{C} a similar characterisation for
proper subterms is obtained:
\begin{enumerate}
\item @{text "s ⊳ t"}
\item @{text "∃i p. i#p∈poss s ∧ s|_(i#p) = t"}
\item @{text "∃C. C ≠ □ ∧ s = C⟨t⟩"}
\end{enumerate}
›
lemma supt_imp_subt_at_nepos:
assumes "s ⊳ t" shows "∃i p. i#p ∈ poss s ∧ s|_ (i#p) = t"
proof -
from assms have "s ⊵ t" and "s ≠ t" unfolding supt_supteq_conv by auto
then obtain p where supteq: "p ∈ poss s" "s|_p = t" using supteq_imp_subt_at by best
have "p ≠ []"
proof
assume "p = []" then have "s = t" using ‹s|_p = t› by simp
then show False using ‹s ≠ t› by simp
qed
then obtain i q where "p = i#q" by (cases p) simp
with supteq show ?thesis by auto
qed
lemma arg_neq:
assumes "i < length ss" and "ss!i = Fun f ss" shows "False"
proof -
from ‹i < length ss› have "(ss!i) ∈ set ss" by auto
with assms show False by simp
qed
lemma subt_at_nepos_neq:
assumes "i#p ∈ poss s" shows "s|_(i#p) ≠ s"
proof (cases s)
fix x assume "s = Var x"
then have "i#p ∉ poss s" by simp
with assms show ?thesis by simp
next
fix f ss assume "s = Fun f ss" show ?thesis
proof
assume "s|_ (i#p) = s"
from assms have "i < length ss" unfolding ‹s = Fun f ss› by auto
then have "ss!i ∈ set ss" by simp
then have "Fun f ss ⊳ ss!i" by (rule supt.arg)
then have "Fun f ss ≠ ss!i" unfolding supt_supteq_conv by simp
from ‹s|_(i#p) = s› and assms
have "ss!i ⊵ Fun f ss" using subt_at_imp_supteq' unfolding ‹s = Fun f ss› by auto
with supt_not_sym[OF ‹Fun f ss ⊳ ss!i›] have "ss!i = Fun f ss" by auto
with ‹i < length ss› show False by (rule arg_neq)
qed
qed
lemma subt_at_nepos_imp_supt:
assumes "i#p ∈ poss s" shows "s ⊳ s |_ (i#p)"
proof -
from assms have "s ⊵ s|_(i#p)" by (rule subt_at_imp_supteq)
from assms have "s|_(i#p) ≠ s" by (rule subt_at_nepos_neq)
from ‹s ⊵ s|_(i#p)› and ‹s|_(i#p) ≠ s› show ?thesis by (auto simp: supt_supteq_conv)
qed
lemma subt_at_nepos_imp_nectxt:
assumes "i#p ∈ poss s" and "s|_(i#p) = t" shows "∃C. C ≠ □ ∧ C⟨t⟩ = s"
proof -
from assms obtain C where "C⟨s|_(i#p)⟩ = s" using subt_at_imp_ctxt by best
from ‹i#p ∈ poss s›
have "t ≠ s" unfolding ‹s|_(i#p) = t›[symmetric] using subt_at_nepos_neq by best
from assms and ‹C⟨s|_(i#p)⟩ = s› have "C⟨t⟩ = s" by simp
have "C ≠ □"
proof
assume "C = □"
with ‹C⟨t⟩ = s› have "t = s" by simp
with ‹t ≠ s› show False by simp
qed
with ‹C⟨t⟩ = s› show ?thesis by auto
qed
lemma supteq_subst_cases':
"s ⋅ σ ⊵ t ⟹ (∃ u. s ⊵ u ∧ is_Fun u ∧ t = u ⋅ σ) ∨ (∃ x. x ∈ vars_term s ∧ σ x ⊵ t)"
proof (induct s)
case (Fun f ss)
from Fun(2)
show ?case
proof (cases rule: supteq.cases)
case refl
show ?thesis
by (intro disjI1 exI[of _ "Fun f ss"], auto simp: refl)
next
case (subt v ts g)
then obtain si where si: "si ∈ set ss" "si ⋅ σ ⊵ t" by auto
from Fun(1)[OF this] si(1) show ?thesis by auto
qed
qed simp
lemma size_const_subst[simp]: "size (t ⋅ (λ _ . Fun f [])) = size t"
proof (induct t)
case (Fun f ts)
then show ?case by (induct ts, auto)
qed simp
type_synonym ('f, 'v) terms = "('f, 'v) term set"
lemma supteq_subst_cases [consumes 1, case_names in_term in_subst]:
"s ⋅ σ ⊵ t ⟹
(⋀ u. s ⊵ u ⟹ is_Fun u ⟹ t = u ⋅ σ ⟹ P) ⟹
(⋀ x. x ∈ vars_term s ⟹ σ x ⊵ t ⟹ P) ⟹
P"
using supteq_subst_cases' by blast
lemma poss_subst_apply_term:
assumes "p ∈ poss (t ⋅ σ)" and "p ∉ fun_poss t"
obtains q r x where "p = q @ r" and "q ∈ poss t" and "t |_ q = Var x" and "r ∈ poss (σ x)"
using assms
proof (induct t arbitrary: p)
case (Fun f ts)
then show ?case by (auto) (metis append_Cons nth_mem subt_at.simps(2))
qed simp
lemma subt_at_subst [simp]:
assumes "p ∈ poss t" shows "(t ⋅ σ) |_ p = (t |_ p) ⋅ σ"
using assms by (induct t arbitrary: p) auto
lemma vars_term_size:
assumes "x ∈ vars_term t"
shows "size (σ x) ≤ size (t ⋅ σ)"
using assms
by (induct t)
(auto, metis (no_types) comp_apply le_SucI size_list_estimation')
text ‹Restrict a substitution to a set of variables.›
definition
subst_restrict :: "('f, 'v) subst ⇒ 'v set ⇒ ('f, 'v) subst"
(infix "|s" 67)
where
"σ |s V = (λx. if x ∈ V then σ(x) else Var x)"
lemma subst_restrict_Int [simp]:
"(σ |s V ) |s W = σ |s (V ∩ W)"
by (rule ext) (simp add: subst_restrict_def)
lemma subst_domain_Var_conv [iff]:
"subst_domain σ = {} ⟷ σ = Var"
proof
assume "subst_domain σ = {}"
show "σ = Var"
proof (rule ext)
fix x show "σ(x) = Var x"
proof (rule ccontr)
assume "σ(x) ≠ Var x"
then have "x ∈ subst_domain σ" by (simp add: subst_domain_def)
with ‹subst_domain σ = {}› show False by simp
qed
qed
next
assume "σ = Var" then show "subst_domain σ = {}" by simp
qed
lemma subst_compose_Var[simp]: "σ ∘⇩s Var = σ" by (simp add: subst_compose_def)
lemma Var_subst_compose[simp]: "Var ∘⇩s σ = σ" by (simp add: subst_compose_def)
text ‹We use the same logical constant as for the power operations on
functions and relations, in order to share their syntax.›
overloading
substpow ≡ "compow :: nat ⇒ ('f, 'v) subst ⇒ ('f, 'v) subst"
begin
primrec substpow :: "nat ⇒ ('f, 'v) subst ⇒ ('f, 'v) subst" where
"substpow 0 σ = Var"
| "substpow (Suc n) σ = σ ∘⇩s substpow n σ"
end
lemma subst_power_compose_distrib:
"μ ^^ (m + n) = (μ ^^ m ∘⇩s μ ^^ n)" by (induct m) (simp_all add: ac_simps)
lemma subst_power_Suc: "μ ^^ (Suc i) = μ ^^ i ∘⇩s μ"
proof -
have "μ ^^ (Suc i) = μ ^^ (i + Suc 0)" by simp
then show ?thesis unfolding subst_power_compose_distrib by simp
qed
lemma subst_pow_mult: "((σ :: ('f,'v)subst)^^ n) ^^ m = σ ^^ (n * m)"
by (induct m arbitrary: n, auto simp: subst_power_compose_distrib)
lemma subst_domain_pow: "subst_domain (σ ^^ n) ⊆ subst_domain σ"
unfolding subst_domain_def
by (induct n, auto simp: subst_compose_def)
lemma subt_at_Cons_distr [simp]:
assumes "i # p ∈ poss t" and "p ≠ []"
shows "t |_ (i # p) = (t |_ [i]) |_ p"
using assms by (induct t) auto
lemma subt_at_append [simp]:
"p ∈ poss t ⟹ t |_ (p @ q) = (t |_ p) |_ q"
proof (induct t arbitrary: p)
case (Fun f ts)
show ?case
proof (cases p)
case (Cons i p')
with Fun(2) have i: "i < length ts" and p': "p' ∈ poss (ts ! i)" by auto
from i have ti: "ts ! i ∈ set ts" by auto
show ?thesis using Fun(1)[OF ti p'] unfolding Cons by auto
qed auto
qed auto
lemma subt_at_pos_diff:
assumes "p <⇩p q" and p: "p ∈ poss s"
shows "s |_ p |_ pos_diff q p = s |_ q"
using assms unfolding subt_at_append [OF p, symmetric] by simp
lemma empty_pos_in_poss[simp]: "[] ∈ poss t" by (induct t) auto
lemma poss_append_poss[simp]: "(p @ q ∈ poss t) = (p ∈ poss t ∧ q ∈ poss (t |_ p))" (is "?l = ?r")
proof
assume ?r
with pos_append_poss[of p t q] show ?l by auto
next
assume ?l
then show ?r
proof (induct p arbitrary: t)
case (Cons i p t)
then obtain f ts where t: "t = Fun f ts" by (cases t, auto)
note IH = Cons[unfolded t]
from IH(2) have i: "i < length ts" and rec: "p @ q ∈ poss (ts ! i)" by auto
from IH(1)[OF rec] i show ?case unfolding t by auto
qed auto
qed
lemma subterm_poss_conv:
assumes "p ∈ poss t" and [simp]: "p = q @ r" and "t |_ q = s"
shows "t |_ p = s |_ r ∧ r ∈ poss s" (is "?A ∧ ?B")
proof -
have qr: "q @ r ∈ poss t" using assms(1) by simp
then have q_in_t: "q ∈ poss t" using poss_append_poss by auto
show ?thesis
proof
have "t |_ p = t |_ (q @ r)" by simp
also have "... = s |_ r" using subt_at_append[OF q_in_t] assms(3) by simp
finally show "?A" .
next
show "?B" using poss_append_poss qr assms(3) by auto
qed
qed
lemma poss_imp_subst_poss [simp]:
assumes "p ∈ poss t"
shows "p ∈ poss (t ⋅ σ)"
using assms by (induct t arbitrary: p) auto
lemma iterate_term:
assumes id: "t ⋅ σ |_ p = t" and pos: "p ∈ poss (t ⋅ σ)"
shows "t ⋅ σ ^^ n |_ (p^n) = t ∧ p ^ n ∈ poss (t ⋅ σ ^^ n)"
proof (induct n)
case (Suc n)
then have p: "p ^ n ∈ poss (t ⋅ σ ^^ n)" by simp
note p' = poss_imp_subst_poss[OF p]
note p'' = subt_at_append[OF p']
have idt: "t ⋅ σ ^^ (Suc n) = t ⋅ σ^^ n ⋅ σ" unfolding subst_power_Suc by simp
have "t ⋅ σ ^^ (Suc n) |_ (p ^ Suc n)
= t ⋅ σ ^^ n ⋅ σ |_ (p ^ n @ p)" unfolding idt power_pos_Suc ..
also have "... = ((t ⋅ σ ^^ n |_ p ^ n) ⋅ σ) |_ p" unfolding p'' subt_at_subst[OF p] ..
also have "... = t ⋅ σ |_ p" unfolding Suc[THEN conjunct1] ..
also have "... = t" unfolding id ..
finally have one: "t ⋅ σ ^^ Suc n |_ (p ^ Suc n) = t" .
show ?case
proof (rule conjI[OF one])
show "p ^ Suc n ∈ poss (t ⋅ σ ^^ Suc n)"
unfolding power_pos_Suc poss_append_poss idt
proof (rule conjI[OF poss_imp_subst_poss[OF p]])
have "t ⋅ σ ^^ n ⋅ σ |_ (p ^ n) = t ⋅ σ ^^ n |_ (p ^ n) ⋅ σ"
by (rule subt_at_subst[OF p])
also have "... = t ⋅ σ" using Suc by simp
finally show "p ∈ poss (t ⋅ σ ^^ n ⋅ σ |_ p ^ n)" using pos by auto
qed
qed
qed simp
lemma hole_pos_poss [simp]: "hole_pos C ∈ poss (C⟨t⟩)"
by (induct C) auto
lemma hole_pos_poss_conv: "(hole_pos C @ q) ∈ poss (C⟨t⟩) ⟷ q ∈ poss t"
by (induct C) auto
lemma subt_at_hole_pos [simp]: "C⟨t⟩ |_ hole_pos C = t"
by (induct C) auto
lemma hole_pos_power_poss [simp]: "(hole_pos C) ^ (n::nat) ∈ poss ((C ^ n)⟨t⟩)"
by (induct n) (auto simp: hole_pos_poss_conv)
lemma poss_imp_ctxt_subst_poss [simp]:
assumes "p ∈ poss (C⟨t⟩)"
shows "p ∈ poss ((C ⋅⇩c σ)⟨t ⋅ σ⟩)"
proof -
have "p ∈ poss (C⟨t⟩ ⋅ σ)" by (rule poss_imp_subst_poss [OF assms])
then show ?thesis by simp
qed
lemma poss_Cons_poss[simp]: "(i # p ∈ poss t) = (i < length (args t) ∧ p ∈ poss (args t ! i))"
by (cases t, auto)
lemma less_pos_imp_supt:
assumes less: "p' <⇩p p" and p: "p ∈ poss t"
shows "t |_ p ⊲ t |_ p'"
proof -
from less obtain p'' where p'': "p = p' @ p''" unfolding less_pos_def less_eq_pos_def by auto
with less have ne: "p'' ≠ []" by auto
then obtain i q where ne: "p'' = i # q" by (cases p'', auto)
from p have p': "p' ∈ poss t" unfolding p'' by simp
from p have "p'' ∈ poss (t |_ p')" unfolding p'' by simp
from subt_at_nepos_imp_supt[OF this[unfolded ne]] have "t |_ p' ⊳ t |_ p' |_ p''" unfolding ne by simp
then show "t |_ p' ⊳ t |_ p" unfolding p'' subt_at_append[OF p'] .
qed
lemma less_eq_pos_imp_supt_eq:
assumes less_eq: "p' ≤⇩p p" and p: "p ∈ poss t"
shows "t |_ p ⊴ t |_ p'"
proof -
from less_eq obtain p'' where p'': "p = p' @ p''" unfolding less_eq_pos_def by auto
from p have p': "p' ∈ poss t" unfolding p'' by simp
from p have "p'' ∈ poss (t |_ p')" unfolding p'' by simp
from subt_at_imp_supteq[OF this] have "t |_ p' ⊵ t |_ p' |_ p''" by simp
then show "t |_ p' ⊵ t |_ p" unfolding p'' subt_at_append[OF p'] .
qed
lemma funas_term_poss_conv:
"funas_term t = {(f, length ts) | p f ts. p ∈ poss t ∧ t|_p = Fun f ts}"
proof (induct t)
case (Fun f ts)
let ?f = "λ f ts. (f,length ts)"
let ?fs = "λ t. {?f f ts | p f ts. p ∈ poss t ∧ t|_p = Fun f ts}"
let ?l = "funas_term (Fun f ts)"
let ?r = "?fs (Fun f ts)"
{
fix gn
have "(gn ∈ ?l) = (gn ∈ ?r)"
proof (cases "gn = (f,length ts)")
case False
obtain g n where gn: "gn = (g,n)" by force
have "(gn ∈ ?l) = (∃ t ∈ set ts. gn ∈ funas_term t)" using False by auto
also have "... = (∃ i < length ts. gn ∈ funas_term (ts ! i))" unfolding set_conv_nth by auto
also have "... = (∃ i < length ts. (g,n) ∈ ?fs (ts ! i))" using Fun[unfolded set_conv_nth] gn by blast
also have "... = ((g,n) ∈ ?fs (Fun f ts))" (is "?l' = ?r'")
proof
assume ?l'
then obtain i p ss where p: "p ∈ poss (ts ! i)" "ts ! i |_ p = Fun g ss" "n = length ss" "i < length ts" by auto
show ?r'
by (rule, rule exI[of _ "i # p"], intro exI conjI, unfold p(3), rule refl, insert p(1) p(2) p(4), auto)
next
assume ?r'
then obtain p ss where p: "p ∈ poss (Fun f ts)" "Fun f ts |_ p = Fun g ss" "n = length ss" by auto
from p False gn obtain i p' where pp: "p = i # p'" by (cases p, auto)
show ?l'
by (rule exI[of _ i], insert p pp, auto)
qed
finally show ?thesis unfolding gn .
qed force
}
then show ?case by blast
qed simp
inductive
subst_instance :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool" ("(_/ ≼ _)" [56, 56] 55)
where
subst_instanceI [intro]:
"s ⋅ σ = t ⟹ s ≼ t"
lemma subst_instance_trans[trans]:
assumes "s ≼ t" and "t ≼ u" shows "s ≼ u"
proof -
from ‹s ≼ t› obtain σ where "s⋅σ = t" by (cases rule: subst_instance.cases) best
from ‹t ≼ u› obtain τ where "t⋅τ = u" by (cases rule: subst_instance.cases) best
then have "(s⋅σ)⋅τ = u" unfolding ‹s⋅σ = t› .
then have "s⋅(σ ∘⇩s τ) = u" by simp
then show ?thesis by (rule subst_instanceI)
qed
lemma subst_instance_refl: "s ≼ s"
using subst_instanceI[where σ = "Var" and s = s and t = s] by simp
lemma subst_neutral: "subst_domain σ ⊆ V ⟹ (Var x)⋅(σ |s (V - {x})) = (Var x)"
by (auto simp: subst_domain_def subst_restrict_def)
lemma subst_restrict_domain[simp]: "σ |s subst_domain σ = σ"
proof -
have "σ |s subst_domain σ = (λx. if x ∈ subst_domain σ then σ(x) else Var x)"
by (simp add: subst_restrict_def)
also have "… = σ" by (rule ext) (simp add: subst_domain_def)
finally show ?thesis .
qed
lemma notin_subst_domain_imp_Var:
assumes "x ∉ subst_domain σ"
shows "σ x = Var x"
using assms by (auto simp: subst_domain_def)
lemma subst_domain_neutral[simp]:
assumes "subst_domain σ ⊆ V"
shows "(σ |s V) = σ"
proof -
{
fix x
have "(if x ∈ V then σ(x) else Var x) = (if x ∈ subst_domain σ then σ(x) else Var x)"
proof (cases "x ∈ subst_domain σ")
case True
then have x: "x ∈ V = True" using assms by auto
show ?thesis unfolding x using True by simp
next
case False
then have x: "x ∉ subst_domain (σ)" .
show ?thesis unfolding notin_subst_domain_imp_Var[OF x] if_cancel ..
qed
}
then have "⋀x.(if x ∈ V then σ x else Var x) = (if x ∈ subst_domain σ then σ x else Var x)" .
then have "⋀x.(λx. if x ∈ V then σ x else Var x) x = (λx. if x ∈ subst_domain σ then σ x else Var x) x" .
then have "⋀x. (λx. if x ∈ V then σ x else Var x) x = σ x" by (auto simp: subst_domain_def)
then have "(λx. if x ∈ V then σ x else Var x) = σ" by (rule ext)
then have "σ |s V = σ" by (simp add: subst_restrict_def)
then show ?thesis .
qed
lemma subst_restrict_UNIV[simp]: "σ |s UNIV = σ" by (auto simp: subst_restrict_def)
lemma subst_restrict_empty[simp]: "σ |s {} = Var" by (simp add: subst_restrict_def)
lemma vars_term_subst_pow:
"vars_term (t ⋅ σ^^n) ⊆ vars_term t ∪ ⋃(vars_term ` subst_range σ)" (is "_ ⊆ ?R t")
unfolding vars_term_subst
proof (induct n arbitrary: t)
case (Suc n t)
show ?case
proof
fix x
assume "x ∈ ⋃(vars_term ` (σ ^^ Suc n) ` vars_term t)"
then obtain y u where 1: "y ∈ vars_term t" "u = (σ ^^ Suc n) y" "x ∈ vars_term u"
by auto
from 1(2) have "u = σ y ⋅ σ ^^ n" by (auto simp: subst_compose_def)
from 1(3)[unfolded this, unfolded vars_term_subst]
have "x ∈ ⋃(vars_term ` (σ ^^ n) ` vars_term (σ y))" .
with Suc[of "σ y"] have x: "x ∈ ?R (σ y)" by auto
then show "x ∈ ?R t"
proof
assume "x ∈ vars_term (σ y)"
then show ?thesis using 1(1) by (cases "σ y = Var y", auto simp: subst_domain_def)
qed auto
qed
qed auto
lemma coincidence_lemma:
"t ⋅ σ = t ⋅ (σ |s vars_term t)"
unfolding term_subst_eq_conv subst_restrict_def by auto
lemma subst_domain_vars_term_subset:
"subst_domain (σ |s vars_term t) ⊆ vars_term t"
by (auto simp: subst_domain_def subst_restrict_def)
lemma subst_restrict_single_Var [simp]:
assumes "x ∉ subst_domain σ" shows "σ |s {x} = Var"
proof -
have A: "⋀x. x ∉ subst_domain σ ⟹ σ x = Var x" by (simp add: subst_domain_def)
have "σ |s {x} = (λy. if y ∈ {x} then σ y else Var y)" by (simp add: subst_restrict_def)
also have "… = (λy. if y = x then σ y else Var y)" by simp
also have "… = (λy. if y = x then σ x else Var y)" by (simp cong: if_cong)
also have "… = (λy. if y = x then Var x else Var y)" unfolding A[OF assms] by simp
also have "… = (λy. if y = x then Var y else Var y)" by (simp cong: if_cong)
also have "… = (λy. Var y)" by simp
finally show ?thesis by simp
qed
lemma subst_restrict_single_Var':
assumes "x ∉ subst_domain σ" and "σ |s V = Var" shows "σ |s ({x} ∪ V) = Var"
proof -
have "(λy. if y ∈ V then σ y else Var y) = (λy. Var y)"
using ‹σ |s V = Var› by (simp add: subst_restrict_def)
then have "(λy. if y ∈ V then σ y else Var y) = (λy. Var y)" by simp
then have A: "⋀y. (if y ∈ V then σ y else Var y) = Var y" by (rule fun_cong)
{
fix y
have "(if y ∈ {x} ∪ V then σ y else Var y) = Var y"
proof (cases "y = x")
assume "y = x" then show ?thesis using ‹x ∉ subst_domain σ› by (auto simp: subst_domain_def)
next
assume "y ≠ x" then show ?thesis using A by simp
qed
}
then have "⋀y. (if y ∈ {x} ∪ V then σ y else Var y) = Var y" by simp
then show ?thesis by (auto simp: subst_restrict_def)
qed
lemma subst_restrict_empty_set:
"finite V ⟹ V ∩ subst_domain σ = {} ⟹ σ |s V = Var"
proof (induct rule: finite.induct)
case (insertI V x)
then have "V ∩ subst_domain σ = {}" by simp
with insertI have "σ |s V = Var" by simp
then show ?case using insertI subst_restrict_single_Var'[where σ = σ and x = x and V = V] by simp
qed auto
lemma subst_restrict_Var: "x ≠ y ⟹ Var y ⋅ (σ |s (UNIV - {x})) = Var y ⋅ σ"
by (auto simp: subst_restrict_def)
lemma var_cond_stable:
assumes "vars_term r ⊆ vars_term l"
shows "vars_term (r ⋅ μ) ⊆ vars_term (l ⋅ μ)"
unfolding vars_term_subst using assms by blast
lemma instance_no_supt_imp_no_supt:
assumes "¬ s ⋅ σ ⊳ t ⋅ σ"
shows "¬ s ⊳ t"
proof
assume "s ⊳ t"
hence "s ⋅ σ ⊳ t ⋅ σ" by (rule supt_subst)
with assms show "False" by simp
qed
lemma subst_image_subterm:
assumes "x ∈ vars_term (Fun f ss)"
shows "Fun f ss ⋅ σ ⊳ σ x"
proof -
have "Fun f ss ⊵ Var x" using supteq_Var[OF assms(1)] .
then have "Fun f ss ⊳ Var x" by cases auto
from supt_subst [OF this]
show ?thesis by simp
qed
lemma funas_term_subst_pow:
"funas_term (t ⋅ σ^^n) ⊆ funas_term t ∪ ⋃(funas_term ` subst_range σ)"
proof -
{
fix Xs
have "⋃(funas_term ` (σ ^^ n) ` Xs) ⊆ ⋃(funas_term ` subst_range σ)"
proof (induct n arbitrary: Xs)
case (Suc n Xs)
show ?case (is "⋃ ?L ⊆ ?R")
proof (rule subsetI)
fix f
assume "f ∈ ⋃ ?L"
then obtain x where "f ∈ funas_term ((σ ^^ Suc n) x)" by auto
then have "f ∈ funas_term (σ x ⋅ σ ^^ n)" by (auto simp: subst_compose_def)
from this[unfolded funas_term_subst]
show "f ∈ ?R" using Suc[of "vars_term (σ x)"]
unfolding subst_range.simps subst_domain_def by (cases "σ x = Var x", auto)
qed
qed auto
}
then show ?thesis unfolding funas_term_subst by auto
qed
lemma funas_term_subterm_args:
assumes sF: "funas_term s ⊆ F"
and q: "q ∈ poss s"
shows "⋃(funas_term ` set (args (s |_ q))) ⊆ F"
proof -
from subt_at_imp_ctxt[OF q] obtain C where s: "s = C ⟨ s |_ q ⟩" by metis
from sF arg_cong[OF this, of "funas_term"] have "funas_term (s |_ q) ⊆ F" by auto
then show ?thesis by (cases "s |_ q", auto)
qed
lemma get_var_or_const: "∃ C t. s = C⟨t⟩ ∧ args t = []"
proof (induct s)
case (Var y)
show ?case by (rule exI[of _ Hole], auto)
next
case (Fun f ts)
show ?case
proof (cases ts)
case Nil
show ?thesis unfolding Nil
by (rule exI[of _ Hole], auto)
next
case (Cons s ss)
then have "s ∈ set ts" by auto
from Fun[OF this] obtain C where C: "∃ t. s = C⟨t⟩ ∧ args t = []" by auto
show ?thesis unfolding Cons
by (rule exI[of _ "More f [] C ss"], insert C, auto)
qed
qed
lemma supteq_Var_id [simp]:
assumes "Var x ⊵ s" shows "s = Var x"
using assms by (cases)
lemma arg_not_term [simp]:
assumes "t ∈ set ts" shows "Fun f ts ≠ t"
proof (rule ccontr)
assume "¬ Fun f ts ≠ t"
then have "size (Fun f ts) = size t" by simp
moreover have "size t < size_list size ts" using assms by (induct ts) auto
ultimately show False by simp
qed
lemma arg_subteq [simp]: "t ∈ set ts ⟹ Fun f ts ⊵ t"
by auto
lemma supt_imp_args:
assumes "∀t. s ⊳ t ⟶ P t"
shows "∀t∈set (args s). P t"
using assms by (cases s) simp_all
lemma ctxt_apply_eq_False[simp]: "(More f ss1 D ss2)⟨t⟩ ≠ t" (is "?C⟨_⟩ ≠ _")
proof
assume eq: "?C⟨t⟩ = t"
have "?C ≠ □" by auto
from ctxt_supt[OF this eq[symmetric]]
have "t ⊳ t" .
then show False by auto
qed
lemma supteq_imp_funs_term_subset: "t ⊵ s ⟹ funs_term s ⊆ funs_term t"
by (induct rule:supteq.induct) auto
lemma funs_term_subst: "funs_term (t ⋅ σ) = funs_term t ∪ ⋃ ((λ x. funs_term (σ x)) ` (vars_term t))"
by (induct t) auto
lemma set_set_cons:
assumes "P x" and "⋀y. y ∈ set xs ⟹ P y"
shows "y ∈ set (x # xs) ⟹ P y"
using assms by auto
lemma ctxt_power_compose_distr: "C ^ (m + n) = C ^ m ∘⇩c C ^ n"
by (induct m) (simp_all add: ac_simps)
lemma subst_apply_id':
assumes "vars_term t ∩ V = {}"
shows "t ⋅ (σ |s V) = t"
using assms
proof (induct t)
case (Var x) then show ?case by (simp add: subst_restrict_def)
next
case (Fun f ts)
then have "∀s∈set ts. s ⋅ (σ |s V) = s" by auto
with map_idI [of ts "λt. t ⋅ (σ |s V)"] show ?case by simp
qed
lemma subst_apply_ctxt_id:
assumes "vars_ctxt C ∩ V = {}"
shows "C ⋅⇩c (σ |s V) = C"
using assms
proof (induct C)
case (More f ss1 D ss2)
then have IH: "D ⋅⇩c (σ |s V) = D" by auto
from More have "∀s∈set(ss1@ss2). vars_term s ∩ V = {}" by auto
with subst_apply_id' have args: "∀s∈set(ss1@ss2). s⋅(σ |s V) = s" by best
from args have "∀s∈set ss1. s⋅(σ |s V) = s" by simp
with map_idI[of ss1 "λt. t⋅(σ |s V)"] have ss1: "map (λs. s⋅(σ |s V)) ss1 = ss1" by best
from args have "∀s∈set ss2. s⋅(σ |s V) = s" by simp
with map_idI[of ss2 "λt. t⋅(σ |s V)"] have ss2: "map (λs. s⋅(σ |s V)) ss2 = ss2" by best
show ?case by (simp add: ss1 ss2 IH)
qed simp
lemma vars_term_Var_id: "vars_term o Var = (λx. {x})"
by (rule ext) simp
lemma ctxt_exhaust_rev[case_names Hole More]:
assumes "C = □ ⟹ P" and
"⋀D f ss1 ss2. C = D ∘⇩c (More f ss1 □ ss2) ⟹ P"
shows "P"
proof (cases C)
case Hole with assms show ?thesis by simp
next
case (More g ts1 E ts2)
then have "∃D f ss1 ss2. C = D ∘⇩c (More f ss1 □ ss2)"
proof (induct E arbitrary: C g ts1 ts2)
case Hole then have "C = □ ∘⇩c (More g ts1 □ ts2)" by simp
then show ?case by best
next
case (More h us1 F us2)
from More(1)[of "More h us1 F us2"]
obtain G i vs1 vs2 where IH: "More h us1 F us2 = G ∘⇩c More i vs1 □ vs2" by force
from More have "C = (More g ts1 □ ts2 ∘⇩c G) ∘⇩c More i vs1 □ vs2" unfolding IH by simp
then show ?case by best
qed
then show ?thesis using assms by auto
qed
fun
subst_extend :: "('f, 'v, 'w) gsubst ⇒ ('v × ('f, 'w) term) list ⇒ ('f, 'v, 'w) gsubst"
where
"subst_extend σ vts = (λx.
(case map_of vts x of
Some t ⇒ t
| None ⇒ σ(x)))"
lemma subst_extend_id:
assumes "V ∩ set vs = {}" and "vars_term t ⊆ V"
shows "t ⋅ subst_extend σ (zip vs ts) = t ⋅ σ"
using assms
proof (induct t)
case (Var x) then show ?case
using map_of_SomeD[of "zip vs ts" x]
using set_zip_leftD [of x _ vs ts]
using IntI [of x V "set vs"]
using emptyE
by (case_tac "map_of (zip vs ts) x") auto
qed auto
lemma funas_term_args:
"⋃(funas_term ` set (args t)) ⊆ funas_term t"
by (cases t) auto
lemma subst_extend_absorb:
assumes "distinct vs" and "length vs = length ss"
shows "map (λt. t ⋅ subst_extend σ (zip vs ss)) (map Var vs) = ss" (is "?ss = _")
proof -
let ?σ = "subst_extend σ (zip vs ss)"
from assms have "length vs ≤ length ss" by simp
from assms have "length ?ss = length ss" by simp
moreover have "∀i<length ?ss. ?ss ! i = ss ! i"
proof (intro allI impI)
fix i assume "i < length ?ss"
then have i: "i < length (map Var vs)" by simp
then have len: "i < length vs" by simp
have "?ss!i = (map Var vs ! i) ⋅ ?σ" unfolding nth_map[OF i, of "λt. t⋅?σ"] by simp
also have "… = Var(vs!i)⋅?σ" unfolding nth_map[OF len] by simp
also have "… = (case map_of (zip vs ss) (vs ! i) of None ⇒ σ (vs ! i) | Some t ⇒ t)" by simp
also have "… = ss ! i" using ‹distinct vs› ‹length vs ≤ length ss› len
by (simp add: assms(2) map_of_zip_nth)
finally show "?ss!i = ss!i" by simp
qed
ultimately show ?thesis by (metis nth_equalityI)
qed
abbreviation "map_funs_term f ≡ term.map_term f (λx. x)"
abbreviation "map_funs_ctxt f ≡ ctxt.map_ctxt f (λx. x)"
lemma funs_term_map_funs_term_id: "(⋀ f. f ∈ funs_term t ⟹ h f = f) ⟹ map_funs_term h t = t"
proof (induct t)
case (Fun f ts)
then have "⋀ t. t ∈ set ts ⟹ map_funs_term h t = t" by auto
with Fun(2)[of f] show ?case
by (auto intro: nth_equalityI)
qed simp
lemma funs_term_map_funs_term:
"funs_term (map_funs_term h t) ⊆ range h"
by (induct t) auto
fun map_funs_subst :: "('f ⇒ 'g) ⇒ ('f, 'v) subst ⇒ ('g, 'v) subst" where
"map_funs_subst fg σ = (λx. map_funs_term fg (σ x))"
lemma map_funs_term_comp:
"map_funs_term fg (map_funs_term gh t) = map_funs_term (fg ∘ gh) t"
by (induct t) simp_all
lemma map_funs_subst_distrib [simp]:
"map_funs_term fg (t ⋅ σ) = map_funs_term fg t ⋅ map_funs_subst fg σ"
by (induct t) simp_all
lemma size_map_funs_term [simp]:
"size (map_funs_term fg t) = size t"
proof (induct t)
case (Fun f ts)
then show ?case by (induct ts) auto
qed simp
lemma fold_ident [simp]: "Term_More.fold Var Fun t = t"
by (induct t) (auto simp: map_ext [of _ "Term_More.fold Var Fun" id])
lemma map_funs_term_ident [simp]:
"map_funs_term id t = t"
by (induct t) (simp_all add: map_idI)
lemma ground_map_funs_term [simp]:
"ground (map_funs_term fg t) = ground t"
by (induct t) auto
lemma map_funs_term_power:
fixes f :: "'f ⇒ 'f"
shows "((map_funs_term f) ^^ n) = map_funs_term (f ^^ n)"
proof (rule sym, intro ext)
fix t :: "('f,'v)term"
show "map_funs_term (f ^^ n) t = (map_funs_term f ^^ n) t"
proof (induct n)
case 0
show ?case by (simp add: term.map_ident)
next
case (Suc n)
show ?case by (simp add: Suc[symmetric] map_funs_term_comp o_def)
qed
qed
lemma map_funs_term_ctxt_distrib [simp]:
"map_funs_term fg (C⟨t⟩) = (map_funs_ctxt fg C)⟨map_funs_term fg t⟩"
by (induct C) (auto)
text ‹mapping function symbols (w)ith (a)rities taken into account (wa)›
fun map_funs_term_wa :: "('f × nat ⇒ 'g) ⇒ ('f, 'v) term ⇒ ('g, 'v) term"
where
"map_funs_term_wa fg (Var x) = Var x" |
"map_funs_term_wa fg (Fun f ts) = Fun (fg (f, length ts)) (map (map_funs_term_wa fg) ts)"
lemma map_funs_term_map_funs_term_wa:
"map_funs_term (fg :: ('f ⇒ 'g)) = map_funs_term_wa (λ (f,n). (fg f))"
proof (intro ext)
fix t :: "('f,'v)term"
show "map_funs_term fg t = map_funs_term_wa (λ (f,n). fg f) t"
by (induct t, auto)
qed
fun map_funs_ctxt_wa :: "('f × nat ⇒ 'g) ⇒ ('f, 'v) ctxt ⇒ ('g, 'v) ctxt"
where
"map_funs_ctxt_wa fg □ = □" |
"map_funs_ctxt_wa fg (More f bef C aft) =
More (fg (f, Suc (length bef + length aft))) (map (map_funs_term_wa fg) bef) (map_funs_ctxt_wa fg C) (map (map_funs_term_wa fg) aft)"
abbreviation map_funs_subst_wa :: "('f × nat ⇒ 'g) ⇒ ('f, 'v) subst ⇒ ('g, 'v) subst" where
"map_funs_subst_wa fg σ ≡ (λx. map_funs_term_wa fg (σ x))"
lemma map_funs_term_wa_subst [simp]:
"map_funs_term_wa fg (t ⋅ σ) = map_funs_term_wa fg t ⋅ map_funs_subst_wa fg σ"
by (induct t, auto)
lemma map_funs_term_wa_ctxt [simp]:
"map_funs_term_wa fg (C⟨t⟩) = (map_funs_ctxt_wa fg C) ⟨map_funs_term_wa fg t⟩"
by (induct C, auto)
lemma map_funs_term_wa_funas_term_id:
assumes t: "funas_term t ⊆ F"
and id: "⋀ f n. (f,n) ∈ F ⟹ fg (f,n) = f"
shows "map_funs_term_wa fg t = t"
using t
proof (induct t)
case (Fun f ss)
then have IH: "⋀ s. s ∈ set ss ⟹ map_funs_term_wa fg s = s" by auto
from Fun(2) id have [simp]: "fg (f, length ss) = f" by simp
show ?case by (simp, insert IH, induct ss, auto)
qed simp
lemma funas_term_map_funs_term_wa:
"funas_term (map_funs_term_wa fg t) = (λ (f,n). (fg (f,n),n)) ` (funas_term t)"
by (induct t) auto+
lemma notin_subst_restrict [simp]:
assumes "x ∉ V" shows "(σ |s V) x = Var x"
using assms by (auto simp: subst_restrict_def)
lemma in_subst_restrict [simp]:
assumes "x ∈ V" shows "(σ |s V) x = σ x"
using assms by (auto simp: subst_restrict_def)
lemma coincidence_lemma':
assumes "vars_term t ⊆ V"
shows "t ⋅ (σ |s V) = t ⋅ σ"
using assms by (metis in_mono in_subst_restrict term_subst_eq)
lemma vars_term_map_funs_term [simp]:
"vars_term ∘ map_funs_term (f :: ('f ⇒ 'g)) = vars_term"
proof
fix t :: "('f,'v)term"
show "(vars_term ∘ map_funs_term f) t = vars_term t"
by (induct t) (auto)
qed
lemma vars_term_map_funs_term2 [simp]:
"vars_term (map_funs_term f t) = vars_term t"
using fun_cong [OF vars_term_map_funs_term, of f t]
by (simp del: vars_term_map_funs_term)
lemma map_funs_term_wa_ctxt_split:
assumes "map_funs_term_wa fg s = lC⟨lt⟩"
shows "∃ C t. s = C⟨t⟩ ∧ map_funs_term_wa fg t = lt ∧ map_funs_ctxt_wa fg C = lC"
using assms
proof (induct lC arbitrary: s)
case Hole
show ?case
by (rule exI[of _ Hole], insert Hole, auto)
next
case (More lf lbef lC laft s)
from More(2) obtain fs ss where s: "s = Fun fs ss" by (cases s, auto)
note More = More[unfolded s, simplified]
let ?lb = "length lbef"
let ?la = "length laft"
let ?n = "Suc (?lb + ?la)"
let ?m = "map_funs_term_wa fg"
from More(2) have rec: "map ?m ss = lbef @ lC⟨lt⟩ # laft"
and lf: "lf = fg (fs,length ss)" by blast+
from arg_cong[OF rec, of length] have len: "length ss = ?n" by auto
then have lb: "?lb < length ss" by auto
note ss = id_take_nth_drop[OF this]
from rec ss have "map ?m (take ?lb ss @ ss ! ?lb # drop (Suc ?lb) ss) = lbef @ lC⟨lt⟩ # laft" by auto
then have id: "take ?lb (map ?m ss) @ ?m (ss ! ?lb) # drop (Suc ?lb) (map ?m ss) = lbef @ lC⟨lt⟩ # laft"
(is "?l1 @ ?l2 # ?l3 = ?r1 @ ?r2 # ?r3")
unfolding take_map drop_map
by auto
from len have len2: "⋀ P. length ?l1 = length ?r1 ∨ P"
unfolding length_take by auto
from id[unfolded List.append_eq_append_conv[OF len2]]
have id: "?l1 = ?r1" "?l2 = ?r2" "?l3 = ?r3" by auto
from More(1)[OF id(2)] obtain C t where sb: "ss ! ?lb = C⟨t⟩" and map: "map_funs_term_wa fg t = lt" and ma: "map_funs_ctxt_wa fg C = lC" by auto
let ?C = "More fs (take ?lb ss) C (drop (Suc ?lb) ss)"
have s: "s = ?C⟨t⟩"
unfolding s using ss[unfolded sb] by simp
have len3: "Suc (length (take ?lb ss) + length (drop (Suc ?lb) ss)) = length ss"
unfolding length_take length_drop len by auto
show ?case
proof (intro exI conjI, rule s, rule map)
show "map_funs_ctxt_wa fg ?C = More lf lbef lC laft"
unfolding map_funs_ctxt_wa.simps
unfolding len3
using id ma lf
unfolding take_map drop_map
by auto
qed
qed
lemma subst_extend_flat_ctxt:
assumes dist: "distinct vs"
and len1: "length(take i (map Var vs)) = length ss1"
and len2: "length(drop (Suc i) (map Var vs)) = length ss2"
and i: "i < length vs"
shows "More f (take i (map Var vs)) □ (drop (Suc i) (map Var vs)) ⋅⇩c subst_extend σ (zip (take i vs@drop (Suc i) vs) (ss1@ss2)) = More f ss1 □ ss2"
proof -
let ?V = "map Var vs"
let ?vs1 = "take i vs" and ?vs2 = "drop (Suc i) vs"
let ?ss1 = "take i ?V" and ?ss2 = "drop (Suc i) ?V"
let ?σ = "subst_extend σ (zip (?vs1@?vs2) (ss1@ss2))"
from len1 and len2 have len: "length(?vs1@?vs2) = length(ss1@ss2)" using i by simp
from dist i have "distinct(?vs1@?vs2)"
by (simp add: set_take_disj_set_drop_if_distinct)
from subst_extend_absorb[OF this len,of "σ"]
have map: "map (λt. t⋅?σ) (?ss1@?ss2) = ss1@ss2" unfolding take_map drop_map map_append .
from len1 and map have "map (λt. t⋅?σ) ?ss1 = ss1" by auto
moreover from len2 and map have "map (λt. t⋅?σ) ?ss2 = ss2" by auto
ultimately show ?thesis by simp
qed
lemma subst_extend_flat_ctxt'':
assumes dist: "distinct vs"
and len1: "length(take i (map Var vs)) = length ss1"
and len2: "length(drop i (map Var vs)) = length ss2"
and i: "i < length vs"
shows "More f (take i (map Var vs)) □ (drop i (map Var vs)) ⋅⇩c subst_extend σ (zip (take i vs@drop i vs) (ss1@ss2)) = More f ss1 □ ss2"
proof -
let ?V = "map Var vs"
let ?vs1 = "take i vs" and ?vs2 = "drop i vs"
let ?ss1 = "take i ?V" and ?ss2 = "drop i ?V"
let ?σ = "subst_extend σ (zip (?vs1@?vs2) (ss1@ss2))"
from len1 and len2 have len: "length(?vs1@?vs2) = length(ss1@ss2)" using i by simp
have "distinct(?vs1@?vs2)" using dist unfolding append_take_drop_id by simp
from subst_extend_absorb[OF this len,of "σ"]
have map: "map (λt. t⋅?σ) (?ss1@?ss2) = ss1@ss2" unfolding take_map drop_map map_append .
from len1 and map have "map (λt. t⋅?σ) ?ss1 = ss1" unfolding map_append by auto
moreover from len2 and map have "map (λt. t⋅?σ) ?ss2 = ss2" unfolding map_append by auto
ultimately show ?thesis by simp
qed
lemma distinct_map_Var:
assumes "distinct xs" shows "distinct (map Var xs)"
using assms by (induct xs) auto
lemma variants_imp_is_Var:
assumes "s ⋅ σ = t" and "t ⋅ τ = s"
shows "∀x∈vars_term s. is_Var (σ x)"
using assms
proof (induct s arbitrary: t)
case (Var x)
then show ?case by (cases "σ x") auto
next
case (Fun f ts)
then show ?case
by (auto simp: o_def) (metis map_eq_conv map_ident)
qed
text ‹The range (in a functional sense) of a substitution.›
definition subst_fun_range :: "('f, 'v, 'w) gsubst ⇒ 'w set"
where
"subst_fun_range σ = ⋃(vars_term ` range σ)"
lemma subst_variants_imp_is_Var:
assumes "σ ∘⇩s σ' = τ" and "τ ∘⇩s τ' = σ"
shows "∀x∈subst_fun_range σ. is_Var (σ' x)"
using assms by (auto simp: subst_compose_def subst_fun_range_def) (metis variants_imp_is_Var)
lemma variants_imp_image_vars_term_eq:
assumes "s ⋅ σ = t" and "t ⋅ τ = s"
shows "(the_Var ∘ σ) ` vars_term s = vars_term t"
using assms
proof (induct s arbitrary: t)
case (Var x)
then show ?case by (cases t) auto
next
case (Fun f ss)
then have IH: "⋀t. ∀i<length ss. (ss ! i) ⋅ σ = t ∧ t ⋅ τ = ss ! i ⟶
(the_Var ∘ σ) ` vars_term (ss ! i) = vars_term t"
by (auto simp: o_def)
from Fun.prems have t: "t = Fun f (map (λt. t ⋅ σ) ss)"
and ss: "ss = map (λt. t ⋅ σ ⋅ τ) ss" by (auto simp: o_def)
have "∀i<length ss. (the_Var ∘ σ) ` vars_term (ss ! i) = vars_term (ss ! i ⋅ σ)"
proof (intro allI impI)
fix i
assume *: "i < length ss"
have "(ss ! i) ⋅ σ = (ss ! i) ⋅ σ" by simp
moreover have "(ss ! i) ⋅ σ ⋅ τ = ss ! i"
using * by (subst (2) ss) simp
ultimately show "(the_Var ∘ σ) ` vars_term (ss ! i) = vars_term ((ss ! i) ⋅ σ)"
using IH and * by blast
qed
then have "∀s∈set ss. (the_Var ∘ σ) ` vars_term s = vars_term (s ⋅ σ)" by (metis in_set_conv_nth)
then show ?case by (simp add: o_def t image_UN)
qed
lemma terms_to_vars:
assumes "∀t∈set ts. is_Var t"
shows "⋃(set (map vars_term ts)) = set (map the_Var ts)"
using assms by (induct ts) auto
lemma Var_the_Var_id:
assumes "∀t∈set ts. is_Var t"
shows "map Var (map the_Var ts) = ts"
using assms by (induct ts) auto
lemma distinct_the_vars:
assumes "∀t∈set ts. is_Var t"
and "distinct ts"
shows "distinct (map the_Var ts)"
using assms by (induct ts) auto
lemma map_funs_term_eq_imp_map_funs_term_map_vars_term_eq:
"map_funs_term fg s = map_funs_term fg t ⟹ map_funs_term fg (map_vars_term vw s) = map_funs_term fg (map_vars_term vw t)"
proof (induct s arbitrary: t)
case (Var x t)
then show ?case by (cases t, auto)
next
case (Fun f ss t)
then obtain g ts where t: "t = Fun g ts" by (cases t, auto)
from Fun(2)[unfolded t, simplified]
have f: "fg f = fg g" and ss: "map (map_funs_term fg) ss = map (map_funs_term fg) ts" by auto
from arg_cong[OF ss, of length] have "length ss = length ts" by simp
from this ss Fun(1) have "map (map_funs_term fg ∘ map_vars_term vw) ss = map (map_funs_term fg ∘ map_vars_term vw) ts"
by (induct ss ts rule: list_induct2, auto)
then show ?case unfolding t by (simp add: f)
qed
lemma var_type_conversion:
assumes inf: "infinite (UNIV :: 'v set)"
and fin: "finite (T :: ('f, 'w) terms)"
shows "∃ (σ :: ('f, 'w, 'v) gsubst) τ. ∀t∈T. t = t ⋅ σ ⋅ τ"
proof -
obtain V where V: "V = ⋃(vars_term ` T)" by auto
have fin: "finite V" unfolding V
by (rule, rule, rule fin,
insert finite_vars_term, auto)
from finite_imp_inj_to_nat_seg[OF fin] obtain to_nat :: "'w ⇒ nat" and n :: nat
where to_nat: "to_nat ` V = {i. i < n}" "inj_on to_nat V" by blast+
from infinite_countable_subset[OF inf] obtain of_nat :: "nat ⇒ 'v" where
of_nat: "range of_nat ⊆ UNIV" "inj of_nat" by auto
let ?conv = "λ v. of_nat (to_nat v)"
have inj: "inj_on ?conv V" using of_nat(2) to_nat(2) unfolding inj_on_def by auto
let ?rev = "the_inv_into V ?conv"
note rev = the_inv_into_f_eq[OF inj]
obtain σ where σ: "σ = (λ v. Var (?conv v) :: ('f,'v)term)" by simp
obtain τ where τ: "τ = (λ v. Var (?rev v) :: ('f,'w)term)" by simp
show ?thesis
proof (rule exI[of _ σ], rule exI[of _ τ], intro ballI)
fix t
assume t: "t ∈ T"
have "t ⋅ σ ⋅ τ = t ⋅ (σ ∘⇩s τ)" by simp
also have "... = t ⋅ Var"
proof (rule term_subst_eq)
fix x
assume "x ∈ vars_term t"
with t have x: "x ∈ V" unfolding V by auto
show "(σ ∘⇩s τ) x = Var x" unfolding σ τ subst_compose_def
eval_term.simps term.simps
by (rule rev[OF refl x])
qed
finally show "t = t ⋅ σ ⋅ τ" by simp
qed
qed
text ‹combine two substitutions via sum-type›
fun
merge_substs :: "('f, 'u, 'v) gsubst ⇒ ('f, 'w, 'v) gsubst ⇒ ('f, 'u + 'w, 'v) gsubst"
where
"merge_substs σ τ = (λx.
(case x of
Inl y ⇒ σ y
| Inr y ⇒ τ y))"
lemma merge_substs_left:
"map_vars_term Inl s ⋅ (merge_substs σ δ) = s ⋅ σ"
by (induct s) auto
lemma merge_substs_right:
"map_vars_term Inr s ⋅ (merge_substs σ δ) = s ⋅ δ"
by (induct s) auto
fun map_vars_subst_ran :: "('w ⇒ 'u) ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'v, 'u) gsubst"
where
"map_vars_subst_ran m σ = (λv. map_vars_term m (σ v))"
lemma map_vars_subst_ran:
shows "map_vars_term m (t ⋅ σ) = t ⋅ map_vars_subst_ran m σ"
by (induct t) (auto)
lemma size_subst: "size t ≤ size (t ⋅ σ)"
proof (induct t)
case (Var x)
then show ?case by (cases "σ x") auto
next
case (Fun f ss)
then show ?case
by (simp add: o_def, induct ss, force+)
qed
lemma eq_ctxt_subst_iff [simp]:
"(t = C⟨t ⋅ σ⟩) ⟷ C = □ ∧ (∀x∈vars_term t. σ x = Var x)" (is "?L = ?R")
proof
assume t: "?L"
then have "size t = size (C⟨t ⋅ σ⟩)" by simp
with size_ne_ctxt [of C "t ⋅ σ"] and size_subst [of t σ]
have [simp]: "C = □" by auto
have "∀x∈vars_term t. σ x = Var x" using t and term_subst_eq_conv [of t Var] by simp
then show ?R by auto
next
assume ?R
then show ?L using term_subst_eq_conv [of t Var] by simp
qed
lemma Fun_Nil_supt[elim!]: "Fun f [] ⊳ t ⟹ P" by auto
lemma map_vars_term_vars_term:
assumes "⋀ x. x ∈ vars_term t ⟹ f x = g x"
shows "map_vars_term f t = map_vars_term g t"
using assms
proof (induct t)
case (Fun h ts)
{
fix t
assume t: "t ∈ set ts"
with Fun(2) have "⋀ x. x ∈ vars_term t ⟹ f x = g x"
by auto
from Fun(1)[OF t this] have "map_vars_term f t = map_vars_term g t" by simp
}
then show ?case by auto
qed simp
lemma map_funs_term_ctxt_decomp:
assumes "map_funs_term fg t = C⟨s⟩"
shows "∃ D u. C = map_funs_ctxt fg D ∧ s = map_funs_term fg u ∧ t = D⟨u⟩"
using assms
proof (induct C arbitrary: t)
case Hole
show ?case
by (rule exI[of _ Hole], rule exI[of _ t], insert Hole, auto)
next
case (More g bef C aft)
from More(2) obtain f ts where t: "t = Fun f ts" by (cases t, auto)
from More(2)[unfolded t] have f: "fg f = g" and ts: "map (map_funs_term fg) ts = bef @ C⟨s⟩ # aft" (is "?ts = ?bca") by auto
from ts have "length ?ts = length ?bca" by auto
then have len: "length ts = length ?bca" by auto
let ?i = "length bef"
from len have i: "?i < length ts" by auto
from arg_cong[OF ts, of "λ xs. xs ! ?i"] len
have "map_funs_term fg (ts ! ?i) = C⟨s⟩" by auto
from More(1)[OF this] obtain D u where D: "C = map_funs_ctxt fg D" and
u: "s = map_funs_term fg u" and id: "ts ! ?i = D⟨u⟩" by auto
from ts have "take ?i ?ts = take ?i ?bca" by simp
also have "... = bef" by simp
finally have bef: "map (map_funs_term fg) (take ?i ts) = bef" by (simp add: take_map)
from ts have "drop (Suc ?i) ?ts = drop (Suc ?i) ?bca" by simp
also have "... = aft" by simp
finally have aft: "map (map_funs_term fg) (drop (Suc ?i) ts) = aft" by (simp add:drop_map)
let ?bda = "take ?i ts @ D⟨u⟩ # drop (Suc ?i) ts"
show ?case
proof (rule exI[of _ "More f (take ?i ts) D (drop (Suc ?i) ts)"],
rule exI[of _ u], simp add: u f D bef aft t)
have "ts = take ?i ts @ ts ! ?i # drop (Suc ?i) ts"
by (rule id_take_nth_drop[OF i])
also have "... = ?bda" by (simp add: id)
finally show "ts = ?bda" .
qed
qed
lemma funas_term_map_vars_term [simp]:
"funas_term (map_vars_term τ t) = funas_term t"
by (induct t) auto
lemma funs_term_funas_term:
"funs_term t = fst ` (funas_term t)"
by (induct t) auto
lemma funas_term_map_funs_term:
"funas_term (map_funs_term fg t) = (λ (f,n). (fg f,n)) ` (funas_term t)"
by (induct t) auto+
lemma supt_imp_arg_or_supt_of_arg:
assumes "Fun f ss ⊳ t"
shows "t ∈ set ss ∨ (∃s ∈ set ss. s ⊳ t)"
using assms by (rule supt.cases) auto
lemma supt_Fun_imp_arg_supteq:
assumes "Fun f ss ⊳ t" shows "∃s ∈ set ss. s ⊵ t"
using assms by (cases rule: supt.cases) auto
lemma subt_iff_eq_or_subt_of_arg:
assumes "s = Fun f ss"
shows "{t. s ⊵ t} = ((⋃u ∈ set ss. {t. u ⊵ t})∪{s})"
using assms proof (induct s)
case (Var x) then show ?case by auto
next
case (Fun g ts)
then have "g = f" and "ts = ss" by auto
show ?case
proof
show "{a. Fun g ts ⊵ a} ⊆ (⋃u∈set ss. {a. u ⊵ a}) ∪ {Fun g ts}"
proof
fix x
assume "x ∈ {a. Fun g ts ⊵ a}"
then have "Fun g ts ⊵ x" by simp
then have "Fun g ts ⊳ x ∨ Fun g ts = x" by auto
then show "x ∈ (⋃u∈set ss. {a. u ⊵a}) ∪ {Fun g ts}"
proof
assume "Fun g ts ⊳ x"
then obtain u where "u ∈ set ts" and "u ⊵ x" using supt_Fun_imp_arg_supteq by best
then have "x ∈ {a. u ⊵ a}" by simp
with ‹u ∈ set ts› have "x ∈ (⋃u∈set ts. {a. u ⊵ a})" by auto
then show ?thesis unfolding ‹ts = ss› by simp
next
assume "Fun g ts = x" then show ?thesis by simp
qed
qed
next
show "(⋃u∈set ss. {a. u ⊵ a}) ∪ {Fun g ts} ⊆ {a. Fun g ts ⊵ a}"
proof
fix x
assume "x ∈ (⋃u∈set ss. {a. u ⊵ a}) ∪ {Fun g ts}"
then have "x ∈ (⋃u∈set ss. {a. u ⊵ a}) ∨ x = Fun g ts" by auto
then show "x ∈ {a. Fun g ts ⊵ a}"
proof
assume "x ∈ (⋃u∈set ss. {a. u ⊵ a})"
then obtain u where "u ∈ set ss" and "u ⊵ x" by auto
then show ?thesis unfolding ‹ts = ss› by auto
next
assume "x = Fun g ts" then show ?thesis by auto
qed
qed
qed
qed
text ‹The set of subterms of a term is finite.›
lemma finite_subterms: "finite {s. t ⊵ s}"
proof (induct t)
case (Var x)
then have "⋀s. (Var x ⊵ s) = (Var x = s)" using supteq.cases by best
then show ?case unfolding ‹⋀s. (Var x ⊵ s) = (Var x = s)› by simp
next
case (Fun f ss)
have "Fun f ss = Fun f ss" by simp
from Fun show ?case
unfolding subt_iff_eq_or_subt_of_arg[OF ‹Fun f ss = Fun f ss›] by auto
qed
lemma Fun_supteq: "Fun f ts ⊵ u ⟷ Fun f ts = u ∨ (∃t∈set ts. t ⊵ u)"
using subt_iff_eq_or_subt_of_arg[of "Fun f ts" f ts] by auto
lemma subst_ctxt_distr: "s = C⟨t⟩⋅σ ⟹ ∃D. s = D⟨t⋅σ⟩"
using subst_apply_term_ctxt_apply_distrib by auto
lemma ctxt_of_pos_term_subst:
assumes "p ∈ poss t"
shows "ctxt_of_pos_term p (t ⋅ σ) = ctxt_of_pos_term p t ⋅⇩c σ"
using assms
proof (induct p arbitrary: t)
case (Cons i p t)
then obtain f ts where t: "t = Fun f ts" and i: "i < length ts" and p: "p ∈ poss (ts ! i)" by (cases t, auto)
note id = id_take_nth_drop[OF i, symmetric]
with t have t: "t = Fun f (take i ts @ ts ! i # drop (Suc i) ts)" by auto
from i have i': "min (length ts) i = i" by simp
show ?case unfolding t using Cons(1)[OF p, symmetric] i'
by (simp add: id, insert i, auto simp: take_map drop_map)
qed simp
lemma subt_at_ctxt_of_pos_term:
assumes t: "(ctxt_of_pos_term p t)⟨u⟩ = t" and p: "p ∈ poss t"
shows "t |_ p = u"
proof -
let ?C = "ctxt_of_pos_term p t"
from t and ctxt_supt_id [OF p] have "?C⟨u⟩ = ?C⟨t |_ p⟩" by simp
then show ?thesis by simp
qed
lemma subst_ext:
assumes "∀x∈V. σ x = τ x" shows "σ |s V = τ |s V"
proof
fix x show "(σ |s V) x = (τ |s V) x" using assms
unfolding subst_restrict_def by (cases "x ∈ V") auto
qed
abbreviation "map_vars_ctxt f ≡ ctxt.map_ctxt (λx. x) f"
lemma map_vars_term_ctxt_commute:
"map_vars_term m (c⟨t⟩) = (map_vars_ctxt m c)⟨map_vars_term m t⟩"
by (induct c) auto
lemma map_vars_term_inj_compose:
assumes inj: "⋀ x. n (m x) = x"
shows "map_vars_term n (map_vars_term m t) = t"
unfolding map_vars_term_compose o_def inj by (auto simp: term.map_ident)
lemma inj_map_vars_term_the_inv:
assumes "inj f"
shows "map_vars_term (the_inv f) (map_vars_term f t) = t"
unfolding map_vars_term_compose o_def the_inv_f_f[OF assms]
by (simp add: term.map_ident)
lemma map_vars_ctxt_subst:
"map_vars_ctxt m (C ⋅⇩c σ) = C ⋅⇩c map_vars_subst_ran m σ"
by (induct C) (auto simp: map_vars_subst_ran)
lemma poss_map_vars_term [simp]:
"poss (map_vars_term f t) = poss t"
by (induct t) auto
lemma map_vars_term_subt_at [simp]:
"p ∈ poss t ⟹ map_vars_term f (t |_ p) = (map_vars_term f t) |_ p"
proof (induct p arbitrary: t)
case Nil show ?case by auto
next
case (Cons i p t)
from Cons(2) obtain g ts where t: "t = Fun g ts" by (cases t, auto)
from Cons show ?case unfolding t by auto
qed
lemma hole_pos_subst[simp]: "hole_pos (C ⋅⇩c σ) = hole_pos C"
by (induct C, auto)
lemma hole_pos_ctxt_compose[simp]: "hole_pos (C ∘⇩c D) = hole_pos C @ hole_pos D"
by (induct C, auto)
lemma subst_left_right: "t ⋅ μ^^n ⋅ μ = t ⋅ μ ⋅ μ^^n"
proof -
have "t ⋅ μ ^^ n ⋅ μ = t ⋅ (μ ^^ n ∘⇩s μ)" by simp
also have "... = t ⋅ (μ ∘⇩s μ ^^ n)"
using subst_power_compose_distrib[of n "Suc 0" μ] by auto
finally show ?thesis by simp
qed
lemma subst_right_left: "t ⋅ μ ⋅ μ^^n = t ⋅ μ^^n ⋅ μ" unfolding subst_left_right ..
lemma subt_at_id_imp_eps:
assumes p: "p ∈ poss t" and id: "t |_ p = t"
shows "p = []"
proof (cases p)
case (Cons i q)
from subt_at_nepos_imp_supt[OF p[unfolded Cons], unfolded Cons[symmetric]
, unfolded id] have False by simp
then show ?thesis by auto
qed simp
lemma pos_into_subst:
assumes t: "t ⋅ σ = s" and p: "p ∈ poss s" and nt: "¬ (p ∈ poss t ∧ is_Fun (t |_ p))"
shows "∃q q' x. p = q @ q' ∧ q ∈ poss t ∧ t |_ q = Var x"
using p nt unfolding t[symmetric]
proof (induct t arbitrary: p)
case (Var x)
show ?case
by (rule exI[of _ "[]"], rule exI[of _ p], rule exI[of _ x], insert Var, auto)
next
case (Fun f ts)
from Fun(3) obtain i q where p: "p = i # q" by (cases p, auto)
note Fun = Fun[unfolded p]
from Fun(2) have i: "i < length ts" and q: "q ∈ poss (ts ! i ⋅ σ)" by auto
then have mem: "ts ! i ∈ set ts" by auto
from Fun(3) i have "¬ (q ∈ poss (ts ! i) ∧ is_Fun (ts ! i |_ q))" by auto
from Fun(1)[OF mem q this]
obtain r r' x where q: "q = r @ r' ∧ r ∈ poss (ts ! i) ∧ ts ! i |_ r = Var x" by blast
show ?case
by (rule exI[of _ "i # r"], rule exI[of _ r'], rule exI[of _ x],
unfold p, insert i q, auto)
qed
abbreviation (input) "replace_at t p s ≡ (ctxt_of_pos_term p t)⟨s⟩"
lemma replace_at_ident:
assumes "p ∈ poss t" and "t |_ p = s"
shows "replace_at t p s = t"
using assms by (metis ctxt_supt_id)
lemma ctxt_of_pos_term_append:
assumes "p ∈ poss t"
shows "ctxt_of_pos_term (p @ q) t = ctxt_of_pos_term p t ∘⇩c ctxt_of_pos_term q (t |_ p)"
using assms
proof (induct p arbitrary: t)
case Nil show ?case by simp
next
case (Cons i p t)
from Cons(2) obtain f ts where t: "t = Fun f ts" and i: "i < length ts" and p: "p ∈ poss (ts ! i)" by (cases t, auto)
from Cons(1)[OF p]
show ?case unfolding t using i by auto
qed
lemma parallel_replace_at:
fixes p1 :: pos
assumes parallel: "p1 ⊥ p2"
and p1: "p1 ∈ poss t"
and p2: "p2 ∈ poss t"
shows "replace_at (replace_at t p1 s1) p2 s2 = replace_at (replace_at t p2 s2) p1 s1"
proof -
from parallel_remove_prefix[OF parallel]
obtain p i j q1 q2 where p1_id: "p1 = p @ i # q1" and p2_id: "p2 = p @ j # q2"
and ij: "i ≠ j" by blast
from p1 p2 show ?thesis unfolding p1_id p2_id
proof (induct p arbitrary: t)
case (Cons k p)
from Cons(3) obtain f ts where t: "t = Fun f ts" and k: "k < length ts" by (cases t, auto)
note Cons = Cons[unfolded t]
let ?p1 = "p @ i # q1" let ?p2 = "p @ j # q2"
from Cons(2) Cons(3) have "?p1 ∈ poss (ts ! k)" "?p2 ∈ poss (ts ! k)" by auto
from Cons(1)[OF this] have rec: "replace_at (replace_at (ts ! k) ?p1 s1) ?p2 s2 = replace_at (replace_at (ts ! k) ?p2 s2) ?p1 s1" .
from k have min: "min (length ts) k = k" by simp
show ?case unfolding t using rec min k
by (simp add: nth_append)
next
case Nil
from Nil(2) obtain f ts where t: "t = Fun f ts" and j: "j < length ts" by (cases t, auto)
note Nil = Nil[unfolded t]
from Nil have i: "i < length ts" by auto
let ?p1 = "i # q1"
let ?p2 = "j # q2"
let ?s1 = "replace_at (ts ! i) q1 s1"
let ?s2 = "replace_at (ts ! j) q2 s2"
let ?ts1 = "ts[i := ?s1]"
let ?ts2 = "ts[j := ?s2]"
from j have j': "j < length ?ts1" by simp
from i have i': "i < length ?ts2" by simp
have "replace_at (replace_at t ?p1 s1) ?p2 s2 = replace_at (Fun f ?ts1) ?p2 s2"
unfolding t upd_conv_take_nth_drop[OF i] by simp
also have "... = Fun f (?ts1[j := ?s2])"
unfolding upd_conv_take_nth_drop[OF j'] using ij by simp
also have "... = Fun f (?ts2[i := ?s1])" using list_update_swap[OF ij]
by simp
also have "... = replace_at (Fun f ?ts2) ?p1 s1"
unfolding upd_conv_take_nth_drop[OF i'] using ij by simp
also have "... = replace_at (replace_at t ?p2 s2) ?p1 s1" unfolding t
upd_conv_take_nth_drop[OF j] by simp
finally show ?case by simp
qed
qed
lemma parallel_replace_at_subt_at:
fixes p1 :: pos
assumes parallel: "p1 ⊥ p2"
and p1: "p1 ∈ poss t"
and p2: "p2 ∈ poss t"
shows " (replace_at t p1 s1) |_ p2 = t |_ p2"
proof -
from parallel_remove_prefix[OF parallel]
obtain p i j q1 q2 where p1_id: "p1 = p @ i # q1" and p2_id: "p2 = p @ j # q2"
and ij: "i ≠ j" by blast
from p1 p2 show ?thesis unfolding p1_id p2_id
proof (induct p arbitrary: t)
case (Cons k p)
from Cons(3) obtain f ts where t: "t = Fun f ts" and k: "k < length ts" by (cases t, auto)
note Cons = Cons[unfolded t]
let ?p1 = "p @ i # q1" let ?p2 = "p @ j # q2"
from Cons(2) Cons(3) have "?p1 ∈ poss (ts ! k)" "?p2 ∈ poss (ts ! k)" by auto
from Cons(1)[OF this] have rec: "(replace_at (ts ! k) ?p1 s1) |_ ?p2 = (ts ! k) |_ ?p2" .
from k have min: "min (length ts) k = k" by simp
show ?case unfolding t using rec min k
by (simp add: nth_append)
next
case Nil
from Nil(2) obtain f ts where t: "t = Fun f ts" and j: "j < length ts" by (cases t, auto)
note Nil = Nil[unfolded t]
from Nil have i: "i < length ts" by auto
let ?p1 = "i # q1"
let ?p2 = "j # q2"
let ?s1 = "replace_at (ts ! i) q1 s1"
let ?ts1 = "ts[i := ?s1]"
from j have j': "j < length ?ts1" by simp
have "(replace_at t ?p1 s1) |_ ?p2 = (Fun f ?ts1) |_ ?p2" unfolding t upd_conv_take_nth_drop[OF i] by simp
also have "... = ts ! j |_ q2" using ij by simp
finally show ?case unfolding t by simp
qed
qed
lemma parallel_poss_replace_at:
fixes p1 :: pos
assumes parallel: "p1 ⊥ p2"
and p1: "p1 ∈ poss t"
shows "(p2 ∈ poss (replace_at t p1 s1)) = (p2 ∈ poss t)"
proof -
from parallel_remove_prefix[OF parallel]
obtain p i j q1 q2 where p1_id: "p1 = p @ i # q1" and p2_id: "p2 = p @ j # q2"
and ij: "i ≠ j" by blast
from p1 show ?thesis unfolding p1_id p2_id
proof (induct p arbitrary: t)
case (Cons k p)
from Cons(2) obtain f ts where t: "t = Fun f ts" and k: "k < length ts" by (cases t, auto)
note Cons = Cons[unfolded t]
let ?p1 = "p @ i # q1" let ?p2 = "p @ j # q2"
from Cons(2) have "?p1 ∈ poss (ts ! k)" by auto
from Cons(1)[OF this] have rec: "(?p2 ∈ poss (replace_at (ts ! k) ?p1 s1)) = (?p2 ∈ poss (ts ! k))" .
from k have min: "min (length ts) k = k" by simp
show ?case unfolding t using rec min k
by (auto simp: nth_append)
next
case Nil
then obtain f ts where t: "t = Fun f ts" and i: "i < length ts" by (cases t, auto)
let ?p1 = "i # q1"
let ?s1 = "replace_at (ts ! i) q1 s1"
have "replace_at t ?p1 s1 = Fun f (ts[i := ?s1])" unfolding t upd_conv_take_nth_drop[OF i] by simp
then show ?case unfolding t using ij by auto
qed
qed
lemma replace_at_subt_at: "p ∈ poss t ⟹ (replace_at t p s) |_ p = s"
by (metis hole_pos_ctxt_of_pos_term subt_at_hole_pos)
lemma replace_at_below_poss:
assumes p: "p' ∈ poss t" and le: "p ≤⇩p p'"
shows "p ∈ poss (replace_at t p' s)"
proof -
from le obtain p'' where p'': "p' = p @ p''" unfolding less_eq_pos_def by auto
from p show ?thesis unfolding p''
by (metis hole_pos_ctxt_of_pos_term hole_pos_poss poss_append_poss)
qed
lemma ctxt_of_pos_term_replace_at_below:
assumes p: "p ∈ poss t" and le: "p ≤⇩p p'"
shows "ctxt_of_pos_term p (replace_at t p' u) = ctxt_of_pos_term p t"
proof -
from le obtain p'' where p': "p' = p @ p''" unfolding less_eq_pos_def by auto
from p show ?thesis unfolding p'
proof (induct p arbitrary: t)
case (Cons i p)
from Cons(2) obtain f ts where t: "t = Fun f ts" and i: "i < length ts" and p: "p ∈ poss (ts ! i)"
by (cases t, auto)
from i have min: "min (length ts) i = i" by simp
show ?case unfolding t using Cons(1)[OF p] i by (auto simp: nth_append min)
next
case Nil show ?case by simp
qed
qed
lemma ctxt_of_pos_term_hole_pos[simp]:
"ctxt_of_pos_term (hole_pos C) (C⟨t⟩) = C"
by (induct C) simp_all
lemma ctxt_poss_imp_ctxt_subst_poss:
assumes p:"p' ∈ poss C⟨t⟩" shows "p' ∈ poss C⟨t ⋅ μ⟩"
proof(rule disjE[OF pos_cases[of p' "hole_pos C"]])
assume "p' ≤⇩p hole_pos C"
then show ?thesis using hole_pos_poss by (metis less_eq_pos_def poss_append_poss)
next
assume or:"hole_pos C <⇩p p' ∨ p' ⊥ hole_pos C"
show ?thesis proof(rule disjE[OF or])
assume "hole_pos C <⇩p p'"
then obtain q where dec:"p' = hole_pos C @ q" unfolding less_pos_def less_eq_pos_def by auto
with p have "q ∈ poss (t ⋅ μ)" using hole_pos_poss_conv poss_imp_subst_poss by auto
then show ?thesis using dec hole_pos_poss_conv by auto
next
assume "p' ⊥ hole_pos C"
then have par:"hole_pos C ⊥ p'" by (rule parallel_pos_sym)
have aux:"hole_pos C ∈ poss C⟨t ⋅ μ⟩" using hole_pos_poss by auto
from p show ?thesis using parallel_poss_replace_at[OF par aux,unfolded ctxt_of_pos_term_hole_pos] by fast
qed
qed
lemma var_pos_maximal:
assumes pt:"p ∈ poss t" and x:"t |_ p = Var x" and "q ≠ []"
shows "p @ q ∉ poss t"
proof-
from assms have "q ∉ poss (Var x)" by force
with poss_append_poss[of p q] pt x show ?thesis by simp
qed
text ‹Positions in a context›
definition possc :: "('f, 'v) ctxt ⇒ pos set" where "possc C ≡ {p | p. ∀t. p ∈ poss C⟨t⟩}"
lemma poss_imp_possc: "p ∈ possc C ⟹ p ∈ poss C⟨t⟩" unfolding possc_def by auto
lemma less_eq_hole_pos_in_possc:
assumes pleq:"p ≤⇩p hole_pos C" shows "p ∈ possc C"
unfolding possc_def
using replace_at_below_poss[OF hole_pos_poss pleq, unfolded hole_pos_id_ctxt[OF refl]] by simp
lemma hole_pos_in_possc:"hole_pos C ∈ possc C"
using less_eq_hole_pos_in_possc order_refl by blast
lemma par_hole_pos_in_possc:
assumes par:"hole_pos C ⊥ p" and ex:"p ∈ poss C⟨t⟩" shows "p ∈ possc C"
using parallel_poss_replace_at[OF par hole_pos_poss, unfolded hole_pos_id_ctxt[OF refl], of t] ex
unfolding possc_def by simp
lemma possc_not_below_hole_pos:
assumes "p ∈ possc (C::('a,'b) ctxt)" shows "¬ (hole_pos C <⇩p p)"
proof(rule notI)
assume "hole_pos C <⇩p p"
then obtain r where p':"p = hole_pos C @ r" and r:"r ≠ []"
unfolding less_pos_def less_eq_pos_def by auto
fix x::'b from r have n:"r ∉ poss (Var x)" using poss.simps(1) by auto
from assms have "p ∈ (poss C⟨Var x⟩)" unfolding possc_def by auto
with this[unfolded p'] hole_pos_poss_conv[of C r] have "r ∈ poss (Var x)" by auto
with n show False by simp
qed
lemma possc_subst_not_possc_not_poss:
assumes y:"p ∈ possc (C ⋅⇩c σ)" and n:"p ∉ possc C" shows "p ∉ poss C⟨t⟩"
proof-
from n obtain u where a:"p ∉ poss C⟨u⟩" unfolding possc_def by auto
from possc_not_below_hole_pos[OF y] have b:"¬ (hole_pos C <⇩p p)"
unfolding hole_pos_subst[of C σ] by auto
from n a have c:"¬ (p ≤⇩p hole_pos C)" unfolding less_pos_def using less_eq_hole_pos_in_possc by blast
with pos_cases b have "p ⊥ hole_pos C" by blast
with par_hole_pos_in_possc[OF parallel_pos_sym[OF this]] n show "p ∉ poss (C⟨t⟩)" by fast
qed
text ‹All proper terms in a context›
fun ctxt_to_term_list :: "('f, 'v) ctxt ⇒ ('f, 'v) term list"
where
"ctxt_to_term_list Hole = []" |
"ctxt_to_term_list (More f bef C aft) = ctxt_to_term_list C @ bef @ aft"
lemma ctxt_to_term_list_supt: "t ∈ set (ctxt_to_term_list C) ⟹ C⟨s⟩ ⊳ t"
proof (induct C)
case (More f bef C aft)
from More(2) have choice: "t ∈ set (ctxt_to_term_list C) ∨ t ∈ set bef ∨ t ∈ set aft" by simp
{
assume "t ∈ set bef ∨ t ∈ set aft"
then have "t ∈ set (bef @ C⟨s⟩ # aft)" by auto
then have ?case by auto
}
moreover
{
assume t: "t ∈ set (ctxt_to_term_list C)"
have "(More f bef C aft)⟨s⟩ ⊳ C⟨s⟩" by auto
moreover have "C⟨s⟩ ⊳ t"
by (rule More(1)[OF t])
ultimately have ?case
by (rule supt_trans)
}
ultimately show ?case using choice by auto
qed auto
lemma subteq_Var_imp_in_vars_term:
"r ⊵ Var x ⟹ x ∈ vars_term r"
proof (induct r rule: term.induct)
case (Var y)
then have "x = y" by (cases rule: supteq.cases) auto
then show ?case by simp
next
case (Fun f ss)
from ‹Fun f ss ⊵ Var x› have "(Fun f ss = Var x) ∨ (Fun f ss ⊳ Var x)" by auto
then show ?case
proof
assume "Fun f ss = Var x" then show ?thesis by auto
next
assume "Fun f ss ⊳ Var x"
then obtain s where "s ∈ set ss" and "s ⊵ Var x" using supt_Fun_imp_arg_supteq by best
with Fun have "s ⊵ Var x ⟹ x ∈ vars_term s" by best
with ‹s ⊵ Var x› have "x ∈ vars_term s" by simp
with ‹s ∈ set ss› show ?thesis by auto
qed
qed
fun instance_term :: "('f, 'v) term ⇒ ('f set, 'v) term ⇒ bool"
where
"instance_term (Var x) (Var y) ⟷ x = y" |
"instance_term (Fun f ts) (Fun fs ss) ⟷
f ∈ fs ∧ length ts = length ss ∧ (∀i<length ts. instance_term (ts ! i) (ss ! i))" |
"instance_term _ _ = False"
fun subt_at_ctxt :: "('f, 'v) ctxt ⇒ pos ⇒ ('f, 'v) ctxt" (infixl "|'_c" 67)
where
"C |_c [] = C" |
"More f bef C aft |_c (i#p) = C |_c p"
lemma subt_at_subt_at_ctxt:
assumes "hole_pos C = p @ q"
shows "C⟨t⟩ |_ p = (C |_c p)⟨t⟩"
using assms
proof (induct p arbitrary: C)
case (Cons i p)
then obtain f bef D aft where C: "C = More f bef D aft" by (cases C, auto)
from Cons(2) have "hole_pos D = p @ q" unfolding C by simp
from Cons(1)[OF this] have id: "(D |_c p) ⟨t⟩ = D⟨t⟩ |_ p" by simp
show ?case unfolding C subt_at_ctxt.simps id using Cons(2) C by auto
qed simp
lemma hole_pos_subt_at_ctxt:
assumes "hole_pos C = p @ q"
shows "hole_pos (C |_c p) = q"
using assms
proof (induct p arbitrary: C)
case (Cons i p)
then obtain f bef D aft where C: "C = More f bef D aft" by (cases C, auto)
show ?case unfolding C subt_at_ctxt.simps
by (rule Cons(1), insert Cons(2) C, auto)
qed simp
lemma subt_at_ctxt_compose[simp]: "(C ∘⇩c D) |_c hole_pos C = D"
by (induct C, auto)
lemma split_ctxt:
assumes "hole_pos C = p @ q"
shows "∃ D E. C = D ∘⇩c E ∧ hole_pos D = p ∧ hole_pos E = q ∧ E = C |_c p"
using assms
proof (induct p arbitrary: C)
case Nil
show ?case
by (rule exI[of _ □], rule exI[of _ C], insert Nil, auto)
next
case (Cons i p)
then obtain f bef C' aft where C: "C = More f bef C' aft" by (cases C, auto)
from Cons(2) have "hole_pos C' = p @ q" unfolding C by simp
from Cons(1)[OF this] obtain D E where C': "C' = D ∘⇩c E"
and p: "hole_pos D = p" and q: "hole_pos E = q" and E: "E = C' |_c p"
by auto
show ?case
by (rule exI[of _ "More f bef D aft"], rule exI[of _ E], unfold C C',
insert p[symmetric] q E Cons(2) C, simp)
qed
lemma ctxt_subst_id[simp]: "C ⋅⇩c Var = C" by (induct C, auto)
text ‹the strict subterm relation between contexts and terms›
inductive_set
suptc :: "(('f, 'v) ctxt × ('f, 'v) term) set"
where
arg: "s ∈ set bef ∪ set aft ⟹ s ⊵ t ⟹ (More f bef C aft, t) ∈ suptc"
| ctxt: "(C,s) ∈ suptc ⟹ (D ∘⇩c C, s) ∈ suptc"
hide_const suptcp
abbreviation suptc_pred where "suptc_pred C t ≡ (C, t) ∈ suptc"
notation (xsymbols)
suptc_pred ("(_/ ⊳c _)" [56, 56] 55)
lemma suptc_subst: "C ⊳c s ⟹ C ⋅⇩c σ ⊳c s ⋅ σ"
proof (induct rule: suptc.induct)
case (arg s bef aft t f C)
let ?s = "λ t. t ⋅ σ"
let ?m = "map ?s"
have id: "More f bef C aft ⋅⇩c σ = More f (?m bef) (C ⋅⇩c σ) (?m aft)" by simp
show ?case unfolding id
by (rule suptc.arg[OF _ supteq_subst[OF arg(2)]],
insert arg(1), auto)
next
case (ctxt C s D)
have id: "D ∘⇩c C ⋅⇩c σ = (D ⋅⇩c σ) ∘⇩c (C ⋅⇩c σ)" by simp
show ?case unfolding id
by (rule suptc.ctxt[OF ctxt(2)])
qed
lemma suptc_imp_supt: "C ⊳c s ⟹ C⟨t⟩ ⊳ s"
proof (induct rule: suptc.induct)
case (arg s bef aft u f C)
let ?C = "(More f bef C aft)"
from arg(1) have "s ∈ set (args (?C⟨t⟩))" by auto
then have "?C⟨t⟩ ⊳ s" by auto
from supt_supteq_trans[OF this arg(2)]
show ?case .
next
case (ctxt C s D)
have supteq: "(D ∘⇩c C)⟨t⟩ ⊵ C⟨t⟩" by auto
from supteq_supt_trans[OF this ctxt(2)]
show ?case .
qed
lemma suptc_supteq_trans: "C ⊳c s ⟹ s ⊵ t ⟹ C ⊳c t"
proof (induct rule: suptc.induct)
case (arg s bef aft u f C)
show ?case
by (rule suptc.arg[OF arg(1) supteq_trans[OF arg(2) arg(3)]])
next
case (ctxt C s D)
then have supt: "C ⊳c t" by auto
then show ?case by (rule suptc.ctxt)
qed
lemma supteq_suptc_trans: "C = D ∘⇩c E ⟹ E ⊳c s ⟹ C ⊳c s"
by (auto intro: suptc.ctxt)
hide_fact (open)
suptcp.arg suptcp.cases suptcp.induct suptcp.intros suptc.arg suptc.ctxt
lemma supteq_ctxt_cases': "C ⟨ t ⟩ ⊵ u ⟹
C ⊳c u ∨ t ⊵ u ∨ (∃ D C'. C = D ∘⇩c C' ∧ u = C' ⟨ t ⟩ ∧ C' ≠ □)"
proof (induct C)
case (More f bef C aft)
let ?C = "More f bef C aft"
let ?ba = "bef @ C ⟨ t ⟩ # aft"
from More(2) have "Fun f ?ba ⊵ u" by simp
then show ?case
proof (cases rule: supteq.cases)
case refl
show ?thesis unfolding refl
by (intro disjI2, rule exI[of _ Hole], rule exI[of _ ?C], auto)
next
case (subt v)
show ?thesis
proof (cases "v ∈ set bef ∪ set aft")
case True
from suptc.arg[OF this subt(2)]
show ?thesis by simp
next
case False
with subt have "C⟨ t ⟩ ⊵ u" by simp
from More(1)[OF this]
show ?thesis
proof (elim disjE exE conjE)
assume "C ⊳c u"
from suptc.ctxt[OF this, of "More f bef □ aft"] show ?thesis by simp
next
fix D C'
assume *: "C = D ∘⇩c C'" "u = C'⟨t⟩" "C' ≠ □"
show ?thesis
by (intro disjI2 conjI, rule exI[of _ "More f bef D aft"], rule exI[of _ C'],
insert *, auto)
qed simp
qed
qed
qed simp
lemma supteq_ctxt_cases[consumes 1, case_names in_ctxt in_term sub_ctxt]: "C ⟨ t ⟩ ⊵ u ⟹
(C ⊳c u ⟹ P) ⟹
(t ⊵ u ⟹ P) ⟹
(⋀ D C'. C = D ∘⇩c C' ⟹ u = C' ⟨ t ⟩ ⟹ C' ≠ □ ⟹ P) ⟹ P"
using supteq_ctxt_cases' by blast
definition vars_subst :: "('f, 'v) subst ⇒ 'v set"
where
"vars_subst σ = subst_domain σ ∪ ⋃(vars_term ` subst_range σ)"
lemma range_vars_subst_compose_subset:
"range_vars (σ ∘⇩s τ) ⊆ (range_vars σ - subst_domain τ) ∪ range_vars τ" (is "?L ⊆ ?R")
proof
fix x
assume "x ∈ ?L"
then obtain y where "y ∈ subst_domain (σ ∘⇩s τ)"
and "x ∈ vars_term ((σ ∘⇩s τ) y)" by (auto simp: range_vars_def)
then show "x ∈ ?R"
proof (cases)
assume "y ∈ subst_domain σ" and "x ∈ vars_term ((σ ∘⇩s τ) y)"
moreover then obtain v where "v ∈ vars_term (σ y)"
and "x ∈ vars_term (τ v)" by (auto simp: subst_compose_def vars_term_subst)
ultimately show ?thesis
by (cases "v ∈ subst_domain τ") (auto simp: range_vars_def subst_domain_def)
qed (auto simp: range_vars_def subst_compose_def subst_domain_def)
qed
text ‹
A substitution is idempotent iff the variables in its range are disjoint from its domain. See also
"Term Rewriting and All That" Lemma 4.5.7.
›
lemma subst_idemp_iff:
"σ ∘⇩s σ = σ ⟷ subst_domain σ ∩ range_vars σ = {}"
proof
assume "σ ∘⇩s σ = σ"
then have "⋀x. σ x ⋅ σ = σ x ⋅ Var" by simp (metis subst_compose_def)
then have *: "⋀x. ∀y∈vars_term (σ x). σ y = Var y"
unfolding term_subst_eq_conv by simp
{ fix x y
assume "σ x ≠ Var x" and "x ∈ vars_term (σ y)"
with * [of y] have False by simp }
then show "subst_domain σ ∩ range_vars σ = {}"
by (auto simp: subst_domain_def range_vars_def)
next
assume "subst_domain σ ∩ range_vars σ = {}"
then have *: "⋀x y. σ x = Var x ∨ σ y = Var y ∨ x ∉ vars_term (σ y)"
by (auto simp: subst_domain_def range_vars_def)
have "⋀x. ∀y∈vars_term (σ x). σ y = Var y"
proof
fix x y
assume "y ∈ vars_term (σ x)"
with * [of y x] show "σ y = Var y" by auto
qed
then show "σ ∘⇩s σ = σ"
by (simp add: subst_compose_def term_subst_eq_conv [symmetric])
qed
definition subst_compose' :: "('f, 'v) subst ⇒ ('f, 'v) subst ⇒ ('f, 'v) subst" where
"subst_compose' σ τ = (λ x. if (x ∈ subst_domain σ) then σ x ⋅ τ else Var x)"
lemma vars_subst_compose':
assumes "vars_subst τ ∩ subst_domain σ = {}"
shows "σ ∘⇩s τ = τ ∘⇩s (subst_compose' σ τ)" (is "?l = ?r")
proof
fix x
show "?l x = ?r x"
proof (cases "x ∈ subst_domain σ")
case True
with assms have nmem: "x ∉ vars_subst τ" by auto
then have nmem: "x ∉ subst_domain τ" unfolding vars_subst_def by auto
then have id: "τ x = Var x" unfolding subst_domain_def by auto
have "?l x = σ x ⋅ τ" unfolding subst_compose_def by simp
also have "... = ?r x" unfolding subst_compose'_def subst_compose_def using True unfolding id by simp
finally show ?thesis .
next
case False
then have l: "?l x = τ x ⋅ Var" unfolding subst_domain_def subst_compose_def by auto
let ?στ = "(λ x. if x ∈ subst_domain σ then σ x ⋅ τ else Var x)"
have r: "?r x = τ x ⋅ ?στ"
unfolding subst_compose'_def subst_compose_def ..
show "?l x = ?r x" unfolding l r
proof (rule term_subst_eq)
fix y
assume y: "y ∈ vars_term (τ x)"
have "y ∈ vars_subst τ ∨ τ x = Var x"
proof (cases "x ∈ subst_domain τ")
case True then show ?thesis using y unfolding vars_subst_def by auto
next
case False
then show ?thesis unfolding subst_domain_def by auto
qed
then show "Var y = ?στ y"
proof
assume "y ∈ vars_subst τ"
with assms have "y ∉ subst_domain σ" by auto
then show ?thesis by simp
next
assume "τ x = Var x"
with y have y: "y = x" by simp
show ?thesis unfolding y using False by auto
qed
qed
qed
qed
lemma vars_subst_compose'_pow:
assumes "vars_subst τ ∩ subst_domain σ = {}"
shows "σ ^^ n ∘⇩s τ = τ ∘⇩s (subst_compose' σ τ) ^^ n"
proof (induct n)
case 0 then show ?case by auto
next
case (Suc n)
let ?στ = "subst_compose' σ τ"
have "σ ^^ Suc n ∘⇩s τ = σ ∘⇩s (σ ^^ n ∘⇩s τ)" by (simp add: ac_simps)
also have "... = σ ∘⇩s (τ ∘⇩s ?στ^^n)" unfolding Suc ..
also have "... = (σ ∘⇩s τ) ∘⇩s ?στ ^^ n" by (auto simp: ac_simps)
also have "... = (τ ∘⇩s ?στ) ∘⇩s ?στ ^^ n" unfolding vars_subst_compose'[OF assms] ..
finally show ?case by (simp add: ac_simps)
qed
lemma subst_pow_commute:
assumes "σ ∘⇩s τ = τ ∘⇩s σ"
shows "σ ∘⇩s (τ ^^ n) = τ ^^ n ∘⇩s σ"
proof (induct n)
case (Suc n)
have "σ ∘⇩s τ ^^ Suc n = (σ ∘⇩s τ) ∘⇩s τ ^^ n" by (simp add: ac_simps)
also have "... = τ ∘⇩s (σ ∘⇩s τ ^^ n)" unfolding assms by (simp add: ac_simps)
also have "... = τ ^^ Suc n ∘⇩s σ" unfolding Suc by (simp add: ac_simps)
finally show ?case .
qed simp
lemma subst_power_commute:
assumes "σ ∘⇩s τ = τ ∘⇩s σ"
shows "(σ ^^ n) ∘⇩s (τ ^^ n) = (σ ∘⇩s τ)^^n"
proof (induct n)
case (Suc n)
have "(σ ^^ Suc n) ∘⇩s (τ ^^ Suc n) = (σ^^n ∘⇩s (σ ∘⇩s τ ^^ n) ∘⇩s τ)"
unfolding subst_power_Suc by (simp add: ac_simps)
also have "... = (σ^^n ∘⇩s τ ^^ n) ∘⇩s (σ ∘⇩s τ)"
unfolding subst_pow_commute[OF assms] by (simp add: ac_simps)
also have "... = (σ ∘⇩s τ)^^Suc n" unfolding Suc
unfolding subst_power_Suc ..
finally show ?case .
qed simp
lemma vars_term_ctxt_apply:
"vars_term (C⟨t⟩) = vars_ctxt C ∪ vars_term t"
by (induct C) (auto)
lemma vars_ctxt_pos_term:
assumes "p ∈ poss t"
shows "vars_term t = vars_ctxt (ctxt_of_pos_term p t) ∪ vars_term (t |_ p)"
proof -
let ?C = "ctxt_of_pos_term p t"
have "t = ?C⟨t |_ p⟩" using ctxt_supt_id [OF assms] by simp
then have "vars_term t = vars_term (?C⟨t |_ p⟩)" by simp
then show ?thesis unfolding vars_term_ctxt_apply .
qed
lemma vars_term_subt_at:
assumes "p ∈ poss t"
shows "vars_term (t |_ p) ⊆ vars_term t"
using vars_ctxt_pos_term [OF assms] by simp
lemma Var_pow_Var[simp]: "Var ^^ n = Var"
by (rule, induct n, auto)
definition is_inverse_renaming :: "('f, 'v) subst ⇒ ('f, 'v) subst" where
"is_inverse_renaming σ y = (
if Var y ∈ subst_range σ then Var (the_inv_into (subst_domain σ) σ (Var y))
else Var y)"
lemma is_renaming_inverse_domain:
assumes ren: "is_renaming σ"
and x: "x ∈ subst_domain σ"
shows "Var x ⋅ σ ⋅ is_inverse_renaming σ = Var x" (is "_ ⋅ ?σ = _")
proof -
note ren = ren[unfolded is_renaming_def]
from ren obtain y where σx: "σ x = Var y" by force
from ren have inj: "inj_on σ (subst_domain σ)" by auto
note inj = the_inv_into_f_eq[OF inj, OF σx]
note d = is_inverse_renaming_def
from x have "Var y ∈ subst_range σ" using σx by force
then have "?σ y = Var (the_inv_into (subst_domain σ) σ (Var y))" unfolding d by simp
also have "... = Var x" using inj[OF x] by simp
finally show ?thesis using σx by simp
qed
lemma is_renaming_inverse_range:
assumes varren: "is_renaming σ"
and x: "Var x ∉ subst_range σ"
shows "Var x ⋅ σ ⋅ is_inverse_renaming σ = Var x" (is "_ ⋅ ?σ = _")
proof (cases "x ∈ subst_domain σ")
case True
from is_renaming_inverse_domain[OF varren True]
show ?thesis .
next
case False
then have σx: "σ x = Var x" unfolding subst_domain_def by auto
note ren = varren[unfolded is_renaming_def]
note d = is_inverse_renaming_def
have "Var x ⋅ σ ⋅ ?σ = ?σ x" using σx by auto
also have "... = Var x"
unfolding d using x by simp
finally show ?thesis .
qed
lemma vars_subst_compose:
"vars_subst (σ ∘⇩s τ) ⊆ vars_subst σ ∪ vars_subst τ"
proof
fix x
assume "x ∈ vars_subst (σ ∘⇩s τ)"
from this[unfolded vars_subst_def subst_range.simps]
obtain y where "y ∈ subst_domain (σ ∘⇩s τ) ∧ (x = y ∨ x ∈ vars_term ((σ ∘⇩s τ) y))" by blast
with subst_domain_compose[of σ τ] have y: "y ∈ subst_domain σ ∪ subst_domain τ" and disj:
"x = y ∨ (x ≠ y ∧ x ∈ vars_term (σ y ⋅ τ))" unfolding subst_compose_def by auto
from disj
show "x ∈ vars_subst σ ∪ vars_subst τ"
proof
assume "x = y"
with y show ?thesis unfolding vars_subst_def by auto
next
assume "x ≠ y ∧ x ∈ vars_term (σ y ⋅ τ)"
then obtain z where neq: "x ≠ y" and x: "x ∈ vars_term (τ z)" and z: "z ∈ vars_term (σ y)" unfolding vars_term_subst by auto
show ?thesis
proof (cases "τ z = Var z")
case False
with x have "x ∈ vars_subst τ" unfolding vars_subst_def subst_domain_def subst_range.simps by blast
then show ?thesis by auto
next
case True
with x have x: "z = x" by auto
with z have y: "x ∈ vars_term (σ y)" by auto
show ?thesis
proof (cases "σ y = Var y")
case False
with y have "x ∈ vars_subst σ" unfolding vars_subst_def subst_domain_def subst_range.simps by blast
then show ?thesis by auto
next
case True
with y have "x = y" by auto
with neq show ?thesis by auto
qed
qed
qed
qed
lemma vars_subst_compose_update:
assumes x: "x ∉ vars_subst σ"
shows "σ ∘⇩s τ(x := t) = (σ ∘⇩s τ)(x := t)" (is "?l = ?r")
proof
fix z
note x = x[unfolded vars_subst_def subst_domain_def]
from x have xx: "σ x = Var x" by auto
show "?l z = ?r z"
proof (cases "z = x")
case True
with xx show ?thesis by (simp add: subst_compose_def)
next
case False
then have "?r z = σ z ⋅ τ" unfolding subst_compose_def by auto
also have "... = ?l z" unfolding subst_compose_def
proof (rule term_subst_eq)
fix y
assume "y ∈ vars_term (σ z)"
with False x have v: "y ≠ x" unfolding subst_range.simps subst_domain_def by force
then show "τ y = (τ(x := t)) y" by simp
qed
finally show ?thesis by simp
qed
qed
lemma subst_variants_imp_eq:
assumes "σ ∘⇩s σ' = τ" and "τ ∘⇩s τ' = σ"
shows "⋀x. σ x ⋅ σ' = τ x" "⋀x. τ x ⋅ τ' = σ x"
using assms by (metis subst_compose_def)+
lemma poss_subst_choice: assumes "p ∈ poss (t ⋅ σ)" shows
"p ∈ poss t ∧ is_Fun (t |_ p) ∨
(∃ x q1 q2. q1 ∈ poss t ∧ q2 ∈ poss (σ x) ∧ t |_ q1 = Var x ∧ x ∈ vars_term t
∧ p = q1 @ q2 ∧ t ⋅ σ |_ p = σ x |_ q2)" (is "_ ∨ (∃ x q1 q2. ?p x q1 q2 t p)")
using assms
proof (induct p arbitrary: t)
case (Cons i p t)
show ?case
proof (cases t)
case (Var x)
have "?p x [] (i # p) t (i # p)" using Cons(2) unfolding Var by simp
then show ?thesis by blast
next
case (Fun f ts)
with Cons(2) have i: "i < length ts" and p: "p ∈ poss (ts ! i ⋅ σ)" by auto
from Cons(1)[OF p]
show ?thesis
proof
assume "∃ x q1 q2. ?p x q1 q2 (ts ! i) p"
then obtain x q1 q2 where "?p x q1 q2 (ts ! i) p" by auto
with Fun i have "?p x (i # q1) q2 (Fun f ts) (i # p)" by auto
then show ?thesis unfolding Fun by blast
next
assume "p ∈ poss (ts ! i) ∧ is_Fun (ts ! i |_ p)"
then show ?thesis using Fun i by auto
qed
qed
next
case Nil
show ?case
proof (cases t)
case (Var x)
have "?p x [] [] t []" unfolding Var by auto
then show ?thesis by auto
qed simp
qed
fun vars_term_list :: "('f, 'v) term ⇒ 'v list"
where
"vars_term_list (Var x) = [x]" |
"vars_term_list (Fun _ ts) = concat (map vars_term_list ts)"
lemma set_vars_term_list [simp]:
"set (vars_term_list t) = vars_term t"
by (induct t) simp_all
lemma unary_vars_term_list:
assumes t: "funas_term t ⊆ F"
and unary: "⋀ f n. (f, n) ∈ F ⟹ n ≤ 1"
shows "vars_term_list t = [] ∨ (∃ x ∈ vars_term t. vars_term_list t = [x])"
proof -
from t show ?thesis
proof (induct t)
case Var then show ?case by auto
next
case (Fun f ss)
show ?case
proof (cases ss)
case Nil
then show ?thesis by auto
next
case (Cons t ts)
let ?n = "length ss"
from Fun(2) have "(f,?n) ∈ F" by auto
from unary[OF this] have n: "?n ≤ Suc 0" by auto
with Cons have "?n = Suc 0" by simp
with Cons have ss: "ss = [t]" by (cases ts, auto)
note IH = Fun(1)[unfolded ss, simplified]
from ss have id1: "vars_term_list (Fun f ss) = vars_term_list t" by simp
from ss have id2: "vars_term (Fun f ss) = vars_term t" by simp
from Fun(2) ss have mem: "funas_term t ⊆ F" by auto
show ?thesis unfolding id1 id2 using IH[OF refl mem] by simp
qed
qed
qed
declare vars_term_list.simps [simp del]
text ‹The list of function symbols in a term (without removing duplicates).›
fun funs_term_list :: "('f, 'v) term ⇒ 'f list"
where
"funs_term_list (Var _) = []" |
"funs_term_list (Fun f ts) = f # concat (map funs_term_list ts)"
lemma set_funs_term_list [simp]:
"set (funs_term_list t) = funs_term t"
by (induct t) simp_all
declare funs_term_list.simps [simp del]
text ‹The list of function symbol and arity pairs in a term
(without removing duplicates).›
fun funas_term_list :: "('f, 'v) term ⇒ ('f × nat) list"
where
"funas_term_list (Var _) = []" |
"funas_term_list (Fun f ts) = (f, length ts) # concat (map funas_term_list ts)"
lemma set_funas_term_list [simp]:
"set (funas_term_list t) = funas_term t"
by (induct t) simp_all
declare funas_term_list.simps [simp del]
definition funas_args_term_list :: "('f, 'v) term ⇒ ('f × nat) list"
where
"funas_args_term_list t = concat (map funas_term_list (args t))"
lemma set_funas_args_term_list [simp]:
"set (funas_args_term_list t) = funas_args_term t"
by (simp add: funas_args_term_def funas_args_term_list_def)
lemma vars_term_list_map_funs_term:
"vars_term_list (map_funs_term fg t) = vars_term_list t"
proof (induct t)
case (Var x) then show ?case by (simp add: vars_term_list.simps)
next
case (Fun f ss)
show ?case by (simp add: vars_term_list.simps o_def, insert Fun, induct ss, auto)
qed
lemma funs_term_list_map_funs_term:
"funs_term_list (map_funs_term fg t) = map fg (funs_term_list t)"
proof (induct t)
case (Var x) show ?case by (simp add: funs_term_list.simps)
next
case (Fun f ts)
show ?case
by (simp add: funs_term_list.simps, insert Fun, induct ts, auto)
qed
text ‹
Next we provide some functions to compute multisets instead of sets of
function symbols, variables, etc.
they may be helpful for non-duplicating TRSs.
›
fun funs_term_ms :: "('f,'v)term ⇒ 'f multiset"
where
"funs_term_ms (Var x) = {#}" |
"funs_term_ms (Fun f ts) = {#f#} + ∑⇩# (mset (map funs_term_ms ts))"
fun funs_ctxt_ms :: "('f,'v)ctxt ⇒ 'f multiset"
where
"funs_ctxt_ms Hole = {#}" |
"funs_ctxt_ms (More f bef C aft) =
{#f#} + ∑⇩# (mset (map funs_term_ms bef)) +
funs_ctxt_ms C + ∑⇩# (mset (map funs_term_ms aft))"
lemma funs_term_ms_ctxt_apply:
"funs_term_ms C⟨t⟩ = funs_ctxt_ms C + funs_term_ms t"
by (induct C) (auto simp: multiset_eq_iff)
lemma funs_term_ms_subst_apply:
"funs_term_ms (t ⋅ σ) =
funs_term_ms t + ∑⇩# (image_mset (λ x. funs_term_ms (σ x)) (vars_term_ms t))"
proof (induct t)
case (Fun f ts)
let ?m = "mset"
let ?f = "funs_term_ms"
let ?ts = "∑⇩# (?m (map ?f ts))"
let ?σ = "∑⇩# (image_mset (λx. ?f (σ x)) (∑⇩# (?m (map vars_term_ms ts))))"
let ?tsσ = "∑⇩# (?m (map (λ x. ?f (x ⋅ σ)) ts))"
have ind: "?tsσ = ?ts + ?σ" using Fun
by (induct ts, auto simp: multiset_eq_iff)
then show ?case unfolding multiset_eq_iff by (simp add: o_def)
qed auto
lemma ground_vars_term_ms_empty:
"ground t = (vars_term_ms t = {#})"
unfolding ground_vars_term_empty
unfolding set_mset_vars_term_ms [symmetric]
by (simp del: set_mset_vars_term_ms)
lemma vars_term_ms_map_funs_term [simp]:
"vars_term_ms (map_funs_term fg t) = vars_term_ms t"
proof (induct t)
case (Fun f ts)
then show ?case by (induct ts) auto
qed simp
lemma funs_term_ms_map_funs_term:
"funs_term_ms (map_funs_term fg t) = image_mset fg (funs_term_ms t)"
proof (induct t)
case (Fun f ss)
then show ?case by (induct ss, auto)
qed auto
lemma supteq_imp_vars_term_ms_subset:
"s ⊵ t ⟹ vars_term_ms t ⊆# vars_term_ms s"
proof (induct rule: supteq.induct)
case (subt u ss t f)
from subt(1) obtain bef aft where ss: "ss = bef @ u # aft"
by (metis in_set_conv_decomp)
have "vars_term_ms t ⊆# vars_term_ms u" by fact
also have "… ⊆# ∑⇩# (mset (map vars_term_ms ss))"
unfolding ss by (simp add: ac_simps)
also have "… = vars_term_ms (Fun f ss)" by auto
finally show ?case by auto
qed auto
lemma mset_funs_term_list:
"mset (funs_term_list t) = funs_term_ms t"
proof (induct t)
case (Var x) show ?case by (simp add: funs_term_list.simps)
next
case (Fun f ts)
show ?case
by (simp add: funs_term_list.simps, insert Fun, induct ts, auto simp: funs_term_list.simps multiset_eq_iff)
qed
text ‹Creating substitutions from lists›
type_synonym ('f, 'v, 'w) gsubstL = "('v × ('f, 'w) term) list"
type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL"
definition mk_subst :: "('v ⇒ ('f, 'w) term) ⇒ ('f, 'v, 'w) gsubstL ⇒ ('f, 'v, 'w) gsubst" where
"mk_subst d xts ≡
(λx. case map_of xts x of
None ⇒ d x
| Some t ⇒ t)"
lemma mk_subst_not_mem:
assumes x: "x ∉ set xs"
shows "mk_subst f (zip xs ts) x = f x"
proof -
have "map_of (zip xs ts) x = None"
unfolding map_of_eq_None_iff set_zip using x[unfolded set_conv_nth] by auto
then show ?thesis unfolding mk_subst_def by auto
qed
lemma mk_subst_not_mem':
assumes x: "x ∉ set (map fst ss)"
shows "mk_subst f ss x = f x"
proof -
have "map_of ss x = None"
unfolding map_of_eq_None_iff using x by auto
then show ?thesis unfolding mk_subst_def by auto
qed
lemma mk_subst_distinct:
assumes dist: "distinct xs"
and i: "i < length xs" "i < length ls"
shows "mk_subst f (zip xs ls) (xs ! i) = ls ! i"
proof -
from i have in_zip:"(xs!i, ls!i) ∈ set (zip xs ls)"
using nth_zip[OF i] set_zip by auto
from dist have dist':"distinct (map fst (zip xs ls))"
by (simp add: map_fst_zip_take)
then show ?thesis
unfolding mk_subst_def using map_of_is_SomeI[OF dist' in_zip] by simp
qed
lemma mk_subst_Nil [simp]:
"mk_subst d [] = d"
by (simp add: mk_subst_def)
lemma mk_subst_concat:
assumes "x ∉ set (map fst xs)"
shows "(mk_subst f (xs@ys)) x = (mk_subst f ys) x"
using assms unfolding mk_subst_def map_of_append
by (simp add: dom_map_of_conv_image_fst map_add_dom_app_simps(3))
lemma mk_subst_concat_Cons:
assumes "x ∈ set (map fst ss)"
shows "mk_subst f (concat (ss#ss')) x = mk_subst f ss x"
proof-
from assms obtain y where "map_of ss x = Some y"
by (metis list.set_map map_of_eq_None_iff not_None_eq)
then show ?thesis unfolding mk_subst_def concat.simps map_of_append
by simp
qed
lemma vars_term_var_poss_iff:
"x ∈ vars_term t ⟷ (∃p. p ∈ var_poss t ∧ Var x = t |_ p)" (is "?L ⟷ ?R")
proof
assume x: "?L"
obtain p where "p ∈ poss t" and "Var x = t |_ p"
using supteq_imp_subt_at [OF supteq_Var [OF x]] by force
then show "?R" using var_poss_iff by auto
next
assume p: "?R"
then obtain p where 1: "p ∈ var_poss t" and 2: "Var x = t |_ p" by auto
from var_poss_imp_poss [OF 1] have "p ∈ poss t" .
then show "?L" by (simp add: 2 subt_at_imp_supteq subteq_Var_imp_in_vars_term)
qed
lemma vars_term_poss_subt_at:
assumes "x ∈ vars_term t"
obtains q where "q ∈ poss t" and "t |_ q = Var x"
using assms
proof (induct t)
case (Fun f ts)
then obtain t where t:"t ∈ set ts" and x:"x ∈ vars_term t" by auto
moreover then obtain i where "t = ts ! i" and "i < length ts" using in_set_conv_nth by metis
ultimately show ?case using Fun(1)[OF t _ x] Fun(2)[of "Cons i q" for q] by auto
qed auto
lemma vars_ctxt_subt_at':
assumes "x ∈ vars_ctxt C"
and "p ∈ poss C⟨t⟩"
and "hole_pos C = p"
shows "∃q. q ∈ poss C⟨t⟩ ∧ parallel_pos p q ∧ C⟨t⟩ |_ q = Var x"
using assms
proof (induct C arbitrary: p)
case (More f bef C aft)
then have [simp]: "p = length bef # hole_pos C" by auto
consider
(C) "x ∈ vars_ctxt C" |
(bef) t where "t ∈ set bef" and "x ∈ vars_term t" |
(aft) t where "t ∈ set aft" and "x ∈ vars_term t"
using More by auto
then show ?case
proof (cases)
case C
from More(1)[OF this] obtain q where "q ∈ poss C⟨t⟩ ∧ hole_pos C ⊥ q ∧ C⟨t⟩ |_ q = Var x"
by fastforce
then show ?thesis by (force intro!: exI[of _ "length bef # q"])
next
case bef
then obtain q where "q ∈ poss t" and "t |_ q = Var x"
using vars_term_poss_subt_at by force
moreover from bef obtain i where "i < length bef" and "bef ! i = t"
using in_set_conv_nth by metis
ultimately show ?thesis
by (force simp: nth_append intro!: exI[of _ "i # q"])
next
case aft
then obtain q where "q ∈ poss t" and "t |_ q = Var x"
using vars_term_poss_subt_at by force
moreover from aft obtain i where "i < length aft" and "aft ! i = t"
using in_set_conv_nth by metis
ultimately show ?thesis
by (force simp: nth_append intro!: exI[of _ "(Suc (length bef) + i) # q"])
qed
qed auto
lemma vars_ctxt_subt_at:
assumes "x ∈ vars_ctxt C"
and "p ∈ poss C⟨t⟩"
and "hole_pos C = p"
obtains q where "q ∈ poss C⟨t⟩" and "parallel_pos p q" and "C⟨t⟩ |_ q = Var x"
using vars_ctxt_subt_at' assms by force
lemma poss_is_Fun_fun_poss:
assumes "p ∈ poss t"
and "is_Fun (t |_ p)"
shows "p ∈ fun_poss t"
using assms by (metis DiffI is_Var_def poss_simps(3) var_poss_iff)
lemma fun_poss_map_vars_term:
"fun_poss (map_vars_term f t) = fun_poss t"
unfolding map_vars_term_eq proof(induct t)
case (Fun g ts)
{fix i assume "i < length ts"
with Fun have "fun_poss (map (λt. t ⋅ (Var ∘ f)) ts ! i) = fun_poss (ts!i)"
by fastforce
then have "{i # p |p. p ∈ fun_poss (map (λt. t ⋅ (Var ∘ f)) ts ! i)} = {i # p |p. p ∈ fun_poss (ts ! i)}"
by presburger
}
then show ?case unfolding fun_poss.simps eval_term.simps length_map
by auto
qed simp
lemma fun_poss_append_poss:
assumes "p@q ∈ poss t" "q ≠ []"
shows "p ∈ fun_poss t"
by (meson assms is_Var_def poss_append_poss poss_is_Fun_fun_poss var_pos_maximal)
lemma fun_poss_append_poss':
assumes "p@q ∈ fun_poss t"
shows "p ∈ fun_poss t"
by (metis append.right_neutral assms fun_poss_append_poss fun_poss_imp_poss)
lemma fun_poss_in_ctxt:
assumes "q@p ∈ fun_poss (C⟨t⟩)"
and "hole_pos C = q"
shows "p ∈ fun_poss t"
by (metis Term.term.simps(4) assms fun_poss_fun_conv fun_poss_imp_poss hole_pos_poss hole_pos_poss_conv is_VarE poss_is_Fun_fun_poss subt_at_append subt_at_hole_pos)
lemma args_poss:
assumes "i # p ∈ poss t"
obtains f ts where "t = Fun f ts" "p ∈ poss (ts!i)" "i < length ts"
by (metis Cons_poss_Var assms poss.elims poss_Cons_poss term.sel(4))
lemma var_poss_parallel:
assumes "p ∈ var_poss t" and "q ∈ var_poss t" and "p ≠ q"
shows "p ⊥ q"
using assms proof(induct t arbitrary:p q)
case (Fun f ts)
from Fun(2) obtain i p' where i:"i < length ts" "p' ∈ var_poss (ts!i)" and p:"p = i#p'"
using var_poss_iff by fastforce
with Fun(3) obtain j q' where j:"j < length ts" "q' ∈ var_poss (ts!j)" and q:"q = j#q'"
using var_poss_iff by fastforce
then show ?case proof(cases "i = j")
case True
from Fun(4) have "p' ≠ q'"
unfolding p q True by simp
with Fun(1) i j show ?thesis
unfolding True p q parallel_pos.simps using nth_mem by blast
next
case False
then show ?thesis unfolding p q
by simp
qed
qed simp
lemma ctxt_comp_equals:
assumes poss:"p ∈ poss s" "p ∈ poss t"
and "ctxt_of_pos_term p s ∘⇩c C = ctxt_of_pos_term p t ∘⇩c D"
shows "C = D"
using assms proof(induct p arbitrary:s t)
case (Cons i p)
from Cons(2) obtain f ss where s:"s = Fun f ss" and p:"p ∈ poss (ss!i)"
using args_poss by blast
from Cons(3) obtain g ts where t:"t = Fun g ts" and p':"p ∈ poss (ts!i)"
using args_poss by blast
from Cons(1)[OF p p'] Cons(4) show ?case
unfolding s t ctxt_of_pos_term.simps ctxt_compose.simps by simp
qed simp
lemma ctxt_subst_comp_pos:
assumes "q ∈ poss t" and "p ∈ poss (t ⋅ τ)"
and "(ctxt_of_pos_term q t ⋅⇩c σ) ∘⇩c C = ctxt_of_pos_term p (t ⋅ τ)"
shows "q ≤⇩p p"
using assms by (metis hole_pos_ctxt_compose hole_pos_ctxt_of_pos_term hole_pos_subst less_eq_pos_simps(1))
text ‹Predicate whether a context is ground, i.e., whether the context contains no variables.›
fun ground_ctxt :: "('f,'v)ctxt ⇒ bool" where
"ground_ctxt Hole = True"
| "ground_ctxt (More f ss1 C ss2) =
((∀s∈set ss1. ground s) ∧ (∀s∈set ss2. ground s) ∧ ground_ctxt C)"
lemma ground_ctxt_apply[simp]: "ground (C⟨t⟩) = (ground_ctxt C ∧ ground t)"
by (induct C, auto)
lemma ground_ctxt_compose[simp]: "ground_ctxt (C ∘⇩c D) = (ground_ctxt C ∧ ground_ctxt D)"
by (induct C, auto)
text ‹Linearity of a term›
fun linear_term :: "('f, 'v) term ⇒ bool"
where
"linear_term (Var _) = True" |
"linear_term (Fun _ ts) = (is_partition (map vars_term ts) ∧ (∀t∈set ts. linear_term t))"
lemma subst_merge:
assumes part: "is_partition (map vars_term ts)"
shows "∃σ. ∀i<length ts. ∀x∈vars_term (ts ! i). σ x = τ i x"
proof -
let ?τ = "map τ [0 ..< length ts]"
let ?σ = "fun_merge ?τ (map vars_term ts)"
show ?thesis
by (rule exI[of _ ?σ], intro allI impI ballI,
insert fun_merge_part[OF part, of _ _ ?τ], auto)
qed
text ‹Matching for linear terms›
fun weak_match :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool"
where
"weak_match _ (Var _) ⟷ True" |
"weak_match (Var _) (Fun _ _) ⟷ False" |
"weak_match (Fun f ts) (Fun g ss) ⟷
f = g ∧ length ts = length ss ∧ (∀i < length ts. weak_match (ts ! i) (ss ! i))"
lemma weak_match_refl: "weak_match t t"
by (induct t) auto
lemma weak_match_match: "weak_match (t ⋅ σ) t"
by (induct t) auto
lemma weak_match_map_funs_term:
"weak_match t s ⟹ weak_match (map_funs_term g t) (map_funs_term g s)"
proof (induct s arbitrary: t)
case (Fun f ss t)
from Fun(2) obtain ts where t: "t = Fun f ts" by (cases t, auto)
from Fun(1)[unfolded set_conv_nth] Fun(2)[unfolded t]
show ?case unfolding t by force
qed simp
lemma linear_weak_match:
assumes "linear_term l" and "weak_match t s" and "s = l ⋅ σ"
shows "∃τ. t = l⋅τ ∧ (∀x∈vars_term l. weak_match (Var x ⋅ τ) (Var x ⋅ σ))"
using assms proof (induct l arbitrary: s t)
case (Var x)
show ?case
proof (rule exI[of _ "(λ y. t)"], intro conjI, simp)
from Var show "∀x∈vars_term (Var x). weak_match (Var x ⋅ (λy. t)) (Var x ⋅ σ)"
by force
qed
next
case (Fun f ls)
let ?n = "length ls"
from Fun(4) obtain ss where s: "s = Fun f ss" and lss: "length ss = ?n" by (cases s, auto)
with Fun(4) have match: "⋀ i. i < ?n ⟹ ss ! i = (ls ! i) ⋅ σ" by auto
from Fun(3) s lss obtain ts where t: "t = Fun f ts"
and lts: "length ts = ?n" by (cases t, auto)
with Fun(3) s have weak_match: "⋀ i. i < ?n ⟹ weak_match (ts ! i) (ss ! i)" by auto
from Fun(2) have linear: "⋀ i. i < ?n ⟹ linear_term (ls ! i)" by simp
let ?cond = "λ τ i. ts ! i = ls ! i ⋅ τ ∧ (∀x∈vars_term (ls ! i). weak_match (Var x ⋅ τ) (Var x ⋅ σ))"
{
fix i
assume i: "i < ?n"
then have "ls ! i ∈ set ls" by simp
from Fun(1)[OF this linear[OF i] weak_match[OF i] match[OF i]]
have "∃ τ. ?cond τ i" .
}
then have "∀i. ∃τ. (i < ?n ⟶ ?cond τ i)" by auto
from choice[OF this] obtain subs where subs: "⋀ i. i < ?n ⟹ ?cond (subs i) i" by auto
from Fun(2) have distinct: "is_partition(map vars_term ls)" by simp
from subst_merge[OF this, of subs]
obtain τ where τ: "⋀ i x . i < length ls ⟹ x ∈ vars_term (ls ! i) ⟹ τ x = subs i x" by auto
show ?case
proof (rule exI[of _ τ], simp add: t, intro ballI conjI)
fix li x
assume li: "li ∈ set ls" and x: "x ∈ vars_term li"
from li obtain i where i: "i < ?n" and li: "li = ls ! i" unfolding set_conv_nth by auto
with x have x: "x ∈ vars_term (ls ! i)" by simp
from subs[OF i, THEN conjunct2, THEN bspec, OF x] show "weak_match (τ x) (σ x)" unfolding τ[OF i x[unfolded li]]
by simp
next
show "ts = map (λ t. t ⋅ τ) ls"
proof (rule nth_equalityI, simp add: lts)
fix i
assume "i < length ts"
with lts have i: "i < ?n" by simp
have "ts ! i = ls ! i ⋅ subs i"
by (rule subs[THEN conjunct1, OF i])
also have "... = ls ! i ⋅ τ" unfolding term_subst_eq_conv using τ[OF i] by auto
finally show "ts ! i = map (λ t. t ⋅ τ) ls ! i"
by (simp add: nth_map[OF i])
qed
qed
qed
lemma map_funs_subst_split:
assumes "map_funs_term fg t = s ⋅ σ"
and "linear_term s"
shows "∃ u τ. t = u ⋅ τ ∧ map_funs_term fg u = s ∧ (∀x∈vars_term s. map_funs_term fg (τ x) = (σ x))"
using assms
proof (induct s arbitrary: t)
case (Var x t)
show ?case
proof (intro exI conjI)
show "t = Var x ⋅ (λ _. t)" by simp
qed (insert Var, auto)
next
case (Fun g ss t)
from Fun(2) obtain f ts where t: "t = Fun f ts" by (cases t, auto)
note Fun = Fun[unfolded t, simplified]
let ?n = "length ss"
from Fun have rec: "map (map_funs_term fg) ts = map (λ t. t ⋅ σ) ss"
and g: "fg f = g"
and lin: "⋀ s. s ∈ set ss ⟹ linear_term s"
and part: "is_partition (map vars_term ss)" by auto
from arg_cong[OF rec, of length] have len: "length ts = ?n" by simp
from map_nth_conv[OF rec] have rec: "⋀ i. i < ?n ⟹ map_funs_term fg (ts ! i) = ss ! i ⋅ σ" unfolding len by auto
let ?p = "λ i u τ. ts ! i = u ⋅ τ ∧ map_funs_term fg u = ss ! i ∧ (∀x∈vars_term (ss ! i). map_funs_term fg (τ x) = σ x)"
{
fix i
assume i: "i < ?n"
then have "ss ! i ∈ set ss" by auto
from Fun(1)[OF this rec[OF i] lin[OF this]]
have "∃ u τ. ?p i u τ" .
}
then have "∀i. ∃u τ. i < ?n ⟶ ?p i u τ" by blast
from choice[OF this] obtain us where "∀i. ∃τ. i < ?n ⟶ ?p i (us i) τ" ..
from choice[OF this] obtain τs where p: "⋀ i. i < ?n ⟹ ?p i (us i) (τs i)" by blast
from subst_merge[OF part, of τs] obtain τ where τ: "⋀ i x. i < ?n ⟹ x ∈ vars_term (ss ! i) ⟹ τ x = τs i x" by blast
{
fix i
assume i: "i < ?n"
from p[OF i] have "map_funs_term fg (us i) = ss ! i" by auto
from arg_cong[OF this, of vars_term] vars_term_map_funs_term[of fg]
have "vars_term (us i) = vars_term (ss ! i)" by auto
} note vars = this
let ?us = "map us [0 ..< ?n]"
show ?case
proof (intro exI conjI ballI)
have ss: "ts = map (λ t. t ⋅ τ) ?us"
unfolding list_eq_iff_nth_eq
unfolding len
proof (intro conjI allI impI)
fix i
assume i: "i < ?n"
have us: "?us ! i = us i" using nth_map_upt[of i ?n 0] i by auto
have "(map (λ t. t ⋅ τ) ?us) ! i = us i ⋅ τ"
unfolding us[symmetric]
using nth_map[of i ?us "λ t. t ⋅ τ"] i by force
also have "... = us i ⋅ τs i"
by (rule term_subst_eq, rule τ[OF i], insert vars[OF i], auto )
also have "... = ts ! i" using p[OF i] by simp
finally
show "ts ! i = map (λ t. t ⋅ τ) ?us ! i" ..
qed auto
show "t = Fun f ?us ⋅ τ"
unfolding t
unfolding ss by auto
next
show "map_funs_term fg (Fun f ?us) = Fun g ss"
using p g by (auto simp: list_eq_iff_nth_eq[of _ ss])
next
fix x
assume x: "x ∈ vars_term (Fun g ss)"
then obtain s where s: "s ∈ set ss" and x: "x ∈ vars_term s" by auto
from s[unfolded set_conv_nth] obtain i where s: "s = ss ! i" and i: "i < ?n" by auto
note x = x[unfolded s]
from p[OF i] vars[OF i] x τ[OF i x]
show "map_funs_term fg (τ x) = σ x" by auto
qed
qed
lemma linear_map_funs_term [simp]:
"linear_term (map_funs_term f t) = linear_term t"
by (induct t) simp_all
lemma linear_term_map_inj_on_linear_term:
assumes "linear_term l"
and "inj_on f (vars_term l)"
shows "linear_term (map_vars_term f l)"
using assms
proof (induct l)
case (Fun g ls)
then have part:"is_partition (map vars_term ls)" by auto
{ fix l
assume l:"l ∈ set ls"
then have "vars_term l ⊆ vars_term (Fun g ls)" by auto
then have "inj_on f (vars_term l)" using Fun(3) subset_inj_on by blast
with Fun(1,2) l have "linear_term (map_vars_term f l)" by auto
}
moreover have "is_partition (map (vars_term ∘ map_vars_term f) ls)"
using is_partition_inj_map[OF part, of f] Fun(3) by (simp add: o_def term.set_map)
ultimately show ?case by auto
qed auto
lemma linear_term_replace_in_subst:
assumes "linear_term t"
and "p ∈ poss t"
and "t |_ p = Var x"
and "⋀ y. y ∈ vars_term t ⟹ y ≠ x ⟹ σ y = τ y"
and "τ x = s"
shows "replace_at (t ⋅ σ) p s = t ⋅ τ"
using assms
proof (induct p arbitrary: t)
case (Cons i p t)
then obtain f ts where t [simp]: "t = Fun f ts" and i: "i < length ts" and p: "p ∈ poss (ts ! i)"
by (cases t) auto
from Cons have "linear_term (ts ! i)" and "ts ! i |_ p = Var x" by auto
have id: "replace_at (ts ! i ⋅ σ) p (τ x) = ts ! i ⋅ τ" using Cons by force
let ?l = " (take i (map (λt. t ⋅ σ) ts) @ (ts ! i ⋅ τ) # drop (Suc i) (map (λt. t ⋅ σ) ts))"
from i have len: "length ts = length ?l" by auto
{ fix j
assume j: "j < length ts"
have "ts ! j ⋅ τ = ?l ! j"
proof (cases "j = i")
case True
with i show ?thesis by (auto simp: nth_append)
next
case False
let ?ts = "map (λt. t ⋅ σ) ts"
from i j have le:"j ≤ length ?ts" "i ≤ length ?ts" by auto
from nth_append_take_drop_is_nth_conv[OF le] False have "?l ! j = ?ts ! j" by simp
also have "... = ts ! j ⋅ σ" using j by simp
also have "... = ts ! j ⋅ τ"
proof (rule term_subst_eq)
fix y
assume y: "y ∈ vars_term (ts ! j)"
from p have "ts ! i ⊵ ts ! i |_ p" by (rule subt_at_imp_supteq)
then have x: "x ∈ vars_term (ts ! i)" using ‹ts ! i |_ p = Var x›
by (auto intro: subteq_Var_imp_in_vars_term)
from Cons(2) have "is_partition (map vars_term ts)" by simp
from this[unfolded is_partition_alt is_partition_alt_def, rule_format] j i False
have "vars_term (ts ! i) ∩ vars_term (ts ! j) = {}" by auto
with y x have "y ≠ x" by auto
with Cons(5) y j show "σ y = τ y" by force
qed
finally show ?thesis by simp
qed
}
then show ?case
by (auto simp: ‹τ x = s›[symmetric] id nth_map[OF i, of "λt. t ⋅ σ"])
(metis len map_nth_eq_conv[OF len])
qed auto
lemma var_in_linear_args:
assumes "linear_term (Fun f ts)"
and "i < length ts" and "x ∈ vars_term (ts!i)" and "j < length ts ∧ j ≠ i"
shows "x ∉ vars_term (ts!j)"
proof-
from assms(1) have "is_partition (map vars_term ts)"
by simp
with assms show ?thesis unfolding is_partition_alt is_partition_alt_def
by auto
qed
lemma subt_at_linear:
assumes "linear_term t" and "p ∈ poss t"
shows "linear_term (t|_p)"
using assms proof(induct p arbitrary:t)
case (Cons i p)
then obtain f ts where f:"t = Fun f ts" and i:"i < length ts" and p:"p ∈ poss (ts!i)"
by (meson args_poss)
with Cons(2) have "linear_term (ts!i)"
by force
then show ?case
unfolding f subt_at.simps using Cons.hyps p by blast
qed simp
lemma linear_subterms_disjoint_vars:
assumes "linear_term t"
and "p ∈ poss t" and "q ∈ poss t" and "p ⊥ q"
shows "vars_term (t|_p) ∩ vars_term (t|_q) = {}"
using assms proof(induct t arbitrary: p q)
case (Fun f ts)
from Fun(3,5) obtain i p' where i:"i < length ts" "p' ∈ poss (ts!i)" and p:"p = i#p'"
by auto
with Fun(4,5) obtain j q' where j:"j < length ts" "q' ∈ poss (ts!j)" and q:"q = j#q'"
by auto
then show ?case proof(cases "i=j")
case True
from Fun(5) have "p' ⊥ q'"
unfolding p q True by simp
with Fun(1,2) i j have "vars_term ((ts!j) |_ p') ∩ vars_term ((ts!j) |_ q') = {}"
unfolding True by auto
then show ?thesis unfolding p q subt_at.simps True by simp
next
case False
from i have "vars_term ((Fun f ts)|_p) ⊆ vars_term (ts!i)"
unfolding p subt_at.simps by (simp add: vars_term_subt_at)
moreover from j have "vars_term ((Fun f ts)|_q) ⊆ vars_term (ts!j)"
unfolding q subt_at.simps by (simp add: vars_term_subt_at)
ultimately show ?thesis using False Fun(2) i j
by (meson disjoint_iff subsetD var_in_linear_args)
qed
qed simp
lemma ground_imp_linear_term [simp]: "ground t ⟹ linear_term t"
by (induct t) (auto simp add: is_partition_def ground_vars_term_empty)
text ‹exhaustively apply several maps on function symbols›
fun map_funs_term_enum :: "('f ⇒ 'g list) ⇒ ('f, 'v) term ⇒ ('g, 'v) term list"
where
"map_funs_term_enum fgs (Var x) = [Var x]" |
"map_funs_term_enum fgs (Fun f ts) = (
let
lts = map (map_funs_term_enum fgs) ts;
ss = concat_lists lts;
gs = fgs f
in concat (map (λg. map (Fun g) ss) gs))"
lemma map_funs_term_enum:
assumes gf: "⋀ f g. g ∈ set (fgs f) ⟹ gf g = f"
shows "set (map_funs_term_enum fgs t) = {u. map_funs_term gf u = t ∧ (∀g n. (g,n) ∈ funas_term u ⟶ g ∈ set (fgs (gf g)))}"
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 f 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
let ?cf = "λ u. (∀g n. (g,n) ∈ funas_term u ⟶ g ∈ set (fgs (gf g)))"
have id: "?L = {Fun g ss | g ss. g ∈ set (fgs f) ∧ length ss = length ts ∧ (∀i<length ts. ss ! i ∈ set (map_funs_term_enum fgs (ts ! i)))}" (is "_ = ?M1") by auto
have "?R = {Fun g ss | g ss. map_funs_term gf (Fun g ss) = Fun f ts ∧ ?cf (Fun g ss)}" (is "_ = ?M2")
proof -
{
fix u
assume u: "u ∈ ?R"
then obtain g ss where "u = Fun g ss" by (cases u, auto)
with u have "u ∈ ?M2" by auto
}
then have "?R ⊆ ?M2" by auto
moreover have "?M2 ⊆ ?R" by blast
finally show ?thesis by auto
qed
also have "... = ?M1"
proof -
{
fix u
assume "u ∈ ?M1"
then obtain g ss where u: "u = Fun g ss" and g: "g ∈ set (fgs f)" and
len: "length ss = length ts" and rec: "⋀ i. i < length ts ⟹ ss ! i ∈ set (map_funs_term_enum fgs (ts ! i))" by auto
from gf[OF g] have gf: "gf g = f" by simp
{
fix i
assume i: "i < length ts"
from ind[OF i] rec[OF i]
have "map_funs_term gf (ss ! i) = ts ! i" by auto
} note ssts = this
have "map (map_funs_term gf) ss = ts"
by (unfold map_nth_eq_conv[OF len], insert ssts, auto)
with gf
have mt: "map_funs_term gf (Fun g ss) = Fun f ts" by auto
have "u ∈ ?M2"
proof (rule, rule, rule, rule, rule u, rule, rule mt, intro allI impI)
fix h n
assume h: "(h,n) ∈ funas_term (Fun g ss)"
show "h ∈ set (fgs (gf h))"
proof (cases "(h,n) = (g,length ss)")
case True
then have "h = g" by auto
with g gf show ?thesis by auto
next
case False
with h obtain s where s: "s ∈ set ss" and h: "(h,n) ∈ funas_term s" by auto
from s[unfolded set_conv_nth] obtain i where i: "i < length ss" and si: "s = ss ! i" by force
from i len have i': "i < length ts" by auto
from ind[OF i'] rec[OF i'] h[unfolded si] show ?thesis by auto
qed
qed
}
then have m1m2: "?M1 ⊆ ?M2" by blast
{
fix u
assume u: "u ∈ ?M2"
then obtain g ss where u: "u = Fun g ss"
and map: "map_funs_term gf (Fun g ss) = Fun f ts"
and c: "?cf (Fun g ss)"
by blast
from map have len: "length ss = length ts" by auto
from map have g: "gf g = f" by auto
from map have map: "map (map_funs_term gf) ss = ts" by auto
from c have g2: "g ∈ set (fgs f)" using g by auto
have "u ∈ ?M1"
proof (intro CollectI exI conjI allI impI, rule u, rule g2, rule len)
fix i
assume i: "i < length ts"
with map[unfolded map_nth_eq_conv[OF len]]
have id: "map_funs_term gf (ss ! i) = ts ! i" by auto
from i len have si: "ss ! i ∈ set ss" by auto
show "ss ! i ∈ set (map_funs_term_enum fgs (ts ! i))"
unfolding ind[OF i]
proof (intro CollectI conjI impI allI, rule id)
fix g n
assume "(g,n) ∈ funas_term (ss ! i)"
with c si
show "g ∈ set (fgs (gf g))" by auto
qed
qed
}
then have m2m1: "?M2 ⊆ ?M1" by blast
show "?M2 = ?M1"
by (rule, rule m2m1, rule m1m2)
qed
finally show ?case unfolding id by simp
qed
qed
declare map_funs_term_enum.simps[simp del]
end