Theory NU

(*<*)
theory NU
imports NU_Termination
begin
(*>*)

section ‹Unification›

text ‹
  Proves that all problems that are stuck and fail, have no unifier.
›


definition stuck :: "problem_type set" where
  stuck_def: "stuck ≡ { P1. ¬(∃P2 nabla s. P1 ⊨(nabla,s)⇒P2)}"

                                                        
inductive fail :: "problem_type ⇒ bool" where
fail_occur_abst [intro!]: "⟦occurs X t⟧⟹ fail ((Susp pi X ≈? Abst a t) # xs, ys)" |
fail_occur_func [intro!]: "⟦occurs X t⟧⟹ fail (Susp pi X ≈?Func F t#xs,ys)" |
fail_occur_paar [intro!]: "⟦occurs X t1∨occurs X t2⟧⟹ fail (Susp pi X≈?Paar t1 t2#xs,ys)" |
fail_fresh_atom [intro!]: "fail ([],a♯? Atom a#ys)"|
fail_diff_atoms [intro!]: "a≠b⟹ fail (Atom a≈? Atom b#xs,ys)" |
fail_abst_unit [intro!]: " fail (Abst a t≈?Unit#xs,ys)" |
fail_abst_atom [intro!]: "fail (Abst a t≈?Atom b#xs,ys)" |
fail_abst_paar [intro!]: "fail (Abst a t≈?Paar t1 t2#xs,ys)" | 
fail_func_abst [intro!]: "fail (Func F t1≈?Abst a t#xs,ys)" |
fail_atom_unit [intro!]: "fail (Atom b≈?Unit#xs,ys)" |
fail_paar_unit [intro!]: "fail (Paar t1 t2≈?Unit#xs,ys)" |
fail_func_unit [intro!]: "fail (Func F t1≈?Unit#xs,ys)" | 
fail_atom_paar [intro!]: "fail (Atom a≈?Paar t1 t2#xs,ys)" |
fail_func_atom [intro!]: "fail (Func F t1≈?Atom a#xs,ys)" | 
fail_func_paar [intro!]: "fail (Func F t≈?Paar t1 t2#xs,ys)" |
fail_diff_func [intro!]: "⟦F1≠F2⟧⟹ fail (Func F1 t1≈?Func F2 t2#xs,ys)" |
fail_sym [intro!]: "fail (s ≈? t # xs, ys) ⟹ fail (t ≈? s # xs, ys)"


(*definition of normal form of a problem*)

definition 
  normal_form :: "problem_type ⇒ problem_type set" where 
  "normal_form P1 ≡ if P1 ∈ stuck then {P1} else {P2. ∃nabla s. P1⊨(nabla,s)⇒P2 ∧ P2∈stuck}"


(*the solutions of a problem are the same for symmetric equations -- MOVE to Mgu.thy*)

lemma U_equ_symm:
  shows "U (s≈?t#xs, ys) = U (t≈?s#xs, ys)"
  by(auto simp add: all_solutions_def equ_symm) 


(* a "failed" problem has no unifier *)

lemma fail_then_empty: 
  assumes "fail P1"
  shows "U P1 = {}"
  using assms
proof(induct rule: fail.induct)
  case (fail_occur_abst X t pi a xs ys)
  let ?P = "(Susp pi X ≈? Abst a t # xs, ys)"
  { assume "U ((Susp pi X, Abst a t) # xs, ys) ≠ {}"
    then obtain s nabla where eq1: "nabla ⊢ subst s (Susp pi X) ≈ Abst a (subst s t)"
      by (auto simp add: all_solutions_def)
    moreover
    have "occurs X t" by fact
    then obtain t' pi' where  
      eq2: "nabla ⊢ subst s (Susp pi X) ≈ swap pi' t'" "t'∈sub_trms (subst s t)"
      using occurs_sub_trm_equ by blast
    moreover  
    have eq3: "¬ nabla ⊢ (Abst a (subst s t)) ≈ swap pi' t'"
      using eq2 psub_trm_not_equ by auto
    then have "False" using eq1 eq2 eq3
      by (metis equ_symm equ_trans)
  }
  then show "U ?P = {}" by auto
next
  case (fail_occur_func X t pi F xs ys)
  let ?P = "(Susp pi X ≈? Func F t # xs, ys)"
  { assume "U ((Susp pi X, Func F t) # xs, ys) ≠ {}"
    then obtain s nabla where eq1: "nabla ⊢ subst s (Susp pi X) ≈ Func F (subst s t)"
      by (auto simp add: all_solutions_def)
    moreover
    have "occurs X t" by fact
    then obtain t' pi' where  
      eq2: "nabla ⊢ subst s (Susp pi X) ≈ swap pi' t'" "t'∈sub_trms (subst s t)"
      using occurs_sub_trm_equ by blast
    moreover  
    have eq3: "¬ nabla ⊢ (Func F (subst s t)) ≈ swap pi' t'"
      using eq2 psub_trm_not_equ by auto
    then have "False" using eq1 eq2 eq3
      by (metis equ_symm equ_trans)
  }
  then show "U ?P = {}" by auto
