Theory NU_Computable_Soundness

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

section ‹Soundness of the computable algorithm›

text‹‹sred_fun› is simulated by the reflexive-transitive closure of the equational reductions.›

text‹One unfolding of ‹sred_fun› on a non-empty equation list corresponds to one ‹s_red› step.›

lemma sred_fun_unfold_step:
  assumes "sred_fun (((t1 ≈? t2) # xs, ys), nabla, s) = Some r"
  shows "∃σ Q. ((t1 ≈? t2) # xs, ys) ⊢ σ ↝ Q ∧ sred_fun (Q, nabla, σ ∙ s) = Some r"
proof -
  ― ‹Unfold ‹sred_fun› exactly once: H is the case distinction of the definition, whose 
     value is Some r. From now on ‹sred_fun› is never unfolded again.›
  note H = trans[OF sred_fun.simps(2)[symmetric] assms]
  show ?thesis
  proof (cases t1)
    case Unit
    show ?thesis
    proof (cases t2)
      case Unit
      ― ‹Rule ‹unit_sred›: the equation is simply removed.›
      have step: "((Unit ≈? Unit) # xs, ys) ⊢ [] ↝ (xs, ys)"
        using unit_sred by simp
      have "sred_fun ((xs, ys), nabla, [] ∙ s) = Some r"
        using H unfolding ‹t1 = Unit› ‹t2 = Unit› by (simp del: sred_fun.simps)
      then show ?thesis unfolding ‹t1 = Unit› ‹t2 = Unit› using step by blast
    next
      case (Susp pi X)
      ― ‹Rule ‹var_2_sred›: X is instantiated with Unit.›
      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) = Some r"
        using H unfolding ‹t1 = Unit› ‹t2 = Susp pi X› by (simp del: sred_fun.simps)
      then show ?thesis unfolding ‹t1 = Unit› ‹t2 = Susp pi X› using step by blast
    qed (use H Unit in ‹simp_all del: sred_fun.simps›) ― ‹clashes: ‹sred_fun› returns None›
  next
    case (Atom a)
    show ?thesis
    proof (cases t2)
      case (Atom b)
      ― ‹Rule ‹atom_sred›: only applicable (and only Some) when a = b.›
      have "a = b"
        using H ‹t1 = Atom a› ‹t2 = Atom b› by (simp del: sred_fun.simps split: if_splits)
      have step: "((Atom a ≈? Atom a) # xs, ys) ⊢ [] ↝ (xs, ys)"
        using atom_sred by simp
      have "sred_fun ((xs, ys), nabla, [] ∙ s) = Some r"
        using H unfolding ‹t1 = Atom a› ‹t2 = Atom b› ‹a = b› by (simp del: sred_fun.simps)
      then show ?thesis unfolding ‹t1 = Atom a› ‹t2 = Atom b› ‹a = b› using step by blast
    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) = Some r"
        using H unfolding ‹t1 = Atom a› ‹t2 = Susp pi X› by (simp del: sred_fun.simps)
      then show ?thesis unfolding ‹t1 = Atom a› ‹t2 = Susp pi X› using step by blast
    qed (use H Atom in ‹simp_all del: sred_fun.simps›)
  next
    case (Paar u1 u2)
    show ?thesis
    proof (cases t2)
      case (Paar v1 v2)
      ― ‹Rule ‹paar_sred›: the pair equation is split into two equations.›
      have step: "((Paar u1 u2 ≈? Paar v1 v2) # xs, ys) ⊢ [] ↝ ((u1 ≈? v1) # (u2 ≈? v2) # xs, ys)"
        using paar_sred by simp
      have "sred_fun (((u1 ≈? v1) # (u2 ≈? v2) # xs, ys), nabla, [] ∙ s) = Some r"
        using H unfolding ‹t1 = Paar u1 u2› ‹t2 = Paar v1 v2› by (simp del: sred_fun.simps)
      then show ?thesis unfolding ‹t1 = Paar u1 u2› ‹t2 = Paar v1 v2› using step by blast
    next
      case (Susp pi X)
      ― ‹Rule ‹var_2_sred›: Some is only returned when the occurs check succeeds.›
      have nocc: "¬ occurs X (Paar u1 u2)"
        using H ‹t1 = Paar u1 u2› ‹t2 = Susp pi X› by (auto simp del: sred_fun.simps split: if_splits)
      let ?σ = "[(X, swap (rev pi) (Paar u1 u2))]"
      have step: "((Paar u1 u2 ≈? Susp pi X) # xs, ys) ⊢ ?σ ↝ apply_subst ?σ (xs, ys)"
        using nocc var_2_sred by (simp del: swap.simps)
      have "sred_fun (apply_subst ?σ (xs, ys), nabla, ?σ ∙ s) = Some r"
        using H nocc unfolding ‹t1 = Paar u1 u2› ‹t2 = Susp pi X› by (simp del: sred_fun.simps)
      then show ?thesis unfolding ‹t1 = Paar u1 u2› ‹t2 = Susp pi X› using step by blast
    qed (use H Paar in ‹simp_all del: sred_fun.simps›)
  next
    case (Func F u)
    show ?thesis
    proof (cases t2)
      case (Func G v)
      ― ‹Rule ‹func_sred›: only applicable (and only Some) when F = G.›
      have "F = G"
        using H ‹t1 = Func F u› ‹t2 = Func G v› by (simp del: sred_fun.simps split: if_splits)
      have step: "((Func F u ≈? Func F v) # xs, ys) ⊢ [] ↝ ((u ≈? v) # xs, ys)"
        using func_sred by simp
      have "sred_fun (((u ≈? v) # xs, ys), nabla, [] ∙ s) = Some r"
        using H unfolding ‹t1 = Func F u› ‹t2 = Func G v› ‹F = G› by (simp del: sred_fun.simps)
      then show ?thesis unfolding ‹t1 = Func F u› ‹t2 = Func G v› ‹F = G› using step by blast
    next
      case (Susp pi X)
      ― ‹Rule ‹var_2_sred›: Some is only returned when the occurs check succeeds.›
      have nocc: "¬ occurs X (Func F u)"
        using H ‹t1 = Func F u› ‹t2 = Susp pi X› by (auto simp del: sred_fun.simps split: if_splits)
      let ?σ = "[(X, swap (rev pi) (Func F u))]"
      have step: "((Func F u ≈? Susp pi X) # xs, ys) ⊢ ?σ ↝ apply_subst ?σ (xs, ys)"
        using nocc var_2_sred by (simp del: swap.simps)
      have "sred_fun (apply_subst ?σ (xs, ys), nabla, ?σ ∙ s) = Some r"
        using H nocc unfolding ‹t1 = Func F u› ‹t2 = Susp pi X› by (simp del: sred_fun.simps)
      then show ?thesis unfolding ‹t1 = Func F u› ‹t2 = Susp pi X› using step by blast
    qed (use H Func in ‹simp_all del: sred_fun.simps›)
  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 step: "((Abst a u ≈? Abst a v) # xs, ys) ⊢ [] ↝ ((u ≈? v) # xs, ys)"
          using abst_aa_sred by simp
        have "sred_fun (((u ≈? v) # xs, ys), nabla, [] ∙ s) = Some r"
          using H unfolding ‹t1 = Abst a u› ‹t2 = Abst b v› ‹a = b› by (simp del: sred_fun.simps)
        then show ?thesis unfolding ‹t1 = Abst a u› ‹t2 = Abst b v› ‹a = b› using step by blast
      next
        case False
        ― ‹Rule ‹abst_ab_sred›: different binders, swap a and b in the right body
           and add the freshness constraint ‹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) = Some r"
          using H False unfolding ‹t1 = Abst a u› ‹t2 = Abst b v› by (simp del: sred_fun.simps)
        then show ?thesis unfolding ‹t1 = Abst a u› ‹t2 = Abst b v› using step by blast
      qed
    next
      case (Susp pi X)
      ― ‹Rule ‹var_2_sred›: Some is only returned when the occurs check succeeds.›
      have nocc: "¬ occurs X (Abst a u)"
        using H ‹t1 = Abst a u› ‹t2 = Susp pi X› by (auto simp del: sred_fun.simps split: if_splits)
      let ?σ = "[(X, swap (rev pi) (Abst a u))]"
      have step: "((Abst a u ≈? Susp pi X) # xs, ys) ⊢ ?σ ↝ apply_subst ?σ (xs, ys)"
        using nocc var_2_sred by (simp del: swap.simps)
      have "sred_fun (apply_subst ?σ (xs, ys), nabla, ?σ ∙ s) = Some r"
        using H nocc unfolding ‹t1 = Abst a u› ‹t2 = Susp pi X› by (simp del: sred_fun.simps)
      then show ?thesis unfolding ‹t1 = Abst a u› ‹t2 = Susp pi X› using step by blast
    qed (use H Abst in ‹simp_all del: sred_fun.simps›)
  next
    case (Susp pi X)
    ― ‹Left-hand side is a suspension: unless both sides are suspensions of the same
       variable, the step is always ‹var_1_sred› (X is instantiated with the right side).›
    have var_1: "sred_fun (apply_subst [(X, swap (rev pi) t2)] (xs, ys), nabla, 
                           [(X, swap (rev pi) t2)] ∙ s) = Some r ⟹ ¬ occurs X t2 ⟹ ?thesis"
    proof -
      assume rec: "sred_fun (apply_subst [(X, swap (rev pi) t2)] (xs, ys), nabla, 
                             [(X, swap (rev pi) t2)] ∙ s) = Some r"
        and nocc: "¬ occurs X t2"
      have "((Susp pi X ≈? t2) # xs, ys) ⊢ [(X, swap (rev pi) t2)] ↝ apply_subst [(X, swap (rev pi) t2)] (xs, ys)"
        using nocc var_1_sred by simp
      then show ?thesis unfolding ‹t1 = Susp pi X› using rec by blast
    qed
    show ?thesis
    proof (cases t2)
      case (Susp pi2 Y)
      show ?thesis
      proof (cases "X = Y")
        case True
        ― ‹Rule ‹susp_sred›: same variable, generate freshness constraints for the 
           disagreement set of the two permutations.›
        have step: "((Susp pi X ≈? Susp pi2 X) # xs, ys) ⊢ [] ↝ 
                      (xs, map (λa. a ♯? Susp [] X) (ds_list pi pi2) @ ys)"
          using susp_sred by simp
        have "sred_fun ((xs, map (λa. a ♯? Susp [] X) (ds_list pi pi2) @ ys), nabla, [] ∙ s) = Some r"
          using H unfolding ‹t1 = Susp pi X› ‹t2 = Susp pi2 Y› ‹X = Y›[symmetric] 
          by (simp del: sred_fun.simps)
        then show ?thesis unfolding ‹t1 = Susp pi X› ‹t2 = Susp pi2 Y› ‹X = Y›[symmetric] 
          using step by blast
      next
        case False
        ― ‹Different variables: ‹var_1_sred›, the occurs check holds trivially.›
        have rec: "sred_fun (apply_subst [(X, swap (rev pi) t2)] (xs, ys), nabla,
                             [(X, swap (rev pi) t2)] ∙ s) = Some r"
          using H False unfolding ‹t1 = Susp pi X› ‹t2 = Susp pi2 Y›
          by (simp del: sred_fun.simps)
        have nocc: "¬ occurs X t2"
          using False unfolding ‹t2 = Susp pi2 Y› by simp
        show ?thesis
          using var_1[OF rec nocc] by simp
      qed
    qed (use H Susp in ‹(intro var_1; simp del: sred_fun.simps split: if_splits)›)+
  qed
