Theory SIMP_plus

(*
Created by Yongwang Zhao (zhaoyw@buaa.edu.cn)
School of Computer Science & Engineering, Beihang University, China
*)

section ‹Extending SIMP language with new proof rules ›

theory SIMP_plus
imports "HOL-Hoare_Parallel.RG_Hoare"
begin

subsection ‹ new proof rules ›

inductive rghoare_p :: "['a com option, 'a set, ('a × 'a) set, ('a × 'a) set, 'a set] ⇒ bool"
    ("⊢⇩I _ sat⇩p [_, _, _, _]" [60,0,0,0,0] 45)
where
(*  Some_hoare: "⟦ ⊢ Q sat [pre, rely, guar, post] ⟧ ⟹ ⊢⇩I (Some Q) sat⇩p [pre, rely, guar, post]"*)
  Basic: "⟦ pre ⊆ {s. f s ∈ post}; {(s,t). s ∈ pre ∧ (t=f s)} ⊆ guar;
            stable pre rely; stable post rely ⟧
           ⟹ ⊢⇩I Some (Basic f) sat⇩p [pre, rely, guar, post]"

| Seq: "⟦ ⊢⇩I Some P sat⇩p [pre, rely, guar, mid]; ⊢⇩I Some Q sat⇩p [mid, rely, guar, post] ⟧
           ⟹ ⊢⇩I Some (Seq P Q) sat⇩p [pre, rely, guar, post]"

| Cond: "⟦ stable pre rely; ⊢⇩I Some P1 sat⇩p [pre ∩ b, rely, guar, post];
           ⊢⇩I Some P2 sat⇩p [pre ∩ -b, rely, guar, post]; ∀s. (s,s)∈guar ⟧
          ⟹ ⊢⇩I Some (Cond b P1 P2) sat⇩p [pre, rely, guar, post]"

| While: "⟦ stable pre rely; (pre ∩ -b) ⊆ post; stable post rely;
            ⊢⇩I Some P sat⇩p [pre ∩ b, rely, guar, pre]; ∀s. (s,s)∈guar ⟧
          ⟹ ⊢⇩I Some (While b P) sat⇩p [pre, rely, guar, post]"

| Await: "⟦ stable pre rely; stable post rely;
            ∀V. ⊢⇩I Some P sat⇩p [pre ∩ b ∩ {V}, {(s, t). s = t},
                UNIV, {s. (V, s) ∈ guar} ∩ post] ⟧
           ⟹ ⊢⇩I Some (Await b P) sat⇩p [pre, rely, guar, post]"

| None_hoare: "⟦ stable pre rely; pre ⊆ post ⟧  ⟹ ⊢⇩I None sat⇩p [pre, rely, guar, post]"

| Conseq: "⟦ pre ⊆ pre'; rely ⊆ rely'; guar' ⊆ guar; post' ⊆ post;
             ⊢⇩I P sat⇩p [pre', rely', guar', post'] ⟧
            ⟹ ⊢⇩I P sat⇩p [pre, rely, guar, post]"

