Theory First_Order_Terms.Subterm_and_Context

section ‹Subterms and Contexts›

text ‹
  We define the (proper) sub- and superterm relations on first order terms,
  as well as contexts (you can think of contexts as terms with exactly one hole,
  where we can plug-in another term).
  Moreover, we establish several connections between these concepts as well as
  to other concepts such as substitutions.
›

theory Subterm_and_Context
  imports
    Term
    "Abstract-Rewriting.Abstract_Rewriting"
begin

subsection ‹Subterms›

text ‹The ∗‹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 ∗‹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 ‹Syntactic Sugar›

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)

syntax_consts
  "_All_supteq" "_All_supt" "_All_subteq" "_All_subt" ⇌ All and
  "_Ex_supteq" "_Ex_supt" "_Ex_subteq" "_Ex_subt" ⇌ Ex

(* for parsing *)
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"

(* for printing *)
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 (=) 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 trans_supt: "trans {⊳}" by (auto simp: trans_def dest: supt_trans)


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) then show ?case by (cases "x = y") auto
next
  case (Fun f ss) then show ?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"
  then have "?t ⊳ ?t" by (auto)
  then have "?t ≠ ?t" by (auto dest: supt_neqD)
  then show 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)
  then have "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" then show "s ⊵ t ∧ s ≠ t"
  proof (induct rule: supt.induct)
    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" ..
    then have 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 (auto simp: size_simps)
next
  assume "s ⊵ t ∧ s ≠ t"
  then have "s ⊵ t" and "s ≠ t" by auto
  then show "s ⊳ t" by (induct) (auto)
qed

lemma supt_not_sym: "s ⊳ t ⟹ ¬ (t ⊳ s)"
proof
  assume "s ⊳ t" and "t ⊳ s" then have "s ⊳ s" by (rule supt_trans)
  then show False unfolding supt_supteq_conv by simp
qed

lemma supt_irrefl[iff]: "¬ t ⊳ t"
  using supt_not_sym[of t t] by auto

lemma irrefl_subt: "irrefl {⊲}" by (auto simp: irrefl_def)

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 "(⊴)" "(⊲)"
  by (unfold_locales)
    (rule supt_supteq_not_supteq, auto intro: supteq_trans supteq_antisym supt_supteq_not_supteq)


text ‹More transitivity rules.›
lemma supt_supteq_trans[trans]:
  "s ⊳ t ⟹ t ⊵ u ⟹ s ⊳ u"
  by (metis subterm.le_less_trans)

lemma supteq_supt_trans[trans]:
  "s ⊵ t ⟹ t ⊳ u ⟹ s ⊳ u"
  by (metis subterm.less_le_trans)

declare subterm.le_less_trans[trans]
declare subterm.less_le_trans[trans]

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
  then show ?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

text ‹The superterm relation is strongly normalizing.›
lemma SN_supt:
  "SN {⊳}"
  unfolding SN_iff_wf by (rule wf_subset) (auto intro: supt_size)

lemma supt_not_refl[elim!]:
  assumes "t ⊳ t" shows False
proof -
  from assms have "t ≠ t" by auto
  then 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 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
  then have "Fun f ss ⋅ σ ⊵ u ⋅ σ" unfolding eval_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 eval_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 eval_term.simps by (rule supt.arg)
  with ‹u ⋅ σ ⊳ t ⋅ σ› show ?case by (metis supt_trans)
qed


lemma subterm_induct:
  assumes "⋀t. ∀s⊲t. P s ⟹ P t"
  shows [case_names subterm]: "P t"
  by (rule wf_induct[OF wf_measure[of size], of P t], rule assms, insert supt_size, auto)


subsection ‹Contexts›

text ‹A ∗‹context› is a term containing exactly one ∗‹hole›.›

text ‹We generalize contexts to ∗‹abstract contexts› so
that arguments can be arbitrary elements.›

datatype ('f,'a) actxt =
  Hole (‹□›) | More 'f "'a list" "('f,'a) actxt" "'a list"

declare actxt.map_ident[simp]

type_synonym ('f,'v) ctxt = "('f,('f,'v) term) actxt"

fun map_ctxt where
  "map_ctxt f v □ = □"