qed

text‹Whenever ‹sred_fun› succeeds, the first (equation) list of the resulting problem is empty:
all equations have been solved, only freshness constraints remain.›

lemma sred_fun_some_fst_empty:
  assumes "sred_fun (P, nabla, s) = Some (P', nabla', s')"
  shows "fst 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
    ― ‹No equations left: ‹sred_fun› returns the problem unchanged.›
    then show ?thesis using 1(2) P_def by auto
  next
    case (Cons e xs)
    ― ‹One equation is processed by an ‹s_red› step, after which ‹sred_fun› still succeeds
       on a problem of smaller rank: apply the induction hypothesis.›
    obtain t1 t2 where e_def: "e = (t1 ≈? t2)" by (cases e)
    obtain σ Q where step: "P ⊢ σ ↝ Q" and rec: "sred_fun (Q, nabla, σ ∙ s) = Some (P', nabla', s')"
      using sred_fun_unfold_step 1(2) unfolding P_def Cons e_def by blast
    have "(Q, P) ∈ rank_r"
      using rank_r_sred[OF step] by simp
    then show ?thesis 
      using 1(1) rec by blast
  qed
qed

lemma sred_fun_sred_rtc:
  assumes "sred_fun (P, nabla, s) = Some (P', nabla', s')"
  shows "nabla' = nabla ∧ (∃s1. P ⊢ s1 ↝⇧* P' ∧ s' = s1 ∙ s)"
  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 force
  next
    case (Cons e xs)
    obtain t1 t2 where e_def: "e = (t1 ≈? t2)" by (cases e)
    obtain σ Q where step: "P ⊢ σ ↝ Q" and rec: "sred_fun (Q, nabla, σ ∙ s) = Some (P', nabla', s')"
      using sred_fun_unfold_step 1(2) unfolding P_def Cons e_def by blast
    have "(Q, P) ∈ rank_r"
      using rank_r_sred[OF step] by simp
    hence "nabla' = nabla ∧ (∃s1. Q ⊢ s1 ↝⇧* P' ∧ s' = s1 ∙ (σ ∙ s))"
      using 1(1) rec by blast
    then show ?thesis
      using sred_rtc_step[OF step] comp_assoc by metis
  qed
