Quelle  terms.thy

theory terms

(* N. Peltier - http://membres-lig.imag.fr/peltier/ *)

imports "HOL-ex.Unification"

begin

section ‹Terms›

subsection ‹Basic Syntax›

text ‹We use the same term representation as in the Unification theory provided in Isabelle.
  are represented by binary trees built on variables and constant symbols.›
 
fun is_a_variable 
where
  "(is_a_variable (Var x)) = True" |
  "(is_a_variable (Const x)) = False" |
  "(is_a_variable (Comb x y)) = False"

fun is_a_constant
where
  "(is_a_constant (Var x)) = False" |
  "(is_a_constant (Const x)) = True" |
  "(is_a_constant (Comb x y)) = False"

fun is_compound
where
  "(is_compound (Var x)) = False" |
  "(is_compound (Const x)) = False" |
  "(is_compound (Comb x y)) = True"

definition ground_term :: "'a trm ==> bool"
where
  "(ground_term t) = (vars_of t = {})"

lemma constants_are_not_variables :
  assumes "is_a_constant x"
  shows "¬ (is_a_variable x)"
by (metis assms is_a_constant.elims(2) is_a_variable.elims(2) trm.distinct(2))

lemma constants_are_ground : 
  assumes "is_a_constant x"
  shows "ground_term x"
proof -
  from assms obtain y where "x = (Const y)" using is_a_constant.elims(2) by auto 
  then show ?thesis by (simp add: ground_term_def) 
qed

subsection ‹Positions›

text ‹We define the notion of a position together with functions to access to subterms and
  them. We establish some basic properties of these functions.›

text ‹Since terms are binary trees, positions are sequences of binary digits.›

datatype indices = Left | Right

type_synonym position = "indices list"

fun left_app
  where "left_app x = Left # x"

fun right_app
  where "right_app x = Right # x"

definition strict_prefix
where
  "strict_prefix p q = (∃r. (r ≠ []) ∧ (q = (append p r)))"

fun subterm :: "'a trm ==> position ==> 'a trm ==> bool"
  where 
    "(subterm T [] S) = (T = S)" |
    "(subterm (Var v) (first # next) S) = False" |
    "(subterm (Const c) (first # next) S) = False" |
    "(subterm (Comb x y) (Left # next) S) = (subterm x next S)" |
    "(subterm (Comb x y) (Right # next) S) = (subterm y next S)"

definition occurs_in :: "'a trm ==> 'a trm ==> bool"
  where
    "occurs_in t s = (∃p. subterm s p t)"

definition position_in :: "position ==> 'a trm ==> bool"
  where
    "position_in p s = (∃t. subterm s p t)"

fun subterms_of 
where
  "subterms_of t = { s. (occurs_in s t) }"

fun proper_subterms_of 
where
  "proper_subterms_of t = { s. ∃p. (p ≠ Nil ∧ (subterm t p s)) }"

fun pos_of 
where
  "pos_of t = { p. (position_in p t) }"
 
fun replace_subterm :: 
  "'a trm ==> position ==> 'a trm ==> 'a trm ==> bool"
  where 
    "(replace_subterm T [] u S) = (S = u) " |
    "(replace_subterm (Var x) (first # next) u S) = False" |
    "(replace_subterm (Const c) (first # next) u S) = False" |
    "(replace_subterm (Comb x y) (Left # next) u S) =
      (∃S1. (replace_subterm x next u S1) ∧ (S = Comb S1 y))" |
    "(replace_subterm (Comb x y) (Right # next) u S) =
      (∃S2. (replace_subterm y next u S2) ∧ (S = Comb x S2))"

lemma replace_subterm_is_a_function: 
  shows "∧t u v. subterm t p u ==> ∃s. replace_subterm t p v s"
proof (induction p,auto)
  next case (Cons i q)
    from ‹subterm t (Cons i q) u› obtain t1 t2 where "t = (Comb t1 t2)"
      using subterm.elims(2) by blast 
    have "i = Right ∨ i = Left" using indices.exhaust by auto 
    then show ?case
    proof
      assume "i = Right"
      from this and ‹t = (Comb t1 t2)› and ‹subterm t (Cons i q) u› have "subterm t2 q u" by auto
      from this obtain s where "replace_subterm t2 q v s" using Cons.IH [of t2 u] by auto
      from this and ‹t = (Comb t1 t2)› and ‹i = Right› have "replace_subterm t (Cons i q) v (Comb t1 s)" 
        by auto
      from this show ?case by auto
    next assume "i = Left"
      from this and ‹t = (Comb t1 t2)› and ‹subterm t (Cons i q) u› have "subterm t1 q u" by auto
      from this obtain s where "replace_subterm t1 q v s" using Cons.IH [of t1 u] by auto
      from this and ‹t = (Comb t1 t2)› and ‹i = Left› have "replace_subterm t (Cons i q) v (Comb s t2)" 
        by auto
      from this show ?case by auto
    qed
qed

text ‹We prove some useful lemmata concerning the set of variables or subterms occurring in a
 .›

lemma root_subterm:
  shows "t ∈ (subterms_of t)"
by (metis mem_Collect_eq occurs_in_def subterm.simps(1) subterms_of.simps)

lemma root_position:
  shows "Nil ∈ (pos_of t)"
by (metis mem_Collect_eq subterm.simps(1) position_in_def pos_of.simps)

lemma subterms_of_an_atomic_term:
  assumes "is_a_variable t ∨ is_a_constant t"
  shows "subterms_of t = { t }"
proof 
  show "subterms_of t ⊆ { t }"
  proof 
    fix x assume "x ∈ subterms_of t"
    then have "occurs_in x t" by auto
    then have "∃p. (subterm t p x)" unfolding occurs_in_def by auto
    from this and assms have "x = t" 
     by (metis is_a_constant.simps(3) is_a_variable.simps(3) subterm.elims(2)) 
    thus "x ∈ { t }" by auto
  qed
next 
  show "{ t } ⊆ subterms_of t"
  proof
    fix x assume "x ∈ { t }"
    then show "x ∈ subterms_of t" using root_subterm by auto
  qed
qed

lemma positions_of_an_atomic_term:
  assumes "is_a_variable t ∨ is_a_constant t"
  shows "pos_of t = { Nil }"
proof 
  show "pos_of t ⊆ { Nil }"
  proof 
    fix x assume "x ∈ pos_of t"
    then have "position_in x t" by auto
    then have "∃s. (subterm t x s)" unfolding position_in_def by auto
    from this and assms have "x = Nil" 
     by (metis is_a_constant.simps(3) is_a_variable.simps(3) subterm.elims(2)) 
    thus "x ∈ { Nil }" by auto
  qed
next 
  show "{ Nil } ⊆ pos_of t"
  proof
    fix x :: "indices list" assume "x ∈ { Nil }"
    then show "x ∈ pos_of t" using root_position by auto
  qed
qed

lemma subterm_of_a_subterm_is_a_subterm :
  assumes "subterm u q v"
  shows "∧ t. subterm t p u ==> subterm t (append p q) v"
proof (induction p)
  case Nil
    show "?case" using Nil.prems assms by auto  
  next case (Cons i p')
    from ‹subterm t (Cons i p') u› obtain t1 t2 where "t = (Comb t1 t2)"
      using subterm.elims(2) by blast 
    have "i = Right ∨ i = Left" using indices.exhaust by auto 
    then show ?case
    proof
      assume "i = Right"
      from this and ‹subterm t (Cons i p') u› and ‹t = (Comb t1 t2)›
        have "subterm t2 p' u" by auto
      from this have "subterm t2 (append p' q) v" by (simp add: Cons.IH) 
      from this and  ‹t = (Comb t1 t2)› and ‹i = Right› show "subterm t (append (Cons i p') q) v"
        by simp 
    next assume "i = Left"
      from this and ‹subterm t (Cons i p') u› and ‹t = (Comb t1 t2)›
        have "subterm t1 p' u" by auto
      from this have "subterm t1 (append p' q) v" by (simp add: Cons.IH) 
      from this and  ‹t = (Comb t1 t2)› and ‹i = Left› show "subterm t (append (Cons i p') q) v"
        by simp 
    qed
qed

lemma occur_in_subterm:
  assumes "occurs_in u t"
  assumes "occurs_in t s"
  shows "occurs_in u s"
by (meson assms(1) assms(2) occurs_in_def subterm_of_a_subterm_is_a_subterm)

lemma vars_of_subterm :
  assumes "x ∈ vars_of s"
  shows "∧ t. subterm t p s ==> x ∈ vars_of t"
proof (induction p)
  case Nil
    show "?case" using Nil.prems assms by auto  
  next case (Cons i p')
    from ‹subterm t (Cons i p') s› obtain t1 t2 where "t = (Comb t1 t2)"
      using subterm.elims(2) by blast 
    have "i = Right ∨ i = Left" using indices.exhaust by auto 
    then show ?case
    proof
      assume "i = Right"
      from this and ‹subterm t (Cons i p') s› and ‹t = (Comb t1 t2)›
        have "subterm t2 p' s" by auto
      from this have "x ∈ vars_of t2" by (simp add: Cons.IH) 
      from this and  ‹t = (Comb t1 t2)› and ‹i = Right› show ?case
        by simp 
    next assume "i = Left"
      from this and ‹subterm t (Cons i p') s› and ‹t = (Comb t1 t2)›
        have "subterm t1 p' s" by auto
      from this have "x ∈ vars_of t1" by (simp add: Cons.IH) 
      from this and  ‹t = (Comb t1 t2)› and ‹i = Left› show ?case
        by simp 
    qed
qed

lemma vars_subterm :
  assumes "subterm t p s"
  shows "vars_of s ⊆ vars_of t"
by (meson assms subsetI vars_of_subterm)

lemma vars_subterms_of :
  assumes "s ∈ subterms_of t"
  shows "vars_of s ⊆ vars_of t"
using assms occurs_in_def vars_subterm by fastforce

lemma subterms_of_a_non_atomic_term:
  shows "subterms_of (Comb t1 t2) = (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }"
proof
  show "subterms_of (Comb t1 t2) ⊆ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }"
  proof
    fix x assume "x ∈ (subterms_of (Comb t1 t2))"
    then have "occurs_in x (Comb t1 t2)" by auto
    then obtain p where "subterm (Comb t1 t2) p x" unfolding occurs_in_def by auto
    have "p = [] ∨ (∃i q. p = i #q)" using neq_Nil_conv by blast 
    then show "x ∈ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }"
    proof 
      assume "p = []" 
      from this and ‹subterm (Comb t1 t2) p x› show ?thesis by auto
    next
      assume "∃i q. p = i #q"
      then obtain i q where "p = i # q" by auto 
      have "i = Left ∨ i = Right" using indices.exhaust by blast  
      then show "x ∈ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }"
      proof 
        assume "i = Left"
        from this and ‹p = i # q› and ‹subterm (Comb t1 t2) p x›
          have "subterm t1 q x" by auto
        then have "occurs_in x t1" unfolding occurs_in_def by auto
        then show "x ∈ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }" by auto
      next
        assume "i = Right"
        from this and ‹p = i # q› and ‹subterm (Comb t1 t2) p x›
          have "subterm t2 q x" by auto
        then have "occurs_in x t2" unfolding occurs_in_def by auto
        then show "x ∈ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }" by auto
      qed
    qed
  qed
next
  show "(subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) } ⊆ subterms_of (Comb t1 t2)"
  proof
    fix x assume "x ∈ (subterms_of t1) ∪ (subterms_of t2) ∪ { (Comb t1 t2) }"
    then have "x ∈ (subterms_of t1) ∨ (x ∈ (subterms_of t2) ∨ x = (Comb t1 t2))" by auto
    thus "x ∈ subterms_of (Comb t1 t2)"
    proof
      assume "x ∈ (subterms_of t1)"
      then have "occurs_in x t1" by auto
      then obtain p where "subterm t1 p x" unfolding occurs_in_def by auto 
      then have "subterm (Comb t1 t2) (Left # p) x" by auto
      then have "occurs_in x (Comb t1 t2)" using occurs_in_def by blast
      then show "x ∈ subterms_of (Comb t1 t2)" by auto
    next        
      assume "(x ∈ (subterms_of t2) ∨ x = (Comb t1 t2))"
      then show "x ∈ subterms_of (Comb t1 t2)" 
      proof
        assume "x ∈ (subterms_of t2)"
        then have "occurs_in x t2" by auto
        then obtain p where "subterm t2 p x" unfolding occurs_in_def by auto 
        then have "subterm (Comb t1 t2) (Right # p) x" by auto
        then have "occurs_in x (Comb t1 t2)" using occurs_in_def by blast
        then show "x ∈ subterms_of (Comb t1 t2)" by auto
      next
        assume "x = (Comb t1 t2)"
        show "x ∈ subterms_of (Comb t1 t2)" using ‹x = t1 ⋅ t2› root_subterm by blast 
      qed
    qed
  qed
qed

lemma positions_of_a_non_atomic_term:
  shows "pos_of (Comb t1 t2) = (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }"
proof
  show "pos_of (Comb t1 t2) ⊆ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }"
  proof
    fix x assume "x ∈ pos_of (Comb t1 t2)"
    then have "position_in x (Comb t1 t2)" by auto
    then obtain s where "subterm (Comb t1 t2) x s" unfolding position_in_def by auto
    have "x = [] ∨ (∃i q. x = i #q)" using neq_Nil_conv by blast 
    then show "x ∈ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }"
    proof 
      assume "x = []" 
      from this and ‹subterm (Comb t1 t2) x s› show ?thesis by auto
    next
      assume "∃i q. x = i #q"
      then obtain i q where "x = i # q" by auto 
      have "i = Left ∨ i = Right" using indices.exhaust by blast  
      then show "x ∈ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }"
      proof 
        assume "i = Left"
        from this and ‹x = i # q› and ‹subterm (Comb t1 t2) x s›
          have "subterm t1 q s" by auto
        then have "position_in q t1" unfolding position_in_def by auto
        from this and ‹x = i # q› ‹i = Left›
          show "x ∈ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }" by auto
      next
        assume "i = Right"
        from this and ‹x = i # q› and ‹subterm (Comb t1 t2) x s›
          have "subterm t2 q s" by auto
        then have "position_in q t2" unfolding position_in_def by auto
        from this and ‹x = i # q› ‹i = Right›
          show "x ∈ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }" by auto
      qed
    qed
  qed
next
  show "(left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil } ⊆ pos_of (Comb t1 t2)"
  proof
    fix x assume "x ∈ (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }"
    then have "(x ∈ left_app ` (pos_of t1)) ∨ ((x ∈ (right_app ` (pos_of t2))) ∨ (x = Nil))" by auto
    thus "x ∈ pos_of (Comb t1 t2)"
    proof
      assume "x ∈ left_app ` (pos_of t1)"
      then obtain q where "x = Left # q" and "position_in q t1" by auto
      then obtain s where "subterm t1 q s" unfolding position_in_def by auto 
      then have "subterm (Comb t1 t2) (Left # q) s" by auto
      from this and ‹x = Left # q› have "position_in x (Comb t1 t2)" using position_in_def by blast
      then show "x ∈ pos_of (Comb t1 t2)" by auto
    next    
      assume "(x ∈ (right_app ` (pos_of t2))) ∨ (x = Nil)"
      then show "x ∈ pos_of (Comb t1 t2)" 
      proof
        assume "x ∈ right_app ` (pos_of t2)"
        then obtain q where "x = Right # q" and "position_in q t2" by auto
        then obtain s where "subterm t2 q s" unfolding position_in_def by auto 
        then have "subterm (Comb t1 t2) (Right # q) s" by auto
        from this and ‹x = Right # q› have "position_in x (Comb t1 t2)" using position_in_def by blast
        then show "x ∈ pos_of (Comb t1 t2)" by auto
      next
        assume "x = Nil"
        show "x ∈ pos_of (Comb t1 t2)" using ‹x = Nil› root_position by blast 
      qed
    qed
  qed
qed

lemma set_of_subterms_is_finite :
  shows "(finite (subterms_of (t :: 'a trm)))"
proof (induction t)
    case (Var x)
    then show ?case using subterms_of_an_atomic_term [of "Var x"] by simp
  next
    case (Const x)
    then show ?case using subterms_of_an_atomic_term [of "Const x"]  by simp
  next
    case (Comb t1 t2) assume "finite (subterms_of t1)" and "finite (subterms_of t2)"
    have "subterms_of (Comb t1 t2) = subterms_of t1 ∪ subterms_of t2 ∪ { Comb t1 t2 }" 
      using subterms_of_a_non_atomic_term by auto
    from this and ‹finite (subterms_of t1)› and ‹finite (subterms_of t2)›
      show "finite (subterms_of (Comb t1 t2))" by simp 
qed

lemma set_of_positions_is_finite :
  shows "(finite (pos_of (t :: 'a trm)))"
proof (induction t)
    case (Var x)
    then show ?case using positions_of_an_atomic_term [of "Var x"] by simp
  next
    case (Const x)
    then show ?case using positions_of_an_atomic_term [of "Const x"]  by simp
  next
    case (Comb t1 t2) assume "finite (pos_of t1)" and "finite (pos_of t2)"
    from ‹finite (pos_of t1)› have i: "finite (left_app ` (pos_of t1))" by auto
    from ‹finite (pos_of t2)› have ii: "finite (right_app ` (pos_of t2))" by auto
    have "pos_of (Comb t1 t2) = (left_app ` (pos_of t1)) ∪ (right_app ` (pos_of t2)) ∪ { Nil }" 
      using positions_of_a_non_atomic_term by metis
    from this and i ii show "finite (pos_of (Comb t1 t2))" by simp 
qed

lemma vars_of_instances:
  shows "vars_of (subst t σ)
    = ∪ { V. ∃x. (x ∈ (vars_of t)) ∧ (V = vars_of (subst (Var x) σ)) }"
proof (induction t)
  case (Const a)
    have "vars_of (Const a) = {}" by auto
    then have rhs_empty: "∪ { V. ∃x. (x ∈ (vars_of (Const a))) ∧ (V = vars_of (subst (Var x) σ)) } = {}" by auto
    have lhs_empty: "(subst (Const a) σ) = (Const a)" by auto
    from rhs_empty and lhs_empty show ?case by auto
  next
  case (Var a)
    have "vars_of (Var a) = { a }" by auto
    then have rhs: "∪ { V. ∃x. (x ∈ (vars_of (Var a))) ∧ (V = vars_of (subst (Var x) σ)) } =
     vars_of (subst (Var a) σ)" by auto
    have lhs: "(subst (Var a) σ) = (subst (Var a) σ)" by auto
    from rhs and lhs show ?case by auto
  next
  case (Comb t1 t2)
    have "vars_of (Comb t1 t2) = (vars_of t1) ∪ (vars_of t2)" by auto
    then have "∪ { V. ∃x. (x ∈ (vars_of (Comb t1 t2))) ∧ (V = vars_of (subst (Var x) σ)) }
      = ∪ { V. ∃x. (x ∈ (vars_of t1)) ∧ (V = vars_of (subst(Var x) σ)) }
        ∪ ∪ { V. ∃x. (x ∈ (vars_of t2)) ∧ (V = vars_of (subst (Var x) σ)) }"
        by auto
    then have rhs: "∪ { V. ∃x. (x ∈ (vars_of (Comb t1 t2))) ∧ (V = vars_of (subst (Var x) σ)) }
      = (vars_of (subst t1 σ)) ∪ (vars_of (subst t2 σ))"
      using ‹vars_of (subst t1 σ)
 = ∪ { V. ∃x. (x ∈ (vars_of t1)) ∧ (V = vars_of (subst (Var x) σ)) }›
        and
            ‹vars_of (subst t2 σ)
 = ∪ { V. ∃x. (x ∈ (vars_of t2)) ∧ (V = vars_of (subst (Var x) σ)) }›
      by auto   
    have "(subst (Comb t1 t2) σ) = (Comb (subst t1 σ) (subst t2 σ))" 
      by auto
    then have lhs: "(vars_of (subst (Comb t1 t2) σ)) =
      (vars_of (subst t1 σ)) ∪ (vars_of (subst t2 σ))" by auto
    from lhs and rhs show ?case by auto
qed

lemma subterms_of_instances :
   "∀u v u' s. (u = (subst v s) ⟶ (subterm u p u')
    ⟶ (∃x q1 q2. (is_a_variable x) ∧ (subterm (subst x s) q1 u') ∧
                      (subterm v q2 x) ∧ (p = (append q2 q1))) ∨
        ((∃ v'. ((¬ is_a_variable v') ∧ (subterm v p v') ∧ (u' = (subst v' s))))))" (is "?prop p")
proof (induction p)
  case Nil
  show "?case"
  proof ((rule allI)+,(rule impI)+)
    fix u ::"'a trm" fix v u' s assume "u = (subst v s)" and "subterm u [] u'"
    then have "u = u'" by auto
    show "(∃x q1 q2. (is_a_variable x) ∧ (subterm (subst x s) q1 u') ∧
                      (subterm v q2 x) ∧ ([] = (append q2 q1))) ∨
        ((∃ v'. ((¬ is_a_variable v') ∧ (subterm v [] v') ∧ (u' = (subst v' s)))))" 
    proof (cases)
      assume "is_a_variable v"
        from ‹u = u'›and ‹u = (subst v s)›
          have "(subterm (subst v s) [] u')" by auto
        have "subterm v [] v" by auto
        from this and ‹(subterm (subst v s) [] u')› and ‹is_a_variable v›
          show ?thesis by auto
      next assume "¬ is_a_variable v"
        from ‹u = u'› and ‹u = (subst v s)›
        have "((subterm v [] v) ∧ (u' = (subst v s)))" by auto
        then show ?thesis  by auto
   qed
  qed
  next
  case (Cons i q)
  show ?case
  proof ((rule allI)+,(rule impI)+)
    fix u ::"'a trm" fix v u' s assume "u = (subst v s)" 
      and "subterm u (Cons i q) u'"
    show "(∃x q1 q2. (is_a_variable x) ∧ (subterm (subst x s) q1 u') ∧
                      (subterm v q2 x) ∧ ((Cons i q) = (append q2 q1))) ∨
        ((∃ v'. ((¬ is_a_variable v') ∧ (subterm v (Cons i q) v') ∧ (u' = (subst v' s)))))"
    proof (cases v)
      fix x assume "v = (Var x)"
      then have "subterm v [] v" by auto 
      from ‹v = (Var x)› have "is_a_variable v" by auto
      have "Cons i q = (append [] (Cons i q))" by auto
      from ‹subterm u (Cons i q) u'› and ‹u = (subst v s)›
        and ‹v = (Var x)› have "subterm (subst v s) (Cons i q) u'" by auto
      from ‹is_a_variable v› and ‹subterm v [] v› and ‹Cons i q = (append [] (Cons i q))› and this 
        show ?thesis  by blast
    next
      fix x assume "v = (Const x)"
      from this and ‹u = (subst v s)› have "u = v" by auto
      from this and ‹v = (Const x)› and ‹subterm u (Cons i q) u'› show ?thesis by auto
    next
      fix t1 t2 assume "v = (Comb t1 t2)"
      from this and  ‹u = (subst v s)›
        have "u = (Comb (subst t1 s) (subst t2 s))" by auto
      have "i = Left ∨ i = Right" using indices.exhaust by auto 
      from ‹i = Left ∨ i = Right› and ‹u = (Comb (subst t1 s) (subst t2 s))›
        and ‹subterm u (Cons i q) u'› obtain ti where 
        "subterm (subst ti s) q u'" and "ti = t1 ∨ ti = t2" and "subterm v [i] ti"
        using ‹v = t1 ⋅ t2› by auto
      from ‹?prop q› and ‹subterm (subst ti s) q u'› have
        "(∃x q1 q2. (is_a_variable x) ∧ (subterm (subst x s) q1 u') ∧
                      (subterm ti q2 x) ∧ (q = (append q2 q1))) ∨
                      ((∃ v'. ((¬ is_a_variable v') ∧ (subterm ti q v') ∧ (u' = (subst v' s)))))"  
        by auto
      then show ?thesis
      proof
        assume "(∃x q1 q2. (is_a_variable x) ∧ (subterm (subst x s) q1 u') ∧
                      (subterm ti q2 x) ∧ (q = (append q2 q1)))"
        then obtain x q1 q2 where "is_a_variable x" and "subterm (subst x s) q1 u'" 
            and "subterm ti q2 x" and "q = (append q2 q1)"
         by auto
        from ‹subterm ti q2 x› and ‹subterm v [i] ti› have "subterm v (i # q2) x"
        using ‹i = indices.Left ∨ i = indices.Right› ‹v = t1 ⋅ t2› by auto
        from ‹q = append q2 q1› have "i # q = (append (i # q2) q1)" by auto
        from ‹i # q = (append (i # q2) q1)› and ‹is_a_variable x›
          and ‹subterm (subst x s) q1 u'› and ‹subterm v (i # q2) x›
          show ?thesis by blast 
      next
        assume "((∃ v'. ((¬ is_a_variable v') ∧ (subterm ti q v') ∧ (u' = (subst v' s)))))"
        then obtain v' where "(¬ is_a_variable v')" "(subterm ti q v')" and "u' = (subst v' s)"  by auto
        from ‹subterm ti q v'›  and ‹subterm v [i] ti› have "subterm v (i # q) v'"
          using ‹i = indices.Left ∨ i = indices.Right› ‹v = t1 ⋅ t2› by auto
        from this and ‹(¬ is_a_variable v')› ‹subterm ti q v'› and ‹u' = (subst v' s)›
          show ?thesis by auto
      qed
    qed
  qed
qed

lemma vars_of_replacement:
  shows "∧ t s. x ∈ vars_of s ==> replace_subterm t p v s ==> x ∈ (vars_of t) ∪ (vars_of v)"
proof (induction p)
  case Nil
    from ‹replace_subterm t Nil v s› have "s = v" by auto
    from this and ‹x ∈ vars_of s› show ?case by auto
  next case (Cons i q)
    from ‹replace_subterm t (Cons i q) v s› obtain t1 t2 where
        "t = (Comb t1 t2)"
        by (metis is_a_variable.cases replace_subterm.simps(2) replace_subterm.simps(3)) 
    have "i = Left ∨ i = Right" using indices.exhaust by blast 
    then show ?case
    proof 
      assume "i = Left"
      from this and ‹t = Comb t1 t2› and ‹replace_subterm t (Cons i q) v s›
        obtain s1 where "s = Comb s1 t2" and "replace_subterm t1 q v s1"
          using replace_subterm.simps(4) by auto
      from ‹s = Comb s1 t2› and ‹x ∈ vars_of s› have "x ∈ vars_of s1 ∨ x ∈ vars_of t2"
        by simp
      then show ?case
      proof 
        assume "x ∈ vars_of s1"
        from this and Cons.IH [of s1 t1] and ‹replace_subterm t1 q v s1› have "x ∈ (vars_of t1) ∪ (vars_of v)"
          by auto
        from this and ‹t = (Comb t1 t2)› show ?case by auto
      next
        assume "x ∈ vars_of t2"
        from this and ‹t = (Comb t1 t2)› show ?case by auto
      qed
    next
      assume "i = Right"
      from this and ‹t = Comb t1 t2› and ‹replace_subterm t (Cons i q) v s›
        obtain s2 where "s = Comb t1 s2" and "replace_subterm t2 q v s2"
          using replace_subterm.simps by auto
      from ‹s = Comb t1 s2› and ‹x ∈ vars_of s› have "x ∈ vars_of t1 ∨ x ∈ vars_of s2"
        by simp
      then show ?case
      proof 
        assume "x ∈ vars_of s2"
        from this and Cons.IH [of s2 t2] and ‹replace_subterm t2 q v s2› have "x ∈ (vars_of t2) ∪ (vars_of v)"
          by auto
        from this and ‹t = (Comb t1 t2)› show ?case by auto
      next
        assume "x ∈ vars_of t1"
        from this and ‹t = (Comb t1 t2)› show ?case by auto
      qed
   qed
qed

lemma vars_of_replacement_set:
  assumes "replace_subterm t p v s"
  shows "vars_of s ⊆ (vars_of t) ∪ (vars_of v)"
by (meson assms subsetI vars_of_replacement)

subsection ‹Substitutions and Most General Unifiers›

text ‹Substitutions are defined in the Unification theory. We provide some
  definitions and lemmata.›

fun subst_set :: "'a trm set => 'a subst => 'a trm set"
  where
    "(subst_set S σ) = { u. ∃t. u = (subst t σ) ∧ t ∈ S }"

definition subst_codomain
where
  "subst_codomain σ V = { x. ∃y. (subst (Var y) σ) = (Var x) ∧ (y ∈ V) }"

lemma subst_codomain_is_finite:
  assumes "finite A"
  shows "finite (subst_codomain η A)"
proof -
  have i: "((λx. (Var x)) ` (subst_codomain η A)) ⊆ ((λx. (subst (Var x) η)) ` A)" 
  proof 
    fix x assume "x ∈ ((λx. (Var x)) ` (subst_codomain η A))"
    from this obtain y where "y ∈ (subst_codomain η A)" and "x = (Var y)" by auto
    from ‹y ∈ (subst_codomain η A)›  obtain z where "(subst (Var z) η) = (Var y)" "(z ∈ A)"
      unfolding subst_codomain_def by auto
    from ‹(z ∈ A)› ‹x = (Var y)› ‹(subst (Var z) η) = (Var y)› this show 
      "x ∈ ((λx. (subst (Var x) η)) ` A)"using image_iff by fastforce 
  qed
  have "inj_on (λx. (Var x)) (subst_codomain η A)" by (meson inj_onI trm.inject(1))
  from assms(1) have "finite ((λx. (subst (Var x) η)) ` A)" by auto
  from this and i have "finite ((λx. (Var x)) ` (subst_codomain η A))" 
    using rev_finite_subset by auto
  from this and ‹inj_on (λx. (Var x)) (subst_codomain η A)› show ?thesis using finite_imageD [of "(λx. (Var x))" "subst_codomain η A"]
    by auto
qed

text ‹The notions of unifiers, most general unifiers, the unification algorithm and a
  of correctness are provided in the Unification theory. Below, we prove that the algorithm
  complete.›

lemma subt_decompose:
  shows "∀t1 t2. Comb t1 t2 ≺ s ⟶ (t1 ≺ s ∧ t2≺ s) "
proof ((induction s),(simp),(simp))
    case (Comb s1 s2) 
     show ?case
     proof ((rule allI)+,(rule impI)) 
      fix t1 t2 assume "Comb t1 t2 ≺ Comb s1 s2"
      show "t1 ≺ (Comb s1 s2) ∧ t2 ≺ (Comb s1 s2)"
      proof (rule ccontr)
        assume neg: "¬(t1 ≺ (Comb s1 s2) ∧ t2 ≺ (Comb s1 s2))"
        from ‹Comb t1 t2 ≺ Comb s1 s2› have 
          d: "Comb t1 t2 = s1 ∨ Comb t1 t2 = s2 ∨ Comb t1 t2 ≺ s1 ∨ Comb t1 t2 ≺ s2" 
          by auto
        have i: "¬ (Comb t1 t2 = s1)"
        proof 
          assume "(Comb t1 t2 = s1)"
          then have "t1 ≺ s1" and "t2 ≺ s1" by auto
          from this and neg  show False by auto
        qed
        have ii: "¬ (Comb t1 t2 = s2)"
        proof 
          assume "(Comb t1 t2 = s2)"
          then have "t1 ≺ s2" and "t2 ≺ s2" by auto
          from this and neg  show False by auto
        qed
        have iii: "¬ (Comb t1 t2 ≺ s1)"
        proof 
          assume "(Comb t1 t2 ≺ s1)"
          then have "t1 ≺ s1 ∧ t2 ≺ s1" using Comb.IH by metis 
          from this and neg  show False by auto
        qed
        have iv: "¬ (Comb t1 t2 ≺ s2)"
        proof 
          assume "(Comb t1 t2 ≺ s2)"
          then have "t1 ≺ s2 ∧ t2 ≺ s2" using Comb.IH by metis
          from this and neg show False by auto
        qed
        from d and i ii iii iv show False by auto
     qed
   qed
qed

lemma subt_irrefl:
  shows "¬ (s ≺ s)" 
proof ((induction s),(simp),(simp))
    case (Comb t1 t2) 
     show ?case
    proof 
      assume "Comb t1 t2 ≺ Comb t1 t2"
      then have i: "Comb t1 t2 ≠ t1" using Comb.IH(1) by fastforce 
      from ‹Comb t1 t2 ≺ Comb t1 t2› have ii: "Comb t1 t2 ≠ t2" using Comb.IH(2) by fastforce 
      from i ii and ‹Comb t1 t2 ≺ Comb t1 t2› have "Comb t1 t2 ≺ t1 ∨ Comb t1 t2 ≺ t2" by auto
      then show False
      proof
        assume "Comb t1 t2 ≺ t1"
        then have "t1 ≺ t1"  using subt_decompose [of t1] by metis
        from this show False using Comb.IH by auto
      next
        assume "Comb t1 t2 ≺ t2"
        then have "t2 ≺ t2"  using subt_decompose [of t2] by metis
        from this show False using Comb.IH by auto
      qed
    qed
qed

lemma MGU_exists:
  shows "∀σ. ((subst t σ) = (subst s σ) ⟶ unify t s ≠ None)"
proof (rule unify.induct)
    fix x s1 s2 show "∀σ :: 'a subst .((subst (Const x) σ) = (subst (Comb s1 s2) σ)
      ⟶ unify (Const x) (Comb s1 s2) ≠ None)" by simp 
    next
    fix t1 t2 y show "∀σ :: 'a subst.(subst (Comb t1 t2) σ) = (subst (Const y) σ)
      ⟶ unify (Comb t1 t2) (Const y) ≠ None" by simp 
    next
    fix x y show "∀σ :: 'a subst.(subst (Const x) σ) = (subst (Var y) σ)
      ⟶ unify (Const x) (Var y) ≠ None" using unify.simps(3) by fastforce  
    next
    fix t1 t2 y show "∀σ :: 'a subst.(subst (Comb t1 t2) σ) = (subst (Var y) σ)
      ⟶ unify (Comb t1 t2) (Var y) ≠ None"
       by (metis option.distinct(1) subst_mono subt_irrefl unify.simps(4))
    next
    fix x s show "∀σ :: 'a subst.(subst (Var x) σ) = (subst s σ)
      ⟶ unify (Var x) s ≠ None"
      by (metis option.distinct(1) subst_mono subt_irrefl unify.simps(5))
    next 
    fix x y show "∀σ :: 'a subst.(subst (Const x) σ) = (subst (Const y) σ)
      ⟶ unify (Const x) (Const y) ≠ None" by simp 
    next
    fix t1 t2 s1 s2
    show "∀σ :: 'a subst. (subst t1 σ = subst s1 σ ⟶ unify t1 s1 ≠ None) ==>
       (∧x2. unify t1 s1 = Some x2 ==>
              ∀σ. subst (t2 ⊲ x2) σ = subst (s2 ⊲ x2) σ ⟶
              unify (t2 ⊲ x2) (s2 ⊲ x2) ≠ None) ==>
       ∀σ. (subst (t1 ⋅ t2) σ = subst (s1 ⋅ s2) σ ⟶
       unify (t1 ⋅ t2) (s1 ⋅ s2) ≠ None)"
    proof -
      assume h1: "∀σ. (subst t1 σ = subst s1 σ ⟶ unify t1 s1 ≠ None)"
      assume h2: "(∧x2. unify t1 s1 = Some x2 ==>
              ∀σ. subst (t2 ⊲ x2) σ = subst (s2 ⊲ x2) σ ⟶
              unify (t2 ⊲ x2) (s2 ⊲ x2) ≠ None)"
      show "∀σ. (subst (t1 ⋅ t2) σ = subst (s1 ⋅ s2) σ ⟶
       unify (t1 ⋅ t2) (s1 ⋅ s2) ≠ None)"
      proof ((rule allI),(rule impI))
        fix σ assume h3: "subst (t1 ⋅ t2) σ = subst (s1 ⋅ s2) σ"
        from h3 have "subst t1 σ = subst s1 σ" by auto
        from this and h1 have "unify t1 s1 ≠ None" by auto
        from this obtain θ where "unify t1 s1 = Some θ" and "MGU θ t1 s1"
            by (meson option.exhaust unify_computes_MGU) 
        from ‹subst t1 σ = subst s1 σ› have "Unifier σ t1 s1" 
            unfolding Unifier_def by auto
        from this and ‹MGU θ t1 s1› obtain η where  "σ ≐ θ ◊ η" using MGU_def by metis
        from h3 have "subst t2 σ = subst s2 σ" by auto
        from this and ‹σ ≐ θ ◊ η›   
            have "subst (subst t2 θ) η
              = subst (subst s2 θ) η"
            by (simp add: subst_eq_def)
        from this and ‹unify t1 s1 = Some θ› and h2 [of θ] have "unify (t2 ⊲ θ) (s2 ⊲ θ) ≠ None"
            by auto
        from this show "unify (t1 ⋅ t2) (s1 ⋅ s2) ≠ None" 
          by (simp add: ‹unify t1 s1 = Some θ› option.case_eq_if)  
      qed
   qed
qed

text ‹We establish some useful properties of substitutions and instances.›

definition ground_on :: "'a set ==> 'a subst ==> bool"
  where "ground_on V σ = (∀x ∈ V. (ground_term (subst (Var x) σ)))"

lemma comp_subst_terms:
    assumes "σ ≐ θ ◊ η"
    shows "(subst t σ) = (subst (subst t θ) η)"
proof -
    from ‹σ ≐ θ ◊ η› have "((subst t σ) = (subst t (θ ◊ η)))" by auto
    have "(subst t (θ ◊ η) = (subst (subst t θ) η))" by auto
    from this and ‹((subst t σ) = (subst t (θ ◊ η)))› show ?thesis by auto
qed

lemma ground_instance:
  assumes "ground_on (vars_of t) σ"
  shows "ground_term (subst t σ)"
proof (rule ccontr)
  assume "¬ ground_term (subst t σ)"
  then have "vars_of (subst t σ) ≠ {}"  unfolding ground_term_def by auto
  then obtain x where "x ∈ vars_of (subst t σ)"  by auto
  then have "x ∈ ∪ { V. ∃x. (x ∈ (vars_of t)) ∧ (V = vars_of (subst (Var x) σ)) }"
    using vars_of_instances by force  
  then obtain y where "x ∈ (vars_of (subst (Var y) σ))" and "y ∈ (vars_of t)" by blast
  from assms(1) and ‹y ∈ (vars_of t)› have "ground_term (subst (Var y) σ)" unfolding ground_on_def
    by auto
  from this and ‹x ∈ (vars_of (subst (Var y) σ))› show False unfolding ground_term_def by auto
qed

lemma substs_preserve_groundness:
  assumes "ground_term t"
  shows "ground_term (subst t σ)"
by (metis assms equals0D ground_instance ground_on_def ground_term_def)

lemma ground_subst_exists  :
  "finite V ==> ∃σ. (ground_on V σ)"
proof (induction rule: finite.induct)
  case emptyI
  show ?case unfolding ground_on_def by simp
next
  fix A :: "'a set" and a::'a 
  assume "finite A"
  assume hyp_ind: "∃σ. ground_on A σ" 
  then obtain σ where "ground_on A σ" by auto
  then show "∃σ. ground_on (insert a A) σ"
  proof cases
    assume "a ∈ A"
    from this and hyp_ind show "∃σ. ground_on (insert a A) σ"  
      unfolding ground_on_def by auto
  next
    assume "a ∉ A"
    obtain c where "c = (Const a)" and "is_a_constant c" by auto
    obtain θ where "θ = (a,c) # σ" by auto  
    have "∀x. (x ∈ insert a A ⟶ (ground_term (subst (Var x) θ)))"
    proof ((rule allI)+,(rule impI)+)
      fix x assume "x ∈ insert a A"
      show "ground_term (subst (Var x) θ)"
      proof cases
        assume "x = a"
        from this and ‹θ = (a,c) # σ› have "(subst (Var x) θ) = c" by auto
        from ‹is_a_constant c› have "ground_term c" using constants_are_ground by auto
        from this and ‹(subst (Var x) θ) = c› show "ground_term (subst (Var x) θ)" by auto
      next
        assume "x ≠ a"
        from ‹x ≠ a› and ‹x ∈ insert a A› have "x ∈ A" by auto
        from ‹x ≠ a› and  ‹θ = (a,c) # σ› have "(subst (Var x) θ) = (subst (Var x) σ)" by auto
        from this and ‹x ∈ A› and ‹ground_on A σ›
          show "ground_term (subst (Var x) θ)" unfolding ground_on_def by auto
      qed
    qed
    from this show ?thesis unfolding ground_on_def by auto 
  qed
qed

lemma substs_preserve_ground_terms :
  assumes "ground_term t"
  shows "subst t σ = t"
by (metis agreement assms equals0D ground_term_def subst_Nil)

lemma substs_preserve_subterms :
  shows "∧ t s. subterm t p s ==> subterm (subst t σ) p (subst s σ)"
proof (induction p)
  case Nil
    then have "t = s" using subterm.elims(2) by auto 
    from ‹t = s› have "(subst t σ) = (subst s σ)" by auto
    from this show ?case using Nil.prems by auto
  next case (Cons i q)
    from ‹subterm t (i # q) s› obtain t1 t2 where
        "t = (Comb t1 t2)" using subterm.elims(2) by blast 
    have "i = Left ∨ i = Right" using indices.exhaust by blast 
    then show "subterm (subst t σ) (i # q) (subst s σ)"
    proof 
      assume "i = Left"
      from this and ‹t = Comb t1 t2› and ‹subterm t (i # q) s›  
        have "subterm t1 q s" by auto
      from this have "subterm (subst t1 σ) q (subst s σ)" using Cons.IH by auto 
      from this and ‹t = Comb t1 t2›
        show "subterm (subst t σ) (i # q) (subst s σ)" 
          by (simp add: ‹i = indices.Left›) 
    next assume "i = Right"
      from this and ‹t = Comb t1 t2› and ‹subterm t (i # q) s›  
        have "subterm t2 q s" by auto
      from this have "subterm (subst t2 σ) q (subst s σ)" using Cons.IH by auto 
      from this and ‹t = Comb t1 t2›
        show "subterm (subst t σ) (i # q) (subst s σ)" 
          by (simp add: ‹i = indices.Right›) 
    qed
qed

lemma substs_preserve_occurs_in:
  assumes "occurs_in s t"
  shows "occurs_in (subst s σ) (subst t σ)"
using substs_preserve_subterms
  using assms occurs_in_def by blast 

definition coincide_on 
where "coincide_on σ η V = (∀x ∈ V. (subst (Var x) σ) = ( (subst (Var x) η)))"

lemma coincide_sym:
  assumes "coincide_on σ η V"
  shows "coincide_on η σ V"
by (metis assms coincide_on_def) 

lemma coincide_on_term:
  shows "∧ σ η. coincide_on σ η (vars_of t) ==> subst t σ = subst t η"
proof (induction t)
  case (Var x)
    from this show "subst (Var x) σ = subst (Var x) η" 
      unfolding coincide_on_def by auto
  next case (Const x)
    show "subst (Const x) σ = subst (Const x) η"  by auto
  next case (Comb t1 t2)
    from this show ?case unfolding coincide_on_def by auto
qed

lemma ground_replacement:
  assumes "replace_subterm t p v s"
  assumes "ground_term (subst t σ)"
  assumes "ground_term (subst v σ)"
  shows "ground_term (subst s σ)"
proof -
  from assms(1) have "vars_of s ⊆ (vars_of t) ∪ (vars_of v)" using vars_of_replacement_set [of t p v s]
    by auto
  from assms(2) have "ground_on (vars_of t) σ" unfolding ground_on_def
    by (metis contra_subsetD ex_in_conv ground_term_def 
      occs_vars_subset subst_mono vars_iff_occseq)
  from assms(3) have "ground_on (vars_of v) σ" unfolding ground_on_def
    by (metis contra_subsetD ex_in_conv ground_term_def 
      occs_vars_subset subst_mono vars_iff_occseq)
  from ‹vars_of s ⊆ (vars_of t) ∪ (vars_of v)› ‹ground_on (vars_of t) σ›
    and  ‹ground_on (vars_of v) σ› have "ground_on (vars_of s) σ" 
    by (meson UnE ground_on_def rev_subsetD) 
  from this show ?thesis using ground_instance by blast
qed

text ‹We now show that two disjoint substitutions can always be fused.›

lemma combine_substs:
  assumes "finite V1"
  assumes "V1 ∩ V2 = {}"
  assumes "ground_on V1 η1"
  shows "∃σ. (coincide_on σ η1 V1) ∧ (coincide_on σ η2 V2)"
proof -
  have "finite V1 ==> ground_on V1 η1 ==> V1 ∩ V2 = {} ==> ∃σ. (coincide_on σ η1 V1) ∧ (coincide_on σ η2 V2)"
  proof (induction rule: finite.induct)
      case emptyI
      show ?case unfolding coincide_on_def by auto
    next fix V1 :: "'a set" and a::'a 
      assume "finite V1"
      assume hyp_ind: "ground_on V1 η1 ==> V1 ∩ V2 = {}
        ==> ∃σ. (coincide_on σ η1 V1) ∧ (coincide_on σ η2 V2)" 
      assume  "ground_on (insert a V1) η1" 
      assume "(insert a V1) ∩ V2 = {}"
      from this have "V1 ∩ V2 = {}" by auto
      from ‹ground_on (insert a V1) η1› have "ground_on V1 η1" 
        unfolding ground_on_def by auto
      from this and hyp_ind and ‹V1 ∩ V2 = {}› obtain σ' 
        where c:"(coincide_on σ' η1 V1) ∧ (coincide_on σ' η2 V2)" by auto
      let ?t = "subst (Var a) η1"
      from assms(2) have "ground_term ?t"
        by (meson ‹ground_on (insert a V1) η1› ground_on_def insertI1) 
      let ?σ = "comp [(a,?t)] σ'"
      have "coincide_on ?σ η1 (insert a V1)" 
      proof (rule ccontr)
        assume "¬coincide_on ?σ η1 (insert a V1)"
        then obtain x where "x ∈ (insert a V1)" and 
          "(subst (Var x) ?σ) ≠ ( (subst (Var x) η1))" 
          unfolding coincide_on_def by blast  
        have "subst (Var a) ?σ = subst ?t σ'" by simp  
        from ‹ground_term ?t› have "subst (Var a) ?σ = ?t"
          using substs_preserve_ground_terms by auto  
        from this and ‹(subst (Var x) ?σ) ≠ ( (subst (Var x) η1))›
          have "x ≠ a" by blast
        from this and ‹x ∈ (insert a V1)› have "x ∈ V1" by auto
        from ‹x ≠ a› have "(subst (Var x) ?σ) = (subst (Var x) σ')" by auto
        from c and ‹x ∈ V1› have "(subst (Var x) σ') = (subst (Var x) η1)"
          unfolding coincide_on_def by blast
        from this and ‹(subst (Var x) ?σ) = (subst (Var x) σ')›
          and ‹(subst (Var x) ?σ) ≠ ( (subst (Var x) η1))› show False by auto
      qed
      have "coincide_on ?σ η2 V2" 
      proof (rule ccontr)
        assume "¬coincide_on ?σ η2 V2"
        then obtain x where "x ∈ V2" and 
          "(subst (Var x) ?σ) ≠ ( (subst (Var x) η2))" 
          unfolding coincide_on_def by blast  
        from ‹(insert a V1) ∩ V2 = {}› and ‹x ∈ V2› have "x ≠ a" by auto
        from this  have "(subst (Var x) ?σ) = (subst (Var x) σ')" by auto
        from c and ‹x ∈ V2› have "(subst (Var x) σ') = (subst (Var x) η2)"
          unfolding coincide_on_def by blast
        from this and ‹(subst (Var x) ?σ) = (subst (Var x) σ')›
          and ‹(subst (Var x) ?σ) ≠ ( (subst (Var x) η2))› show False by auto 
      qed
      from ‹coincide_on ?σ η1 (insert a V1)› ‹coincide_on ?σ η2 V2›
        show "∃σ. (coincide_on σ η1 (insert a V1)) ∧ (coincide_on σ η2 V2)" by auto
  qed  
  from this and assms show ?thesis by auto
qed

text ‹We define a map function for substitutions and prove its correctness.›

fun map_subst
  where "map_subst f Nil = Nil" 
      | "map_subst f ((x,y) # l) = (x,(f y)) # (map_subst f l)"
   
lemma map_subst_lemma:
  shows "((subst (Var x) σ) ≠ (Var x) ∨ (subst (Var x) σ) ≠ (subst (Var x) (map_subst f σ)))
            ⟶ ((subst (Var x) (map_subst f σ)) = (f (subst (Var x) σ)))"
proof (induction σ,simp)
  next case (Cons p σ)
    let ?u = "(fst p)"
    let ?v = "(snd p)"
    show ?case
    proof
      assume "((subst (Var x) (Cons p σ)) ≠ (Var x)
        ∨ (subst (Var x) (Cons p σ))
          ≠ (subst (Var x) (map_subst f (Cons p σ))))"
      have  "map_subst f (Cons p σ) = ( (?u, (f ?v)) # (map_subst f σ))"
          by (metis map_subst.simps(2) prod.collapse) 
      show "(subst (Var x) (map_subst f (Cons p σ))) = (f (subst (Var x) (Cons p σ)))"
      proof cases
        assume "x = ?u"
        from this have "subst (Var x) (Cons p σ) = ?v"
          by (metis assoc.simps(2) prod.collapse subst.simps(1))
        from ‹map_subst f (Cons p σ) = ( (?u, (f ?v)) # (map_subst f σ))›
          and ‹x = ?u›
          have "subst (Var x) (map_subst f (Cons p σ)) = (f ?v)" by simp 
        from ‹subst (Var x) (Cons p σ) = ?v› ‹subst (Var x) (map_subst f (Cons p σ)) = (f ?v)› show ?thesis by auto
      next 
        assume "x ≠ ?u"
        from this have "subst (Var x) (Cons p σ) = (subst (Var x) σ)"
          by (metis  assoc.simps(2) prod.collapse subst.simps(1)) 
        from ‹map_subst f (Cons p σ) = ( (?u, (f ?v)) # (map_subst f σ))›
          and ‹x ≠ ?u›
          have "subst (Var x) (map_subst f (Cons p σ)) =
            subst (Var x) (map_subst f σ)" by simp 
        from this and "Cons.IH" have 
          "subst (Var x) (map_subst f (Cons p σ)) = (f (subst (Var x) σ))"
            using ‹subst (Var x) (p # σ) = subst (Var x) σ› ‹subst (Var x) (p # σ) ≠ Var x ∨ subst (Var x) (p # σ) ≠ subst (Var x) (map_subst f (p # σ))› by auto            
        from this and ‹subst (Var x) (Cons p σ) = (subst (Var x) σ)› show ?thesis by auto
      qed
   qed
qed


subsubsection ‹Minimum Idempotent Most General Unifier›

definition min_IMGU :: "'a subst ==> 'a trm ==> 'a trm ==> bool" where
  "min_IMGU μ t u ⟷
    IMGU μ t u ∧ fst ` set μ ⊆ vars_of t ∪ vars_of u ∧ range_vars μ ⊆ vars_of t ∪ vars_of u"

lemma unify_computes_min_IMGU:
  "unify M N = Some σ ==> min_IMGU σ M N"
  by (simp add: min_IMGU_def IMGU_iff_Idem_and_MGU unify_computes_MGU unify_gives_Idem
      unify_gives_minimal_domain unify_gives_minimal_range)

subsection ‹Congruences›

text ‹We now define the notion of a congruence on ground terms, i.e., an equivalence relation
  is closed under contextual embedding.›

type_synonym 'a binary_relation_on_trms = "'a trm ==> 'a trm ==> bool"

definition reflexive :: "'a binary_relation_on_trms ==> bool"
where 
    "(reflexive x) = (∀y. (x y y))"

definition symmetric :: "'a binary_relation_on_trms ==> bool"
where 
    "(symmetric x) = (∀y. ∀z. ((x y z) = (x z y)))"

definition transitive :: "'a binary_relation_on_trms ==> bool"
where 
    "(transitive x) = (∀y. ∀z. ∀u. (x y z) ⟶ (x z u) ⟶ (x y u))"

definition equivalence_relation :: "'a binary_relation_on_trms ==> bool"
where 
  "(equivalence_relation x) = ((reflexive x) ∧ (symmetric x) ∧ (transitive x))"
 
definition compatible_with_structure :: "('a binary_relation_on_trms) ==> bool"
where
   "(compatible_with_structure x) = (∀t1 t2 s1 s2.
      (x t1 s1) ⟶ (x t2 s2) ⟶ (x (Comb t1 t2) (Comb s1 s2)))"

definition congruence :: "'a binary_relation_on_trms ==> bool"
where 
  "(congruence x) = ((equivalence_relation x) ∧ (compatible_with_structure x))"

lemma replacement_preserves_congruences :
  shows "∧ t s. (congruence I) ==> (I (subst u σ) (subst v σ))
          ==> subterm t p u ==> replace_subterm t p v s
          ==> (I (subst t σ) (subst s σ))"
proof (induction p)
  case Nil
    from ‹subterm t Nil u› have "t = u" by auto 
    from ‹replace_subterm t Nil v s› have "s = v" by auto
    from ‹t = u› and ‹s = v› and ‹(I (subst u σ) (subst v σ))›
      show ?case by auto
  next case (Cons i q)
    from ‹subterm t (i # q) u› obtain t1 t2 where
        "t = (Comb t1 t2)" using subterm.elims(2) by blast 
    have "i = Left ∨ i = Right" using indices.exhaust by blast 
    then show "I (subst t σ) (subst s σ)"
    proof 
      assume "i = Left"
      from this and ‹t = Comb t1 t2› and ‹subterm t (i # q) u›  
        have "subterm t1 q u" by auto
      from ‹i = Left› and ‹t = Comb t1 t2› and ‹replace_subterm t (i # q) v s›  
        obtain t1' where "replace_subterm t1 q v t1'" and "s = Comb t1' t2" by auto
      from ‹congruence I› and ‹(I (subst u σ) (subst v σ))›
        and ‹subterm t1 q u› and ‹replace_subterm t1 q v t1'› have 
        "I (subst t1 σ) (subst t1' σ)" using Cons.IH Cons.prems(1) by blast 
      from ‹congruence I› have "I (subst t2 σ) (subst t2 σ)" 
        unfolding congruence_def equivalence_relation_def reflexive_def by auto
      from ‹I (subst t1 σ) (subst t1' σ)›
        and ‹I (subst t2 σ) (subst t2 σ)›
        and ‹congruence I› and ‹t = (Comb t1 t2)› and ‹s = (Comb t1' t2)›
        show "I (subst t σ) (subst s σ)" 
          unfolding congruence_def compatible_with_structure_def by auto
    next 
      assume "i = Right"
      from this and ‹t = Comb t1 t2› and ‹subterm t (i # q) u›  
        have "subterm t2 q u" by auto
      from ‹i = Right› and ‹t = Comb t1 t2› and ‹replace_subterm t (i # q) v s›  
        obtain t2' where "replace_subterm t2 q v t2'" and "s = Comb t1 t2'" by auto
      from ‹congruence I› and ‹(I (subst u σ) (subst v σ))›
        and ‹subterm t2 q u› and ‹replace_subterm t2 q v t2'› have 
        "I (subst t2 σ) (subst t2' σ)" using Cons.IH Cons.prems(1) by blast 
      from ‹congruence I› have "I (subst t1 σ) (subst t1 σ)" 
        unfolding congruence_def equivalence_relation_def reflexive_def by auto
      from ‹I (subst t2 σ) (subst t2' σ)›
        and ‹I (subst t1 σ) (subst t1 σ)›
        and ‹congruence I› and ‹t = (Comb t1 t2)› and ‹s = (Comb t1 t2')›
        show "I (subst t σ) (subst s σ)" 
          unfolding congruence_def compatible_with_structure_def by auto
    qed
qed

definition equivalent_on 
where "equivalent_on σ η V I = (∀x ∈ V.
  (I (subst (Var x) σ) ( (subst (Var x) η))))"

lemma equivalent_on_term:
  assumes "congruence I"
  shows "∧ σ η. equivalent_on σ η (vars_of t) I ==> (I (subst t σ) (subst t η))"
proof (induction t)
  case (Var x)
    from this show "(I (subst (Var x) σ) (subst (Var x) η))" 
      unfolding equivalent_on_def by auto
  next case (Const x)
    from assms(1) show "(I (subst (Const x) σ) (subst (Const x) η))" 
      unfolding congruence_def equivalence_relation_def reflexive_def by auto
  next case (Comb t1 t2)
    from this assms(1) show ?case unfolding equivalent_on_def
      unfolding congruence_def compatible_with_structure_def by auto
qed
   
subsection ‹Renamings›

text ‹We define the usual notion of a renaming. We show that fresh renamings always exist
 provided the set of variables is infinite) and that renamings admit inverses.›

definition renaming
where
  "renaming σ V = (∀x ∈ V. (is_a_variable (subst (Var x) σ))
    ∧ (∀ x y. ((x ∈ V) ⟶ (y ∈ V) ⟶ x ≠ y ⟶ (subst (Var x) σ) ≠ (subst (Var y) σ))))"

lemma renamings_admit_inverse:
  shows "finite V ==> renaming σ V ==> ∃ θ. (∀ x ∈ V. (subst (subst (Var x) σ ) θ) = (Var x))
    ∧ (∀ x. (x ∉ (subst_codomain σ V) ⟶ (subst (Var x) θ) = (Var x)))
    ∧ (∀x. is_a_variable (subst (Var x) θ))"
proof (induction rule: finite.induct)
  case emptyI
    let ?θ = "[]"
    have i: "(∀ x ∈ {}. (subst (subst (Var x) σ ) ?θ) = (Var x))" by auto
    have ii: "(∀ x. (x ∉ (subst_codomain σ {}) ⟶ (subst (Var x) ?θ) = (Var x)))" by auto
    have iii: "∀x. is_a_variable (subst (Var x) ?θ)" by simp
    from i ii iii show ?case  by metis
next
  fix A :: "'a set" and a::'a 
  assume "finite A"
  assume hyp_ind: "renaming σ A ==> ∃ θ. (∀ x ∈ A. (subst (subst (Var x) σ ) θ) = (Var x))
    ∧ (∀ x. (x ∉ (subst_codomain σ A) ⟶ (subst (Var x) θ) = (Var x)))
    ∧ (∀x. is_a_variable (subst (Var x) θ))"
  show "renaming σ (insert a A) ==> ∃ θ. (∀ x ∈ (insert a A). (subst (subst (Var x) σ ) θ) = (Var x))
    ∧ (∀ x. (x ∉ (subst_codomain σ (insert a A)) ⟶ (subst (Var x) θ) = (Var x)))
    ∧ (∀x. is_a_variable (subst (Var x) θ))"
  proof -
    assume "renaming σ (insert a A)" 
    show "∃ θ. (∀ x ∈ (insert a A). (subst (subst (Var x) σ ) θ) = (Var x))
    ∧ (∀ x. (x ∉ (subst_codomain σ (insert a A)) ⟶ (subst (Var x) θ) = (Var x)))
    ∧ (∀x. is_a_variable (subst (Var x) θ))"
    proof (cases)
      assume "a ∈ A"
      from this have "insert a A = A" by auto
      from this and ‹renaming σ (insert a A)› hyp_ind show ?thesis by metis 
    next assume "a ∉ A"
      from ‹renaming σ (insert a A)› have "renaming σ A" unfolding renaming_def by blast
      from this and hyp_ind obtain θ where i: "(∀ x ∈ A. (subst (subst (Var x) σ ) θ) = (Var x))" and 
        ii:  "(∀ x. (x ∉ (subst_codomain σ A) ⟶ (subst (Var x) θ) = (Var x)))" and
        iii: "∀x. is_a_variable (Var x ⊲ θ)" by metis
      from ‹renaming σ (insert a A)› have "is_a_variable (subst (Var a) σ)" unfolding renaming_def by blast
      from this obtain b where "(subst (Var a) σ) = (Var b)" using is_a_variable.elims(2) by auto 
      let ?η = "(b,(Var a)) # θ"
      have i': "(∀ x ∈ (insert a A). (subst (subst (Var x) σ ) ?η) = (Var x))"
      proof 
        fix x assume "x ∈ (insert a A)"
        show "(subst (subst (Var x) σ ) ?η) = (Var x)"
        proof (cases)
          assume "x = a"
          from this 
            have "(subst (Var b) ( (b,(Var a)) # Nil)) = (Var a)"
            by simp
          have "b ∉ (subst_codomain σ A)"
          proof 
            assume "b ∈ (subst_codomain σ A)"
            from this have "∃y. (subst (Var y) σ) = (Var b) ∧ (y ∈ A)" unfolding subst_codomain_def 
              by force 
            then obtain a' where "a' ∈ A" and "subst (Var a') σ = (Var b)" 
              by metis
            from ‹a' ∈ A› and ‹a ∉ A› have "a ≠ a'" by auto
            have "a ∈ (insert a A)" by auto
            from ‹a ≠ a'› and ‹a' ∈ A› and ‹a ∈ (insert a A)› and ‹renaming σ (insert a A)›
              have "(subst (Var a) σ ≠ (subst (Var a') σ))"
              unfolding renaming_def by blast
            from this and ‹subst (Var a') σ = (Var b)› ‹(subst (Var a) σ) = (Var b)›  
              show False by auto
          qed
          from this and ii have "(subst (Var b) θ) = (Var b)" by auto
          from this and ‹x = a› ‹(subst (Var a) σ) = (Var b)›
            ‹(subst (Var b) ( (b,(Var a)) # Nil)) = (Var a)›
            show "(subst (subst (Var x) σ ) ?η) = (Var x)"
            by simp
         next assume "x ≠ a"
          from this and ‹x ∈ insert a A› obtain "x ∈ A" by auto
          from this i have "(subst (subst (Var x) σ ) θ) = (Var x)"
            by auto
          then show "(subst (subst (Var x) σ ) ?η) = (Var x)"
            by (metis ‹subst (Var a) σ = Var b› ‹renaming σ (insert a A)›
                ‹x ∈ insert a A› ‹x ≠ a› insertI1 is_a_variable.elims(2) 
                occs.simps(1) renaming_def repl_invariance vars_iff_occseq)
         qed 
       qed
       have ii': "(∀ x. (x ∉ (subst_codomain σ (insert a A)) ⟶ (subst (Var x) ?η) = (Var x)))"
       proof ((rule allI),(rule impI))
        fix x assume "x ∉ subst_codomain σ (insert a A)"
        from this ‹(subst (Var a) σ) = (Var b)›  have "x≠ b" unfolding subst_codomain_def 
          by auto
        from this have "(subst (Var x) ?η) = (subst (Var x) θ)" by auto
        from ‹x ∉ subst_codomain σ (insert a A)› have "x ∉ (subst_codomain σ A)" unfolding subst_codomain_def 
          by auto
        from this and ii have "(subst (Var x) θ) = (Var x)" by auto
        from ‹(subst (Var x) ?η) = (subst (Var x) θ)›
          and ‹(subst (Var x) θ) = (Var x)› show "(subst (Var x) ?η) = (Var x)" 
          by auto
      qed
      have iii': "∀x. is_a_variable (subst (Var x) ?η)"
        using iii by auto
      from i' ii' iii' show ?thesis by auto
    qed
  qed
qed

lemma renaming_exists:
  assumes "¬ finite (Vars :: ('a set))"
  shows "finite V ==> (∀V'::'a set. finite V' ⟶ (∃η. ((renaming η V) ∧ ((subst_codomain η V) ∩ V') = {})))"
proof (induction rule: finite.induct)
    case emptyI
    let ?η = "[]"
    show ?case unfolding renaming_def subst_codomain_def by auto
next
    fix A :: "'a set" and a::'a 
    assume "finite A"
    assume hyp_ind: "∀V' :: 'a set. finite V' ⟶ (∃η. renaming η A ∧ subst_codomain η A ∩ V' = {})"
    show "∀V':: 'a set. finite V' ⟶ (∃η. renaming η (insert a A) ∧ subst_codomain η (insert a A) ∩ V' = {})"
    proof ((rule allI),(rule impI))
      fix V':: "'a set" assume "finite V'"
      from this have "finite (insert a V')" by auto
      from this and hyp_ind obtain η where "renaming η A" and "(subst_codomain η A) ∩ (insert a V') = {}" by metis
      from ‹finite A› have "finite (subst_codomain η A)" 
        using subst_codomain_is_finite by auto
      from this ‹finite V'› have "finite (V' ∪ (subst_codomain η A))" by auto
      from this have "finite ((insert a V') ∪ (subst_codomain η A))" by auto
      from this ‹¬ finite Vars› have "¬ (Vars ⊆ ((insert a V') ∪ (subst_codomain η A)))" using rev_finite_subset
        by metis
      from this obtain nv where "nv ∈ Vars" and "nv ∉ (insert a V')" and "nv ∉ (subst_codomain η A)" by auto
      let ?η = "(a,(Var nv)) # η"
      have i: "(∀x ∈ (insert a A). (is_a_variable (subst (Var x) ?η)))"
      proof (rule ccontr)
        assume "¬ (∀x ∈ (insert a A). (is_a_variable (subst (Var x) ?η)))"
        then obtain x where "x ∈ (insert a A)" and "¬is_a_variable (subst (Var x) ?η)" 
          by auto
        from ‹¬is_a_variable (subst (Var x) ?η)› have "x ≠ a" by auto
        from this and ‹x ∈ (insert a A)› have "x ∈ A" by auto
        from ‹x ≠ a› have "(subst (Var x) ?η) = (subst (Var x) η)" by auto
        from ‹renaming η A› and ‹x ∈ A› have "is_a_variable (subst (Var x) η)" 
          unfolding renaming_def by metis
        from this and ‹¬is_a_variable (subst (Var x) ?η)›
          ‹(subst (Var x) ?η) = (subst (Var x) η)› show False by auto
      qed
      have ii: "(∀ x y. ((x ∈ (insert a A)) ⟶ (y ∈ (insert a A)) ⟶ x ≠ y
        ⟶ (subst (Var x) ?η) ≠ (subst (Var y) ?η)))"
      proof (rule ccontr)
        assume "¬(∀ x y. ((x ∈ (insert a A)) ⟶ (y ∈ (insert a A)) ⟶ x ≠ y
          ⟶ (subst (Var x) ?η) ≠ (subst (Var y) ?η)))"
        from this obtain x y where "x ∈ insert a A" "y ∈ insert a A" "x ≠ y"
          "(subst (Var x) ?η) = (subst (Var y) ?η)" by blast
        from i obtain y' where "(subst (Var y) ?η) = (Var y')" 
          using is_a_variable.simps using ‹y ∈ insert a A› is_a_variable.elims(2) by auto 
        from i obtain x' where "(subst (Var x) ?η) = (Var x')" 
          using is_a_variable.simps using ‹x ∈ insert a A› is_a_variable.elims(2) by auto 
        from ‹(subst (Var x) ?η) = (Var x')› ‹(subst (Var y) ?η) = (Var y')›
          ‹(subst (Var x) ?η) = (subst (Var y) ?η)› have "x' = y'" by auto
        have "x ≠ a"
        proof 
          assume "x = a"
          from this and ‹x ≠ y› and ‹y ∈ insert a A› have "y ∈ A" by auto
          from this and ‹x ≠ y› and ‹x = a› and ‹(subst (Var y) ?η) = (Var y')›
          have "y' ∈ (subst_codomain η A)" unfolding subst_codomain_def by auto
          from ‹x = a› and ‹(subst (Var x) ?η) = (Var x')› have "x' = nv" by auto
          from this and ‹y' ∈ (subst_codomain η A)› and ‹x' = y'› and ‹nv ∉ (subst_codomain η A)›
          show False by auto
        qed
        from this and ‹x ∈ insert a A› have "x ∈ A" and 
          "(subst (Var x) ?η) = (subst (Var x) η)" by auto
        have "y ≠ a"
        proof 
          assume "y = a"
          from this and ‹x ≠ y› and ‹x ∈ insert a A› have "x ∈ A" by auto
          from this and ‹x ≠ y› and ‹y = a› and ‹(subst (Var x) ?η) = (Var x')›
            have "x' ∈ (subst_codomain η A)" unfolding subst_codomain_def by auto
          from ‹y = a› and ‹(subst (Var y) ?η) = (Var y')› have "y' = nv" by auto
          from this and ‹x' ∈ (subst_codomain η A)› and ‹x' = y'› and ‹nv ∉ (subst_codomain η A)›
            show False by auto
        qed
        from this and ‹y ∈ insert a A› have "y ∈ A" and 
          "(subst (Var y) ?η) = (subst (Var y) η)" by auto
        from ‹(subst (Var x) ?η) = (subst (Var x) η)›
          ‹(subst (Var y) ?η) = (subst (Var y) η)›
          ‹(subst (Var x) ?η) = (subst (Var y) ?η)›
        have "(subst (Var x) η) = (subst (Var y) η)" by auto
        from this and ‹x ∈ A› and ‹y ∈ A›and ‹renaming η A› and ‹x ≠ y› show False 
          unfolding renaming_def by metis
     qed
     from i ii have "renaming ?η (insert a A)" unfolding renaming_def by auto
     have "((subst_codomain ?η (insert a A)) ∩ V') = {}"
     proof (rule ccontr)
      assume "(subst_codomain ?η (insert a A)) ∩ V' ≠ {}"
      then obtain x where "x ∈ (subst_codomain ?η (insert a A))" and "x ∈ V'" by auto
      from ‹x ∈ (subst_codomain ?η (insert a A))› obtain x' where "x' ∈ (insert a A)"  
        and "subst (Var x') ?η = (Var x)" unfolding subst_codomain_def by blast
      have "x' ≠ a"
      proof 
        assume "x' = a"
        from this and ‹subst (Var x') ?η = (Var x)› have "x = nv" by auto
        from this and ‹x ∈ V'› and ‹nv ∉ (insert a V')› show False by auto
      qed
      from this and ‹x' ∈ (insert a A)› have "x' ∈ A" by auto 
      from ‹x' ≠ a› and ‹subst (Var x') ?η = (Var x)› have 
        "(Var x) = (subst (Var x') η)" by auto
      from this and ‹x' ∈ A›  have "x ∈ subst_codomain η A" unfolding subst_codomain_def by auto
      from ‹x ∈ subst_codomain η A› and ‹(subst_codomain η A) ∩ (insert a V') = {}› and ‹x ∈ V'›
        show False  by auto
     qed
     from this and ‹renaming ?η (insert a A)›
      show "∃η. renaming η (insert a A) ∧ subst_codomain η (insert a A) ∩ V' = {}" by auto
   qed
qed

end