| "map_ctxt f v (More g ls C rs) =
  More (f g) (map (map_term f v) ls) (map_ctxt f v C) (map (map_term f v) rs)"

fun vars_ctxt where
  "vars_ctxt □ = {}"
| "vars_ctxt (More f ls C rs) =
  ⋃(vars_term ` set ls) ∪ vars_ctxt C ∪ ⋃(vars_term ` set rs)"

fun funs_ctxt where
  "funs_ctxt □ = {}"
| "funs_ctxt (More f ls C rs) =
  insert f (⋃(funs_term ` set ls) ∪ funs_ctxt C ∪ ⋃(funs_term ` set rs))"

text ‹
  Interpretation of abstract context.
›

primrec intp_actxt (‹(1_⟨_;/_⟩)›[999,0,0]100) where
  "I⟨Hole;a⟩ = a"
| "I⟨More f ls C rs;a⟩ = I f (ls @ I⟨C;a⟩ # rs)"

text ‹
  We also say that we apply a context~@{term C} to a term~@{term t} when we
  replace the hole in a @{term C} by @{term t}.
›

abbreviation ctxt_apply_term (‹_⟨_⟩› [1000, 0] 1000) where
  "C⟨s⟩ ≡ Fun⟨C;s⟩"

primrec actxt_compose (infixl ‹∘⇩c› 75) where
  "Hole ∘⇩c D = D"
| "More f ls C rs ∘⇩c D = More f ls (C ∘⇩c D) rs"

lemma intp_actxt_compose: "I⟨C ∘⇩c D;a⟩ = I⟨C;I⟨D;a⟩⟩"
  by (induct C, auto)

thm intp_actxt_compose[of Fun]
abbreviation "map_args_actxt ≡ map_actxt (λx. x)"

abbreviation eval_ctxt (‹(1_⟦_⟧⇩c/ _)›[999,1,100]100) where
  "I⟦C⟧⇩c α ≡ map_args_actxt (λt. I⟦t⟧α) C"

lemma eval_ctxt_simps:
  "I⟦□⟧⇩c α = □"
  "I⟦More f ls C rs⟧⇩c α = More f [I⟦l⟧α. l ← ls] (I⟦C⟧⇩c α) [I⟦r⟧α. r ← rs]"
  using actxt.map.

lemma eval_ctxt: "I⟦C⟨s⟩⟧α = I⟨I⟦C⟧⇩c α; I⟦s⟧α⟩"
  by (induct C, auto)

text ‹Applying substitutions to contexts.›

abbreviation subst_apply_actxt (infixl ‹⋅⇩c› 67) where
  "C ⋅⇩c θ ≡ map_args_actxt (λt. t ⋅ θ) C"

lemma apply_ctxt_Var[simp]: "C ⋅⇩c Var = C"
  by (simp add: actxt.map_id0[unfolded id_def])

lemma eval_subst_ctxt: "I⟦C ⋅⇩c θ⟧⇩c ρ = I⟦C⟧⇩c I⟦θ⟧⇩s ρ"
  apply (induct C) by (auto simp: eval_subst[symmetric])

lemmas ctxt_subst_subst[simp] = eval_subst_ctxt[of Fun]

lemma ctxt_eq [simp]:
  "(C⟨s⟩ = C⟨t⟩) = (s = t)" by (induct C) auto

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+

interpretation ctxt_monoid_mult: monoid_mult "□" "(∘⇩c)"
proof
  fix C D E :: "('f, 'b) actxt"
  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 actxt :: (type, type) monoid_mult
begin
definition [simp]: "1 = □"
definition [simp]: "(*) = (∘⇩c)"
instance by (intro_classes) (simp_all add: ac_simps)
end

lemmas ctxt_ctxt_compose[simp] = intp_actxt_compose[of Fun]

lemmas ctxt_ctxt = ctxt_ctxt_compose [symmetric]

lemmas subst_apply_term_ctxt_apply_distrib [simp] = eval_ctxt[of Fun]

lemma eval_ctxt_compose_distrib:
  "I⟦C ∘⇩c D⟧⇩c σ = (I⟦C⟧⇩c σ) ∘⇩c (I⟦D⟧⇩c σ)"
  by (induct C) auto