qed

text‹‹cred_fun› is simulated by the reflexive-transitive closure of the freshness reductions.›

lemma cred_fun_cred_rtc:
  assumes "cred_fun ((xs, ys), nabla, s) = Some (P', nabla', s')" and "xs = []"
  shows "s' = s ∧ (∃n1. ([], ys) ⊢ n1 →⇧* P' ∧ nabla' = n1 ∪ nabla)"
  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 cred_rtc_step[OF unit_cred] by (auto simp: Un_assoc)
next
  case (2 xs a t1 t2 ys nabla s)
  then show ?case using cred_rtc_step[OF paar_cred] by (auto simp: Un_assoc)
next
  case (3 xs a F t ys nabla s)
  then show ?case using cred_rtc_step[OF func_cred] by (auto simp: Un_assoc)
next
  case (4 xs a b t ys nabla s)
  then show ?case 
    using cred_rtc_step[OF abst_aa_cred] cred_rtc_step[OF abst_ab_cred]
    by (cases "a = b") (auto simp: Un_assoc)
next
  case (5 xs a b ys nabla s)
  then show ?case using cred_rtc_step[OF atom_cred] by (auto simp: Un_assoc split: if_splits)
next
  case (6 xs a pi X ys nabla s)
  then show ?case using cred_rtc_step[OF susp_cred] by (auto simp: Un_assoc)
