Theory NU_Completeness

(*<*)
theory NU_Completeness
imports NU_Soundness
begin
(*>*)

section‹Completeness›

text‹Defines a reflexive-transitive relation from Freshness and Nominal Equational decomposition
and an inductive schema for proving completeness.›

text‹The reflexive-transitive closures of sred and cred.›

inductive sred_rtc :: "problem_type ⇒ substs ⇒ problem_type ⇒ bool" ("_ ⊢ _ ↝⇧* _" [80,80,80] 80)
  where
sred_refl[intro!]: "P1 ⊢ [] ↝⇧* P1" |
sred_rtc_step[intro!]: "⟦P1 ⊢ s1 ↝ P2; P2 ⊢ s2 ↝⇧* P3⟧ ⟹ P1 ⊢ (s2 ∙ s1) ↝⇧* P3"


inductive cred_rtc :: "problem_type ⇒ fresh_envs ⇒ problem_type ⇒ bool" ("_ ⊢ _ →⇧* _ " [80,80,80] 80)
  where
cred_refl[intro!] : "P1 ⊢ {} →⇧* P1" |
cred_rtc_step[intro!] : "⟦P1 ⊢ nabla1 → P2; P2 ⊢ nabla2 →⇧* P3⟧ ⟹ P1 ⊢ (nabla2 ∪ nabla1) →⇧* P3"

text‹Either the measure reduces or the problem stays the same under equation reductions.›

lemma rank_r_sred_rtc:
  assumes "P1 ⊢ s ↝⇧* P2"
  shows "(P2, P1) ∈ rank_r ∨ P1 = P2"
using assms
proof (induct rule: sred_rtc.induct)
  case (sred_refl P1)
  then show "(P1, P1) ∈ rank_r ∨ P1 = P1" by simp