lemmas subst_compose_ctxt_compose_distrib [simp] =
  eval_ctxt_compose_distrib[of Fun]

lemma eval_ctxt_eval_subst:
  "I⟦C⟧⇩c (I⟦σ⟧⇩s τ) = I⟦C ⋅⇩c σ⟧⇩c τ"
  by (induct C) (auto simp: eval_ctxt eval_subst eval_ctxt_compose_distrib)

lemmas ctxt_compose_subst_compose_distrib [simp] =
  eval_ctxt_eval_subst[of Fun]


subsection ‹The Connection between Contexts and the Superterm Relation›

lemma ctxt_imp_supteq [simp]:
  shows "C⟨t⟩ ⊵ t" by (induct C) auto

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
  then have "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 then show ?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 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
  then have "s ⊳ D⟨t⟩" unfolding s ..
  also have "D⟨t⟩ ⊵ t" by (induct D) auto
  finally show "s ⊳ t" .
qed

lemma supt_ctxt_conv: "(s ⊳ t) = (∃C. C ≠ □ ∧ s = C⟨t⟩)" (is "_ = ?rhs")
proof
  assume "s ⊳ t"
  then have "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" then show "s ⊳ t" by auto
qed

lemma nectxt_imp_supt_ctxt: "C ≠ □ ⟹ C⟨t⟩ ⊳ t" by auto

lemma supt_var: "¬ (Var x ⊳ u)"
proof
  assume "Var x ⊳ u"
  then obtain C where "C ≠ □" and "Var x = C⟨u⟩" ..
  then show 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⟩" ..
  then show False by (cases C) auto
qed

lemma supteq_var_imp_eq:
  "(Var x ⊵ t) = (t = Var x)" (is "_ = (_ = ?x)")
proof
  assume "t = Var x" then show "Var x ⊵ t" by auto
next
  assume st: "?x ⊵ t"
  from st obtain C where "?x = C⟨t⟩" by best
  then show "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 inj_ctxt_apply_term: "inj (ctxt_apply_term C)"
  by (auto simp: inj_on_def)

lemma ctxt_subst_eq: "(⋀x. x ∈ vars_ctxt C ⟹ σ x = τ x) ⟹ C ⋅⇩c σ = C ⋅⇩c τ"
proof (induct C)
  case (More f bef C aft)
  { fix t
    assume t:"t ∈ set bef"
    have "t ⋅ σ = t ⋅ τ" using t More(2) by (auto intro: term_subst_eq)
  }
  moreover
  { fix t
    assume t:"t ∈ set aft"
    have "t ⋅ σ = t ⋅ τ" using t More(2) by (auto intro: term_subst_eq)
  }
  moreover have "C ⋅⇩c σ = C ⋅⇩c τ" using More by auto
  ultimately show ?case by auto
qed auto


text ‹
  A ∗‹signature› is a set of function symbol/arity pairs, where the arity of a function symbol,
  denotes the number of arguments it expects.
›
type_synonym 'f sig = "('f × nat) set"

text ‹The set of all function symbol/ 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))"

lemma finite_funas_term:
  "finite (funas_term t)"
  by (induct t) auto


lemma supt_imp_funas_term_subset:
  assumes "s ⊳ t"
  shows "funas_term t ⊆ funas_term s"
  using assms by induct auto

lemma supteq_imp_funas_term_subset[simp]:
  assumes "s ⊵ t"
  shows "funas_term t ⊆ funas_term s"
  using assms by induct auto

text ‹The set of all function symbol/arity pairs occurring in a context.›
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"
  by (induct C, auto)

lemma funas_term_subst:
  "funas_term (t ⋅ σ) = funas_term t ∪ ⋃(funas_term ` σ ` vars_term t)"
  by (induct t) auto

lemma funas_ctxt_compose [simp]:
  "funas_ctxt (C ∘⇩c D) = funas_ctxt C ∪ funas_ctxt D"
  by (induct C) auto

lemma funas_ctxt_subst [simp]:
  "funas_ctxt (C ⋅⇩c σ) = funas_ctxt C ∪ ⋃(funas_term ` σ ` vars_ctxt C)"
  by (induct C, auto simp: funas_term_subst)


end