Theory NU_Mgu

(*<*)
theory NU_Mgu
imports NU_Substs
begin
(*>*)

section ‹Most General Unifiers›

text ‹
 Defines the notion of unification problems and reduction rules over sets of
 such problems; proves that every reduction leading to the empty set produces an mgu.
›

syntax equ_prob :: "trm ⇒ trm ⇒ (trm × trm)"  (infix "≈?" 81)
  fresh_prob :: "string ⇒ trm ⇒ (string × trm)" (infix "♯?" 81)
translations
 "t1 ≈? t2" ⇀ "(t1, t2)"
 "a ♯? t"  ⇀ "(a,t)"

text ‹
  All solutions for a unification problem.
›

type_synonym problem_type = "((trm × trm) list) × ((string × trm) list)"

type_synonym unifier_type = "fresh_envs × substs"

definition U:: "problem_type ⇒ (unifier_type set)"
  where all_solutions_def: 
    "U P  ≡ {(nabla, s). 
             (∀ (t1,t2) ∈ set (fst P). nabla ⊢ subst s t1 ≈ subst s t2) ∧ 
             (∀ (a,t) ∈ set (snd P). nabla ⊢ a ♯ subst s t)}"

text ‹The set of variables in unification problems.›

type_synonym eprobs = "((trm × trm) list)"
type_synonym fprobs = "((string × trm) list)"
type_synonym probs = "eprobs × fprobs"

fun vars_fprobs:: "((string × trm) list) ⇒ (string set)"
  where
  "vars_fprobs [] = {}" |
  "vars_fprobs (x#xs) = (vars_trm (snd x))∪(vars_fprobs xs)"

fun  vars_eprobs :: "((trm × trm) list) ⇒ (string set)"
  where
   "vars_eprobs [] = {}" |
   "vars_eprobs (x#xs) = (vars_trm (snd x))∪(vars_trm (fst x))∪(vars_eprobs xs)"

definition vars_probs :: "problem_type ⇒ nat"
  where "vars_probs P ≡ card((vars_fprobs (snd P))∪(vars_eprobs (fst P)))"

text ‹Most general unifier›

definition mgu :: "problem_type ⇒ unifier_type ⇒ bool"
  where "mgu P unif ≡ 
   ∀ (nabla,s1)∈ U P. (∃ s2. (nabla ⊨ (subst s2) (fst unif)) ∧ 
                              (nabla ⊨ subst (s2 ∙(snd unif)) ≈ subst s1))"


text ‹Idempotency of a unifier›

definition idem :: "unifier_type ⇒ bool"
  where "idem unif ≡ (fst unif)⊨ subst ((snd unif)∙(snd unif)) ≈ subst (snd unif)"

text ‹Application of a substitution to a problem›

definition apply_subst_eprobs :: "substs ⇒ eprobs ⇒ eprobs"
  where "apply_subst_eprobs s P ≡ map (λ(t1, t2). (subst s t1 ≈? subst s t2)) P"

definition apply_subst_fprobs :: "substs ⇒ fprobs ⇒ fprobs"
  where "apply_subst_fprobs s P ≡ map (λ(a, t). (a ♯? subst s t)) P"

definition apply_subst :: "substs ⇒ problem_type ⇒ problem_type"
  where "apply_subst s P ≡ (map (λ(t1, t2). (subst s t1 ≈? subst s t2)) (fst P),
                      map (λ(a, t). (a ♯? (subst s t))) (snd P))"

text ‹Equality reductions›

inductive s_red :: "problem_type ⇒ substs ⇒ problem_type ⇒ bool"  ("_ ⊢ _ ↝ _ " [80,80,80] 80)
  where
  unit_sred[intro!]:    "((Unit ≈? Unit) # xs, ys) ⊢ [] ↝ (xs, ys)" |
  paar_sred[intro!]:    "((Paar t1 t2 ≈? Paar s1 s2)#xs,ys) ⊢[]↝ ((t1≈?s1)#(t2≈?s2)#xs,ys)" |
  func_sred[intro!]:    "((Func F t1 ≈? Func F t2)#xs,ys) ⊢[]↝ ((t1≈?t2)#xs,ys)" |
  abst_aa_sred[intro!]: "((Abst a t1 ≈? Abst a t2)#xs,ys) ⊢[]↝ ((t1≈?t2)#xs,ys)" |
  abst_ab_sred[intro!]: "a≠b ⟹ 
                       ((Abst a t1≈?Abst b t2)#xs,ys) ⊢[]↝ ((t1≈?swap [(a,b)] t2)#xs,(a♯?t2)#ys)" |
  atom_sred[intro!]:    "((Atom a≈?Atom a)#xs,ys) ⊢[]↝ (xs,ys)" |
  susp_sred[intro!]:    "((Susp pi1 X≈?Susp pi2 X)#xs,ys) 
                                ⊢[]↝ (xs,(map (λa. a♯? Susp [] X) (ds_list pi1 pi2))@ys)" | 
  var_1_sred[intro!]:   "¬(occurs X t) ⟹ ((Susp pi X≈?t)#xs,ys) 
                               ⊢[(X,swap (rev pi) t)]↝ apply_subst [(X,swap (rev pi) t)] (xs,ys)" |
  var_2_sred[intro!]:   "¬(occurs X t) ⟹ ((t≈?Susp pi X)#xs,ys) 
                               ⊢[(X,swap (rev pi) t)]↝ apply_subst [(X,swap (rev pi) t)] (xs,ys)"

inductive_cases s_red_elims:
"((Unit ≈? Unit) # xs, ys) ⊢[] ↝ (xs, ys)"
"((Paar t1 t2 ≈? Paar s1 s2)#xs,ys) ⊢[]↝ ((t1≈?s1)#(t2≈?s2)#xs,ys)"
"((Func F t1 ≈? Func F t2)#xs,ys) ⊢[]↝ ((t1≈?t2)#xs,ys)"
"((Abst a t1 ≈? Abst a t2)#xs,ys) ⊢[]↝ ((t1≈?t2)#xs,ys)"
"((Abst a t1≈?Abst b t2)#xs,ys) ⊢[]↝ ((t1≈?swap [(a,b)] t2)#xs,(a♯?t2)#ys)"
"((Atom a≈?Atom a)#xs,ys) ⊢[]↝ (xs,ys)"
"((Susp pi1 X≈?Susp pi2 X)#xs,ys) ⊢[]↝ (xs,(map (λa. a♯? Susp [] X) (ds_list pi1 pi2))@ys)"
"((Susp pi X≈?t)#xs,ys) ⊢[(X,swap (rev pi) t)]↝ apply_subst [(X,swap (rev pi) t)] (xs,ys)"
"((t≈?Susp pi X)#xs,ys) ⊢[(X,swap (rev pi) t)]↝ apply_subst [(X,swap (rev pi) t)] (xs,ys)"


lemma sred_symm:
  assumes "((t1 ≈? t2) # xs, ys) ⊢ s ↝ P2"
  shows "∃ P3. ((t2 ≈? t1) # xs, ys) ⊢ s ↝ P3"
  using assms
proof(cases rule: s_red.cases)
  case (var_1_sred X pi)
  have "((t2, Susp pi X) # xs,
     ys) ⊢ [(X, swap (rev pi) t2)] ↝ apply_subst [(X, swap (rev pi) t2)] (xs, ys)"
    using var_2_sred[OF ‹¬ occurs X t2›] by simp
  then show ?thesis using var_1_sred by blast