next
  case (sred_rtc_step P1 s1 P' s2 P2)
  then have "(P', P1) ∈ rank_r"
    using rank_r_sred by blast
  moreover have "(P2, P') ∈ rank_r ∨ P' = P2"
    using sred_rtc_step by simp
  ultimately show "(P2, P1) ∈ rank_r ∨ P1 = P2"
    using sred_rtc_step rank_r_trans by blast
qed

text‹If the problem does not change under the reflexive-transitive closure of sred,
the substitution must be empty.›

lemma sred_rtc_no_cycle:
  assumes "P ⊢ s ↝⇧* P"
  shows "s = []"
proof(rule ccontr)
  assume "s ≠ []"
  hence "(P,P) ∈ rank_r"
  proof(cases rule: sred_rtc.cases[OF assms])
    case (1 P1)
    then show ?thesis
      using ‹s ≠ []› by auto
  next
    case (2 P1 s1 P2 s2 P3)
    hence "(P2,P1) ∈ rank_r" 
      using rank_r_sred by simp
    moreover have "P1 = P3" 
      using 2(1,3) by simp
    moreover have "(P3, P2) ∈ rank_r ∨ P2=P3"
      using 2(5) rank_r_sred_rtc by simp
    ultimately have "(P3,P3) ∈ rank_r" 
      using rank_r_trans by blast
    then show "(P, P) ∈ rank_r" 
      using 2(3) by simp
  qed
  thus "False" using wf_rank_r by simp
qed

text‹If P1 reduces to a diferent P2 under steps of sred, then it reduces via ‹red_plus›.›

lemma sred_rtc_to_redplus:
  assumes "P1 ≠ P2"  "P1 ⊢ s ↝⇧* P2"
  shows "P1 ⊨ ({}, s) ⇒ P2"
  using assms
proof(induct rule: sred_rtc.induct[OF assms(2)])
  case (1 P1)
  then show ?case by simp
next
  case (2 P1 s1 P' s2 P2)
  then show "P1 ⊨ ({}, s2 ∙ s1) ⇒ P2"
    proof(cases "P' = P2")
      case True
      with 2(1,2) have 
        i: "P1 ⊢ s1 ↝ P2" "P2 ⊢ s2 ↝⇧* P2" by simp+
      hence "s2 = []" 
        using sred_rtc_no_cycle by simp
      with i have "P1 ⊢ (s2∙s1) ↝ P2" by simp
      then show "P1 ⊨ ({}, s2 ∙ s1) ⇒ P2 " 
        using sred_single by simp
    next
      case False
      with 2(2,3) have "P' ⊨ ({}, s2) ⇒ P2" 
        by simp
      with 2(1) show "P1 ⊨ ({}, s2 ∙ s1) ⇒ P2" 
        using sred_step by simp
    qed
qed

text‹The following two lemmas guarantee that we don't apply any non-trivial step of equational
reductions after applying a freshness reduction.›

lemma no_nontrivial_sred_after_cred_aux:
  assumes "P1 ⊢ nabla → P2" and "P2 ⊢ s ↝⇧* P3"
  shows "P2 = P3"
  using assms
proof(induct rule: sred_rtc.induct[OF assms(2)])
  case (1 P2)
  then show ?case by simp
next
  case (2 P2 s' P' s2 P3)
  hence "fst P2 = []"
    using c_red_eqs_empty by auto
  moreover have "fst P2 ≠ []" 
    using 2(1) sred_eqs_not_empty by simp
  ultimately have False by auto
  then show ?case by simp
qed

lemma no_nontrivial_sred_after_cred:
  assumes "P1 ⊢ nabla1 → P2"
    and "P2 ⊢ s ↝⇧* P'" and "P' ⊢ nabla2 →⇧* P3"
  shows "P1 ⊢ (nabla2 ∪ nabla1) →⇧* P3"
  using assms
proof-
  from assms(1,2) have "P2 = P'" 
    using no_nontrivial_sred_after_cred_aux by simp
  hence "P2 ⊢ nabla2 →⇧* P3" 
    using assms(3) by simp
  with assms(1) show "P1 ⊢ (nabla2 ∪ nabla1) →⇧* P3"
    using cred_rtc_step by simp
qed

text‹If there is a reduction from P1 to P2 via ‹red_plus›, we can split into equational reductions
first and freshness reductions after.›

lemma red_plus_decompose:
  assumes "P1 ⊨ (nabla, s) ⇒ P2"
  shows "∃ P3. P1 ⊢ s ↝⇧* P3 ∧ P3 ⊢ nabla →⇧* P2"
  using assms
proof (induction P1≡"P1" nablas≡"(nabla, s)" P2≡"P2" arbitrary: nabla s P1 P2 rule: red_plus.induct)
  case (sred_single P1 s1 P2)
  hence "P1 ⊢ s1 ↝⇧* P2"
    using sred_rtc_step[OF sred_single sred_refl] by simp
  moreover have "P2 ⊢ {} →⇧* P2"
   using cred_refl by simp
  ultimately show "∃P3. P1 ⊢ s1 ↝⇧* P3 ∧ P3 ⊢ {} →⇧* P2" by blast
next
  case (cred_single P1 nabla1 P2)
  hence "P1 ⊢ nabla1 →⇧* P2"
    using cred_rtc_step[OF cred_single cred_refl] by simp
  moreover have "P1 ⊢ [] ↝⇧* P1"
    using sred_refl by simp
  ultimately show "∃P3. P1 ⊢ [] ↝⇧* P3 ∧ P3 ⊢ nabla1 →⇧* P2" by blast
next
  case (sred_step P1 s1 P' nabla2 s2 P2)
  have "P1 ⊢ s1 ↝ P'" by fact
  moreover obtain P3 where
    IH: "P' ⊢ s2 ↝⇧* P3" "P3 ⊢ nabla2 →⇧* P2"
    using sred_step(3) by auto
  ultimately have "P1 ⊢ s2 ∙ s1 ↝⇧* P3" 
    using sred_rtc_step by simp
  with IH(2) show "∃P3. P1 ⊢ s2 ∙ s1 ↝⇧* P3 ∧ P3 ⊢ nabla2 →⇧* P2"
    by blast
next
  case (cred_step P1 nabla1 P' nabla2 P2)
  have i: "P1 ⊢ nabla1 → P'" by fact
  moreover obtain P3 where
    IH: "P' ⊢ [] ↝⇧* P3" "P3 ⊢ nabla2 →⇧* P2"
    using cred_step(3) by auto
  ultimately have "P1 ⊢ (nabla2 ∪ nabla1) →⇧* P2"
    using no_nontrivial_sred_after_cred by simp
  moreover have "P1 ⊢ [] ↝⇧* P1"
    using sred_refl by simp
  ultimately show "∃P3. P1 ⊢ [] ↝⇧* P3 ∧ P3 ⊢ (nabla2 ∪ nabla1) →⇧* P2"
    by blast
qed

text‹A form of transitivity of ‹red_plus›.›

lemma red_plus_transitivity:
  assumes "P1 ⊨ (nabla1, s1) ⇒ P2"
      and "P2 ⊨ (nabla2, s2) ⇒ P3"
    shows "∃ nabla3 s3. P1 ⊨ (nabla3, s3) ⇒ P3"
  using assms
proof (induction rule: red_plus.induct[OF assms(1)])
  case (2 P1 nabla1 P2)
  then obtain P' where
  i: "P2 ⊢ s2 ↝⇧* P'"
    using red_plus_decompose by blast
  with 2(1) have "P2 = P'" 
   using no_nontrivial_sred_after_cred_aux by simp
  hence "s2 = []" 
    using i(1) sred_rtc_no_cycle by simp
  hence "P2 ⊨ (nabla2, []) ⇒ P3" 
    using 2(3) by simp
  with 2(1) show "∃nabla3 s3. P1 ⊨ (nabla3, s3) ⇒ P3"
    using cred_step by auto
next
  case (4 P1 nabla P' nabla' P2)
  then obtain nabla3 s3 where
    P_prime_to_P3: "P' ⊨ (nabla3, s3) ⇒ P3" by auto
  then obtain P'' where "P' ⊢ s3 ↝⇧* P''" "P'' ⊢ nabla3 →⇧* P3"
    using red_plus_decompose by blast
  with 4(1) have "P' = P''" 
    using  no_nontrivial_sred_after_cred_aux by simp
  moreover have "s3 =[]"
    using ‹P' ⊢ s3 ↝⇧* P''› sred_rtc_no_cycle calculation by simp
  hence "P' ⊨ (nabla3, []) ⇒ P3" 
    using P_prime_to_P3 by simp
  with 4(1) show "∃nabla3 s3. P1 ⊨ (nabla3, s3) ⇒ P3"
    using cred_step by auto
qed (auto)



text‹Every problem has a normal form.›

lemma normal_form_exists:
  shows "P ∈ stuck ∨ (∃ P2 nabla s. P ⊨(nabla,s)⇒P2 ∧ P2∈stuck )"
proof(induction P rule: wf_induct_rule[OF wf_rank_r])
  case (1 P)
  then show "P ∈ stuck ∨ (∃P2 nabla s. P ⊨ (nabla, s) ⇒ P2  ∧ P2 ∈ stuck)"
  proof (cases "P ∈ stuck")
    case True
    then show "P ∈ stuck ∨ (∃P2 nabla s. P ⊨ (nabla, s) ⇒ P2  ∧ P2 ∈ stuck)" by simp
  next
    case False
    then obtain P' nabla s where P_to_P_prime:
      "P ⊨(nabla,s)⇒P'"
      unfolding stuck_def by auto
    hence "(P', P) ∈ rank_r"
      using rank_r_red_plus by simp
    hence aux: "P' ∈ stuck ∨ (∃P2 nabla s. P' ⊨ (nabla, s) ⇒ P2 ∧ P2 ∈ stuck)"
      using 1 by simp
    then show "P ∈ stuck ∨ (∃P2 nabla s. P ⊨ (nabla, s) ⇒ P2  ∧ P2 ∈ stuck)"
    proof(cases "P' ∈ stuck")
      case True
      then show ?thesis 
        using P_to_P_prime by blast
    next
      case False
      then obtain P2 nabla' s' where
      P_prime_to_P2: "P' ⊨ (nabla', s') ⇒ P2" "P2 ∈ stuck"
        using aux by auto
      then obtain nabla1 s1 where "P ⊨ (nabla1, s1) ⇒ P2" "P2∈ stuck"
        using P_to_P_prime red_plus_transitivity by blast
      then show ?thesis by blast
    qed
  qed
qed


text‹The procedure is complete, i.e., if a non-empty problem has a solution, then ‹red_plus› finds
the most general solution.›

theorem completeness:
  assumes "P1 ≠ ([],[])" "U P1 ≠ {}"
  shows "∃ nabla' s'. P1 ⊨ (nabla', s') ⇒ ([],[]) ∧ mgu P1 (nabla', s')"
proof-
  have P1_not_stuck: "P1 ∉ stuck" 
  proof
    assume "P1∈ stuck"
    hence "P1 = ([],[])∨ fail P1" 
      unfolding stuck_equiv by simp
    hence "P1 =([],[])"
      using assms(2) fail_then_empty by blast
    thus False using assms(1) by simp
  qed
  then obtain P2 nabla' s' where 
    normal_form: "P1 ⊨ (nabla', s') ⇒ P2" "P2 ∈ stuck"
    using normal_form_exists by blast
  hence "P2 ∈ normal_form P1" 
    using P1_not_stuck unfolding normal_form_def by auto
  hence "P2=([],[])"
    using not_empty_then_not_fail[OF assms(2)] normal_form(2) stuck_equiv by auto
  with normal_form(1) have "P1 ⊨ (nabla', s') ⇒ ([],[])" by simp
  moreover have "mgu P1 (nabla',s')" 
    using mgu calculation by simp
  ultimately show "∃nabla' s'. P1 ⊨ (nabla', s') ⇒ ([], [])  ∧ mgu P1 (nabla', s')"
    by auto
qed
  

(*<*)
end
(*>*)