Theory NU_Computable_Completeness

(*<*)
theory NU_Computable_Completeness
  imports NU_Computable_Soundness
begin
(*>*)

section ‹Completeness of the computable algorithm›

text‹One unfolding of a failing ‹sred_fun› either hits a failure pattern or performs an ‹s_red› step
after which ‹sred_fun› still fails.›

lemma sred_fun_unfold_none:
  assumes "sred_fun (((t1 ≈? t2) # xs, ys), nabla, s) = None"
  shows "fail ((t1 ≈? t2) # xs, ys) ∨ 
         (∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None)"
proof -
  ― ‹Unfold ‹sred_fun› exactly once: H is the case distinction of the definition, whose 
     value is None. From now on ‹sred_fun› is never unfolded again.›
  note H = trans[OF sred_fun.simps(2)[symmetric] assms]
  ― ‹The goal has two ways out: either the problem is a failure pattern (a fail fact),
     or one ‹s_red› step leads to a problem on which ‹sred_fun› still fails.›
  show ?thesis
  proof (cases t1)
    case Unit
    show ?thesis
    proof (cases t2)
      case Unit
      ― ‹Rule ‹unit_sred›: the equation is removed, the recursive call fails.›
      have "sred_fun ((xs, ys), nabla, [] ∙ s) = None"
        using H unfolding ‹t1 = Unit› ‹t2 = Unit› by (simp del: sred_fun.simps)
      then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
        using unit_sred unfolding ‹t1 = Unit› ‹t2 = Unit› by blast
      then show ?thesis by simp
    next
      case (Susp pi X)
      ― ‹Rule ‹var_2_sred›: X is instantiated with Unit, the recursive call fails.›
      let ?σ = "[(X, swap (rev pi) Unit)]"
      have step: "((Unit ≈? Susp pi X) # xs, ys) ⊢ ?σ ↝ apply_subst ?σ (xs, ys)"
        using var_2_sred by (simp del: swap.simps)
      have "sred_fun (apply_subst ?σ (xs, ys), nabla, ?σ ∙ s) = None"
        using H unfolding ‹t1 = Unit› ‹t2 = Susp pi X› by (simp del: sred_fun.simps)
      then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
        using step unfolding ‹t1 = Unit› ‹t2 = Susp pi X› by blast
      then show ?thesis by simp
    next
      case (Atom b)
      ― ‹Clash: Unit vs. Atom.›
      have "fail ((Unit ≈? Atom b) # xs, ys)"
        using fail_sym[OF fail_atom_unit] by simp
      then show ?thesis unfolding ‹t1 = Unit› ‹t2 = Atom b›
        by simp
    next
      case (Paar v1 v2)
      ― ‹Clash: Unit vs. Paar.›
      have "fail ((Unit ≈? Paar v1 v2) # xs, ys)"
        using fail_sym[OF fail_paar_unit] by simp
      then show ?thesis unfolding ‹t1 = Unit› ‹t2 = Paar v1 v2›
        by simp
    next
      case (Func G v)
      ― ‹Clash: Unit vs. Func.›
      have "fail ((Unit ≈? Func G v) # xs, ys)"
        using fail_sym[OF fail_func_unit] by simp
      then show ?thesis unfolding ‹t1 = Unit› ‹t2 = Func G v›
        by simp
    next
      case (Abst b v)
      ― ‹Clash: Unit vs. Abst.›
      have "fail ((Unit ≈? Abst b v) # xs, ys)"
        using fail_sym[OF fail_abst_unit] by simp
      then show ?thesis unfolding ‹t1 = Unit› ‹t2 = Abst b v›
        by simp
    qed
  next
    case (Atom a)
    show ?thesis
    proof (cases t2)
      case (Atom b)
      show ?thesis
      proof (cases "a = b")
        case True
        ― ‹Rule ‹atom_sred›: equal atoms are removed, the recursive call fails.›
        have "sred_fun ((xs, ys), nabla, [] ∙ s) = None"
          using H unfolding ‹t1 = Atom a› ‹t2 = Atom b› ‹a = b› by (simp del: sred_fun.simps)
        then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
          using atom_sred unfolding ‹t1 = Atom a› ‹t2 = Atom b› ‹a = b› by blast
        then show ?thesis by simp
      next
        case False
        ― ‹Clash: different atoms.›
        have "fail ((Atom a ≈? Atom b) # xs, ys)"
          using False fail_diff_atoms by simp
        then show ?thesis unfolding ‹t1 = Atom a› ‹t2 = Atom b›
          by simp
      qed
    next
      case (Susp pi X)
      ― ‹Rule ‹var_2_sred›: X is instantiated with the (permuted) atom.›
      let ?σ = "[(X, swap (rev pi) (Atom a))]"
      have step: "((Atom a ≈? Susp pi X) # xs, ys) ⊢ ?σ ↝ apply_subst ?σ (xs, ys)"
        using var_2_sred by (simp del: swap.simps)
      have "sred_fun (apply_subst ?σ (xs, ys), nabla, ?σ ∙ s) = None"
        using H unfolding ‹t1 = Atom a› ‹t2 = Susp pi X› by (simp del: sred_fun.simps)
      then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
        using step unfolding ‹t1 = Atom a› ‹t2 = Susp pi X› by blast
      then show ?thesis by simp
    next
      case Unit
      ― ‹Clash: Atom vs. Unit.›
      have "fail ((Atom a ≈? Unit) # xs, ys)"
        using fail_atom_unit by simp
      then show ?thesis unfolding ‹t1 = Atom a› ‹t2 = Unit›
        by simp
    next
      case (Paar v1 v2)
      ― ‹Clash: Atom vs. Paar.›
      have "fail ((Atom a ≈? Paar v1 v2) # xs, ys)"
        using fail_atom_paar by simp
      then show ?thesis unfolding ‹t1 = Atom a› ‹t2 = Paar v1 v2›
        by simp
    next
      case (Func G v)
      ― ‹Clash: Atom vs. Func.›
      have "fail ((Atom a ≈? Func G v) # xs, ys)"
        using fail_sym[OF fail_func_atom] by simp
      then show ?thesis unfolding ‹t1 = Atom a› ‹t2 = Func G v›
        by simp
    next
      case (Abst b v)
      ― ‹Clash: Atom vs. Abst.›
      have "fail ((Atom a ≈? Abst b v) # xs, ys)"
        using fail_sym[OF fail_abst_atom] by simp
      then show ?thesis unfolding ‹t1 = Atom a› ‹t2 = Abst b v›
        by simp
    qed
  next
    case (Paar u1 u2)
    show ?thesis
    proof (cases t2)
      case (Paar v1 v2)
      ― ‹Rule ‹paar_sred›: split into two equations, the recursive call fails.›
      have "sred_fun (((u1 ≈? v1) # (u2 ≈? v2) # xs, ys), nabla, [] ∙ s) = None"
        using H unfolding ‹t1 = Paar u1 u2› ‹t2 = Paar v1 v2› by (simp del: sred_fun.simps)
      then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
        using paar_sred unfolding ‹t1 = Paar u1 u2› ‹t2 = Paar v1 v2› by blast
      then show ?thesis by simp
    next
      case (Susp pi X)
      show ?thesis
      proof (cases "occurs X (Paar u1 u2)")
        case True
        ― ‹Occurs check fails.›
        have "fail ((Susp pi X ≈? Paar u1 u2) # xs, ys)"
          using True fail_occur_paar by (simp split: if_splits)
        then have "fail ((Paar u1 u2 ≈? Susp pi X) # xs, ys)"
          using fail_sym by simp
        then show ?thesis unfolding ‹t1 = Paar u1 u2› ‹t2 = Susp pi X›
          by simp
      next
        case False
        ― ‹Rule ‹var_2_sred›: X is instantiated with the pair, the recursive call fails.›
        let ?σ = "[(X, swap (rev pi) (Paar u1 u2))]"
        have step: "((Paar u1 u2 ≈? Susp pi X) # xs, ys) ⊢ ?σ ↝ apply_subst ?σ (xs, ys)"
          using False var_2_sred by (simp del: swap.simps)
        have "sred_fun (apply_subst ?σ (xs, ys), nabla, ?σ ∙ s) = None"
          using H False unfolding ‹t1 = Paar u1 u2› ‹t2 = Susp pi X› by (simp del: sred_fun.simps)
        then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
          using step unfolding ‹t1 = Paar u1 u2› ‹t2 = Susp pi X› by blast
        then show ?thesis by simp
      qed
    next
      case Unit
      ― ‹Clash: Paar vs. Unit.›
      have "fail ((Paar u1 u2 ≈? Unit) # xs, ys)"
        using fail_paar_unit by simp
      then show ?thesis unfolding ‹t1 = Paar u1 u2› ‹t2 = Unit›
        by simp
    next
      case (Atom b)
      ― ‹Clash: Paar vs. Atom.›
      have "fail ((Paar u1 u2 ≈? Atom b) # xs, ys)"
        using fail_sym[OF fail_atom_paar] by simp
      then show ?thesis unfolding ‹t1 = Paar u1 u2› ‹t2 = Atom b›
        by simp
    next
      case (Func G v)
      ― ‹Clash: Paar vs. Func.›
      have "fail ((Paar u1 u2 ≈? Func G v) # xs, ys)"
        using fail_sym[OF fail_func_paar] by simp
      then show ?thesis unfolding ‹t1 = Paar u1 u2› ‹t2 = Func G v›
        by simp
    next
      case (Abst b v)
      ― ‹Clash: Paar vs. Abst.›
      have "fail ((Paar u1 u2 ≈? Abst b v) # xs, ys)"
        using fail_sym[OF fail_abst_paar] by simp
      then show ?thesis unfolding ‹t1 = Paar u1 u2› ‹t2 = Abst b v›
        by simp
    qed
  next
    case (Func F u)
    show ?thesis
    proof (cases t2)
      case (Func G v)
      show ?thesis
      proof (cases "F = G")
        case True
        ― ‹Rule ‹func_sred›: compare the arguments, the recursive call fails.›
        have "sred_fun (((u ≈? v) # xs, ys), nabla, [] ∙ s) = None"
          using H unfolding ‹t1 = Func F u› ‹t2 = Func G v› ‹F = G› by (simp del: sred_fun.simps)
        then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
          using func_sred unfolding ‹t1 = Func F u› ‹t2 = Func G v› ‹F = G› by blast
        then show ?thesis by simp
      next
        case False
        ― ‹Clash: different function symbols.›
        have "fail ((Func F u ≈? Func G v) # xs, ys)"
          using False fail_diff_func by simp
        then show ?thesis unfolding ‹t1 = Func F u› ‹t2 = Func G v›
          by simp
      qed
    next
      case (Susp pi X)
      show ?thesis
      proof (cases "occurs X (Func F u)")
        case True
        ― ‹Occurs check fails.›
        have "fail ((Susp pi X ≈? Func F u) # xs, ys)"
          using True fail_occur_func by (simp split: if_splits)
        then have "fail ((Func F u ≈? Susp pi X) # xs, ys)"
          using fail_sym by simp
        then show ?thesis unfolding ‹t1 = Func F u› ‹t2 = Susp pi X›
          by simp
      next
        case False
        ― ‹Rule ‹var_2_sred›: X is instantiated with the function application.›
        let ?σ = "[(X, swap (rev pi) (Func F u))]"
        have step: "((Func F u ≈? Susp pi X) # xs, ys) ⊢ ?σ ↝ apply_subst ?σ (xs, ys)"
          using False var_2_sred by (simp del: swap.simps)
        have "sred_fun (apply_subst ?σ (xs, ys), nabla, ?σ ∙ s) = None"
          using H False unfolding ‹t1 = Func F u› ‹t2 = Susp pi X› by (simp del: sred_fun.simps)
        then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
          using step unfolding ‹t1 = Func F u› ‹t2 = Susp pi X› by blast
        then show ?thesis by simp
      qed
    next
      case Unit
      ― ‹Clash: Func vs. Unit.›
      have "fail ((Func F u ≈? Unit) # xs, ys)"
        using fail_func_unit by simp
      then show ?thesis unfolding ‹t1 = Func F u› ‹t2 = Unit›
        by simp
    next
      case (Atom b)
      ― ‹Clash: Func vs. Atom.›
      have "fail ((Func F u ≈? Atom b) # xs, ys)"
        using fail_func_atom by simp
      then show ?thesis unfolding ‹t1 = Func F u› ‹t2 = Atom b›
        by simp
    next
      case (Paar v1 v2)
      ― ‹Clash: Func vs. Paar.›
      have "fail ((Func F u ≈? Paar v1 v2) # xs, ys)"
        using fail_func_paar by simp
      then show ?thesis unfolding ‹t1 = Func F u› ‹t2 = Paar v1 v2›
        by simp
    next
      case (Abst b v)
      ― ‹Clash: Func vs. Abst.›
      have "fail ((Func F u ≈? Abst b v) # xs, ys)"
        using fail_func_abst by simp
      then show ?thesis unfolding ‹t1 = Func F u› ‹t2 = Abst b v›
        by simp
    qed
  next
    case (Abst a u)
    show ?thesis
    proof (cases t2)
      case (Abst b v)
      show ?thesis
      proof (cases "a = b")
        case True
        ― ‹Rule ‹abst_aa_sred›: same binder, compare the bodies.›
        have "sred_fun (((u ≈? v) # xs, ys), nabla, [] ∙ s) = None"
          using H unfolding ‹t1 = Abst a u› ‹t2 = Abst b v› ‹a = b› by (simp del: sred_fun.simps)
        then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
          using abst_aa_sred unfolding ‹t1 = Abst a u› ‹t2 = Abst b v› ‹a = b› by blast
        then show ?thesis by simp
      next
        case False
        ― ‹Rule ‹abst_ab_sred›: different binders, swap in the right body and add ‹a # v›.›
        have step: "((Abst a u ≈? Abst b v) # xs, ys) ⊢ [] ↝ ((u ≈? swap [(a, b)] v) # xs, (a ♯? v) # ys)"
          using False abst_ab_sred by simp
        have "sred_fun (((u ≈? swap [(a, b)] v) # xs, (a ♯? v) # ys), nabla, [] ∙ s) = None"
          using H False unfolding ‹t1 = Abst a u› ‹t2 = Abst b v› by (simp del: sred_fun.simps)
        then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
          using step unfolding ‹t1 = Abst a u› ‹t2 = Abst b v› by blast
        then show ?thesis by simp
      qed
    next
      case (Susp pi X)
      show ?thesis
      proof (cases "occurs X (Abst a u)")
        case True
        ― ‹Occurs check fails.›
        have "fail ((Susp pi X ≈? Abst a u) # xs, ys)"
          using True fail_occur_abst by (simp split: if_splits)
        then have "fail ((Abst a u ≈? Susp pi X) # xs, ys)"
          using fail_sym by simp
        then show ?thesis unfolding ‹t1 = Abst a u› ‹t2 = Susp pi X›
          by simp
      next
        case False
        ― ‹Rule ‹var_2_sred›: X is instantiated with the abstraction.›
        let ?σ = "[(X, swap (rev pi) (Abst a u))]"
        have step: "((Abst a u ≈? Susp pi X) # xs, ys) ⊢ ?σ ↝ apply_subst ?σ (xs, ys)"
          using False var_2_sred by (simp del: swap.simps)
        have "sred_fun (apply_subst ?σ (xs, ys), nabla, ?σ ∙ s) = None"
          using H False unfolding ‹t1 = Abst a u› ‹t2 = Susp pi X› by (simp del: sred_fun.simps)
        then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
          using step unfolding ‹t1 = Abst a u› ‹t2 = Susp pi X› by blast
        then show ?thesis by simp
      qed
    next
      case Unit
      ― ‹Clash: Abst vs. Unit.›
      have "fail ((Abst a u ≈? Unit) # xs, ys)"
        using fail_abst_unit by simp
      then show ?thesis unfolding ‹t1 = Abst a u› ‹t2 = Unit›
        by simp
    next
      case (Atom b)
      ― ‹Clash: Abst vs. Atom.›
      have "fail ((Abst a u ≈? Atom b) # xs, ys)"
        using fail_abst_atom by simp
      then show ?thesis unfolding ‹t1 = Abst a u› ‹t2 = Atom b›
        by simp
    next
      case (Paar v1 v2)
      ― ‹Clash: Abst vs. Paar.›
      have "fail ((Abst a u ≈? Paar v1 v2) # xs, ys)"
        using fail_abst_paar by simp
      then show ?thesis unfolding ‹t1 = Abst a u› ‹t2 = Paar v1 v2›
        by simp
    next
      case (Func G v)
      ― ‹Clash: Abst vs. Func.›
      have "fail ((Abst a u ≈? Func G v) # xs, ys)"
        using fail_sym[OF fail_func_abst] by simp
      then show ?thesis unfolding ‹t1 = Abst a u› ‹t2 = Func G v›
        by simp
    qed
  next
    case (Susp pi X)
    ― ‹Left-hand side is a suspension: unless both sides are suspensions of the same
       variable or the occurs check fails, the step is ‹var_1_sred›.›
    have var_1: "¬ occurs X t2 ⟹ sred_fun (apply_subst [(X, swap (rev pi) t2)] (xs, ys), nabla, 
                           [(X, swap (rev pi) t2)] ∙ s) = None ⟹ ?thesis"
    proof -
      assume nocc: "¬ occurs X t2"
        and rec: "sred_fun (apply_subst [(X, swap (rev pi) t2)] (xs, ys), nabla, 
                           [(X, swap (rev pi) t2)] ∙ s) = None"
      have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
        using var_1_sred[OF nocc] rec unfolding ‹t1 = Susp pi X› by blast
      then show ?thesis by simp
    qed
    show ?thesis
    proof (cases t2)
      case (Susp pi2 Y)
      show ?thesis
      proof (cases "X = Y")
        case True
        ― ‹Rule ‹susp_sred›: same variable, freshness constraints for the disagreement set.›
        have "sred_fun ((xs, map (λa. a ♯? Susp [] X) (ds_list pi pi2) @ ys), nabla, [] ∙ s) = None"
          using H unfolding ‹t1 = Susp pi X› ‹t2 = Susp pi2 Y› ‹X = Y›[symmetric] 
          by (simp del: sred_fun.simps)
        then have "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
          using susp_sred unfolding ‹t1 = Susp pi X› ‹t2 = Susp pi2 Y› ‹X = Y›[symmetric] by blast
        then show ?thesis by simp
      next
        case False
        ― ‹Different variables: ‹var_1_sred›, the occurs check holds trivially.›
        have nocc: "¬ occurs X t2"
          using False unfolding ‹t2 = Susp pi2 Y› by simp
        have rec: "sred_fun (apply_subst [(X, swap (rev pi) t2)] (xs, ys), nabla,
                             [(X, swap (rev pi) t2)] ∙ s) = None"
          using H False unfolding ‹t1 = Susp pi X› ‹t2 = Susp pi2 Y›
          by (simp del: sred_fun.simps)
        show ?thesis
          using var_1[OF nocc rec] by simp
      qed
    next
      case Unit
      ― ‹Rule ‹var_1_sred›: X is instantiated with Unit.›
      show ?thesis
        using H by (intro var_1) (simp_all add: ‹t1 = Susp pi X› ‹t2 = Unit› del: sred_fun.simps)
    next
      case (Atom b)
      ― ‹Rule ‹var_1_sred›: X is instantiated with the (permuted) atom.›
      show ?thesis
        using H by (intro var_1) (simp_all add: ‹t1 = Susp pi X› ‹t2 = Atom b› del: sred_fun.simps)
    next
      case (Paar v1 v2)
      show ?thesis
      proof (cases "occurs X (Paar v1 v2)")
        case True
        ― ‹Occurs check fails.›
        have "fail ((Susp pi X ≈? Paar v1 v2) # xs, ys)"
          using True fail_occur_paar by (simp split: if_splits)
        then show ?thesis unfolding ‹t1 = Susp pi X› ‹t2 = Paar v1 v2›
          by simp
      next
        case False
        ― ‹Rule ‹var_1_sred›: X is instantiated with the pair.›
        show ?thesis
          using H False by (intro var_1) (simp_all add: ‹t1 = Susp pi X› ‹t2 = Paar v1 v2› del: sred_fun.simps)
      qed
    next
      case (Func G v)
      show ?thesis
      proof (cases "occurs X (Func G v)")
        case True
        ― ‹Occurs check fails.›
        have "fail ((Susp pi X ≈? Func G v) # xs, ys)"
          using True fail_occur_func by (simp split: if_splits)
        then show ?thesis unfolding ‹t1 = Susp pi X› ‹t2 = Func G v›
          by simp
      next
        case False
        ― ‹Rule ‹var_1_sred›: X is instantiated with the function application.›
        show ?thesis
          using H False by (intro var_1) (simp_all add: ‹t1 = Susp pi X› ‹t2 = Func G v› del: sred_fun.simps)
      qed
    next
      case (Abst b v)
      show ?thesis
      proof (cases "occurs X (Abst b v)")
        case True
        ― ‹Occurs check fails.›
        have "fail ((Susp pi X ≈? Abst b v) # xs, ys)"
          using True fail_occur_abst by (simp split: if_splits)
        then show ?thesis unfolding ‹t1 = Susp pi X› ‹t2 = Abst b v›
          by simp
      next
        case False
        ― ‹Rule ‹var_1_sred›: X is instantiated with the abstraction.›
        show ?thesis
          using H False by (intro var_1) (simp_all add: ‹t1 = Susp pi X› ‹t2 = Abst b v› del: sred_fun.simps)
      qed
    qed
  qed