next
  case (7 xs nabla s)
  then show ?case by force
qed

lemma cred_fun_some_fst:
  assumes "cred_fun ((xs, ys), nabla, s) = Some (P', nabla', s')"
  shows "fst P' = xs"
  using assms 
  by (induct "((xs, ys), nabla, s)" arbitrary: xs ys nabla s rule: cred_fun.induct, auto split: if_splits)

text‹Gluing the closures of the equational and freshness reductions into ‹red_plus›.›

lemma sred_rtc_red_plus_append:
  assumes "P1 ⊢ s ↝⇧* P2" and "P2 ⊨ (nabla, []) ⇒ P3"
  shows "P1 ⊨ (nabla, s) ⇒ P3"
  using assms by (induct rule: sred_rtc.induct) auto

lemma cred_rtc_red_plus:
  assumes "P1 ⊢ nabla →⇧* P2"
  shows "(P1 = P2 ∧ nabla = {}) ∨ P1 ⊨ (nabla, []) ⇒ P2"
  using assms
proof(induct rule: cred_rtc.induct)
  case (cred_refl P1)
  then show ?case by simp
next
  case (cred_rtc_step P1 nabla1 P2 nabla2 P3)
  show ?case
  proof(cases "P2 = P3 ∧ nabla2 = {}")
    case True
    then show ?thesis using cred_single[OF cred_rtc_step(1)] by simp
  next
    case False
    hence "P2 ⊨ (nabla2, []) ⇒ P3" 
      using cred_rtc_step(3) False by auto
    then show ?thesis using cred_step[OF cred_rtc_step(1)] by simp
  qed