next
  case (fail_occur_paar X t1 t2 pi xs ys)
  let ?P = "(Susp pi X ≈? Paar t1 t2 # xs, ys)"
  have "occurs X t1 ∨ occurs X t2" by fact
  then show "U ?P = {}"
  proof
    {assume "occurs X t1"
      {assume "U ((Susp pi X, Paar t1 t2) # xs, ys) ≠ {}"
    then obtain s nabla where eq1: "nabla ⊢ subst s (Susp pi X) ≈ Paar (subst s t1) (subst s t2)"
      by (auto simp add: all_solutions_def)
    moreover
    have "occurs X t1" by fact
     then obtain t' pi' where  
      eq2: "nabla ⊢ subst s (Susp pi X) ≈ swap pi' t'" "t'∈sub_trms (subst s t1)"
      using occurs_sub_trm_equ by blast
    moreover  
    have eq3: "¬ nabla ⊢ (Paar (subst s t1) (subst s t2)) ≈ swap pi' t'"
      using eq2 psub_trm_not_equ by auto
    then have "False" using eq1 eq2 eq3
      by (metis equ_symm equ_trans)}
  then show "U ?P = {}" by auto}

    {assume "occurs X t2"
    {assume "U ((Susp pi X, Paar t1 t2) # xs, ys) ≠ {}"
      then obtain s nabla where eq1: "nabla ⊢ subst s (Susp pi X) ≈ Paar (subst s t1) (subst s t2)"
        by (auto simp add: all_solutions_def)
      moreover
      have "occurs X t2" by fact
      then obtain t' pi' where  
        eq2: "nabla ⊢ subst s (Susp pi X) ≈ swap pi' t'" "t'∈sub_trms (subst s t2)"
        using occurs_sub_trm_equ by blast
      moreover  
      have eq3: "¬ nabla ⊢ (Paar (subst s t1) (subst s t2)) ≈ swap pi' t'"
        using eq2 psub_trm_not_equ by auto
      then have "False" using eq1 eq2 eq3
        by (metis equ_symm equ_trans)
    }
    then show "U ?P = {}" by auto}
  qed
next
  case (fail_fresh_atom a ys)
  let ?P = "([], a ♯? Atom a # ys)"
  have "∄ nabla s. nabla ⊢ a ♯ subst s (Atom a)"
    using subst_atom Fresh_elims(3) by auto
  thus "U ?P = {}"
    using all_solutions_def by simp
next
  case (fail_diff_atoms a b xs ys)
  let ?P = "(Atom a ≈? Atom b # xs, ys)"
  from ‹a ≠ b› have "∄ nabla s. nabla ⊢ subst s (Atom a) ≈ subst s (Atom b)"
    using Equ_elims(1) by auto
  thus "U ?P = {}"
    using all_solutions_def by simp
next
  case (fail_abst_unit a t xs ys)
  let ?P = "(Abst a t ≈? Unit # xs, ys)"
  have "∄ nabla s. nabla ⊢ subst s (Abst a t) ≈ subst s Unit"
    by (auto elim: equ.cases)
  thus "U ?P = {}" 
    using all_solutions_def by simp
next
  case (fail_abst_atom a t b xs ys)
  let ?P = "(Abst a t ≈? Atom b # xs, ys)"
  have "∄ nabla s. nabla ⊢ subst s (Abst a t) ≈ subst s (Atom b)"
     by (auto elim: equ.cases)
  thus "U ?P = {}" 
    using all_solutions_def by simp
next
  case (fail_abst_paar a t t1 t2 xs ys)
  let ?P = "(Abst a t ≈? Paar t1 t2 # xs, ys)"
  have "∄ nabla s. nabla ⊢ subst s (Abst a t) ≈ subst s (Paar t1 t2)"
     by (auto elim: equ.cases)
  thus "U ?P = {}"
    using all_solutions_def by simp
next
  case (fail_func_abst F t1 a t xs ys)
  let ?P = "(Func F t1 ≈? Abst a t # xs, ys)"
  have "∄ nabla s. nabla ⊢ subst s (Func F t1) ≈ subst s (Abst a t)"
     by (auto elim: equ.cases)
  thus "U ?P = {}"
    using all_solutions_def by simp
next
  case (fail_atom_unit b xs ys)
  let ?P = "(Atom b ≈? Unit # xs, ys)"
  have "∄ nabla s. nabla ⊢ subst s (Atom b) ≈ subst s (Unit)"
     by (auto elim: equ.cases)
  thus "U ?P = {}" 
    using all_solutions_def by simp