qed

text‹If ‹sred_fun› fails, the problem has no solution.›

lemma sred_fun_none_empty:
  assumes "sred_fun (P, nabla, s) = None"
  shows "U P = {}"
  using assms
proof(induct P arbitrary: s rule: wf_induct[OF wf_rank_r])
  case (1 P)
  obtain eqs ys where P_def: "P = (eqs, ys)" by (cases P)
  show ?case
  proof(cases eqs)
    case Nil
    then show ?thesis using 1(2) P_def by simp
  next
    case (Cons e xs)
    obtain t1 t2 where e_def: "e = (t1 ≈? t2)" by (cases e)
    have H: "sred_fun (((t1 ≈? t2) # xs, ys), nabla, s) = None"
      using 1(2) unfolding P_def Cons e_def by simp
    have "fail P ∨ (∃σ Q. P ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None)"
      using sred_fun_unfold_none[OF H] unfolding P_def Cons e_def by simp
    then show ?thesis
    proof
      assume "fail P"
      then show ?thesis using fail_then_empty by simp
    next
      assume "∃σ Q. P ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = None"
      then obtain σ Q where step: "P ⊢ σ ↝ Q" and rec: "sred_fun (Q, nabla, σ ∙ s) = None"
        by blast
      have "(Q, P) ∈ rank_r"
        using rank_r_sred[OF step] by simp
      hence "U Q = {}"
        using 1(1) rec by blast
      then show ?thesis 
        using u_empty_sred[OF step] by simp
    qed
  qed