next
  case (var_2_sred X pi)
  have "((Susp pi X, t1) # xs,
     ys) ⊢ [(X, swap (rev pi) t1)] ↝ apply_subst [(X, swap (rev pi) t1)] (xs, ys)"
    using var_1_sred[OF ‹¬ occurs X t1›] by simp
  then show ?thesis using var_2_sred by blast
qed (auto)

text ‹Weakening of freshness›

lemma solution_weak:
  assumes "(nabla1, s) ∈ U P"
  shows "(nabla1 ∪ nabla3, s) ∈ U P"
  using assms
  unfolding all_solutions_def using fresh_weak equ_weak by auto

lemma solution_comp_id: 
  shows "((nabla, s) ∈ U P) = ((nabla, s ∙ []) ∈ U P)" and 
    "((nabla, s) ∈ U P) = ((nabla, [] ∙ s) ∈ U P)"
  unfolding all_solutions_def by auto

lemma solutions_subst_assoc:
   "((nabla, s1 ∙ (s2 ∙ s3)) ∈ U P) = ((nabla, (s1 ∙ s2) ∙ s3) ∈ U P)"
  unfolding all_solutions_def using subst_assoc by simp

text ‹Freshness reductions›

inductive c_red :: "problem_type ⇒ fresh_envs ⇒ problem_type ⇒ bool" ("_ ⊢ _ → _ " [80,80,80] 80)
  where
  unit_cred[intro!]:    "([],(a ♯? Unit)#xs) ⊢{}→ ([],xs)" |
  paar_cred[intro!]:    "([],(a ♯? Paar t1 t2)#xs) ⊢{}→ ([],(a♯?t1)#(a♯?t2)#xs)" |
  func_cred[intro!]:    "([],(a ♯? Func F t)#xs) ⊢{}→ ([],(a♯?t)#xs)" |
  abst_aa_cred[intro!]: "([],(a ♯? Abst a t)#xs) ⊢{}→ ([],xs)" |
  abst_ab_cred[intro!]: "a≠b ⟹([],(a ♯? Abst b t)#xs) ⊢{}→ ([],(a♯?t)#xs)" |
  atom_cred[intro!]:    "a≠b ⟹([],(a ♯? Atom b)#xs) ⊢{}→ ([],xs)" |
  susp_cred[intro!]:    "([],(a ♯? Susp pi X)#xs) ⊢ {((swapas (rev pi) a),X)}→ ([],xs)"

text‹It only reduces the freshness part after the equations list is empty ›

lemma c_red_eqs_empty:
  assumes "P1 ⊢ s → P2"
  shows "fst P1 = []"
  using assms by (auto elim: c_red.cases)

text ‹Unification reduction sequences›

inductive red_plus :: "problem_type ⇒ unifier_type ⇒ problem_type ⇒ bool" ("_ ⊨ _ ⇒ _ " [80,80,80] 80)
  where
  sred_single[intro!]: "⟦P1⊢s1 ↝ P2⟧ ⟹ P1⊨({},s1)⇒P2" |
  cred_single[intro!]: "⟦P1⊢nabla1→P2⟧ ⟹ P1 ⊨ (nabla1,[]) ⇒ P2" |
  sred_step[intro!]:   "⟦P1⊢s1↝P2; P2⊨(nabla2,s2)⇒P3⟧ ⟹ P1⊨(nabla2,(s2∙s1))⇒P3" |
  cred_step[intro!]:   "⟦P1⊢nabla1→P2; P2⊨(nabla2,[])⇒P3⟧ ⟹ P1⊨(nabla2∪nabla1,[])⇒P3"

text‹Symmetry of the reduction›

lemma red_plus_symm:
assumes"P1 = ((t1 ≈? t2) # xs, ys)"
  and "P1 ⊨ (nabla, s) ⇒ P2"
shows "∃ nabla1 s1 P3. ((t2 ≈? t1) # xs, ys) ⊨ (nabla1, s1) ⇒ P3"
  using assms
proof (induction arbitrary: nabla s rule: red_plus.induct[OF assms(2)])
  case (1 P1 s1 P)
  hence "(((t1, t2) # xs, ys)) ⊢ s1 ↝ P" by simp
  hence "∃ P3. ((t2 ≈? t1) # xs, ys) ⊢ s1 ↝ P3"
    using sred_symm by simp
  hence "∃ P3. ((t2 ≈? t1) # xs, ys) ⊨ ({}, s1) ⇒ P3" 
    using sred_single by auto
  then show "∃nabla1 s1 P3. ((t2, t1) # xs, ys) ⊨ (nabla1, s1) ⇒ P3" by auto
next
  case (2 P1 nabla1 P2)
  hence "fst P1 ≠ []" by simp
  moreover from 2(1) have "fst P1 = []"
    using c_red_eqs_empty by simp
  ultimately have False by simp
  then show ?case by simp