next
  case (fail_paar_unit t1 t2 xs ys)
  let ?P = "(Paar t1 t2 ≈? Unit # xs, ys)"
  have "∄ nabla s. nabla ⊢ subst s (Paar t1 t2) ≈ subst s (Unit)"
     by (auto elim: equ.cases)
  thus "U ?P = {}" 
    using all_solutions_def by simp
next
  case (fail_func_unit F t1 xs ys)
  let ?P = "(Func F t1≈? Unit # xs, ys)"
  have "∄ nabla s. nabla ⊢ subst s (Func F t1) ≈ subst s (Unit)"
     by (auto elim: equ.cases)
  thus "U ?P = {}" 
    using all_solutions_def by simp
next
  case (fail_atom_paar b t1 t2 xs ys)
  let ?P = "(Atom b ≈? Paar t1 t2 # xs, ys)"
  have "∄ nabla s. nabla ⊢ subst s (Atom b) ≈ subst s (Paar t1 t2)"
     by (auto elim: equ.cases)
  thus "U ?P = {}" 
    using all_solutions_def by simp
next
  case (fail_func_atom F t1 b xs ys)
  let ?P = "(Func F t1 ≈? Atom b # xs, ys)"
  have "∄ nabla s. nabla ⊢ subst s (Func F t1) ≈ subst s (Atom b)"
     by (auto elim: equ.cases)
  thus "U ?P = {}" 
    using all_solutions_def by simp
next
  case (fail_func_paar F t t1 t2 xs ys)
  let ?P = "(Func F t ≈? Paar t1 t2 # xs, ys)"
  have "∄ nabla s. nabla ⊢ subst s (Func F t) ≈ subst s (Paar t1 t2)"
     by (auto elim: equ.cases)
  thus "U ?P = {}" 
    using all_solutions_def by simp
next
  case (fail_diff_func F1 F2 t1 t2 xs ys)
  let ?P = "(Func F1 t1 ≈? Func F2 t2 # xs, ys)"
  from ‹F1 ≠ F2› have "∄ nabla s. nabla ⊢ subst s (Func F1 t1) ≈ subst s (Func F2 t2)"
     by (auto elim: equ.cases)
  thus "U ?P = {}" 
    using all_solutions_def by simp
next
  case (fail_sym s t xs ys)
  let ?P = "(t ≈? s # xs, ys)"
  have "fail ((s, t) # xs, ys)"
    "U ((s, t) # xs, ys) = {}" by fact+
  thus "U ?P = {}"
   using all_solutions_def U_equ_symm by simp
qed


(* the only stuck problems are the "failed" problems and the empty problem *)

lemma not_reduce_then_fail:
  assumes "¬ (∃nabla s P'. ((t1 ≈? t2) # xs, ys) ⊨ (nabla,s) ⇒ P')"
  shows "fail ((t1 ≈? t2) # xs, ys)"
  using assms