qed

text‹If ‹cred_fun› fails, the (freshness) problem has no solution.›

lemma cred_fun_none_empty:
  assumes "cred_fun ((xs, ys), nabla, s) = None" and "xs = []"
  shows "U ([], ys) = {}"
  using assms
proof(induct "((xs, ys), nabla, s)" arbitrary: xs ys nabla s rule: cred_fun.induct)
  case (1 xs a ys nabla s)
  then show ?case using u_empty_cred[OF unit_cred] by auto
next
  case (2 xs a t1 t2 ys nabla s)
  then show ?case using u_empty_cred[OF paar_cred] by auto
next
  case (3 xs a F t ys nabla s)
  then show ?case using u_empty_cred[OF func_cred] by auto
next
  case (4 xs a b t ys nabla s)
  then show ?case 
    using u_empty_cred[OF abst_aa_cred] u_empty_cred[OF abst_ab_cred]
    by (cases "a = b") auto
next
  case (5 xs a b ys nabla s)
  then show ?case 
    using u_empty_cred[OF atom_cred] fail_then_empty[OF fail_fresh_atom]
    by (cases "a = b") auto
next
  case (6 xs a pi X ys nabla s)
  then show ?case using u_empty_cred[OF susp_cred] by auto
next
  case (7 xs nabla s)
  then show ?case by simp
