chapter ‹First-Order Terms›
theory Term_More
imports
More_Abstract_Rewriting
Position
"../Auxiliaries/Util"
"../Auxiliaries/Multiset2"
"../Termination_and_Complexity/Sharp_Syntax"
First_Order_Terms.Term
begin
text ‹
A \emph{signature} is a set of function symbols arity pairs, where the arity of a function symbol,
denotes the number of arguments it expects.
›
type_synonym 'f sig = "('f × nat) set"
subsection ‹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
lemma is_FunE [elim]:
"is_Fun t ⟹ (⋀f ts. t = Fun f ts ⟹ P) ⟹ P"
by (cases t) auto
declare term.disc [intro]
lemmas is_VarI = term.disc(1)
lemmas is_FunI = term.disc(2)
text ‹
The set of all function symbol and arity pairs occurring in a term.
›
fun funas_term :: "('f, 'v) term ⇒ 'f sig"
where
"funas_term (Var _) = {}" |
"funas_term (Fun f ts) = {(f, length ts)} ∪ ⋃(set (map funas_term ts))"
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)))"
text ‹
The \emph{root symbol} of a term is defined by:
›
fun root :: "('f, 'v) term ⇒ ('f × nat) option"
where
"root (Var x) = None" |
"root (Fun f ts) = Some (f, length ts)"
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)
lemma finite_funas_term:
"finite (funas_term t)"
by (induct t) auto
text ‹A term is called \emph{ground} if it does not contain any variables.›
fun ground :: "('f, 'v) term ⇒ bool"
where
"ground (Var x) ⟷ False" |
"ground (Fun f ts) ⟷ (∀t ∈ set ts. ground t)"
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))"
subsection ‹Subterms›
text ‹The \emph{superterm} relation.›
inductive_set
supteq :: "(('f, 'v) term × ('f, 'v) term) set"
where
refl [simp, intro]: "(t, t) ∈ supteq" |
subt [intro]: "u ∈ set ss ⟹ (u, t) ∈ supteq ⟹ (Fun f ss, t) ∈ supteq"
text ‹The \emph{proper superterm} relation.›
inductive_set
supt :: "(('f, 'v) term × ('f, 'v) term) set"
where
arg [simp, intro]: "s ∈ set ss ⟹ (Fun f ss, s) ∈ supt" |
subt [intro]: "s ∈ set ss ⟹ (s, t) ∈ supt ⟹ (Fun f ss, t) ∈ supt"
hide_const suptp supteqp
hide_fact
suptp.arg suptp.cases suptp.induct suptp.intros suptp.subt suptp_supt_eq
hide_fact
supteqp.cases supteqp.induct supteqp.intros supteqp.refl supteqp.subt supteqp_supteq_eq
hide_fact (open) supt.arg supt.subt supteq.refl supteq.subt
subsubsection ‹Syntax for Subterms›
text ‹Infix syntax.›
abbreviation "supt_pred s t ≡ (s, t) ∈ supt"
abbreviation "supteq_pred s t ≡ (s, t) ∈ supteq"
abbreviation (input) "subt_pred s t ≡ supt_pred t s"
abbreviation (input) "subteq_pred s t ≡ supteq_pred t s"
notation
supt ("{⊳}") and
supt_pred ("(_/ ⊳ _)" [56, 56] 55) and
subt_pred (infix "⊲" 55) and
supteq ("{⊵}") and
supteq_pred ("(_/ ⊵ _)" [56, 56] 55) and
subteq_pred (infix "⊴" 55)
abbreviation subt ("{⊲}") where "{⊲} ≡ {⊳}¯"
abbreviation subteq ("{⊴}") where "{⊴} ≡ {⊵}¯"
text ‹Quantifier syntax.›
syntax
"_All_supteq" :: "[idt, 'a, bool] ⇒ bool" ("(3∀_⊵_./ _)" [0, 0, 10] 10)
"_Ex_supteq" :: "[idt, 'a, bool] ⇒ bool" ("(3∃_⊵_./ _)" [0, 0, 10] 10)
"_All_supt" :: "[idt, 'a, bool] ⇒ bool" ("(3∀_⊳_./ _)" [0, 0, 10] 10)
"_Ex_supt" :: "[idt, 'a, bool] ⇒ bool" ("(3∃_⊳_./ _)" [0, 0, 10] 10)
"_All_subteq" :: "[idt, 'a, bool] ⇒ bool" ("(3∀_⊴_./ _)" [0, 0, 10] 10)
"_Ex_subteq" :: "[idt, 'a, bool] ⇒ bool" ("(3∃_⊴_./ _)" [0, 0, 10] 10)
"_All_subt" :: "[idt, 'a, bool] ⇒ bool" ("(3∀_⊲_./ _)" [0, 0, 10] 10)
"_Ex_subt" :: "[idt, 'a, bool] ⇒ bool" ("(3∃_⊲_./ _)" [0, 0, 10] 10)
translations
"∀x⊵y. P" ⇀ "∀x. x ⊵ y ⟶ P"
"∃x⊵y. P" ⇀ "∃x. x ⊵ y ∧ P"
"∀x⊳y. P" ⇀ "∀x. x ⊳ y ⟶ P"
"∃x⊳y. P" ⇀ "∃x. x ⊳ y ∧ P"
"∀x⊴y. P" ⇀ "∀x. x ⊴ y ⟶ P"
"∃x⊴y. P" ⇀ "∃x. x ⊴ y ∧ P"
"∀x⊲y. P" ⇀ "∀x. x ⊲ y ⟶ P"
"∃x⊲y. P" ⇀ "∃x. x ⊲ y ∧ P"
print_translation ‹
let
val All_binder = Mixfix.binder_name @{const_syntax All};
val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
val impl = @{const_syntax "implies"};
val conj = @{const_syntax "conj"};
val supt = @{const_syntax "supt_pred"};
val supteq = @{const_syntax "supteq_pred"};
val trans =
[((All_binder, impl, supt), ("_All_supt", "_All_subt")),
((All_binder, impl, supteq), ("_All_supteq", "_All_subteq")),
((Ex_binder, conj, supt), ("_Ex_supt", "_Ex_subt")),
((Ex_binder, conj, supteq), ("_Ex_supteq", "_Ex_subteq"))];
fun matches_bound v t =
case t of (Const ("_bound", _) $ Free (v', _)) => (v = v')
| _ => false
fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false)
fun mk x c n P = Syntax.const c $ Syntax_Trans.mark_bound_body x $ n $ P
fun tr' q = (q,
K (fn [Const ("_bound", _) $ Free (v, T), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
(case AList.lookup (op =) trans (q, c, d) of
NONE => raise Match
| SOME (l, g) =>
if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P
else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P
else raise Match)
| _ => raise Match));
in [tr' All_binder, tr' Ex_binder] end
›
subsubsection ‹Transitivity Reasoning for Subterms›
lemma supt_trans [trans]:
"s ⊳ t ⟹ t ⊳ u ⟹ s ⊳ u"
by (induct s t rule: supt.induct) (auto)
lemma supteq_trans [trans]:
"s ⊵ t ⟹ t ⊵ u ⟹ s ⊵ u"
by (induct s t rule: supteq.induct) (auto)
text ‹Auxiliary lemmas about term size.›
lemma size_simp5:
"s ∈ set ss ⟹ s ⊳ t ⟹ size t < size s ⟹ size t < Suc (size_list size ss)"
by (induct ss) auto
lemma size_simp6:
"s ∈ set ss ⟹ s ⊵ t ⟹ size t ≤ size s ⟹ size t ≤ Suc (size_list size ss)"
by (induct ss) auto
lemma size_simp1:
"t ∈ set ts ⟹ size t < Suc (size_list size ts)"
by (induct ts) auto
lemma size_simp2:
"t ∈ set ts ⟹ size t < Suc (Suc (size s + size_list size ts))"
by (induct ts) auto
lemma size_simp3:
assumes "(x, y) ∈ set (zip xs ys)"
shows "size x < Suc (size_list size xs)"
using set_zip_leftD [OF assms] size_simp1 by auto
lemma size_simp4:
assumes "(x, y) ∈ set (zip xs ys)"
shows "size y < Suc (size_list size ys)"
using set_zip_rightD [OF assms] using size_simp1 by auto
lemmas size_simps =
size_simp1 size_simp2 size_simp3 size_simp4 size_simp5 size_simp6
declare size_simps [termination_simp]
lemma supt_size:
"s ⊳ t ⟹ size s > size t"
by (induct rule: supt.induct) (auto simp: size_simps)
lemma supteq_size:
"s ⊵ t ⟹ size s ≥ size t"
by (induct rule: supteq.induct) (auto simp: size_simps)
text ‹Reflexivity and Asymmetry.›
lemma reflcl_supteq [simp]:
"supteq⇧= = supteq" by auto
lemma trancl_supteq [simp]:
"supteq⇧+ = supteq"
by (rule trancl_id) (auto simp: trans_def intro: supteq_trans)
lemma rtrancl_supteq [simp]:
"supteq⇧* = supteq"
unfolding trancl_reflcl[symmetric] by auto
lemma eq_supteq: "s = t ⟹ s ⊵ t" by auto
lemma supt_neqD: "s ⊳ t ⟹ s ≠ t" using supt_size by auto
lemma supteq_Var [simp]:
"x ∈ vars_term t ⟹ t ⊵ Var x"
proof (induct t)
case (Var y) thus ?case by (cases "x = y") auto
next
case (Fun f ss) thus ?case by (auto)
qed
lemmas vars_term_supteq = supteq_Var
lemma term_not_arg [iff]:
"Fun f ss ∉ set ss" (is "?t ∉ set ss")
proof
assume "?t ∈ set ss"
hence "?t ⊳ ?t" by (auto)
hence "?t ≠ ?t" by (auto dest: supt_neqD)
thus False by simp
qed
lemma supt_Fun [simp]:
assumes "s ⊳ Fun f ss" (is "s ⊳ ?t") and "s ∈ set ss"
shows "False"
proof -
from ‹s ∈ set ss› have "?t ⊳ s" by (auto)
hence "size ?t > size s" by (rule supt_size)
from ‹s ⊳ ?t› have "size s > size ?t" by (rule supt_size)
with ‹size ?t > size s› show False by simp
qed
lemma supt_supteq_conv: "s ⊳ t = (s ⊵ t ∧ s ≠ t)"
proof
assume "s ⊳ t" thus "s ⊵ t ∧ s ≠ t"
proof (induct rule: supt.induct)
case (arg t ss f) show ?case
proof
from arg show "Fun f ss ⊵ t" by (auto)
next
from arg have "size t < size (Fun f ss)" by (auto simp: size_simps)
thus "Fun f ss ≠ t" by auto
qed
next
case (subt s ss t f)
have "s ⊵ s" ..
from ‹s ∈ set ss› have "Fun f ss ⊵ s" by (auto)
from ‹s ⊵ t ∧ s ≠ t› have "s ⊵ t" ..
with ‹Fun f ss ⊵ s› have first: "Fun f ss ⊵ t" by (rule supteq_trans)
from ‹s ∈ set ss› and ‹s ⊳ t› have "Fun f ss ⊳ t" ..
hence second: "Fun f ss ≠ t" by (auto dest: supt_neqD)
from first and second show "Fun f ss ⊵ t ∧ Fun f ss ≠ t" by auto
qed
next
assume "s ⊵ t ∧ s ≠ t"
hence "s ⊵ t" and "s ≠ t" by auto
thus "s ⊳ t" by (induct) (auto)
qed
lemma supt_not_sym: "s ⊳ t ⟹ ¬ (t ⊳ s)"
proof
assume "s ⊳ t" and "t ⊳ s" hence "s ⊳ s" by (rule supt_trans)
thus False unfolding supt_supteq_conv by simp
qed
lemma supt_irrefl[iff]: "¬ t ⊳ t"
using supt_not_sym[of t t] by auto
lemma supt_imp_supteq: "s ⊳ t ⟹ s ⊵ t"
unfolding supt_supteq_conv by auto
lemma supt_supteq_not_supteq: "s ⊳ t = (s ⊵ t ∧ ¬ (t ⊵ s))"
using supt_not_sym unfolding supt_supteq_conv by auto
lemma supteq_supt_conv: "(s ⊵ t) = (s ⊳ t ∨ s = t)" by (auto simp: supt_supteq_conv)
lemma supteq_antisym:
assumes "s ⊵ t" and "t ⊵ s" shows "s = t"
using assms unfolding supteq_supt_conv by (auto simp: supt_not_sym)
text ‹The subterm relation is an order on terms.›
interpretation subterm: order "op ⊴" "op ⊲"
by (unfold_locales)
(rule supt_supteq_not_supteq, auto intro: supteq_trans supteq_antisym supt_supteq_not_supteq)
lemma suptE [elim]: "s ⊳ t ⟹ (s ⊵ t ⟹ P) ⟹ (s ≠ t ⟹ P) ⟹ P"
by (auto simp: supt_supteq_conv)
lemmas suptI [intro] =
subterm.dual_order.not_eq_order_implies_strict
lemma supt_supteq_set_conv:
"{⊳} = {⊵} - Id"
using supt_supteq_conv [to_set] by auto
lemma supteq_supt_set_conv:
"{⊵} = {⊳}⇧="
by (auto simp: supt_supteq_conv)
lemma supteq_imp_vars_term_subset:
"s ⊵ t ⟹ vars_term t ⊆ vars_term s"
by (induct rule: supteq.induct) auto
lemma set_supteq_into_supt [simp]:
assumes "t ∈ set ts" and "t ⊵ s"
shows "Fun f ts ⊳ s"
proof -
from ‹t ⊵ s› have "t = s ∨ t ⊳ s" by auto
thus ?thesis
proof
assume "t = s"
with ‹t ∈ set ts› show ?thesis by auto
next
assume "t ⊳ s"
from supt.subt[OF ‹t ∈ set ts› this] show ?thesis .
qed
qed
declare conj_cong [fundef_cong]
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 PCons_poss_Var [simp]:
"i <# p ∈ poss (Var x) ⟷ False"
by simp
lemma [termination_simp]:
"x ∈ set xs ⟹ size x < size_list size xs"
by (induct xs) auto
fun funposs :: "('f, 'v) term ⇒ pos set"
where
"funposs (Var x) = {}" |
"funposs (Fun f ts) = {ε} ∪ (⋃i<length ts. {i <# p | p. p ∈ funposs (ts ! i)})"
lemma funposs_imp_poss:
assumes "p ∈ funposs t"
shows "p ∈ poss t"
using assms by (induct t arbitrary: p) auto
lemma finite_funposs:
"finite (funposs t)"
by (induct t) auto
fun varposs :: "('f, 'v) term ⇒ pos set"
where
"varposs (Var x) = {ε}" |
"varposs (Fun f ts) = (⋃i<length ts. {i <# p | p. p ∈ varposs (ts ! i)})"
lemma varposs_imp_poss:
assumes "p ∈ varposs t"
shows "p ∈ poss t"
using assms by (induct t arbitrary: p) auto
lemma finite_varposs:
"finite (varposs t)"
by (induct t) auto
lemma poss_simps [symmetric, simp]:
"poss t = funposs t ∪ varposs t"
"poss t = varposs t ∪ funposs t"
"funposs t = poss t - varposs t"
"varposs t = poss t - funposs t"
by (induct_tac [!] t) auto
lemma finite_poss [simp]:
"finite (poss t)"
by (subst poss_simps [symmetric]) (metis finite_Un finite_funposs finite_varposs)
text ‹The subterm relation is strongly normalizing.›
lemma SN_supt:
"SN {⊳}"
unfolding SN_iff_wf by (rule wf_subset) (auto intro: supt_size)
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 varposs_iff:
"p ∈ varposs t ⟷ (∃x. p ∈ poss t ∧ t |_ p = Var x)"
by (induct t arbitrary: p) auto
lemma funposs_fun_conv:
assumes "p ∈ funposs t"
shows "∃ f ts. t |_ p = Fun f ts"
proof (cases "t |_ p")
case (Var x)
have p_in_t: "p ∈ poss t" using funposs_imp_poss[OF assms].
then have "p ∈ poss t - funposs t" using Var(1) varposs_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 Empty thus ?thesis using Fun by auto
next
case (PCons 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: PCons)
from Fun(1) [OF mem p' this]
show ?thesis by (auto simp: PCons i)
qed
qed simp
text ‹
A \emph{context} is a term containing exactly one \emph{hole}.
›
datatype (funs_ctxt: 'f, vars_ctxt: 'v) ctxt =
Hole ("□") |
More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
context
fixes shp :: "'f ⇒ 'f"
begin
interpretation sharp_syntax .
fun sharp_term :: "('f, 'v) term ⇒ ('f, 'v) term"
where
"sharp_term (Var x) = Var x" |
"sharp_term (Fun f ss) = Fun (♯ f) ss"
fun sharp_ctxt :: "('f, 'v) ctxt ⇒ ('f, 'v) ctxt"
where
"sharp_ctxt □ = □" |
"sharp_ctxt (More f ss⇩1 C ss⇩2) = More (♯ f) ss⇩1 C ss⇩2"
abbreviation sharp_sig :: "('f × nat) set ⇒ ('f × nat) set"
where
"sharp_sig ≡ image (λ(f, n). (♯ f, n))"
end
context sharp_syntax
begin
adhoc_overloading
SHARP "sharp_term shp" "sharp_ctxt shp" "sharp_sig shp"
end
text ‹
Replacing the hole in a context~@{text C} by a term ~@{text t} is called, application of @{text C}
to @{text t}.
›
fun
ctxt_apply_term :: "('f, 'v) ctxt ⇒ ('f, 'v) term ⇒ ('f, 'v) term" ("_⟨_⟩" [1000, 0] 1000)
where
"□⟨s⟩ = s" |
"(More f ss1 C ss2)⟨s⟩ = Fun f (ss1 @ C⟨s⟩ # ss2)"
lemma ctxt_eq [simp]:
"(C⟨s⟩ = C⟨t⟩) = (s = t)" by (induct C) auto
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}
›
fun
ctxt_compose :: "('f, 'v) ctxt ⇒ ('f, 'v) ctxt ⇒ ('f, 'v) ctxt" (infixl "∘⇩c" 75)
where
"□ ∘⇩c D = D" |
"(More f ss1 C ss2) ∘⇩c D = More f ss1 (C ∘⇩c D) ss2"
interpretation ctxt_monoid_mult: monoid_mult "□" "op ∘⇩c"
proof
fix C D E :: "('f, 'v) ctxt"
show "C ∘⇩c D ∘⇩c E = C ∘⇩c (D ∘⇩c E)" by (induct C) simp_all
show "□ ∘⇩c C = C" by simp
show "C ∘⇩c □ = C" by (induct C) simp_all
qed
instantiation ctxt :: (type, type) monoid_mult
begin
definition [simp]: "1 = □"
definition [simp]: "op * = op ∘⇩c"
instance by (intro_classes) (simp_all add: ac_simps)
end
lemma ctxt_ctxt_compose [simp]: "(C ∘⇩c D)⟨t⟩ = C⟨D⟨t⟩⟩" by (induct C) simp_all
lemmas ctxt_ctxt = ctxt_ctxt_compose [symmetric]
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 Empty
thus ?thesis using Fun by auto
next
case (PCons i q)
with Fun(2) have i: "i < length ts" and q: "q ∈ poss (ts ! i)" by auto
hence "ts ! i ∈ set ts" by auto
from Fun(1)[OF this q] PCons 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)
thus ?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 (Empty s)
have "□⟨s|_ε⟩ = s" by simp
thus ?case by best
next
case (PCons 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 PCons 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› ..
thus ?case by best
qed
lemma ctxt_imp_supteq [simp]:
shows "C⟨t⟩ ⊵ t" by (induct C) auto
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
thus ?thesis unfolding ‹s|_p = t› using ctxt_imp_supteq by auto
qed
lemma subt_at_imp_supteq:
assumes "p ∈ poss s" shows "s ⊵ s|_p"
proof -
have "s|_p = s|_p" by auto
with assms show ?thesis by (rule subt_at_imp_supteq')
qed
lemma funposs_ctxt_apply_term:
assumes "p ∈ funposs C⟨s⟩"
shows "(∀t. p ∈ funposs C⟨t⟩) ∨ (∃q. p = (hole_pos C) <#> q ∧ q ∈ funposs s)"
using assms
proof (induct p arbitrary: C)
case Empty then show ?case by (cases C) auto
next
case (PCons i p)
then show ?case
proof (cases C)
case (More f bef C' aft)
with PCons(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 ∈ funposs C'⟨s⟩" using More PCons by auto
from PCons(1)[OF this] More C' show ?thesis by auto
qed (insert More PCons, auto simp: nth_append)
qed auto
qed
lemma supteq_ctxtE[elim]:
assumes "s ⊵ t" obtains C where "s = C⟨t⟩"
using assms proof (induct arbitrary: thesis)
case (refl s)
have "s = □⟨s⟩" by simp
from refl[OF this] show ?case .
next
case (subt u ss t f)
then obtain C where "u = C⟨t⟩" by auto
from split_list[OF ‹u ∈ set ss›] obtain ss1 and ss2 where "ss = ss1 @ u # ss2" by auto
hence "Fun f ss = (More f ss1 C ss2)⟨t⟩" using ‹u = C⟨t⟩› by simp
with subt show ?case by best
qed
lemma ctxt_supteq[intro]:
assumes "s = C⟨t⟩" shows "s ⊵ t"
proof (cases C)
case Hole thus ?thesis using assms by auto
next
case (More f ss1 D ss2)
with assms have s: "s = Fun f (ss1 @ D⟨t⟩ # ss2)" (is "_ = Fun _ ?ss") by simp
have "D⟨t⟩ ∈ set ?ss" by simp
moreover have "D⟨t⟩ ⊵ t" by (induct D) auto
ultimately show ?thesis unfolding s ..
qed
lemma supteq_ctxt_conv: "(s ⊵ t) = (∃C. s = C⟨t⟩)" by auto
lemma supt_ctxtE[elim]:
assumes "s ⊳ t" obtains C where "C ≠ □" and "s = C⟨t⟩"
using assms
proof (induct arbitrary: thesis)
case (arg s ss f)
from split_list[OF ‹s ∈ set ss›] obtain ss1 and ss2 where ss: "ss = ss1 @ s # ss2" by auto
let ?C = "More f ss1 □ ss2"
have "?C ≠ □" by simp
moreover have "Fun f ss = ?C⟨s⟩" by (simp add: ss)
ultimately show ?case using arg by best
next
case (subt s ss t f)
then obtain C where "C ≠ □" and "s = C⟨t⟩" by auto
from split_list[OF ‹s ∈ set ss›] obtain ss1 and ss2 where ss: "ss = ss1 @ s # ss2" by auto
have "More f ss1 C ss2 ≠ □" by simp
moreover have "Fun f ss = (More f ss1 C ss2)⟨t⟩" using ‹s = C⟨t⟩› by (simp add: ss)
ultimately show ?case using subt(4) by best
qed
lemma supt_supteq_trans[trans]:
assumes "s ⊳ t" and "t ⊵ u" shows "s ⊳ u"
proof (cases "t = u")
assume "t = u" with assms show ?thesis by simp
next
assume "t ≠ u"
with assms have "t ⊳ u" by auto
with ‹s ⊳ t› show ?thesis by (rule supt_trans)
qed
lemma supteq_supt_trans[trans]:
assumes "s ⊵ t" and "t ⊳ u" shows "s ⊳ u"
proof (cases "s = t")
assume "s = t" with assms show ?thesis by simp
next
assume "s ≠ t"
with assms have "s ⊳ t" by auto
thus ?thesis using ‹t ⊳ u› by (rule supt_trans)
qed
lemma ctxt_supt[intro 2]:
assumes "C ≠ □" and "s = C⟨t⟩" shows "s ⊳ t"
proof (cases C)
case Hole with assms show ?thesis by simp
next
case (More f ss1 D ss2)
with assms have s: "s = Fun f (ss1 @ D⟨t⟩ # ss2)" by simp
have "D⟨t⟩ ∈ set (ss1 @ D⟨t⟩ # ss2)" by simp
hence "s ⊳ D⟨t⟩" unfolding s ..
also have "D⟨t⟩ ⊵ t" by (induct D) auto
finally show "s ⊳ t" .
qed
lemma supt_not_refl[elim!]:
assumes "t ⊳ t" shows False
proof -
from assms have "t ≠ t" by auto
thus False by simp
qed
lemma supt_ctxt_conv: "(s ⊳ t) = (∃C. C ≠ □ ∧ s = C⟨t⟩)" (is "_ = ?rhs")
proof
assume "s ⊳ t"
hence "s ⊵ t" and "s ≠ t" by auto
from ‹s ⊵ t› obtain C where "s = C⟨t⟩" by auto
with ‹s ≠ t› have "C ≠ □" by auto
with ‹s = C⟨t⟩› show "?rhs" by auto
next
assume "?rhs" thus "s ⊳ t" by auto
qed
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 = ε" hence "s = t" using ‹s|_p = t› by simp
thus 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 supteq_not_supt [elim]:
assumes "s ⊵ t" and "¬ (s ⊳ t)"
shows "s = t"
using assms by (induct) auto
lemma supteq_not_supt_conv [simp]:
"{⊵} - {⊳} = Id" by auto
lemma subt_at_nepos_neq:
assumes "i<#p ∈ poss s" shows "s|_(i<#p) ≠ s"
proof (cases s)
fix x assume "s = Var x"
hence "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
hence "ss!i ∈ set ss" by simp
hence "Fun f ss ⊳ ss!i" by (rule supt.arg)
hence "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 nectxt_imp_supt_ctxt: "C ≠ □ ⟹ C⟨t⟩ ⊳ t"
proof (induct C)
case Hole thus ?case by auto
next
case (More f ls C rs) thus ?case
proof (cases "C = □")
case True
hence a: "(More f ls C rs)⟨t⟩ = Fun f (ls @ t#rs)" by auto
hence "t ∈ set (ls @ t#rs)" by auto
hence "Fun f (ls@t#rs) ⊳ t" by (rule supt.arg)
with a show ?thesis by auto
next
case False
from ‹C ≠ □› and ‹C ≠ □ ⟹ C⟨t⟩ ⊳ t› have b: "C⟨t⟩ ⊳ t" by simp
have c: "(More f ls C rs)⟨t⟩ = Fun f (ls @ C⟨t⟩#rs)" by auto
have d: "C⟨t⟩ ∈ set (ls @ C⟨t⟩#rs)" by auto
have "Fun f (ls @ C⟨t⟩#rs) ⊳ t"
using supt.arg[where s = "C⟨t⟩" and ss = "ls@C⟨t⟩#rs",OF d] b by (rule supt_trans)
with c show ?thesis by auto
qed
qed
lemma supt_var: "¬ (Var x ⊳ u)"
proof
assume "Var x ⊳ u"
then obtain C where "C ≠ □" and "Var x = C⟨u⟩" ..
thus False by (cases C) auto
qed
lemma supt_const: "¬ (Fun f [] ⊳ u)"
proof
assume "Fun f [] ⊳ u"
then obtain C where "C ≠ □" and "Fun f [] = C⟨u⟩" ..
thus False by (cases C) auto
qed
lemma supteq_var_imp_eq:
"(Var x ⊵ t) = (t = Var x)" (is "_ = (_ = ?x)")
proof
assume "t = Var x" thus "Var x ⊵ t" by auto
next
assume st: "?x ⊵ t"
from st obtain C where "?x = C⟨t⟩" by best
thus "t = ?x" by (cases C) auto
qed
lemma Var_supt [elim!]:
assumes "Var x ⊳ t" shows P
using assms supt_var[of x t] by simp
lemma Fun_supt [elim]:
assumes "Fun f ts ⊳ s" obtains t where "t ∈ set ts" and "t ⊵ s"
using assms by (cases) (auto simp: supt_supteq_conv)
lemma subterm_induct:
assumes "⋀t. ∀s⊲t. P s ⟹ P t"
shows [case_names subterm]: "P t"
proof -
have "∀s⊴t. P s"
proof (induct t)
case (Var x)
have "∀s⊲Var x. P s" by blast
with assms show ?case by (auto simp: supteq_var_imp_eq)
next
case (Fun f ts)
have "∀s⊲Fun f ts. P s"
proof (intro allI impI)
fix s assume "Fun f ts ⊳ s"
then obtain t where "t ∈ set ts" and "t ⊵ s" ..
with Fun show "P s" by simp
qed
with assms show ?case by (auto simp: subterm.order.order_iff_strict)
qed
thus ?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)
thus ?case by (induct ts, auto)
qed simp
text ‹Applying a substitution to every term of a given set.›
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 ∉ funposs 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_PCons 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')
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"
hence "x ∈ subst_domain σ" by (simp add: subst_domain_def)
with ‹subst_domain σ = {}› show False by simp
qed
qed
next
assume "σ = Var" thus "subst_domain σ = {}" by simp
qed
fun
subst_apply_ctxt :: "('f, 'v) ctxt ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'w) ctxt" (infixl "⋅⇩c" 67)
where
"□ ⋅⇩c σ = □" |
"(More f ss1 D ss2) ⋅⇩c σ = More f (map (λt. t ⋅ σ) ss1) (D ⋅⇩c σ) (map (λt. t ⋅ σ) ss2)"
lemma subst_apply_term_ctxt_apply_distrib [simp]:
"C⟨t⟩ ⋅ μ = (C ⋅⇩c μ)⟨t ⋅ μ⟩"
by (induct C) auto
lemma subst_compose_ctxt_compose_distrib [simp]:
"(C ∘⇩c D) ⋅⇩c σ = (C ⋅⇩c σ) ∘⇩c (D ⋅⇩c σ)"
by (induct C) auto
lemma ctxt_compose_subst_compose_distrib [simp]:
"C ⋅⇩c (σ ∘⇩s τ) = (C ⋅⇩c σ) ⋅⇩c τ"
by (induct C) (auto)
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
thus ?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_PCons_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 (Var x) thus ?case by auto
next
case (Fun f ts)
show ?case
proof (cases p)
case Empty
thus ?thesis by auto
next
case (PCons 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 PCons by auto
qed
qed
lemma subt_at_pos_diff:
assumes "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
thus ?r
proof (induct p arbitrary: t)
case Empty
thus ?case by auto
next
case (PCons i p t)
then obtain f ts where t: "t = Fun f ts" by (cases t, auto)
note IH = PCons[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
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 0 show ?case by simp
next
case (Suc n)
hence 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
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])
thus ?thesis by simp
qed
lemma poss_PCons_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" 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
thus "t |_ p' ⊳ t |_ p" unfolding p'' subt_at_append[OF p'] .
qed
lemma less_eq_pos_imp_supt_eq:
assumes less_eq: "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
thus "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 True
thus ?thesis by force
next
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
}
thus ?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
hence "(s⋅σ)⋅τ = u" unfolding ‹s⋅σ = t› .
hence "s⋅(σ ∘⇩s τ) = u" by simp
thus ?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
hence x: "x ∈ V = True" using assms by auto
show ?thesis unfolding x using True by simp
next
case False
hence x: "x ∉ subst_domain (σ)" .
show ?thesis unfolding notin_subst_domain_imp_Var[OF x] if_cancel ..
qed
}
hence "⋀x.(if x ∈ V then σ x else Var x) = (if x ∈ subst_domain σ then σ x else Var x)" .
hence "⋀x.(λx. if x ∈ V then σ x else Var x) x = (λx. if x ∈ subst_domain σ then σ x else Var x) x" .
hence "⋀x. (λx. if x ∈ V then σ x else Var x) x = σ x" by (auto simp: subst_domain_def)
hence "(λx. if x ∈ V then σ x else Var x) = σ" by (rule ext)
hence "(σ) |s V = σ" by (simp add: subst_restrict_def)
thus ?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
thus "x ∈ ?R t"
proof
assume "x ∈ vars_term (σ y)"
thus ?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)
hence "(λy. if y ∈ V then σ y else Var y) = (λy. Var y)" by simp
hence 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" thus ?thesis using ‹x ∉ subst_domain σ› by (auto simp: subst_domain_def)
next
assume "y ≠ x" thus ?thesis using A by simp
qed
}
hence "⋀y. (if y ∈ {x} ∪ V then σ y else Var y) = Var y" by simp
thus ?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)
hence "V ∩ subst_domain σ = {}" by simp
with insertI have "σ |s V = Var" by simp
thus ?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 vars_term_subset_subst_eq:
assumes "vars_term t ⊆ vars_term s"
and "s ⋅ σ = s ⋅ τ"
shows "t ⋅ σ = t ⋅ τ"
using assms by (induct t) (induct s, auto)
lemma var_cond_stable:
assumes "vars_term r ⊆ vars_term l"
shows "vars_term (r ⋅ μ) ⊆ vars_term (l ⋅ μ)"
proof
fix y
assume r: "y ∈ vars_term (r ⋅ μ)"
then obtain z t where z:"z ∈ vars_term r" and μz:"μ z = t" and t:"y ∈ vars_term t"
by (induct r, auto)
from z assms have "z ∈ vars_term l" by auto
with μz t show "y ∈ vars_term (l ⋅ μ)" by (induct l, auto)
qed
lemma supteq_subst [simp, intro]:
assumes "s ⊵ t" shows "s ⋅ σ ⊵ t ⋅ σ"
using assms
proof (induct rule: supteq.induct)
case (subt u ss t f)
from ‹u ∈ set ss› have "u ⋅ σ ∈ set (map (λt. t ⋅ σ) ss)" "u ⋅ σ ⊵ u ⋅ σ" by auto
hence "Fun f ss ⋅ σ ⊵ u ⋅ σ" unfolding subst_apply_term.simps by blast
from this and ‹u ⋅ σ ⊵ t ⋅ σ› show ?case by (rule supteq_trans)
qed auto
lemma supt_subst [simp, intro]:
assumes "s ⊳ t" shows "s ⋅ σ ⊳ t ⋅ σ"
using assms
proof (induct rule: supt.induct)
case (arg s ss f)
then have "s ⋅ σ ∈ set (map (λt. t ⋅ σ) ss)" by simp
then show ?case unfolding subst_apply_term.simps by (rule supt.arg)
next
case (subt u ss t f)
from ‹u ∈ set ss› have "u ⋅ σ ∈ set (map (λt. t ⋅ σ) ss)" by simp
then have "Fun f ss ⋅ σ ⊳ u ⋅ σ" unfolding subst_apply_term.simps by (rule supt.arg)
with ‹u ⋅ σ ⊳ t ⋅ σ› show ?case by (metis supt_trans)
qed
lemma instance_no_supt_imp_no_supt:
assumes "¬ s ⋅ σ ⊳ t ⋅ σ"
shows "¬ s ⊳ t"
proof (rule ccontr)
assume "¬ ¬ s ⊳ t"
have "s ⊳ t ⟹ s ⋅ σ ⊳ t ⋅ σ" by (rule supt_subst)
with ‹¬ ¬ s ⊳ t› have "s ⋅ σ ⊳ t ⋅ σ" by simp
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)] .
hence "Fun f ss ⊳ Var x" by cases auto
from supt_subst [OF this]
show ?thesis by simp
qed
fun funas_ctxt :: "('f, 'v) ctxt ⇒ 'f sig"
where
"funas_ctxt Hole = {}" |
"funas_ctxt (More f ss1 D ss2) = {(f, Suc (length (ss1 @ ss2)))}
∪ funas_ctxt D ∪ ⋃(set (map funas_term (ss1 @ ss2)))"
lemma funas_term_ctxt_apply [simp]:
"funas_term (C⟨t⟩) = funas_ctxt C ∪ funas_term t"
proof (induct t)
case (Var x) show ?case by (induct C) auto
next
case (Fun f ts) show ?case by (induct C arbitrary: f ts) auto
qed
lemma funas_term_subst:
"funas_term (t ⋅ σ) = funas_term t ∪ ⋃(funas_term ` σ ` vars_term t)"
by (induct t) auto
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
hence "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
}
thus ?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
thus ?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)
hence "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"
hence "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]:
assumes "t ∈ set ts" shows "Fun f ts ⊵ t"
using assms 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]:
assumes "t = (More f ss1 D ss2)⟨t⟩" (is "_ = ?C⟨_⟩")
shows "False"
proof -
have "?C ≠ □" by auto
from this and assms have "t ⊳ t" by (rule ctxt_supt)
thus 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 supteq_imp_funas_term_subset [simp]:
assumes "s ⊵ t" shows "funas_term t ⊆ funas_term s"
using assms by (induct) auto
lemma funas_ctxt_compose [simp]:
"funas_ctxt (C ∘⇩c D) = funas_ctxt C ∪ funas_ctxt D"
by (induct C) 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) thus ?case by (simp add: subst_restrict_def)
next
case (Fun f ts)
hence "∀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)
hence 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)
hence "∃D f ss1 ss2. C = D ∘⇩c (More f ss1 □ ss2)"
proof (induct E arbitrary: C g ts1 ts2)
case Hole hence "C = □ ∘⇩c (More g ts1 □ ts2)" by simp
thus ?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
thus ?case by best
qed
thus ?thesis using assms by auto
qed
lemma funas_ctxt_subst [simp]:
"funas_ctxt (C ⋅⇩c σ) = funas_ctxt C ∪ ⋃(funas_term ` σ ` vars_ctxt C)"
proof (induct C)
case (More f bef C aft)
let ?n = "Suc (length bef + length aft)"
let ?σ = "map (λ t. t ⋅ σ)"
let ?C = "More f bef C aft"
obtain ba where ba: "ba = bef @ aft" by auto
let ?fba = "⋃(funas_term ` (set (?σ ba)))"
let ?fba' = "⋃ {funas_term (ba ! i ⋅ σ) | i. i < length ba}"
let ?fba'' = "⋃(funas_term ` (set ba)) ∪ ⋃(funas_term ` σ ` ⋃(vars_term ` (set ba)))"
let ?fC = "funas_ctxt (C ⋅⇩c σ)"
let ?fC' = "funas_ctxt C ∪ ⋃(funas_term ` σ ` vars_ctxt C)"
have "?fba = ?fba'" unfolding set_conv_nth by auto
also have "... = ?fba''" unfolding funas_term_subst set_conv_nth by auto
finally have fba: "?fba = ?fba''" .
have "funas_ctxt (?C ⋅⇩c σ) = {(f,?n)} ∪ ?fC ∪ ?fba" by (simp add: ba)
also have "... = {(f,?n)} ∪ ?fC' ∪ ?fba''" unfolding More fba ..
finally have id: "funas_ctxt (?C ⋅⇩c σ) = {(f,?n)} ∪ ?fC' ∪ ?fba''" .
show ?case unfolding id by (auto simp: ba)
qed simp
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) thus ?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"
hence i: "i < length (map Var vs)" by simp
hence 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"
unfolding map_of_nth_zip_Some [OF ‹distinct vs› ‹length vs ≤ length ss› len] by simp
finally show "?ss!i = ss!i" by simp
qed
ultimately show ?thesis by (rule nth_equalityI)
qed
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))"
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)
hence "⋀ 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)
thus ?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)
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)
hence 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+
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 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 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
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"
hence "ls ! i ∈ set ls" by simp
from Fun(1)[OF this linear[OF i] weak_match[OF i] match[OF i]]
have "∃ τ. ?cond τ i" .
}
hence "∀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, intro allI impI)
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 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_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"
hence "ss ! i ∈ set ss" by auto
from Fun(1)[OF this rec[OF i] lin[OF this]]
have "∃ u τ. ?p i u τ" .
}
hence "∀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 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
hence 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
hence 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 distinct_take_drop[OF dist i] have "distinct(?vs1@?vs2)" .
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 variants_imp_bij_betw_vars:
assumes "s ⋅ σ = t" and "t ⋅ τ = s"
shows "bij_betw (the_Var ∘ σ) (vars_term s) (vars_term t)"
proof -
have [simp]: "(the_Var ∘ σ) ` vars_term s = vars_term t"
using variants_imp_image_vars_term_eq [OF assms] by simp
then have "card (vars_term t) ≤ card (vars_term s)"
by (metis card_image_le finite_vars_term)
moreover have "(the_Var ∘ τ) ` vars_term t = vars_term s"
using variants_imp_image_vars_term_eq [OF assms(2, 1)] by simp
ultimately have "card (vars_term t) = card (vars_term s)"
by (metis card_image_le eq_iff finite_vars_term)
then have "card ((the_Var ∘ σ) ` vars_term s) = card (vars_term s)" by simp
from finite_card_eq_imp_bij_betw [OF _ this]
show ?thesis by simp
qed
text ‹When two terms are substitution instances of each other, then
there is a variable renaming (with finite domain) between them.›
lemma variants_imp_renaming:
fixes s t :: "('f, 'v) term"
assumes "s ⋅ σ = t" and "t ⋅ τ = s"
shows "∃f. bij f ∧ finite {x. f x ≠ x} ∧ s ⋅ (Var ∘ f) = t"
proof -
from variants_imp_bij_betw_vars [OF assms, THEN bij_betw_extend, of UNIV]
obtain g where *: "∀x∈vars_term s. g x = (the_Var ∘ σ) x"
and "finite {x. g x ≠ x}"
and "bij g" by auto
moreover have "∀x∈vars_term s. (Var ∘ g) x = σ x"
proof
fix x
assume "x ∈ vars_term s"
with * have "g x = (the_Var ∘ σ) x" by simp
with variants_imp_is_Var [OF assms] and ‹x ∈ vars_term s›
show "(Var ∘ g) x = σ x" by simp
qed
moreover then have "s ⋅ (Var ∘ g) = t"
using ‹s ⋅ σ = t› by (auto simp: term_subst_eq_conv)
ultimately show ?thesis by blast
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 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_map_funs_term [simp]:
"linear_term (map_funs_term f t) = linear_term t"
by (induct t) simp_all
abbreviation "map_vars_term f ≡ term.map_term (λx. x) f"
lemma map_vars_term_as_subst:
"map_vars_term f t = t ⋅ (λ x. Var (f x))"
by (induct t) simp_all
lemma map_vars_term_eq:
"map_vars_term f s = s ⋅ (Var ∘ f)"
by (induct s) auto
lemma ground_map_vars_term [simp]:
"ground (map_vars_term f t) = ground t"
by (induct t) simp_all
lemma map_vars_term_subst [simp]:
"map_vars_term f (t ⋅ σ) = t ⋅ (λ x. map_vars_term f (σ x))"
by (induct t) simp_all
lemma map_vars_term_compose:
"map_vars_term m1 (map_vars_term m2 t) = map_vars_term (m1 o m2) t"
by (induct t) simp_all
lemma map_vars_term_id [simp]:
"map_vars_term id t = t"
by (induct t) (auto intro: map_idI)
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)
thus ?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)
thus ?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
subst_apply_term.simps term.simps
by (rule rev[OF refl x])
qed
finally show "t = t ⋅ σ ⋅ τ" by simp
qed
qed
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 apply_subst_map_vars_term:
"map_vars_term m t ⋅ σ = t ⋅ (σ ∘ m)"
by (induct t) (auto)
lemma size_subst: "size t ≤ size (t ⋅ σ)"
proof (induct t)
case (Var x)
thus ?case by (cases "σ x") auto
next
case (Fun f ss)
thus ?case
by (simp add: o_def, induct ss, force+)
qed
lemma size_ctxt: "size t ≤ size (C⟨t⟩)"
by (induct C) simp_all
lemma size_ne_ctxt: "C ≠ □ ⟹ size t < size (C⟨t⟩)"
by (induct C) force+
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
}
thus ?case by auto
qed simp
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 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
hence len: "length ts = length ?bca" by auto
note id = ts[unfolded map_nth_eq_conv[OF len], THEN spec, THEN mp]
let ?i = "length bef"
from len have i: "?i < length ts" by auto
from id[of ?i] 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 ground_vars_term_empty:
"ground t ⟷ vars_term t = {}"
by (induct t) simp_all
lemma ground_subst [simp]:
"ground (t ⋅ σ) ⟷ (∀x ∈ vars_term t. ground (σ x))"
by (induct t) simp_all
lemma ground_subst_apply:
assumes "ground t"
shows "t ⋅ σ = t"
proof -
have "t = t ⋅ Var" by simp
also have "… = t ⋅ σ"
by (rule term_subst_eq, insert assms[unfolded ground_vars_term_empty], auto)
finally show ?thesis by simp
qed
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)
lemma funas_term_map_vars_term [simp]:
"funas_term (map_vars_term τ t) = funas_term t"
by (induct t) auto
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"
hence "t = Var x" by (cases t, auto)
}
thus ?thesis by auto
qed
next
case (Fun f ts)
show ?case (is "?L = ?R")
proof -
{
fix i
assume "i < length ts"
hence "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
}
hence "?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
hence "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
}
hence 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
}
hence 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]
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) thus ?case by auto
next
case (Fun g ts)
hence "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}"
hence "Fun g ts ⊵ x" by simp
hence "Fun g ts ⊳ x ∨ Fun g ts = x" by auto
thus "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
hence "x ∈ {a. u ⊵ a}" by simp
with ‹u ∈ set ts› have "x ∈ (⋃u∈set ts. {a. u ⊵ a})" by auto
thus ?thesis unfolding ‹ts = ss› by simp
next
assume "Fun g ts = x" thus ?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}"
hence "x ∈ (⋃u∈set ss. {a. u ⊵ a}) ∨ x = Fun g ts" by auto
thus "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
thus ?thesis unfolding ‹ts = ss› by auto
next
assume "x = Fun g ts" thus ?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)
hence "⋀s. (Var x ⊵ s) = (Var x = s)" using supteq.cases by best
thus ?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 (PCons 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 PCons(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 Empty show ?case by auto
next
case (PCons i p t)
from PCons(2) obtain g ts where t: "t = Fun g ts" by (cases t, auto)
from PCons 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 (PCons i q)
from subt_at_nepos_imp_supt[OF p[unfolded PCons], unfolded PCons[symmetric]
, unfolded id] have False by simp
thus ?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
hence 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 Empty show ?case by simp
next
case (PCons i p t)
from PCons(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 PCons(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_pos_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 (PCons k p)
from PCons(3) obtain f ts where t: "t = Fun f ts" and k: "k < length ts" by (cases t, auto)
note PCons = PCons[unfolded t]
let ?p1 = "p <#> i <# q1" let ?p2 = "p <#> j <# q2"
from PCons(2) PCons(3) have "?p1 ∈ poss (ts ! k)" "?p2 ∈ poss (ts ! k)" by auto
from PCons(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 Empty
from Empty(2) obtain f ts where t: "t = Fun f ts" and j: "j < length ts" by (cases t, auto)
note Empty = Empty[unfolded t]
from Empty 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_pos_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 (PCons k p)
from PCons(3) obtain f ts where t: "t = Fun f ts" and k: "k < length ts" by (cases t, auto)
note PCons = PCons[unfolded t]
let ?p1 = "p <#> i <# q1" let ?p2 = "p <#> j <# q2"
from PCons(2) PCons(3) have "?p1 ∈ poss (ts ! k)" "?p2 ∈ poss (ts ! k)" by auto
from PCons(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 Empty
from Empty(2) obtain f ts where t: "t = Fun f ts" and j: "j < length ts" by (cases t, auto)
note Empty = Empty[unfolded t]
from Empty 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_pos_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 (PCons k p)
from PCons(2) obtain f ts where t: "t = Fun f ts" and k: "k < length ts" by (cases t, auto)
note PCons = PCons[unfolded t]
let ?p1 = "p <#> i <# q1" let ?p2 = "p <#> j <# q2"
from PCons(2) have "?p1 ∈ poss (ts ! k)" by auto
from PCons(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 Empty
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
thus ?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'"
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'"
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 (PCons i p)
from PCons(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 PCons(1)[OF p] i by (auto simp: nth_append min)
next
case Empty show ?case by simp
qed
qed
lemma "p ∈ poss t ⟹ hole_pos(ctxt_of_pos_term p t) = p"
by (induct p t rule: ctxt_of_pos_term.induct) auto
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 position_cases[of p' "hole_pos C"]])
assume "p' ≤ hole_pos C"
thus ?thesis using hole_pos_poss by (metis less_eq_pos_def poss_append_poss)
next
assume or:"hole_pos C < p' ∨ p' ⊥ hole_pos C"
show ?thesis proof(rule disjE[OF or])
assume "hole_pos C < 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
thus ?thesis using dec hole_pos_poss_conv by auto
next
assume "p' ⊥ hole_pos C"
hence 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
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 ≤ 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 "¬ (p > hole_pos C)"
proof(rule notI)
assume "p > hole_pos C"
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:"¬ (p > hole_pos C)"
unfolding hole_pos_subst[of C σ] by auto
from n a have c:"¬ (p ≤ hole_pos C)" unfolding less_pos_def using less_eq_hole_pos_in_possc by blast
with position_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
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 Hole thus ?case by auto
next
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"
hence "t ∈ set (bef @ C⟨s⟩ # aft)" by auto
hence ?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
lemma subteq_Var_imp_in_vars_term:
"r ⊵ Var x ⟹ x ∈ vars_term r"
proof (induct r rule: term.induct)
case (Var y) hence "x = y" by (cases rule: supteq.cases) auto
thus ?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
thus ?case
proof
assume "Fun f ss = Var x" thus ?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
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 (PCons 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 PCons have "linear_term (ts ! i)" and "ts ! i |_ p = Var x" by auto
have id: "replace_at (ts ! i ⋅ σ) p (τ x) = ts ! i ⋅ τ" using PCons 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 PCons(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 PCons(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
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 (PCons i p)
then obtain f bef D aft where C: "C = More f bef D aft" by (cases C, auto)
from PCons(2) have "hole_pos D = p <#> q" unfolding C by simp
from PCons(1)[OF this] have id: "(D |_c p) ⟨t⟩ = D⟨t⟩ |_ p" by simp
show ?case unfolding C subt_at_ctxt.simps id using PCons(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 (PCons 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 PCons(1), insert PCons(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 Empty
show ?case
by (rule exI[of _ □], rule exI[of _ C], insert Empty, auto)
next
case (PCons i p)
then obtain f bef C' aft where C: "C = More f bef C' aft" by (cases C, auto)
from PCons(2) have "hole_pos C' = p <#> q" unfolding C by simp
from PCons(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 PCons(2) C, simp)
qed
lemma ctxt_subst_id[simp]: "C ⋅⇩c Var = C" by (induct C, auto)
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 ("op ⊳c") and
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
hence "?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)
hence supt: "C ⊳c t" by auto
thus ?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
thus ?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_varsE [elim]:
assumes "x ∈ range_vars σ"
and "⋀t. x ∈ vars_term t ⟹ t ∈ subst_range σ ⟹ P"
shows "P"
using assms by (auto simp: range_vars_def)
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
hence nmem: "x ∉ subst_domain τ" unfolding vars_subst_def by auto
hence 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
hence 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 thus ?thesis using y unfolding vars_subst_def by auto
next
case False
thus ?thesis unfolding subst_domain_def by auto
qed
thus "Var y = ?στ y"
proof
assume "y ∈ vars_subst τ"
with assms have "y ∉ subst_domain σ" by auto
thus ?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 thus ?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
hence "vars_term t = vars_term (?C⟨t |_ p⟩)" by simp
thus ?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
hence "?σ 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
hence σ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 subst_domain_compose:
"subst_domain (σ ∘⇩s τ) ⊆ subst_domain σ ∪ subst_domain τ"
unfolding subst_domain_def subst_compose_def by auto
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
thus ?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
thus ?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
hence "?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
thus "τ 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 (PCons i p t)
show ?case
proof (cases t)
case (Var x)
have "?p x ε (i <# p) t (i <# p)" using PCons(2) unfolding Var by simp
thus ?thesis by blast
next
case (Fun f ts)
with PCons(2) have i: "i < length ts" and p: "p ∈ poss (ts ! i ⋅ σ)" by auto
from PCons(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
thus ?thesis unfolding Fun by blast
next
assume "p ∈ poss (ts ! i) ∧ is_Fun (ts ! i |_ p)"
thus ?thesis using Fun i by auto
qed
qed
next
case Empty
show ?case
proof (cases t)
case (Var x)
have "?p x ε ε t ε" unfolding Var by auto
thus ?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 thus ?case by auto
next
case (Fun f ss)
show ?case
proof (cases ss)
case Nil
thus ?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) thus ?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
context
fixes shp :: "'f ⇒ 'f"
begin
interpretation sharp_syntax .
lemma sharp_term_ctxt_apply [simp]:
"C ≠ □ ⟹ ♯(C⟨t⟩) = (♯ C)⟨t⟩"
by (cases C) simp_all
lemma supt_sharp_term_subst [simp]:
"♯ s ⋅ σ ⊳ t ⟷ s ⋅ σ ⊳ t"
by (cases s) auto
end
lemma sharp_term_id [simp]:
"sharp_term id t = t"
"sharp_term (λx. x) t = t"
by (induct t) simp_all
text ‹
here we give some function 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)
fun vars_term_ms :: "('f,'v)term ⇒ 'v multiset"
where
"vars_term_ms (Var x) = {#x#}" |
"vars_term_ms (Fun f ts) = ⋃# (mset (map vars_term_ms ts))"
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)
thus ?case unfolding multiset_eq_iff by (simp add: o_def)
qed auto
lemma set_mset_vars_term_ms [simp]:
"set_mset (vars_term_ms t) = vars_term t"
by (induct t) 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 vars_term_ms_subst [simp]:
"vars_term_ms (t ⋅ σ) =
⋃# (image_mset (λ x. vars_term_ms (σ x)) (vars_term_ms t))" (is "_ = ?V t")
proof (induct t)
case (Fun f ts)
have IH: "map (λ t. vars_term_ms (t ⋅ σ)) ts = map (λ t. ?V t) ts"
by (rule map_cong[OF refl Fun])
show ?case by (simp add: o_def IH, induct ts, auto)
qed simp
lemma vars_term_ms_subst_mono:
assumes "vars_term_ms s ⊆# vars_term_ms t"
shows "vars_term_ms (s ⋅ σ) ⊆# vars_term_ms (t ⋅ σ)"
proof -
from assms[unfolded mset_subset_eq_exists_conv] obtain u where t: "vars_term_ms t = vars_term_ms s + u" by auto
show ?thesis unfolding vars_term_ms_subst unfolding t by auto
qed
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)
thus ?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
lemma supt_imp_funas_subset:
assumes "s ⊳ t"
shows "funas_term t ⊆ funas_term s"
using assms by (induct) auto
subsection ‹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
thus ?thesis unfolding mk_subst_def by auto
qed
lemma mk_subst_distinct:
assumes dist: "distinct xs"
and len: "length ls = length xs"
and i: "i < length xs"
shows "mk_subst f (zip xs ls) (xs ! i) = ls ! i"
proof -
from map_of_zip_is_None[OF len[symmetric], of "xs ! i"] i
obtain l where map: "map_of (zip xs ls) (xs ! i) = Some l" by auto
from map_of_SomeD[OF map] have "(xs ! i, l) ∈ set (zip xs ls)" by auto
from this[unfolded set_conv_nth length_zip len] obtain j where
j: "j < length xs" and id: "(xs ! i, l) = zip xs ls ! j" by auto
from arg_cong[OF id, of fst] j len have "xs ! i = xs ! j" by auto
with nth_eq_iff_index_eq[OF dist i j] have "i = j" by auto
with id j len have l: "l = ls ! i" by auto
with map show ?thesis unfolding mk_subst_def by auto
qed
lemma mk_subst_Nil [simp]:
"mk_subst d [] = d"
by (simp add: mk_subst_def)
lemma vars_term_disjoint_imp_unifier:
fixes σ :: "('f, 'v, 'w) gsubst"
assumes "vars_term s ∩ vars_term t = {}"
and "s ⋅ σ = t ⋅ τ"
shows "∃μ :: ('f, 'v, 'w) gsubst. s ⋅ μ = t ⋅ μ"
proof -
let ?μ = "λx. if x ∈ vars_term s then σ x else τ x"
have "s ⋅ σ = s ⋅ ?μ"
unfolding term_subst_eq_conv
by (induct s) (simp_all)
moreover have "t ⋅ τ = t ⋅ ?μ"
using assms(1)
unfolding term_subst_eq_conv
by (induct s arbitrary: t) (auto)
ultimately have "s ⋅ ?μ = t ⋅ ?μ" using assms(2) by simp
then show ?thesis by blast
qed
lemma ground_imp_linear_term [simp]:
"ground t ⟹ linear_term t"
by (induct t) (auto simp add: is_partition_def ground_vars_term_empty)
lemma vars_term_varposs_iff:
"x ∈ vars_term t ⟷ (∃p. p ∈ varposs 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 varposs_iff by auto
next
assume p: "?R"
then obtain p where 1: "p ∈ varposs t" and 2: "Var x = t |_ p" by auto
from varposs_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 "PCons 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_funposs:
assumes "p ∈ poss t"
and "is_Fun (t |_ p)"
shows "p ∈ funposs t"
using assms by (metis DiffI is_Var_def poss_simps(3) varposs_iff)
end