| Unprecond: "⟦ ⊢⇩I P sat⇩p [pre, rely, guar, post]; ⊢⇩I P sat⇩p [pre', rely, guar, post] ⟧
            ⟹ ⊢⇩I P sat⇩p [pre ∪ pre', rely, guar, post]"

| Intpostcond: "⟦ ⊢⇩I P sat⇩p [pre, rely, guar, post]; ⊢⇩I P sat⇩p [pre, rely, guar, post'] ⟧
            ⟹ ⊢⇩I P sat⇩p [pre, rely, guar, post ∩ post']"

| Allprecond: "∀v∈U. ⊢⇩I P sat⇩p [{v}, rely, guar, post]
            ⟹ ⊢⇩I P sat⇩p [U, rely, guar, post]"

| Emptyprecond: "⊢⇩I P sat⇩p [{}, rely, guar, post]"


definition prog_validity :: "'a com option ⇒ 'a set ⇒ ('a × 'a) set ⇒ ('a × 'a) set ⇒ 'a set ⇒ bool"
                 ("⊨⇩I _ sat⇩p [_, _, _, _]" [60,0,0,0,0] 45) where
  "⊨⇩I P sat⇩p [pre, rely, guar, post] ≡
   ∀s. cp P s ∩ assum(pre, rely) ⊆ comm(guar, post)"


subsection ‹lemmas of SIMP›

lemma etran_or_ctran2_disjI3:
  "⟦ x∈cptn; Suc i<length x; ¬ x!i -c→ x!Suc i⟧ ⟹ x!i -e→ x!Suc i"
apply(induct x arbitrary:i)
 apply simp
apply clarify
apply(rule cptn.cases)
  apply simp+
  using less_Suc_eq_0_disj etran.intros apply force
  apply(case_tac i,simp)
  by simp


lemma stable_id: "stable P Id"
  unfolding stable_def Id_def by auto

lemma stable_id2: "stable P {(s,t). s = t}"
  unfolding stable_def by auto

lemma stable_int2: "stable s r ⟹ stable t r ⟹ stable (s ∩ t) r"
  by (metis (full_types) IntD1 IntD2 IntI stable_def)

lemma stable_int3: "stable k r ⟹ stable s r ⟹ stable t r ⟹ stable (k ∩ s ∩ t) r"
  by (metis (full_types) IntD1 IntD2 IntI stable_def)

lemma stable_un2: "stable s r ⟹ stable t r ⟹ stable (s ∪ t) r"
  by (simp add: stable_def)

(*
lemma Seq2: "⟦ ⊢ P sat [pre, rely, guar, mida]; mida ⊆ midb; ⊢ Q sat [midb, rely, guar, post] ⟧
  ⟹ ⊢⇩I Some (Seq P Q) sat⇩p [pre, rely, guar, post]"
  using Seq[of P pre rely guar mida Q post] Some_hoare[of "Seq P Q" pre rely guar post]
        RG_Hoare.Conseq[of mida midb rely rely guar guar post post Q]
  by blast*)

lemma Seq2: "⟦ ⊢⇩I Some P sat⇩p [pre, rely, guar, mida]; mida ⊆ midb; ⊢⇩I Some Q sat⇩p [midb, rely, guar, post] ⟧
  ⟹ ⊢⇩I Some (Seq P Q) sat⇩p [pre, rely, guar, post]"
  using Seq[of P pre rely guar mida Q post]
        Conseq[of mida midb rely rely guar guar post post]
  by blast

subsection‹Soundness of the Rule of Consequence›

lemma Conseq_sound:
  "⟦pre ⊆ pre'; rely ⊆ rely'; guar' ⊆ guar; post' ⊆ post;
  ⊨⇩I P sat⇩p [pre', rely', guar', post']⟧
  ⟹ ⊨⇩I P sat⇩p [pre, rely, guar, post]"
apply(simp add:prog_validity_def assum_def comm_def)
apply clarify
apply(erule_tac x=s in allE)
apply(drule_tac c=x in subsetD)
 apply force
apply force
done

subsection‹Soundness of the Rule of Unprecond›

lemma Unprecond_sound:
  assumes p0: " ⊨⇩I P sat⇩p [pre, rely, guar, post]"
    and  p1: " ⊨⇩I P sat⇩p [pre', rely, guar, post]"
   shows " ⊨⇩I P sat⇩p [pre ∪ pre', rely, guar, post]"
proof -
{
  fix s c
  assume "c ∈ cp P s ∩ assum(pre ∪ pre', rely)"
  hence a1: "c ∈ cp P s" and
        a2: "c ∈ assum(pre ∪ pre', rely)" by auto
  hence "c ∈ assum(pre, rely) ∨ c ∈ assum(pre', rely)"
    by (metis (no_types, lifting) CollectD CollectI Un_iff assum_def prod.simps(2))
  hence "c ∈ comm(guar, post)"
    proof
      assume "c ∈ assum (pre, rely)"
      with p0 a1 show "c ∈ comm (guar, post)"
        unfolding prog_validity_def by auto
    next
      assume "c ∈ assum (pre', rely)"
      with p1 a1 show "c ∈ comm (guar, post)"
        unfolding prog_validity_def by auto
    qed
}
then show ?thesis unfolding prog_validity_def by auto
qed

subsection‹Soundness of the Rule of Intpostcond›

lemma Intpostcond_sound:
  assumes p0: " ⊨⇩I P sat⇩p [pre, rely, guar, post]"
    and  p1: " ⊨⇩I P sat⇩p [pre, rely, guar, post']"
   shows " ⊨⇩I P sat⇩p [pre, rely, guar, post ∩ post']"
proof -
{
  fix s c
  assume a0: "c ∈ cp P s ∩ assum(pre, rely)"
  with p0 have "c ∈ comm(guar, post)" unfolding prog_validity_def by auto
  moreover
  from a0 p1 have "c ∈ comm(guar, post')" unfolding prog_validity_def by auto
  ultimately have "c ∈ comm(guar, post ∩ post')"
    by (simp add: comm_def)
}
then show ?thesis unfolding prog_validity_def by auto
qed

subsection‹Soundness of the Rule of Allprecond›

lemma Allprecond_sound:
  assumes p1: "∀v∈U. ⊨⇩I P sat⇩p [{v}, rely, guar, post]"
    shows " ⊨⇩I P sat⇩p [U, rely, guar, post]"
proof -
{
  fix s c
  assume a0: "c ∈ cp P s ∩ assum(U, rely)"
  then obtain x where a1: "x∈U ∧ snd (c!0) = x"
    by (metis (no_types, lifting) CollectD IntD2 assum_def prod.simps(2))

  with p1 have "⊨⇩I P sat⇩p [{x}, rely, guar, post]" by simp
  hence a2: "∀s. cp P s ∩ assum({x}, rely) ⊆ comm(guar, post)" unfolding prog_validity_def by simp

  from a0 have "c ∈ assum(U, rely)" by simp
  hence "snd (c!0) ∈ U ∧ (∀i. Suc i<length c ⟶
               c!i -e→ c!(Suc i) ⟶ (snd (c!i), snd (c!Suc i)) ∈ rely)" by (simp add:assum_def)
  with a1 have "snd (c!0) ∈ {x} ∧ (∀i. Suc i<length c ⟶
               c!i -e→ c!(Suc i) ⟶ (snd (c!i), snd (c!Suc i)) ∈ rely)" by simp

  hence "c∈assum({x}, rely)" by (simp add:assum_def)
  with a0 a2 have "c ∈ comm(guar, post)" by auto
}
then show ?thesis using prog_validity_def by blast
qed