proof(cases t1)
  case (Abst a t1')
  have t1_def: "t1 = Abst a t1'" by fact
  then show "fail ((t1, t2) # xs, ys)"
  proof(cases t2)
    case (Abst b t2')
    with t1_def
    have "((t1 ≈? t2)#xs,ys) ⊢[]↝ ((t1'≈?t2')#xs,ys) ∨ 
    ((t1≈? t2)#xs,ys) ⊢[]↝ ((t1'≈?swap [(a,b)] t2')#xs,(a♯?t2')#ys)"
      using abst_aa_sred abst_ab_sred by (cases "a=b") auto
    hence "∃ P2. ((t1 ≈? t2)#xs,ys) ⊨({},[])⇒P2"
      using sred_single by blast
    thus "fail ((t1, t2) # xs, ys)"
      using assms by simp
  next
    case (Susp pi X)
    have t2_def: "t2 = Susp pi X" by fact
    with t1_def
    show "fail ((t1, t2) # xs, ys)" 
    proof(cases "occurs X t1'")
      case True
      with t1_def t2_def
      show "fail ((t1, t2) # xs, ys)" 
      using fail_sym[OF fail_occur_abst[OF True]] by simp
    next
      case False
      with t1_def 
      have not_occurs: "¬ occurs X t1" by simp
      hence "((t1≈? Susp pi X)#xs,ys) 
                    ⊢[(X,swap (rev pi) t1)]↝ apply_subst [(X,swap (rev pi) t1)] (xs,ys)"
        using t1_def var_2_sred[OF not_occurs] by simp
       hence "∃ P2 s. ((t1 ≈? t2)#xs,ys) ⊨({},s)⇒P2"
         using t1_def t2_def sred_single by blast
       thus "fail ((t1, t2) # xs, ys)" 
         using assms by simp
    qed
  qed (auto)
next
  case (Susp pi X)
  have t1_def: "t1 = Susp pi X" by fact
  then show "fail ((t1, t2) # xs, ys)"
  proof(cases "occurs X t2")
    case True
    then show "fail ((t1, t2) # xs, ys)"
    proof(cases t2)
      case (Abst a t2')
      have t2_def: "t2 = Abst a t2'" by fact
      with True
      have "occurs X t2'" unfolding occurs.simps(4) t2_def by argo
      thus "fail ((t1, t2) # xs, ys)"
        using t1_def t2_def fail_occur_abst by simp
    next
      case (Susp pi' Y)
      have t2_def: "t2 = Susp pi' Y" by fact
      have "X = Y" 
        using True unfolding t2_def occurs.simps(3)
        by argo
      hence "((Susp pi X≈?Susp pi' Y)#xs,ys) 
                                ⊢[]↝ (xs,(map (λa. a♯? Susp [] X) (ds_list pi pi'))@ys)"
        using susp_sred by simp
      hence "∃ P2. ((t1 ≈? t2)#xs,ys) ⊨({},[])⇒P2"
        using sred_single t1_def t2_def by blast
      thus"fail ((t1, t2) # xs, ys)"
        using assms by simp
    next
      case (Paar t21 t22)
      have t2_def: "t2 = Paar t21 t22" by fact
      with True
      have "occurs X t21 ∨ occurs X t22" unfolding occurs.simps(5) t2_def by argo
      thus "fail ((t1, t2) # xs, ys)"
        using t1_def t2_def fail_occur_paar by simp
    next
      case (Func f t2')
      have t2_def: "t2 = Func f t2'" by fact
      with True
      have "occurs X t2'" unfolding occurs.simps(6) t2_def by argo
      thus "fail ((t1, t2) # xs, ys)"
        using t1_def t2_def fail_occur_func by simp
    qed (auto simp add: True)
  next
    case False
    hence "((Susp pi X, t2) # xs, ys) ⊢ 
    [(X, swap (rev pi) t2)] ↝ apply_subst [(X, swap (rev pi) t2)] (xs, ys)"
      using var_1_sred[OF False] by simp
    hence "∃ P2 s. ((t1 ≈? t2)#xs,ys) ⊨({},s)⇒P2"
      using t1_def sred_single by blast
    thus "fail ((t1, t2) # xs, ys)" 
      using assms by simp
  qed
next
  case Unit
  have t1_def: "t1 = Unit" by fact
  then show "fail ((t1, t2) # xs, ys)"
  proof(cases t2)
    case (Susp pi X)
    have t2_def: "t2 =  Susp pi X" by fact
    with t1_def have not_occurs: "¬ occurs X t1" by simp
    hence "((t1≈? Susp pi X)#xs,ys) 
                    ⊢[(X,swap (rev pi) t1)]↝ apply_subst [(X,swap (rev pi) t1)] (xs,ys)"
      using t1_def var_2_sred[OF not_occurs] by simp
    hence "∃ P2 s. ((t1 ≈? t2)#xs,ys) ⊨({},s)⇒P2"
      using t1_def t2_def sred_single by blast
    thus "fail ((t1, t2) # xs, ys)" 
      using assms by simp
  next
    case Unit
    with t1_def
    have "((t1 ≈? t2)#xs,ys) ⊢[]↝ (xs,ys)"
      using unit_sred by auto
    hence "∃ P2. ((t1 ≈? t2)#xs,ys) ⊨({},[])⇒P2"
      using sred_single by blast
    thus "fail ((t1, t2) # xs, ys)"
      using assms by simp
  qed (auto)
next
  case (Atom a)
  have t1_def: "t1 = Atom a" by fact
  then show "fail ((t1, t2) # xs, ys)" 
  proof(cases t2)
    case (Susp pi X)
    have t2_def: "t2 =  Susp pi X" by fact
    with t1_def have not_occurs: "¬ occurs X t1" by simp
    hence "((t1≈? Susp pi X)#xs,ys) 
                    ⊢[(X,swap (rev pi) t1)]↝ apply_subst [(X,swap (rev pi) t1)] (xs,ys)"
      using t1_def var_2_sred[OF not_occurs] by simp
    hence "∃ P2 s. ((t1 ≈? t2)#xs,ys) ⊨({},s)⇒P2"
      using t1_def t2_def sred_single by blast
    thus "fail ((t1, t2) # xs, ys)" 
      using assms by simp
  next
    case (Atom b)
    have t2_def: "t2 = Atom b" by fact
    then show "fail ((t1, t2) # xs, ys)"
    proof(cases "a=b")
      case True
      hence "((t1 ≈? t2)#xs,ys) ⊢[]↝ (xs,ys)"
        using t2_def t1_def atom_sred by simp
      hence "∃ P2. ((t1 ≈? t2)#xs,ys) ⊨({},[])⇒P2"
        using sred_single by blast
      thus "fail ((t1, t2) # xs, ys)"
        using assms by simp
    qed (simp add: t1_def t2_def fail_diff_atoms)
  qed(auto)
next
  case (Paar t11 t12)
  have t1_def: "t1 = Paar t11 t12" by fact
  then show "fail ((t1, t2) # xs, ys)"
  proof(cases t2)
  next
    case (Susp pi X)
    have t2_def: "t2 = Susp pi X" by fact
    then show "fail ((t1, t2) # xs, ys)" 
    proof(cases "occurs X t11 ∨ occurs X t12")
      case True
      then show "fail ((t1, t2) # xs, ys)" 
        using t1_def t2_def fail_sym[OF fail_occur_paar[OF True]] by simp
    next
      case False
      hence "¬ occurs X t1"
        using t1_def by simp
      hence "((t1≈?Susp pi X)#xs,ys) 
                               ⊢[(X,swap (rev pi) t1)]↝ apply_subst [(X,swap (rev pi) t1)] (xs,ys)"
        by auto
      hence "∃ P2 s. ((t1 ≈? t2)#xs,ys) ⊨({},s)⇒P2"
        using t1_def t2_def sred_single by blast
      thus "fail ((t1, t2) # xs, ys)" 
        using assms by simp
    qed
  next
    case (Paar t21 t22)
    have t2_def: "t2 = Paar t21 t22" by fact
    with t1_def have
    "((t1 ≈? t2)#xs,ys) ⊢[]↝ ((t11≈?t21)#(t12≈?t22)#xs,ys)"
      using paar_sred by simp
    hence "∃ P2. ((t1 ≈? t2)#xs,ys) ⊨({},[])⇒P2"
      using sred_single by blast
    thus "fail ((t1, t2) # xs, ys)"
      using assms by simp
  qed(auto)
next
  case (Func f t1')
  have t1_def: "t1 = Func f t1'" by fact
  then show "fail ((t1, t2) # xs, ys)"
  proof(cases t2)
    case (Susp pi X)
     have t2_def: "t2 = Susp pi X" by fact
     with t1_def
    show "fail ((t1, t2) # xs, ys)" 
    proof(cases "occurs X t1'")
      case True
      with t1_def t2_def
      show "fail ((t1, t2) # xs, ys)" 
      using fail_sym[OF fail_occur_func[OF True]] by simp
    next
      case False
      with t1_def 
      have not_occurs: "¬ occurs X t1" by simp
      hence "((t1≈? Susp pi X)#xs,ys) 
                    ⊢[(X,swap (rev pi) t1)]↝ apply_subst [(X,swap (rev pi) t1)] (xs,ys)"
        using t1_def var_2_sred[OF not_occurs] by simp
       hence "∃ P2 s. ((t1 ≈? t2)#xs,ys) ⊨({},s)⇒P2"
         using t1_def t2_def sred_single by blast
       thus "fail ((t1, t2) # xs, ys)" 
         using assms by simp
    qed
  next
    case (Func g t2')
     have t2_def: "t2 = Func g t2'" by fact
     then show "fail ((t1, t2) # xs, ys)"
     proof(cases "f=g")
       case True
       hence "((t1 ≈? t2)#xs,ys) ⊢[]↝ ((t1'≈?t2')#xs,ys)"
         using t1_def t2_def func_sred by simp
       hence "∃ P2. ((t1 ≈? t2)#xs,ys) ⊨({},[])⇒P2"
         using sred_single by blast
       thus "fail ((t1, t2) # xs, ys)"
         using assms by simp
     next
       case False
       then show "fail ((t1, t2) # xs, ys)"
         using t1_def t2_def fail_diff_func[OF False] by simp
     qed
  qed(auto)
qed


lemma fresh_reduces_if_not_atom:
  assumes "t ≠ Atom a"
  shows "∃P2 nabla s. ([], (a ♯? t) # xs) ⊨ (nabla,s) ⇒ P2"
  using assms cred_single
proof(cases t)
  case (Abst b t')
  then show "∃P2 nabla s. ([], (a ♯? t) # xs) ⊨ (nabla, s) ⇒ P2"
  proof(cases "a=b")
    case True
    hence "([], (a ♯? t) # xs) ⊢{}→ ([],xs)"
      unfolding Abst using abst_aa_cred by simp
    then show "∃P2 nabla s. ([], (a ♯? t) # xs) ⊨ (nabla, s) ⇒ P2"
      using cred_single by blast
  next
    case False
    hence "([], (a ♯? t) # xs) ⊢{}→ ([], (a♯? t') # xs)"
      unfolding  Abst using abst_ab_cred by simp
    then show "∃P2 nabla s. ([], (a ♯? t) # xs) ⊨ (nabla, s) ⇒ P2"
      using cred_single by blast
  qed
next
  case (Atom b)
  with assms
  have "a ≠ b" by simp
  hence "([], (a ♯? t) # xs) ⊢ {}→ ([],xs)"
    unfolding Atom using atom_cred by simp
  then show "∃P2 nabla s. ([], (a ♯? t) # xs) ⊨ (nabla, s) ⇒ P2"
    using cred_single by blast
qed (simp add: cred_single, blast+)


lemma empty_stuck:
  shows "([],[]) ∈ stuck"
proof-
  have "¬ (∃P2 nabla s. ([],[]) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  thus "([],[]) ∈ stuck"
    unfolding stuck_def by auto
qed

lemma fail_is_stuck:
  assumes "fail P"
  shows "P ∈ stuck"
  using assms
proof(induct rule: fail.induct)
  case (fail_occur_abst X t pi a xs ys)
  have t_occurs: "occurs X t" by fact
  moreover have "¬ (∃P2 nabla s. ((Susp pi X ≈? Abst a t) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
  proof
    assume "∃P2 nabla s. ((Susp pi X ≈? Abst a t) # xs, ys) ⊨ (nabla,s) ⇒ P2"
    then obtain P2 nabla s where
    red: "((Susp pi X ≈? Abst a t) # xs, ys) ⊨ (nabla,s) ⇒ P2"
      by auto
    thus False 
    proof (cases rule: red_plus.cases)
      case sred_single
      have "((Susp pi X, Abst a t) # xs, ys) ⊢ s ↝ P2" by fact
      hence "¬ occurs X t" 
         by (auto elim: s_red.cases)
      with t_occurs show False by simp
    next
      case cred_single
      have "((Susp pi X, Abst a t) # xs, ys) ⊢ nabla → P2" by fact
      moreover have "fst ((Susp pi X, Abst a t) # xs, ys) ≠ []"
        by simp
      ultimately show False 
        using c_red_eqs_empty by blast
    next
      case (sred_step s1 P3 s2)
      have "((Susp pi X, Abst a t) # xs, ys) ⊢ s1 ↝ P3" by fact
      hence "¬ occurs X t" 
        by (auto elim: s_red.cases)
      with t_occurs show False by simp
    next
      case (cred_step nabla1 P3 nabla2)
      have "((Susp pi X, Abst a t) # xs, ys) ⊢ nabla1 → P3" by fact
       moreover have "fst ((Susp pi X, Abst a t) # xs, ys) ≠ []"
        by simp
      ultimately show False 
        using c_red_eqs_empty by blast
    qed
  qed
  then show "((Susp pi X, Abst a t) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_occur_func X t pi F xs ys)
  have t_occurs: "occurs X t" by fact
  moreover have "¬ (∃P2 nabla s. ((Susp pi X ≈? Func F t) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
  proof
    assume "∃P2 nabla s. ((Susp pi X ≈? Func F t) # xs, ys) ⊨ (nabla,s) ⇒ P2"
    then obtain P2 nabla s where
    red: "((Susp pi X ≈? Func F t) # xs, ys) ⊨ (nabla,s) ⇒ P2"
      by auto
    thus False 
    proof (cases rule: red_plus.cases)
      case sred_single
      have "((Susp pi X, Func F t) # xs, ys) ⊢ s ↝ P2" by fact
      hence "¬ occurs X t" 
         by (auto elim: s_red.cases)
      with t_occurs show False by simp
    next
      case cred_single
      have "((Susp pi X, Func F t) # xs, ys) ⊢ nabla → P2" by fact
      moreover have "fst ((Susp pi X, Func F t) # xs, ys) ≠ []"
        by simp
      ultimately show False 
        using c_red_eqs_empty by blast
    next
      case (sred_step s1 P3 s2)
      have "((Susp pi X, Func F t) # xs, ys) ⊢ s1 ↝ P3" by fact
      hence "¬ occurs X t" 
         by (auto elim: s_red.cases)
      with t_occurs show False by simp
    next
      case (cred_step nabla1 P3 nabla2)
      have "((Susp pi X, Func F t) # xs, ys) ⊢ nabla1 → P3" by fact
       moreover have "fst ((Susp pi X, Func F t) # xs, ys) ≠ []"
        by simp
      ultimately show False 
        using c_red_eqs_empty by blast
    qed
  qed
  then show "((Susp pi X, Func F t) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_occur_paar X t1 t2 pi xs ys)
  have "occurs X t1 ∨ occurs X t2" by fact
  hence t_occurs: "occurs X (Paar t1 t2)"
    using occurs.simps(5) by auto
  moreover have "¬ (∃P2 nabla s. ((Susp pi X ≈? Paar t1 t2) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
  proof
    assume "∃P2 nabla s. ((Susp pi X ≈? Paar t1 t2) # xs, ys) ⊨ (nabla,s) ⇒ P2"
    then obtain P2 nabla s where
    red: "((Susp pi X ≈? Paar t1 t2) # xs, ys) ⊨ (nabla,s) ⇒ P2"
      by auto
    thus False 
    proof (cases rule: red_plus.cases)
      case sred_single
      have "((Susp pi X, Paar t1 t2) # xs, ys) ⊢ s ↝ P2" by fact
      hence "¬ occurs X (Paar t1 t2)" 
        by (auto elim: s_red.cases)
      with t_occurs show False by simp
    next
      case cred_single
      have "((Susp pi X, Paar t1 t2) # xs, ys) ⊢ nabla → P2" by fact
      moreover have "fst ((Susp pi X, Paar t1 t2) # xs, ys) ≠ []"
        by simp
      ultimately show False 
        using c_red_eqs_empty by blast
    next
      case (sred_step s1 P3 s2)
      have "((Susp pi X, Paar t1 t2) # xs, ys) ⊢ s1 ↝ P3" by fact
      hence "¬ occurs X (Paar t1 t2)" 
        by (auto elim: s_red.cases)
      with t_occurs show False by simp
    next
      case (cred_step nabla1 P3 nabla2)
      have "((Susp pi X, Paar t1 t2) # xs, ys) ⊢ nabla1 → P3" by fact
       moreover have "fst ((Susp pi X, Paar t1 t2) # xs, ys) ≠ []"
        by simp
      ultimately show False 
        using c_red_eqs_empty by blast
    qed
  qed
  then show "((Susp pi X, Paar t1 t2) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_fresh_atom a ys)
  have "¬ (∃P2 nabla s. ([], (a, Atom a) # ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "([], (a, Atom a) # ys) ∈ stuck" 
    unfolding stuck_def by simp
next
  case (fail_diff_atoms a b xs ys)
  hence "¬ (∃P2 nabla s. ((Atom a, Atom b) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Atom a, Atom b) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_abst_unit a t xs ys)
  hence "¬ (∃P2 nabla s. ((Abst a t, Unit) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Abst a t, Unit) # xs, ys) ∈ stuck"
     unfolding stuck_def by simp
next
  case (fail_abst_atom a t b xs ys)
  hence "¬ (∃P2 nabla s. ((Abst a t, Atom b) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Abst a t, Atom b) # xs, ys) ∈ stuck"
     unfolding stuck_def by simp
next
  case (fail_abst_paar a t t1 t2 xs ys)
  hence "¬ (∃P2 nabla s. ((Abst a t, Paar t1 t2) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Abst a t, Paar t1 t2) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_func_abst F t1 a t xs ys)
  hence "¬ (∃P2 nabla s. ((Func F t1, Abst a t) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Func F t1, Abst a t) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_atom_unit b xs ys)
  hence "¬ (∃P2 nabla s. ((Atom b, Unit) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Atom b, Unit) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_paar_unit t1 t2 xs ys)
  hence "¬ (∃P2 nabla s. ((Paar t1 t2, Unit) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Paar t1 t2, Unit) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_func_unit F t1 xs ys)
  hence "¬ (∃P2 nabla s. ((Func F t1, Unit) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Func F t1, Unit) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_atom_paar a t1 t2 xs ys)
  hence "¬ (∃P2 nabla s. ((Atom a, Paar t1 t2) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Atom a, Paar t1 t2) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_func_atom F t1 a xs ys)
  hence "¬ (∃P2 nabla s. ((Func F t1, Atom a) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Func F t1, Atom a) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_func_paar F t t1 t2 xs ys)
   hence "¬ (∃P2 nabla s. ((Func F t, Paar t1 t2) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Func F t, Paar t1 t2) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_diff_func F1 F2 t1 t2 xs ys)
   hence "¬ (∃P2 nabla s. ((Func F1 t1, Func F2 t2) # xs, ys) ⊨ (nabla,s) ⇒ P2)"
    by (auto elim: red_plus.cases s_red.cases c_red.cases)
  then show "((Func F1 t1, Func F2 t2) # xs, ys) ∈ stuck"
    unfolding stuck_def by simp
next
  case (fail_sym s t xs ys)
  hence not_reduce: "∄ P2 nabla s1. ((s, t) # xs, ys) ⊨ (nabla, s1) ⇒ P2"
    unfolding stuck_def by simp
  have"∄ P2 nabla s1. ((t, s) # xs, ys) ⊨ (nabla, s1) ⇒ P2"
  proof
    assume "∃P2 nabla s1. ((t, s) # xs, ys) ⊨ (nabla, s1) ⇒ P2"
    then obtain P2 nabla s1 where 
      reduces: "((t, s) # xs, ys) ⊨ (nabla, s1) ⇒ P2"
      by auto
    hence "∃ P3 nabla1 s2. ((s, t) # xs, ys) ⊨ (nabla1, s2) ⇒ P3"
      using red_plus_symm[of ‹((t, s) # xs, ys)› t s xs ys nabla s1 P2] by auto
    with not_reduce show False by simp
  qed
  then show "((t, s) # xs, ys) ∈ stuck" unfolding stuck_def by simp
qed


lemma stuck_equiv: 
  shows "stuck = {([],[])} ∪ {P1. fail P1}"      
proof (rule set_eqI, rule iffI)
  fix P
  {assume P_is_stuck: "P ∈ stuck"
  then obtain eqs freshs where 
    P_def: "P = (eqs, freshs)" by (cases P)
  show "P ∈ {([], [])} ∪ {P1. fail P1}"
  proof(cases eqs)
    case Nil
    then show "P ∈ {([], [])} ∪ {P1. fail P1}"
    proof(cases freshs)
      case Nil
      with ‹eqs = []›
      show "P ∈ {([], [])} ∪ {P1. fail P1}" using P_def by simp
    next
      case (Cons c freshs')
      then obtain a t where c_def: "c = a ♯? t" by force
      have "t = Atom a" 
        using fresh_reduces_if_not_atom P_is_stuck 
        unfolding stuck_def P_def Nil Cons c_def by blast
      hence "fail P" 
        unfolding P_def Nil Cons c_def using fail_fresh_atom by simp
      thus "P ∈ {([], [])} ∪ {P1. fail P1}" by auto
    qed
  next
    case(Cons e eqs')
    then obtain s t where e_def: "e = s ≈? t" by force
    have "fail P" 
      using P_is_stuck unfolding P_def Cons e_def 
        stuck_def using not_reduce_then_fail by simp
    thus "P ∈ {([], [])} ∪ {P1. fail P1}" by auto
  qed }

  {assume "P ∈ {([], [])} ∪ {P1. fail P1}"
    then show "P ∈ stuck" 
      using empty_stuck fail_is_stuck by blast
      }
qed


(*if reduces to a non-solvable problem, then it is non-solvable *)

lemma u_empty_sred: 
  assumes "P1⊢s↝P2" and "U P2 ={}"
  shows "U P1 = {}"
  using assms P1_from_P2_sred all_solutions_def P1_to_P2_sred by blast


lemma u_empty_cred:
  assumes "P1⊢nabla→P2" and "U P2 ={}"
  shows "U P1={}"
  using assms P1_from_P2_cred all_solutions_def P1_to_P2_cred by blast


lemma u_empty_red_plus: 
  assumes "P1⊨(nabla,s)⇒P2" and "U P2 ={}"
  shows "U P1={}"
  using assms P1_from_P2_red_plus all_solutions_def P1_to_P2_red_plus1 by fast


(* all problems that cannot be solved produce "failed" problems only *)

lemma empty_then_fail: 
assumes "U P1={}"
shows" (∀P ∈ normal_form P1. fail P)"
proof
  fix P
  assume P_is_nf: "P ∈ normal_form P1"
  hence P_is_stuck: "P ∈ stuck"
    using normal_form_def by (cases "P1 ∈ stuck") auto
  hence P_is_empty_or_fails: "P = ([],[]) ∨ fail P"
    using stuck_equiv by auto
  have "P ≠ ([],[])"
  proof
    assume P_empty: "P = ([],[])"
    hence solution: "({},[]) ∈ U P"
      using all_solutions_def by simp
    hence P_neq: "P ≠ P1" 
    using assms by auto
    show False
    proof(cases "P1∈ stuck")
      case True
      then have "normal_form P1 = {P1}"
        unfolding normal_form_def by simp
      with P_is_nf have "P = P1" by simp
      with P_neq show False by simp
    next
      case False
      with P_is_nf
      obtain nabla s where P1_goes_to_P: "P1 ⊨ (nabla, s) ⇒ P" 
        unfolding normal_form_def by auto
      hence "({} ∪ nabla, [] ∙ s) ∈ U P1"
        using P1_from_P2_red_plus[OF P1_goes_to_P solution ext_subst_id] by simp
      with assms show False by simp
    qed
  qed
  thus "fail P"
    using P_is_empty_or_fails by simp
qed


(* if a problem can be solved then no "failed" problem is produced *)

lemma not_empty_then_not_fail: 
  assumes "U P1≠{}"
  shows "¬(∃P∈ normal_form P1. fail P)"
proof(simp, rule ballI)
  fix P
  assume P_is_nf: "P ∈ normal_form P1"
  show "¬ fail P"
  proof
    assume P_fails: "fail P"
    show False
    proof(cases "P1∈ stuck")
      case True
      have "normal_form P1 = {P1}"
        unfolding normal_form_def using True by simp
      hence "P = P1" using P_is_nf by simp
      with P_fails have "U P1 = {}"
        using fail_then_empty by simp
      thus False using assms by simp
      next
        case False
        with P_is_nf
        obtain nabla s where P1_goes_to_P: "P1 ⊨ (nabla, s) ⇒ P"
          unfolding normal_form_def by auto
        moreover have "U P = {}" 
          using P_fails fail_then_empty by simp
        ultimately have "U P1 = {}" 
          using u_empty_red_plus by simp
        then show False 
          using assms by simp
      qed
    qed
  qed




(*<*)
end
(*>*)