qed

lemma u_empty_sred_rtc:
  assumes "P1 ⊢ s ↝⇧* P2" and "U P2 = {}"
  shows "U P1 = {}"
  using assms
proof(induct rule: sred_rtc.induct)
  case (sred_refl P1)
  then show ?case by simp
next
  case (sred_rtc_step P1 s1 P2 s2 P3)
  then have "U P2 = {}" by simp
  then show ?case using u_empty_sred[OF sred_rtc_step(1)] by simp
qed

text‹Completeness: whenever the algorithm fails, the problem has no solution.›

theorem nomu_unify_none:
  assumes "nomu_unify P = None"
  shows "U P = {}"
proof(cases "sred_fun (P, {}, [])")
  case None
  then show ?thesis using sred_fun_none_empty by blast
next
  case (Some R)
  then obtain xs ys nabla0 s0 where S: "sred_fun (P, {}, []) = Some ((xs, ys), nabla0, s0)"
    by (cases R) auto
  have "xs = []"
    using sred_fun_some_fst_empty[OF S] by simp
  obtain s1 where rtc: "P ⊢ s1 ↝⇧* ([], ys)"
    using sred_fun_sred_rtc[OF S] ‹xs = []› by auto
  show ?thesis
  proof(cases "cred_fun (([], ys), nabla0, s0)")
    case None
    then have "U ([], ys) = {}" 
      using cred_fun_none_empty by blast
    then show ?thesis 
      using u_empty_sred_rtc[OF rtc] by simp
  next
    case (Some C)
    then obtain P1 nabla1 s1' where C: "cred_fun (([], ys), nabla0, s0) = Some (P1, nabla1, s1')"
      by (cases C) auto
    have "P1 = ([],[])"
      using cred_fun_some_fst[OF C] cred_fun_some_snd_empty[OF C] by (cases P1) auto
    hence "nomu_unify P = Some (nabla1, s1')"
      using S C ‹xs = []› by simp
    then show ?thesis using assms by simp
  qed