subsection‹Soundness of the Rule of Emptyprecond›

lemma Emptyprecond_sound: " ⊨⇩I P sat⇩p [{}, rely, guar, post]"
unfolding prog_validity_def by(simp add:assum_def)


subsection‹Soundness of None rule›

lemma none_all_none: "c!0=(None,s) ∧ c ∈ cptn ⟹ ∀i<length c. fst (c ! i) = None"
proof(induct c arbitrary:s)
  case Nil
  then show ?case by simp
next
  case (Cons a c)
  assume p1: "⋀s. c ! 0 = (None, s) ∧ c ∈ cptn ⟹ ∀i<length c. fst (c ! i) = None"
    and  p2: "(a # c) ! 0 = (None, s) ∧ a # c ∈ cptn"
  hence a0: "a = (None,s)" by simp
  thus ?case
    proof(cases "c = []")
      case True
      with a0 show ?thesis by auto
    next
      case False
      assume b0: "c ≠ []"
      with p2 have c_cpts: "c ∈ cptn" using tl_in_cptn by fast
      from b0 obtain c' and b where bc': "c = b # c'"
        using list.exhaust by blast
      from a0 have "¬ a -c→ b" by(force elim: ctran.cases)
      with p2 have "a -e→ b"  using bc' etran_or_ctran2_disjI3[of "a#c" 0] by auto
      hence "fst b = None" using etran.cases
        by (metis a0 prod.collapse)
      with p1 bc' c_cpts have "∀i<length c. fst (c ! i) = None"
        by (metis nth_Cons_0 prod.collapse)
      with a0 show ?thesis
        by (simp add: nth_Cons')
    qed

qed

lemma None_sound_h: "∀x. x ∈ pre ⟶ (∀y. (x, y) ∈ rely ⟶ y ∈ pre) ⟹
         pre ⊆ post ⟹
         snd (c ! 0) ∈ pre ⟹
         c ≠ [] ⟹ ∀i. Suc i < length c ⟶ (snd (c ! i), snd (c ! Suc i)) ∈ rely
      ⟹ i < length c ⟹ snd (c ! i) ∈ pre"
apply(induct i) by auto

lemma None_sound:
  "⟦ stable pre rely; pre ⊆ post ⟧
  ⟹ ⊨⇩I None sat⇩p [pre, rely, guar, post]"
proof -
  assume p0: "stable pre rely"
    and  p2: "pre ⊆ post"
  {
    fix s c
    assume a0: "c ∈ cp None s ∩ assum(pre, rely)"
    hence c1: "c!0=(None,s) ∧ c ∈ cptn" by (simp add:cp_def)
    from a0 have c2: "snd (c!0) ∈ pre ∧ (∀i. Suc i<length c ⟶
               c!i -e→ c!(Suc i) ⟶ (snd (c!i), snd (c!Suc i)) ∈ rely)"
      by (simp add:assum_def)
    from c1 have c_ne_empty: "c ≠ []"
      by auto
    from c1 have c_all_none: "∀i<length c. fst (c ! i) = None" using none_all_none by fast

    (* have "(∀i. Suc i<length c ⟶
               c!i -impc→ c!(Suc i) ⟶ (gets_p (c!i), gets_p (c!Suc i)) ∈ guar)" *)
    {
      fix i
      assume suci: "Suc i<length c"
        and cc: "c!i -c→ c!(Suc i)"
      from suci c_all_none have "c!i -e→ c!(Suc i)"
        by (metis Suc_lessD etran.intros prod.collapse)
      with cc have"(snd (c!i), snd (c!Suc i)) ∈ guar"
        using c1 etran_or_ctran2_disjI1 suci by auto
    }
    moreover
    {
      assume last_none: "fst (last c) = None"
      from c2 c_all_none have "∀i. Suc i<length c ⟶ (snd (c!i), snd (c!Suc i)) ∈ rely"
        by (metis Suc_lessD etran.intros prod.collapse)
      with p0 p2 c2 c_ne_empty have "∀i. i < length c ⟶ snd (c ! i) ∈ pre"
        apply(simp add: stable_def) apply clarify using None_sound_h by blast
      with p2 c_ne_empty have "snd (last c) ∈ post"
        using One_nat_def c_ne_empty last_conv_nth by force
    }
    ultimately have "c ∈ comm(guar, post)" by (simp add:comm_def)
  }
  thus "⊨⇩I None sat⇩p [pre, rely, guar, post]" using prog_validity_def by blast