next
  case (3 P1 s1 P' nabla2 s2 P3)
  hence "(((t1, t2) # xs, ys)) ⊢ s1 ↝ P'" by simp
  hence "∃ P3. ((t2 ≈? t1) # xs, ys) ⊢ s1 ↝ P3"
    using sred_symm by simp
  hence "∃ P3. ((t2 ≈? t1) # xs, ys) ⊨ ({}, s1) ⇒ P3" 
    using sred_single by auto
  then show "∃nabla1 s1 P3. ((t2, t1) # xs, ys) ⊨ (nabla1, s1) ⇒ P3" by auto
next
  case (4 P1 nabla1 P' nabla2 P3)
  hence "fst P1 ≠ []" by simp
  moreover from 4(1) have "fst P1 = []"
    using c_red_eqs_empty by simp
  ultimately have False by simp
  then show ?case by simp
qed


lemma mgu_idem: 
  assumes "(nabla1,s1) ∈ U P"
    and "∀(nabla2,s2) ∈ U P. nabla2 ⊨(subst s2) nabla1 ∧  nabla2⊨subst(s2 ∙ s1)≈subst s2"
  shows "mgu P (nabla1,s1) ∧ idem (nabla1,s1)"
  using assms mgu_def idem_def by auto

lemma problem_subst_comm: 
  shows "((nabla,s2) ∈ U (apply_subst s1 P)) = ((nabla,(s2∙s1))∈U P)"
  using all_solutions_def apply_subst_def subst_comp_expand by auto

text ‹Preservation of solutions›

lemma P1_to_P2_sred:
  assumes "(nabla1,s1) ∈ U P1" and "P1 ⊢s2 ↝ P2"
  shows "(nabla1,s1) ∈ U P2  ∧ (nabla1⊨subst (s1∙s2)≈subst s1)"
  using assms
proof(induction arbitrary: nabla1 s1 rule: s_red.induct[OF ‹P1 ⊢ s2 ↝ P2›])
  case (1 xs ys)
   then have subst: "nabla1 ⊨ subst (s1 ∙ []) ≈ subst s1" 
     using equ_refl subst_equ_def by simp
   from 1
   have eqs: "∀ (t1,t2) ∈ set xs. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2" 
     and fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst s1 t" 
     using all_solutions_def by simp_all
   with subst show ?case
     using all_solutions_def by auto
 next
   case (2 t1 t2 t3 t4 xs ys)
   then have subst: "nabla1 ⊨ subst (s1∙ []) ≈ subst s1" 
     using equ_refl subst_equ_def by simp

   from 2
   have fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst s1 t"
     using all_solutions_def by simp

   from 2
   have i: "∀ (t1,t2) ∈ set ((Paar t1 t2, Paar t3 t4) # xs). nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     using all_solutions_def by simp
   hence "nabla1 ⊢ subst s1 t1 ≈ subst s1 t3" 
    "nabla1 ⊢ subst s1 t2 ≈ subst s1 t4"
    using Equ_elims(4)[of nabla1 ‹(subst s1 t1)›  ‹(subst s1 t2)›  ‹(subst s1 t3)›  ‹(subst s1 t4)›] 
      subst_paar[of s1] by auto+
    with i have eqs:
    "∀ (t1,t2) ∈ set ((t1,t3)#(t2, t4) # xs). nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
      by auto

    from fresh eqs subst 
    show ?case using all_solutions_def by simp
 next
   case (3 F t1 t2 xs ys)
   then have subst: "nabla1 ⊨ subst (s1 ∙ []) ≈ subst s1" 
     using equ_refl subst_equ_def by simp

   from 3
   have fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst s1 t"
     using all_solutions_def by simp

   from 3
   have i: "∀ (t1,t2) ∈ set ((Func F t1, Func F t2) # xs). nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     using all_solutions_def by simp
   hence "nabla1 ⊢ subst s1 t1 ≈ subst s1 t2" 
     using Equ_elims(5)[of nabla1 F ‹subst s1 t1› ‹subst s1 t2›] 
      subst_func by auto
   with i have eqs: 
     "∀ (t1,t2) ∈ set ((t1, t2) # xs). nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     by auto

   from subst fresh eqs
   show ?case using all_solutions_def by simp
 next
   case (4 a t1 t2 xs ys)
   then have subst: "nabla1 ⊨ subst (s1 ∙ []) ≈ subst s1" 
     using equ_refl subst_equ_def by simp

   from 4
   have fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst s1 t"
     using all_solutions_def by simp

   from 4
   have i: "∀ (t1,t2) ∈ set ((Abst a t1, Abst a t2) # xs). nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     using all_solutions_def by simp
   hence "nabla1 ⊢ subst s1 t1 ≈ subst s1 t2" 
     using Equ_elims(6)[of nabla1 a ‹subst s1 t1› ‹subst s1 t2›] 
      subst_abst by auto
   with i have eqs: 
     "∀ (t1,t2) ∈ set ((t1, t2) # xs). nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     by auto

   from subst fresh eqs
   show ?case using all_solutions_def by simp
 next
   case (5 a b t1 t2 xs ys)
   then have subst: "nabla1 ⊨ subst (s1 ∙ []) ≈ subst s1" 
     using equ_refl subst_equ_def by simp

   from 5
   have eqsP1: "∀ (t1,t2) ∈ set ((Abst a t1, Abst b t2) # xs). nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     using all_solutions_def by simp
   hence i: "nabla1 ⊢ Abst a (subst s1 t1) ≈ Abst b (subst s1 t2)"
     using subst_abst[of s1] by simp
   
   from 5
   have ii: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst s1 t"
     using all_solutions_def by auto
   from 5 i
   have "nabla1 ⊢ a ♯ subst s1 t2"
     using Equ_elims(7) by blast
   with ii 
   have fresh: "∀ (a,t) ∈ set ((a,t2) # ys). nabla1 ⊢ a ♯ subst s1 t"
     by simp
   
   from i 5
   have "nabla1 ⊢ subst s1 t1 ≈ subst s1 (swap [(a, b)] t2)" 
     using 5 Equ_elims(7)[of nabla1 a ‹subst s1 t1› b ‹subst s1 t2›]  
       subst_swap_comm by simp
   with eqsP1 have eqs: 
     "∀ (t1,t2) ∈ set ((t1, swap [(a,b)] t2) # xs). nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     by auto
    
   from subst fresh eqs 
   show ?case using all_solutions_def by simp
 next
   case (6 a xs ys)
   then have subst: "nabla1 ⊨ subst (s1 ∙ []) ≈ subst s1" 
     using equ_refl subst_equ_def by simp

   from 6
   have fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst s1 t"
     using all_solutions_def by auto

   from 6
   have eqs: "∀ (t1,t2) ∈ set xs. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     using all_solutions_def by auto
  
   from subst fresh eqs
   show ?case using all_solutions_def by simp
 next
   case (7 pi1 X pi2 xs ys)
   then have subst: "nabla1 ⊨ subst (s1 ∙ []) ≈ subst s1" 
     using equ_refl subst_equ_def by simp

   from 7
   have i: "∀ (t1,t2) ∈ set ((Susp pi1 X, Susp pi2 X) # xs). nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst s1 t"
     using all_solutions_def by simp+


   from 7(1)
   have "nabla1 ⊢ swap pi1 (look_up X s1) ≈ swap pi2 (look_up X s1)"
     using all_solutions_def subst_susp by simp
   hence "∀a∈ds pi1 pi2.  nabla1 ⊢ a ♯ (look_up X s1)"
     using equ_pi1_pi2_dec by simp
   hence "∀a∈ set (ds_list pi1 pi2). nabla1 ⊢ a ♯ subst s1 (Susp [] X)"
     using subst_susp ds_list_equ_ds[of pi1 pi2] by simp
   hence "∀ (a,t) ∈ set (map (λa. a ♯? Susp [] X) (ds_list pi1 pi2)). nabla1 ⊢ a ♯ subst s1 t"
    by (auto split: prod.splits)
   with 7 i(2)
   have fresh: 
     "∀ (a,t) ∈ set (map (λa. (a, Susp [] X)) (ds_list pi1 pi2) @ ys). nabla1 ⊢ a ♯ subst s1 t"
    by auto

   from i(1)
   have eqs:  
    "∀ (t1,t2) ∈ set xs. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     by simp
  
   from subst fresh eqs
   show ?case using all_solutions_def by simp
 next
   case (8 X t' pi xs ys)
   hence "nabla1 ⊢ subst s1 (Susp pi X) ≈ subst s1 t'"
     using all_solutions_def[of ‹((Susp pi X, t') # xs, ys)›] by auto
   hence subst: "nabla1 ⊨ subst (s1 ∙ [(X, swap (rev pi) t')]) ≈ subst s1"
     using unif_1 by simp

   from 8
   have eqs_old:
     "∀(t1,t2)∈set xs. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     and fresh_old:
     "∀(a,t)∈set ys. nabla1 ⊢ a ♯ subst s1 t"
     using all_solutions_def by auto

   from eqs_old 
   have eqs: "∀(t1,t2)∈set xs. 
    nabla1 ⊢ subst (s1 ∙ [(X, swap (rev pi) t')]) t1 ≈  subst (s1 ∙ [(X, swap (rev pi) t')]) t2"
     using unif_2a[OF subst] by auto

   from fresh_old 
   have fresh: "∀(a,t)∈set ys. nabla1 ⊢ a ♯ subst (s1 ∙ [(X, swap (rev pi) t')]) t"
     using unif_2b[OF subst] by auto

   from eqs fresh
   have "(nabla1, (s1 ∙ [(X, swap (rev pi) t')])) ∈ U (xs, ys)"
     using all_solutions_def by simp
   hence U: "(nabla1, s1) ∈ U (apply_subst [(X, swap (rev pi) t')] (xs, ys))"
     using problem_subst_comm by simp
   
   from subst U
   show ?case by simp
 next
   case (9 X t' pi xs ys)
   hence "nabla1 ⊢  subst s1 t' ≈ subst s1 (Susp pi X)"
     using all_solutions_def[of ‹((t', Susp pi X) # xs, ys)›] by simp
   hence subst: "nabla1 ⊨ subst (s1 ∙ [(X, swap (rev pi) t')]) ≈ subst s1 "
     using unif_1[OF equ_symm] by blast

   from 9
   have eqs_old:
    "∀(t1,t2)∈set xs. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     and fresh_old:
    "∀(a,t)∈ set ys. nabla1 ⊢ a ♯ subst s1 t"
      using all_solutions_def by auto

   from eqs_old 
   have eqs: "∀(t1,t2)∈set xs. 
    nabla1 ⊢ subst (s1 ∙ [(X, swap (rev pi) t')]) t1 ≈  subst (s1 ∙ [(X, swap (rev pi) t')]) t2"
    using unif_2a[OF subst] by auto

   from fresh_old 
   have fresh: "∀(a,t)∈set ys. nabla1 ⊢ a ♯ subst (s1 ∙ [(X, swap (rev pi) t')]) t"
     using unif_2b[OF subst] by auto

   from eqs fresh
   have "(nabla1, (s1 ∙ [(X, swap (rev pi) t')])) ∈ U (xs, ys)"
     using all_solutions_def by simp
   hence U: "(nabla1, s1) ∈ U (apply_subst [(X, swap (rev pi) t')] (xs, ys))"
     using problem_subst_comm by simp

   from subst U
  show ?case by simp
qed

text ‹Auxiliary lemma for completeness›

lemma P1_from_P2_sred: 
  assumes "(nabla1,s1)∈ U P2" and "P1⊢s2↝P2"
  shows "(nabla1,s1∙s2)∈ U P1"
 using assms
proof(induction arbitrary: nabla1 s1 rule: s_red.induct[OF ‹P1 ⊢ s2 ↝ P2›])
  case (1 xs ys)
  hence "∀ (t1,t2) ∈ set xs. nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2" 
     and fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst (s1 ∙ []) t"
    using all_solutions_def by simp_all
  hence eqs: 
    "∀ (t1,t2) ∈ set ((Unit, Unit) # xs). nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2"
    using subst_unit[of ‹(s1 ∙ [])›] equ_refl[of nabla1 Unit] by auto
  from fresh eqs show ?case
    using all_solutions_def by simp
next
  case (2 t1 t2 t3 t4 xs ys)
   hence eqs_old: "∀ (t1,t2) ∈ set ((t1, t3) # (t2, t4) # xs). nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2" 
     and fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst (s1 ∙ []) t"
     using all_solutions_def by simp_all
   hence "nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t3" 
     "nabla1 ⊢ subst (s1 ∙ []) t2 ≈ subst (s1 ∙ []) t4" by simp_all
   hence "nabla1 ⊢ subst (s1 ∙ []) (Paar t1 t2) ≈ subst (s1 ∙ []) (Paar t3 t4)"
     using equ_paar by simp
   with eqs_old have eqs:
     "∀ (t1,t2) ∈ set ((Paar t1 t2, Paar t3 t4) # xs). nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2"
     by auto
   from fresh eqs show ?case
    using all_solutions_def by simp
next
  case (3 f t1 t2 xs ys)
  hence eqs_old: "∀ (t1,t2) ∈ set ((t1, t2) # xs). nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2" 
     and fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst (s1 ∙ []) t"
    using all_solutions_def by simp_all
  hence "nabla1 ⊢ subst (s1 ∙ []) (Func f t1) ≈ subst (s1 ∙ []) (Func f t2)"
    using equ_func by simp
  with eqs_old have eqs:
     "∀ (t1,t2) ∈ set ((Func f t1, Func f t2) # xs). nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2"
     by auto
  from fresh eqs show ?case
    using all_solutions_def by simp
next
  case (4 a t1 t2 xs ys)
  hence eqs_old: "∀ (t1,t2) ∈ set ((t1, t2) # xs). nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2" 
     and fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst (s1 ∙ []) t"
    using all_solutions_def by simp_all
  hence "nabla1 ⊢ subst (s1 ∙ []) (Abst a t1) ≈ subst (s1 ∙ []) (Abst a t2)"
    using equ_abst_aa by simp
  with eqs_old have eqs:
     "∀ (t1,t2) ∈ set ((Abst a t1, Abst a t2) # xs). nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2"
     by auto
  from fresh eqs show ?case
    using all_solutions_def by simp
next
  case (5 a b t1 t2 xs ys)
  hence eqs_old: "∀ (t1,t2) ∈ set ((t1, swap [(a, b)] t2) # xs). nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2" 
    and fresh: "∀ (a,t) ∈ set ((a, t2) # ys). nabla1 ⊢ a ♯ subst (s1 ∙ []) t"
    using all_solutions_def by simp_all
  hence "nabla1 ⊢ subst (s1 ∙ []) t1 ≈ swap [(a, b)] (subst (s1 ∙ []) t2)"
      "nabla1 ⊢ a ♯ subst (s1 ∙ []) t2" 
    using subst_swap_comm[of ‹(s1 ∙ [])› ‹[(a, b)]› t2] by simp_all
  hence "nabla1 ⊢ subst (s1 ∙ []) (Abst a t1) ≈ subst (s1 ∙ []) (Abst b t2)"
    using equ_abst_ab[OF 5(1) ‹nabla1 ⊢ a ♯ subst (s1 ∙ []) t2›] subst_abst by simp
  with eqs_old have eqs:
     "∀ (t1,t2) ∈ set ((Abst a t1, Abst b t2) # xs). nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2"
     by auto
  from fresh eqs show ?case
    using all_solutions_def by simp
next
  case (6 a xs ys)
  hence "∀ (t1,t2) ∈ set xs. nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2" 
     and fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst (s1 ∙ []) t"
    using all_solutions_def by simp_all
  hence eqs: 
    "∀ (t1,t2) ∈ set ((Atom a, Atom a) # xs). nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2"
    using subst_unit[of ‹(s1 ∙ [])›] equ_refl[of nabla1 Unit] by auto
  from fresh eqs show ?case
    using all_solutions_def by simp
next
  case (7 pi1 X pi2 xs ys)
  hence eqs_old: "∀ (t1,t2) ∈ set xs. nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2" 
     and fresh_old: 
     "∀ (a,t) ∈ set (map (λa. (a, Susp [] X)) (ds_list pi1 pi2) @ ys). nabla1 ⊢ a ♯ subst (s1 ∙ []) t"
    using all_solutions_def by simp_all
  hence "∀c∈ set (ds_list pi1 pi2). nabla1 ⊢ c ♯ subst (s1 ∙ []) (Susp [] X)"
    by (auto split: prod.splits)
  hence "∀c ∈ ds pi1 pi2. nabla1 ⊢ c ♯ subst (s1 ∙ []) (Susp [] X)"
    using ds_list_equ_ds by simp
  hence "∀c ∈ ds pi1 pi2. nabla1 ⊢ c ♯ (look_up X (s1 ∙ []))"
    using subst_susp[of ‹(s1 ∙ [])› ‹[]› X] swap_id by simp
  hence "nabla1 ⊢ subst (s1 ∙ []) (Susp pi1 X) ≈ subst (s1 ∙ []) (Susp pi2 X)"
    using  equ_equiv_pi subst_susp[of ‹(s1 ∙ [])› _ X] by auto
  with eqs_old fresh_old have
  eqs: "∀ (t1,t2) ∈ set ((Susp pi1 X, Susp pi2 X)#xs). 
    nabla1 ⊢ subst (s1 ∙ []) t1 ≈ subst (s1 ∙ []) t2"
  and fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst (s1 ∙ []) t"
    by simp_all
  then show ?case 
    using all_solutions_def by simp
next
  case (8 X t' pi xs ys)
  hence "(nabla1, s1 ∙ [(X, swap (rev pi) t')]) ∈ U (xs, ys)"
    using problem_subst_comm by simp
  hence eqs_old: 
    "∀ (t1,t2) ∈ set xs. 
    nabla1 ⊢ subst (s1 ∙ [(X, swap (rev pi) t')]) t1 ≈ subst (s1 ∙ [(X, swap (rev pi) t')]) t2"
  and fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst (s1 ∙ [(X, swap (rev pi) t')]) t"
    using all_solutions_def by simp_all

  have "subst (s1 ∙ [(X, swap (rev pi) t')]) (Susp pi X) = subst s1 (swap pi (swap (rev pi) t'))"
    using subst_susp subst_swap_comm subst_comp_expand eq_fst_iff look_up.simps(2) snd_eqD by metis
  also have "... = swap pi (swap (rev pi) (subst s1 t'))"
    using subst_swap_comm by simp
  hence "nabla1 ⊢ subst (s1 ∙ [(X, swap (rev pi) t')]) (Susp pi X) ≈ subst s1 t'"
    using equ_refl calculation rev_pi_pi_equ[of nabla1 pi ‹subst s1 t'›]
      equ_trans[of nabla1 ‹subst (s1 ∙ [(X, swap (rev pi) t')]) (Susp pi X)› 
        ‹swap (rev pi) (swap pi (subst s1 t'))› ‹subst s1 t'›]
       swap_inv_side by auto

  with 8 eqs_old
  have eqs: "∀ (t1,t2) ∈ set ((Susp pi X, t')#xs). 
    nabla1 ⊢ subst (s1 ∙ [(X, swap (rev pi) t')]) t1 ≈ subst (s1 ∙ [(X, swap (rev pi) t')]) t2"
    using subst_comp_expand subst_not_occurs by simp

  from fresh eqs show ?case
    using all_solutions_def by simp
next
  case (9 X t' pi xs ys)
  hence "(nabla1, s1 ∙ [(X, swap (rev pi) t')]) ∈ U (xs, ys)"
    using problem_subst_comm by simp
  hence eqs_old: 
    "∀ (t1,t2) ∈ set xs. 
    nabla1 ⊢ subst (s1 ∙ [(X, swap (rev pi) t')]) t1 ≈ subst (s1 ∙ [(X, swap (rev pi) t')]) t2"
  and fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst (s1 ∙ [(X, swap (rev pi) t')]) t"
    using all_solutions_def by simp_all

  have "subst (s1 ∙ [(X, swap (rev pi) t')]) (Susp pi X) = subst s1 (swap pi (swap (rev pi) t'))"
    using subst_susp subst_swap_comm subst_comp_expand eq_fst_iff look_up.simps(2) snd_eqD by metis
  also have "... = swap pi (swap (rev pi) (subst s1 t'))"
    using subst_swap_comm by simp
  hence "nabla1 ⊢ subst (s1 ∙ [(X, swap (rev pi) t')]) (Susp pi X) ≈ subst s1 t'"
    using equ_refl calculation rev_pi_pi_equ[of nabla1 pi ‹subst s1 t'›]
      equ_trans[of nabla1 ‹subst (s1 ∙ [(X, swap (rev pi) t')]) (Susp pi X)› 
        ‹swap (rev pi) (swap pi (subst s1 t'))› ‹subst s1 t'›]
       swap_inv_side by auto
  hence "nabla1 ⊢ subst s1 t' ≈ subst (s1 ∙ [(X, swap (rev pi) t')]) (Susp pi X)"
    using equ_symm by simp

  with 9 eqs_old
  have eqs: "∀ (t1,t2) ∈ set ((t', Susp pi X)#xs). 
    nabla1 ⊢ subst (s1 ∙ [(X, swap (rev pi) t')]) t1 ≈ subst (s1 ∙ [(X, swap (rev pi) t')]) t2"
    using subst_comp_expand subst_not_occurs by simp

  from fresh eqs show ?case
    using all_solutions_def by simp
qed

lemma P1_to_P2_cred: 
  assumes "(nabla1,s1)∈ U P1"
  and "P1 ⊢nabla2 → P2"
shows "(nabla1,s1)∈ U P2  ∧ (nabla1⊨(subst s1) nabla2)"
  using assms
proof(induction arbitrary: nabla1 s1 rule: c_red.induct[OF ‹P1 ⊢nabla2→ P2›])
  case (2 a t1 t2 ys)
  hence fresh_old: "∀ (a,t) ∈ set ((a, Paar t1 t2) # ys). nabla1 ⊢ a ♯ subst s1 t"
    and eqs: "∀ (t1,t2) ∈ set []. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
    using all_solutions_def by simp_all
  hence "nabla1 ⊢ a ♯ subst s1 (Paar t1 t2)" 
    by simp
  hence "nabla1 ⊢ a ♯ subst s1 t1" "nabla1 ⊢ a ♯ subst s1 t2"
    using Fresh_elims(5)[of nabla1 a ‹subst s1 t1›
        ‹subst s1 t2›] by auto
  with fresh_old have
   fresh: "∀ (a,t) ∈ set ((a, t1) # (a, t2) # ys). nabla1 ⊢ a ♯ subst s1 t"
    by auto
  from fresh eqs
  show ?case
    using all_solutions_def ext_subst_def by simp
next
  case (3 a f t ys)
  hence fresh_old: "∀ (a,t) ∈ set ((a, Func f t) # ys). nabla1 ⊢ a ♯ subst s1 t"
    and eqs: "∀ (t1,t2) ∈ set []. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
    using all_solutions_def by simp_all
  hence "nabla1 ⊢ a ♯ subst s1 (Func f t)" 
    by simp
  hence "nabla1 ⊢ a ♯ subst s1 t" 
    using Fresh_elims(6) by auto
  with fresh_old have
   fresh: "∀ (a,t) ∈ set ((a, t) # ys). nabla1 ⊢ a ♯ subst s1 t"
    by auto
  from fresh eqs
  show ?case
    using all_solutions_def ext_subst_def by simp
next
  case (5 a b t ys)
  hence fresh_old: "∀ (a,t') ∈ set ((a, Abst b t) # ys). nabla1 ⊢ a ♯ subst s1 t'"
    and eqs: "∀ (t1,t2) ∈ set []. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
    using all_solutions_def by simp_all
  hence "nabla1 ⊢ a ♯ subst s1 (Abst b t)"
    by simp
  hence "nabla1 ⊢ a ♯ subst s1 t"
    using 5 Fresh_elims(1)[of nabla1 a b ‹subst s1 t›] by auto
  with fresh_old have
  fresh: "∀ (a,t') ∈ set ((a, t) # ys). nabla1 ⊢ a ♯ subst s1 t'"
    by auto
  from fresh eqs
  show ?case
    using all_solutions_def ext_subst_def by simp
next
  case (7 b pi X ys)
  hence fresh_old: "∀ (a,t) ∈ set ((b, Susp pi X) # ys). nabla1 ⊢ a ♯ subst s1 t"
    and eqs: "∀ (t1,t2) ∈ set []. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
    using all_solutions_def by simp_all
  hence fresh: "∀ (a,t) ∈ set ys. nabla1 ⊢ a ♯ subst s1 t" by simp
  from fresh_old have
  "nabla1 ⊢ b ♯ subst s1 (Susp pi X)" by simp
  hence "nabla1 ⊢ swapas (rev pi) b ♯ subst s1 (Susp [] X)"
    using fresh_swap_left subst_susp by simp
  hence ext: "nabla1 ⊨ (subst s1) {(swapas (rev pi) b, X)}"
    using ext_subst_def by simp
  from fresh eqs ext
    show ?case using all_solutions_def by simp
qed (auto simp add: all_solutions_def ext_subst_def)

lemma P1_from_P2_cred:
  assumes "(nabla1,s1)∈U P2"
    and "P1 ⊢nabla2→ P2" and "nabla3⊨(subst s1) nabla2"
  shows "(nabla1∪nabla3,s1)∈ U P1" 
  using assms
proof(induction arbitrary: nabla1 s1 rule: c_red.induct[OF ‹P1 ⊢nabla2→ P2›])
  case (2 a t1 t2 xs)
  hence fresh_old:
    "∀(b,t)∈set ((a,t1)#(a,t2)#xs). nabla1 ⊢ b ♯ subst s1 t"
    and "∀ (t1, t2) ∈ set []. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
    using all_solutions_def by auto
  hence weak1: "∀(b,t)∈set xs. (nabla1 ∪ nabla3) ⊢ b ♯ subst s1 t"
        "∀ (t1, t2) ∈ set []. (nabla1 ∪ nabla3) ⊢ subst s1 t1 ≈ subst s1 t2"
    using fresh_weak by auto
  from fresh_old have "nabla1 ⊢ a ♯ subst s1 t1" "nabla1 ⊢ a ♯ subst s1 t2"
    by simp+
  hence "nabla1 ⊢ a ♯ subst s1 (Paar t1 t2)"
    using fresh_paar subst_paar by auto
  hence "(nabla1 ∪ nabla3) ⊢ a ♯ subst s1 (Paar t1 t2)"
    using fresh_weak by auto
  with weak1
  have fresh: "∀(b,t)∈set ((a,Paar t1 t2)#xs). (nabla1 ∪ nabla3) ⊢ b ♯ subst s1 t"
    by simp
  with weak1(2) show ?case 
    using all_solutions_def ext_subst_def by simp
next
  case (3 a f t' xs)
  hence fresh_old:
    "∀(b,t)∈set ((a,t')#xs). nabla1 ⊢ b ♯ subst s1 t"
    and "∀ (t1, t2) ∈ set []. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
    using all_solutions_def by auto
  hence weak1: "∀(b,t)∈set xs. (nabla1 ∪ nabla3) ⊢ b ♯ subst s1 t"
        "∀ (t1, t2) ∈ set []. (nabla1 ∪ nabla3) ⊢ subst s1 t1 ≈ subst s1 t2"
    using fresh_weak by auto
  from fresh_old have "nabla1 ⊢ a ♯ subst s1 t'" 
    by simp
  hence "nabla1 ⊢ a ♯ subst s1 (Func f t')"
    using fresh_paar subst_paar by auto
  hence "(nabla1 ∪ nabla3) ⊢ a ♯ subst s1 (Func f t')"
    using fresh_weak by auto
  with weak1
  have fresh: "∀(b,t)∈set ((a, Func f t')#xs). (nabla1 ∪ nabla3) ⊢ b ♯ subst s1 t"
    by simp
  with weak1(2) show ?case 
    using all_solutions_def ext_subst_def by simp
next
  case (5 a b t' xs)
   hence fresh_old:
    "∀(c,t)∈set ((a,t')#xs). nabla1 ⊢ c ♯ subst s1 t"
    and "∀ (t1, t2) ∈ set []. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
     using all_solutions_def by auto
   hence weak1: "∀(c,t)∈set xs. (nabla1 ∪ nabla3) ⊢ c ♯ subst s1 t"
      "∀ (t1, t2) ∈ set []. (nabla1 ∪ nabla3) ⊢ subst s1 t1 ≈ subst s1 t2"
     using fresh_weak by auto
   from fresh_old have "nabla1 ⊢ a ♯ subst s1 t'" 
     by simp
   hence "nabla1 ⊢ a ♯ subst s1 (Abst b t')"
   using fresh_abst_ab[OF ‹nabla1 ⊢ a ♯ subst s1 t'› 5(1)] subst_abst by auto
   hence "(nabla1 ∪ nabla3) ⊢ a ♯ subst s1 (Abst b t')"
     using fresh_weak by auto
   with weak1
   have fresh: "∀(b,t)∈set ((a, Abst b t')#xs). (nabla1 ∪ nabla3) ⊢ b ♯ subst s1 t"
     by simp
   with weak1(2) show ?case 
     using all_solutions_def ext_subst_def by simp
next
  case (7 b pi X xs)
  hence fresh_old: "∀ (a,t) ∈ set xs. nabla1 ⊢ a ♯ subst s1 t"
    and eqs: "∀ (t1,t2) ∈ set []. nabla1 ⊢ subst s1 t1 ≈ subst s1 t2"
    using all_solutions_def by simp_all
  hence weak1: "∀(a,t)∈set xs. (nabla1 ∪ nabla3) ⊢ a ♯ subst s1 t"
      "∀ (t1, t2) ∈ set []. (nabla1 ∪ nabla3) ⊢ subst s1 t1 ≈ subst s1 t2"
     using fresh_weak by auto
  from 7 have "nabla3 ⊢ swapas (rev pi) b ♯ subst s1 (Susp [] X)"
    using ext_subst_def by auto
  hence "nabla3 ⊢ b ♯ subst s1 (Susp pi X)"
    using fresh_swap_right subst_susp by auto
  hence weak2: "(nabla1 ∪ nabla3) ⊢ b ♯ subst s1 (Susp pi X)"
    using fresh_weak[of nabla3 b _ nabla1] Un_commute[of nabla3 nabla1] by auto
  with weak1(1) 
  have "∀(a,t)∈set ((b,Susp pi X)#xs). (nabla1 ∪ nabla3) ⊢ a ♯ subst s1 t"
    by simp
  with weak2 show ?case 
    using ext_subst_def all_solutions_def by simp
qed (auto simp add: ext_subst_def all_solutions_def fresh_weak)

lemma P1_to_P2_red_plus1: 
  assumes "P1 ⊨ (nabla,s) ⇒ P2"
  and "(nabla1,s1) ∈ U P1"
  shows "(nabla1,s1) ∈ U P2"
  using assms
proof(induction P1≡"P1" nabla≡"(nabla, s)" P2≡"P2" arbitrary: s nabla1 nabla s1 P1 P2 rule: red_plus.induct)
  case (sred_single P1 s P2 nabla1 s1)
  have "P1 ⊢ s ↝ P2" "(nabla1, s1) ∈ U P1" by fact+
  then show "(nabla1, s1) ∈ U P2"
    using P1_to_P2_sred by blast
next
  case (cred_single P1 nabla1 P2 nabla2 s1)
  have "P1 ⊢ nabla1 →P2" "(nabla2, s1) ∈ U P1" by fact+
  then show "(nabla2, s1) ∈ U P2"
    using P1_to_P2_cred by blast
next
  case (sred_step P1 s P2 nabla2 s2 P3 nabla1 s1)
  have "P1 ⊢ s ↝ P2" and "(nabla1, s1) ∈ U P1" by fact+
  then have "(nabla1, s1) ∈ U P2" using P1_to_P2_sred by blast 
  moreover 
  have IH: "(nabla1, s1) ∈ U P2 ⟹ (nabla1, s1) ∈ U P3" by fact
  ultimately 
  show "(nabla1, s1) ∈ U P3" by simp 
next
  case (cred_step P1 nabla1 P2 nabla2 P3 nabla3 s1)
  have "P1 ⊢ nabla1 → P2" and "(nabla3, s1) ∈ U P1" by fact+
  then have "(nabla3, s1) ∈ U P2" using P1_to_P2_cred by blast 
  moreover 
  have IH: "(nabla3, s1) ∈ U P2 ⟹ (nabla3, s1) ∈ U P3" by fact
  ultimately show "(nabla3, s1) ∈ U P3" by simp
qed

lemma P1_to_P2_red_plus3: 
  assumes "P1 ⊨ (nabla,s) ⇒ P2"
  and "(nabla1,s1)∈ U P1"
  shows "nabla1⊨(subst s1) nabla"
  using assms
proof(induction P1≡"P1" nabla≡"(nabla, s)" P2≡"P2" arbitrary: s nabla1 nabla s1 P1 P2 rule: red_plus.induct)
  case (sred_single P1 s P2 nabla1 s1)
  then show "nabla1 ⊨ (subst s1) {}" by (simp add: ext_subst_def) 
next
  case (cred_single P1 nabla1 P2 nabla2 s1)
  have "P1  ⊢ nabla1 → P2" "(nabla2, s1) ∈ U P1" by fact+
  then show "nabla2 ⊨ (subst s1) nabla1" using P1_to_P2_cred by blast
next
  case (sred_step P1 s P2 nabla2 s2 P3 nabla1 s1)
  have "P1  ⊢ s ↝ P2" "(nabla1, s1)∈ U P1" by fact+ 
  then have "(nabla1, s1)∈ U P2" using P1_to_P2_sred by blast 
  moreover have IH: "(nabla1, s1)∈ U P2 ⟹  nabla1 ⊨ (subst s1) nabla2" by fact 
  ultimately show "nabla1 ⊨ (subst s1) nabla2" by simp 
next
  case (cred_step P1 nabla1 P2 nabla2 P3 nabla3 s1)
  have IH: "(nabla3, s1) ∈ U P2 ⟹ nabla3 ⊨ (subst s1) nabla2" by fact
  have as: "P1 ⊢ nabla1 → P2" "(nabla3, s1) ∈ U P1" by fact+ 
  
  from as have "nabla3 ⊨ (subst s1) nabla1" using P1_to_P2_cred by blast    
  moreover 
  from as have "(nabla3, s1) ∈ U P2" using P1_to_P2_cred by blast 
  then have "nabla3 ⊨ (subst s1) nabla2" using IH by blast
  ultimately show "nabla3 ⊨ (subst s1) (nabla2 ∪ nabla1)"
    by(auto simp add: ext_subst_def)
qed

lemma P1_to_P2_red_plus2:
  assumes "P1 ⊨ (nabla, s) ⇒ P2"
  and "(nabla1, s1) ∈ U P1"
shows "nabla1 ⊨ subst (s1 ∙ s) ≈ subst s1"
  using assms
proof(induction P1≡"P1" nablas≡"(nabla, s)" P2≡"P2" arbitrary: s nabla1 nabla s1 P1 P2 rule: red_plus.induct)
  case (sred_single P1 s P2 nabla1 s1)
  have "P1 ⊢s ↝P2" "(nabla1, s1) ∈ U P1" by fact+
  then show "nabla1 ⊨ subst (s1 ∙ s) ≈subst s1"
    using P1_to_P2_sred by blast
next
  case (cred_single P1 nabla1 P2 nabla2 s1)
  show "nabla2 ⊨ subst (s1 ∙ []) ≈subst s1"
    by (simp add: subst_equ_refl) 
next
  case (sred_step P1 s P2 nabla2 s2 P3 nabla1 s1)
  have IH: "(nabla1, s1) ∈ U P2 ⟹  nabla1 ⊨ subst (s1 ∙ s2) ≈subst s1" by fact
  have as: "P1 ⊢s ↝P2" "(nabla1, s1) ∈ U P1" by fact+

  from as have "(nabla1, s1) ∈ U P2" using P1_to_P2_sred by blast 
  with IH have "nabla1 ⊨ subst (s1 ∙ s2) ≈ subst s1" by blast
  then have "nabla1 ⊨ subst ((s1 ∙ s2) ∙ s) ≈ subst (s1 ∙ s)"
    by (simp add: subst_cancel_right)  
  moreover
  from as have "nabla1 ⊨ subst (s1 ∙ s) ≈subst s1"
    using P1_to_P2_sred by blast 
  ultimately
  show "nabla1 ⊨ subst (s1 ∙ (s2 ∙ s)) ≈ subst s1"
    using subst_assoc subst_trans by metis
next
  case (cred_step P1 nabla1 P2 nabla2 P3)
  show "nabla1 ⊨ subst (s1 ∙ []) ≈ subst s1"
    by (simp add: subst_equ_refl)
qed

lemma P1_from_P2_red_plus:
  assumes "P1 ⊨(nabla,s)⇒P2"
    and "(nabla1,s1)∈ U P2" and "nabla3⊨(subst s1)(nabla)"
  shows "(nabla1∪nabla3,(s1 ∙ s))∈ U P1"
  using assms
proof(induction P1 ≡ "P1" nablas≡"(nabla, s)" P2≡"P2" arbitrary: s nabla1 nabla nabla3 s1 P1 P2 rule: red_plus.induct)
  case (sred_single P1 s P2 nabla1 nabla3)
  have "P1 ⊢ s ↝ P2" "(nabla1, s1) ∈ U P2" by fact+
  then have "(nabla1, s1 ∙ s) ∈ U P1"
    using P1_from_P2_sred by simp
  then show "(nabla1 ∪ nabla3, s1 ∙ s) ∈ U P1"
    using P1_from_P2_sred solution_weak by simp
next
  case (cred_single P1 nabla P2 nabla1 nabla3)
  have "P1 ⊢ nabla → P2"
      "(nabla1, s1) ∈ U P2" 
      "nabla3 ⊨ (subst s1) nabla" by fact+
  hence "(nabla1 ∪ nabla3, s1) ∈ U P1"
    using P1_from_P2_cred by simp
  then show "(nabla1 ∪ nabla3, s1 ∙ []) ∈ U P1"
    using solution_comp_id by auto
next
  case (sred_step P1 s P2 nabla2 s2 P3 nabla1 nabla3)
  have IH: "(nabla1, s1) ∈ U P3 ⟹
     nabla3 ⊨ (subst s1) nabla2  ⟹ (nabla1 ∪ nabla3, s1 ∙ s2) ∈ U P2" by fact+
  have as: "(nabla1, s1) ∈ U P3" 
    "nabla3 ⊨ (subst s1) nabla2" 
    "P1 ⊢ s ↝ P2" by fact+
  hence "(nabla1 ∪ nabla3, s1 ∙ s2) ∈ U P2"
    using IH by simp
  hence "(nabla1 ∪ nabla3, (s1 ∙ s2) ∙ s) ∈ U P1"
    using as(3)
    by (simp add: P1_from_P2_sred)
  then show "(nabla1 ∪ nabla3, s1 ∙ (s2 ∙ s)) ∈ U P1"
    using solutions_subst_assoc by simp
next
  case (cred_step P1 nabla P2 nabla2 P3)
  have IH: "(nabla1, s1) ∈ U P3 ⟹
     nabla3 ⊨ (subst s1) nabla2  ⟹ (nabla1 ∪ nabla3, s1 ∙ []) ∈ U P2" by fact
  have as: "P1 ⊢ nabla → P2"
           "(nabla1, s1) ∈ U P3"
           "nabla3 ⊨ (subst s1) (nabla2 ∪ nabla)" by fact+
  have ext_substs: "nabla3 ⊨ (subst s1) (nabla2)" 
    "nabla3 ⊨ (subst s1) nabla"
    using ext_subst_strong[OF as(3)] by simp+
  hence a: "(nabla1 ∪ nabla3, s1 ∙ []) ∈ U P2"
    using IH as(2) by simp
  hence "(nabla1 ∪ nabla3 ∪ nabla3, s1 ∙ []) ∈ U P1"
    using as(1) ext_substs(2) P1_from_P2_cred solution_comp_id by blast
  then show "(nabla1 ∪ nabla3, s1 ∙ []) ∈ U P1"
    unfolding all_solutions_def using Un_absorb by simp
qed

lemma mgu: 
  assumes "P ⊨(nabla,s)⇒([],[])"
  shows "mgu P (nabla,s) ∧ idem (nabla,s)"
proof(rule mgu_idem)
  have i: "({},[]) ∈ U ([],[])"
    unfolding all_solutions_def by simp
  then show "(nabla, s) ∈ U P"
    using P1_from_P2_red_plus[OF assms i] 
      ext_subst_id  solution_comp_id(2) by simp
                            
  show "∀(nabla2, s2)∈ U P.  nabla2 ⊨ (subst s2) nabla ∧  
                       nabla2 ⊨ subst (s2 ∙ s) ≈ subst s2"
  proof
    fix x
    assume "x ∈ U P"
    then show "case x of (nabla2, s2) ⇒ 
               nabla2 ⊨ (subst s2) nabla ∧  
                       nabla2 ⊨ subst (s2 ∙ s) ≈ subst s2"
    proof (cases x)
      case (Pair nabla2 s2)
      hence "(nabla2,s2) ∈ U P"
        using ‹x ∈ U P› by auto
      hence "nabla2 ⊨ (subst s2) nabla ∧ nabla2 ⊨ subst (s2 ∙ s) ≈ subst s2"
        using assms P1_to_P2_red_plus2 P1_to_P2_red_plus3 by auto+
      with Pair show ?thesis by simp
    qed
  qed
qed



(*<*)
end
(*>*)