qed

text‹A successful run of the algorithm corresponds to a sequence of equational reductions 
followed by a sequence of freshness reductions ending in the empty problem.›

lemma nomu_unify_some_rtc:
  assumes "nomu_unify P = Some (nabla, s)"
  shows "∃P3. P ⊢ s ↝⇧* P3 ∧ P3 ⊢ nabla →⇧* ([],[])"
proof-
  obtain R where R: "red_plus_fun (P, {}, []) = Some R"
    using assms by (cases "red_plus_fun (P, {}, [])") auto
  obtain xs ys nabla0 s0 where S: "sred_fun (P, {}, []) = Some ((xs, ys), nabla0, s0)"
    using R by (cases "sred_fun (P, {}, [])") auto
  have "xs = []"
    using sred_fun_some_fst_empty[OF S] by simp
  obtain P1 nabla1 s1 where C: "cred_fun (([], ys), nabla0, s0) = Some (P1, nabla1, s1)"
    using R S ‹xs = []› by (cases R) auto
  have "P1 = ([],[])"
    using cred_fun_some_fst[OF C] cred_fun_some_snd_empty[OF C] by (cases P1) auto
  hence "nabla1 = nabla" "s1 = s"
    using assms R S C ‹xs = []› by auto
  obtain s2 where "nabla0 = {}" "P ⊢ s2 ↝⇧* ([], ys)" "s0 = s2"
    using sred_fun_sred_rtc[OF S] ‹xs = []› by auto
  moreover obtain n where "s1 = s0" "([], ys) ⊢ n →⇧* P1" "nabla1 = n ∪ nabla0"
    using cred_fun_cred_rtc[OF C] by auto
  ultimately show ?thesis
    using ‹P1 = ([],[])› ‹nabla1 = nabla› ‹s1 = s› by auto
qed

text‹For a non-trivial problem, a successful run of the algorithm corresponds to a ‹red_plus› 
derivation to the empty problem.›

lemma nomu_unify_some_red_plus:
  assumes "nomu_unify P = Some (nabla, s)" and "P ≠ ([],[])"
  shows "P ⊨ (nabla, s) ⇒ ([],[])"
proof-
  obtain P3 where sred: "P ⊢ s ↝⇧* P3" and cred: "P3 ⊢ nabla →⇧* ([],[])"
    using nomu_unify_some_rtc[OF assms(1)] by blast
  show ?thesis
  proof(cases "P3 = ([],[]) ∧ nabla = {}")
    case True
    then show ?thesis 
      using sred_rtc_to_redplus[of P "([],[])" s] sred assms(2) by simp
  next
    case False
    then have "P3 ⊨ (nabla, []) ⇒ ([],[])" 
      using cred_rtc_red_plus[OF cred] by metis
    then show ?thesis 
      using sred_rtc_red_plus_append[OF sred] by simp
  qed
qed

text‹Soundness: whenever the algorithm returns a result, it is an idempotent most general 
unifier of the input problem.›

theorem nomu_unify_sound:
  assumes "nomu_unify P = Some (nabla, s)"
  shows "(nabla, s) ∈ U P ∧ mgu P (nabla, s) ∧ idem (nabla, s)"
proof(cases "P = ([],[])")
  case True
  have "nabla = {}" and "s = []"
    using assms True by simp_all
  then show ?thesis
    using True subst_equ_refl
    unfolding all_solutions_def mgu_def idem_def ext_subst_def by auto
next
  case False
  have red: "P ⊨ (nabla, s) ⇒ ([],[])"
    using nomu_unify_some_red_plus[OF assms False] by simp
  have "(nabla, s) ∈ U P"
    using P1_from_P2_red_plus[OF red _ ext_subst_id, of "{}"]
    by (simp add: all_solutions_def[of "([],[])"])
  moreover have "mgu P (nabla, s) ∧ idem (nabla, s)"
    using mgu[OF red] by simp
  ultimately show ?thesis by simp
qed

(*<*)
end
(*>*)