qed

subsection‹Soundness of the Await rule›

lemma Await_sound:
  "⟦stable pre rely; stable post rely;
  ∀V. ⊢⇩I Some P sat⇩p [pre ∩ b ∩ {s. s = V}, {(s, t). s = t},
                 UNIV, {s. (V, s) ∈ guar} ∩ post] ∧
  ⊨⇩I Some P sat⇩p [pre ∩ b ∩ {s. s = V}, {(s, t). s = t},
                 UNIV, {s. (V, s) ∈ guar} ∩ post] ⟧
  ⟹ ⊨⇩I Some (Await b P) sat⇩p [pre, rely, guar, post]"
apply(unfold prog_validity_def)
apply clarify
apply(simp add:comm_def)
apply(rule conjI)
 apply clarify
 apply(simp add:cp_def assum_def)
 apply clarify
 apply(frule_tac j=0 and k=i and p=pre in stability,simp_all)
   apply(erule_tac x=ia in allE,simp)
  apply(subgoal_tac "x∈ cp (Some(Await b P)) s")
  apply(erule_tac i=i in unique_ctran_Await,force,simp_all)
  apply(simp add:cp_def)
(*--‹here starts the different part.›*)
 apply(erule ctran.cases,simp_all)
 apply(drule Star_imp_cptn)
 apply clarify
 apply(erule_tac x=sa in allE)
 apply clarify
 apply(erule_tac x=sa in allE)
 apply(drule_tac c=l in subsetD)
  apply (simp add:cp_def)
  apply clarify
  apply(erule_tac x=ia and P="λi. H i ⟶ (J i, I i)∈ctran" for H J I in allE,simp)
  apply(erule etranE,simp)
 apply simp
apply clarify
apply(simp add:cp_def)
apply clarify
apply(frule_tac i="length x - 1" in exists_ctran_Await_None,force)
  apply (case_tac x,simp+)
 apply(rule last_fst_esp,simp add:last_length)
 apply(case_tac x, simp+)
apply clarify
apply(simp add:assum_def)
apply clarify
apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all)
  apply(erule_tac x=i in allE,simp)
 apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
apply(case_tac "x!j")
apply clarify
apply simp
apply(drule_tac s="Some (Await b P)" in sym,simp)
apply(case_tac "x!Suc j",simp)
apply(rule ctran.cases,simp)
apply(simp_all)
apply(drule Star_imp_cptn)
apply clarify
apply(erule_tac x=sa in allE)
apply clarify
apply(erule_tac x=sa in allE)
apply(drule_tac c=l in subsetD)
 apply (simp add:cp_def)
 apply clarify
 apply(erule_tac x=i and P="λi. H i ⟶ (J i, I i)∈ctran" for H J I in allE,simp)
 apply(erule etranE,simp)
apply simp
apply clarify
apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
 apply(case_tac x,simp+)
 apply(erule_tac x=i in allE)
apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
 apply arith+
apply(case_tac x)
apply(simp add:last_length)+
done

theorem rgsound_p:
  "⊢⇩I P sat⇩p [pre, rely, guar, post] ⟹ ⊨⇩I P sat⇩p [pre, rely, guar, post]"
apply(erule rghoare_p.induct)
using RG_Hoare.Basic_sound apply(simp add:prog_validity_def com_validity_def) apply blast
using RG_Hoare.Seq_sound apply(simp add:prog_validity_def com_validity_def) apply blast
using RG_Hoare.Cond_sound apply(simp add:prog_validity_def com_validity_def) apply blast
using RG_Hoare.While_sound apply(simp add:prog_validity_def com_validity_def) apply blast
using Await_sound apply fastforce
apply(force elim:None_sound)
apply(erule Conseq_sound,simp+)
apply(erule Unprecond_sound,simp+)
apply(erule Intpostcond_sound,simp+)
using Allprecond_sound apply force
using Emptyprecond_sound apply force
done


end