qed

text‹Together with soundness: the algorithm fails exactly on the problems without solutions.›

corollary nomu_unify_none_iff:
  shows "nomu_unify P = None ⟷ U P = {}"
proof
  assume "nomu_unify P = None"
  then show "U P = {}" using nomu_unify_none by simp
next
  assume "U P = {}"
  show "nomu_unify P = None"
  proof(rule ccontr)
    assume "nomu_unify P ≠ None"
    then obtain nabla s where "nomu_unify P = Some (nabla, s)" by auto
    then have "(nabla, s) ∈ U P" using nomu_unify_sound by simp
    then show False using ‹U P = {}› by simp
  qed
qed

text‹Completeness in the style of @{thm [source] completeness}: whenever a problem has a
solution, the algorithm returns a result that is an idempotent most general unifier.›

theorem nomu_unify_complete:
  assumes "U P ≠ {}"
  shows "∃nabla s. nomu_unify P = Some (nabla, s) ∧ mgu P (nabla, s) ∧ idem (nabla, s)"
proof-
  obtain nabla s where res: "nomu_unify P = Some (nabla, s)"
    using assms nomu_unify_none_iff by (cases "nomu_unify P") auto
  moreover have "mgu P (nabla, s)" "idem (nabla, s)"
    using nomu_unify_sound[OF res] by simp+
  ultimately show ?thesis using res by blast
qed


(*<*)
end
(*>*)