Theory PiCore_ext

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

section ‹Rely-guarantee-based Safety Reasoning›

theory PiCore_ext
  imports PiCore_Hoare
begin

definition "list_of_set aset ≡ (SOME l. set l = aset)"

lemma set_of_list_of_set:
  assumes fin: "finite aset"
  shows "set (list_of_set aset) = aset"
proof(simp add: list_of_set_def)
  from fin obtain l where "set l = aset" using finite_list by auto
  then show "set (SOME l. set l = aset) = aset"
    by (metis (mono_tags, lifting) some_eq_ex)
qed

context event_hoare
begin

fun OR_list :: "('l,'k,'s,'prog) esys list ⇒ ('l,'k,'s,'prog) esys" where
  "OR_list [a] = a" |
  "OR_list (a#b#ax) = a OR (OR_list (b#ax))" |
  "OR_list [] = fin"

lemma "OR_list [a] = a" by auto
lemma "OR_list [a,b] = a OR b" by auto
lemma "OR_list [a,b,c] = a OR (b OR c)" by auto


lemma Evt_OR_list:
  "ess ≠ [] ⟹ ∀i<length ess. Γ ⊢ (ess!i) sat⇩e [pre, rely, guar, post]
  ⟹ Γ ⊢ (OR_list ess) sat⇩e [pre, rely, guar, post]"
  apply(induct ess) apply simp
  apply(case_tac "ess=[]") apply auto[1]
  by (metis Evt_Choice OR_list.simps(2) length_Cons less_Suc_eq_0_disj list.exhaust nth_Cons_0 nth_Cons_Suc)

fun AND_list :: "('l,'k,'s,'prog) esys list ⇒ ('l,'k,'s,'prog) esys" where
  "AND_list [a] = a" |
  "AND_list (a#b#ax) = a ⋈ (AND_list (b#ax))" |
  "AND_list [] = fin"

lemma "AND_list [a] = a" by auto
lemma "AND_list [a,b] = a ⋈ b" by auto
lemma "AND_list [a,b,c] = a ⋈ (b ⋈ c)" by auto

lemma Int_list_lm: "P a ∩ (⋂i<length ess. P (ess ! i)) = (⋂i<length (a # ess). P ((a # ess) ! i))"
  apply(induct ess) apply auto[1]
  apply(rule subset_antisym)
   apply auto[1] apply (metis lessThan_iff less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc)
  apply auto
  by (metis Suc_leI le_imp_less_Suc lessThan_iff nth_Cons_Suc)


lemma Evt_AND_list:
  "ess ≠ [] ⟹
  ∀i<length ess. Γ ⊢ Com (ess!i) sat⇩e [Pre (ess!i), Rely (ess!i), Guar (ess!i), Post (ess!i)] ⟹
  ∀i<length ess. ∀s. (s,s)∈Guar (ess!i) ⟹
  ∀i j. i < length ess ∧ j < length ess ∧ i ≠ j ⟶ Guar (ess!i) ⊆ Rely (ess!j) ⟹
  Γ ⊢ (AND_list (map Com ess)) sat⇩e [⋂i<length ess. Pre (ess!i), ⋂i<length ess. Rely (ess!i),
          ⋃i<length ess. Guar (ess!i), ⋂i<length ess. Post (ess!i)]"
  apply(induct ess) apply simp
  apply(case_tac "ess=[]") apply auto[1]
proof-
  fix a ess
    (**)
  assume a0: "ess ≠ [] ⟹
          ∀i<length ess. Γ ⊢ Com (ess ! i) sat⇩e [Pre (ess ! i), Rely (ess ! i), Guar (ess ! i), Post (ess ! i)] ⟹
          ∀i<length ess. ∀s. (s, s) ∈ Guar (ess ! i) ⟹
          ∀i j. i < length ess ∧ j < length ess ∧ i ≠ j ⟶ Guar (ess ! i) ⊆ Rely (ess ! j) ⟹
          Γ ⊢ AND_list (map Com ess) sat⇩e [⋂i<length ess. Pre (ess ! i), ⋂i<length ess. Rely (ess ! i),
            ⋃i<length ess. Guar (ess ! i), ⋂i<length ess. Post (ess ! i)]"
    and a1: "a # ess ≠ []"
    and a2: "∀i<length (a # ess). Γ ⊢ Com ((a # ess) ! i) sat⇩e [Pre ((a # ess) ! i),
                  Rely ((a # ess) ! i), Guar ((a # ess) ! i), Post ((a # ess) ! i)]"
    and a3: "∀i<length (a # ess). ∀s. (s, s) ∈ Guar ((a # ess) ! i)"
    and a4: "∀i j. i < length (a # ess) ∧ j < length (a # ess) ∧ i ≠ j
              ⟶ Guar ((a # ess) ! i) ⊆ Rely ((a # ess) ! j)"
    and a5: "ess ≠ []"
  let ?pre = "⋂i<length ess. Pre (ess ! i)"
  let ?rely = "⋂i<length ess. Rely (ess ! i)"
  let ?guar = "⋃i<length ess. Guar (ess ! i)"
  let ?post = "⋂i<length ess. Post (ess ! i)"
  let ?pre' = "⋂i<length (a # ess). Pre ((a # ess) ! i)"
  let ?rely' = "⋂i<length (a # ess). Rely ((a # ess) ! i)"
  let ?guar' = "⋃i<length (a # ess). Guar ((a # ess) ! i)"
  let ?post' = "⋂i<length (a # ess). Post ((a # ess) ! i)"

  from a2 have a6: "∀i<length ess. Γ ⊢ Com (ess ! i) sat⇩e [Pre (ess ! i), Rely (ess ! i), Guar (ess ! i), Post (ess ! i)]"
    by auto
  moreover
  from a3 have a7: "∀i<length ess. ∀s. (s, s) ∈ Guar (ess ! i)" by auto
  moreover
  from a4 have a8: "∀i j. i < length ess ∧ j < length ess ∧ i ≠ j ⟶ Guar (ess ! i) ⊆ Rely (ess ! j)"
    by fastforce
  ultimately have b1: "Γ ⊢ AND_list (map Com ess) sat⇩e [?pre, ?rely, ?guar, ?post]"
    using a0 a5 by auto
  have b2: "AND_list (map Com (a # ess)) = Com a ⋈ AND_list (map Com ess)"
    by (metis (no_types, hide_lams) AND_list.simps(2) a5 list.exhaust list.simps(9))
  from a2 have b3: "Γ ⊢ Com a sat⇩e [Pre a, Rely a, Guar a, Post a]"
    by fastforce
  have b4: "Γ ⊢ AND_list (map Com ess) sat⇩e [?pre', ?rely, ?guar, ?post]"
    apply(rule Evt_conseq[of ?pre' ?pre ?rely ?rely ?guar ?guar ?post ?post])
        apply fastforce using b1 by simp+
  have b5: "Γ ⊢ Com a sat⇩e [?pre', Rely a, Guar a, Post a]"
    apply(rule Evt_conseq[of ?pre' "Pre a" "Rely a" "Rely a" "Guar a" "Guar a" "Post a" "Post a"])
        apply fastforce
    using b3 by simp+
  show "Γ ⊢ AND_list (map Com (a # ess)) sat⇩e [?pre', ?rely', ?guar', ?post']"
    apply(rule subst[where t="AND_list (map Com (a # ess))" and s= "Com a ⋈ AND_list (map Com ess)"])
    using b2 apply simp
    apply(rule subst[where s="Post a ∩ ?post" and t="?post'"])
     prefer 2
     apply(rule Evt_Join[of Γ "Com a" ?pre' "Rely a" "Guar a" "Post a" "AND_list (map Com ess)"
          ?pre' ?rely ?guar ?post ?pre' ?rely' ?guar'])
    using b5 apply fast
    using b4 apply fast
    apply blast
        apply(rule Un_least) apply fastforce apply clarsimp using a4
        apply (smt Suc_mono a1 drop_Suc_Cons hd_drop_conv_nth length_Cons length_greater_0_conv nat.simps(3) nth_Cons_0 set_mp)
       apply(rule Un_least) apply fastforce apply clarsimp using a4
       apply (smt Suc_mono a1 drop_Suc_Cons hd_drop_conv_nth length_Cons length_greater_0_conv nat.simps(3) nth_Cons_0 set_mp)
    using a3 apply force using a3 a5 a7 apply auto[1]
     apply auto[1]
    using Int_list_lm by metis
qed


lemma Evt_AND_list2:
  "ess ≠ [] ⟹
  ∀i<length ess. Γ ⊢ Com (ess!i) sat⇩e [Pre (ess!i), Rely (ess!i), Guar (ess!i), Post (ess!i)] ⟹
  ∀i<length ess. ∀s. (s,s)∈Guar (ess!i) ⟹
  ∀i<length ess. P ⊆ Pre (ess!i) ⟹
  ∀i<length ess. Guar (ess!i) ⊆ G ⟹
  ∀i<length ess. R ⊆ Rely (ess!i) ⟹
  ∀i j. i<length ess ∧ j < length ess ∧ i ≠ j ⟶ Guar (ess!i) ⊆ Rely (ess!j) ⟹
  ∀i<length ess. Post (ess!i) ⊆ Q ⟹
  Γ ⊢ (AND_list (map Com ess)) sat⇩e [P, R, G, Q]"

  apply(rule Evt_conseq[of P "⋂i<length ess. Pre (ess!i)"
        R "⋂i<length ess. Rely (ess!i)"
        "⋃i<length ess. Guar (ess!i)" G
        "⋂i<length ess. Post (ess!i)" Q
        Γ "AND_list (map Com ess)"])
      apply fast apply fast apply fast apply fastforce
  using Evt_AND_list by metis

definition ‹react_sys l ≡ EWhile UNIV (OR_list l)›

lemma fin_sat:
  ‹stable P R ⟹ Γ ⊨ fin sat⇩e [P, R, G, P]›
proof(simp, rule allI, rule allI, standard)
  let ?P = ‹lift_state_set P›
  let ?R = ‹lift_state_pair_set R›
  let ?G = ‹lift_state_pair_set G›

  fix s0 x0
  fix cpt
  assume stable: ‹stable P R›
  assume ‹cpt ∈ {cpt ∈ cpts (estran Γ). hd cpt = (fin, s0, x0)} ∩ assume ?P ?R›

  then have cpt: ‹cpt ∈ cpts (estran Γ)› and hd_cpt: ‹hd cpt = (fin, s0, x0)› and cpt_assume: ‹cpt ∈ assume ?P ?R› by auto
  from cpts_nonnil[OF cpt] have ‹cpt≠[]› .
  from hd_cpt ‹cpt≠[]› obtain cs where cpt_Cons: ‹cpt = (fin, s0, x0) # cs› by (metis hd_Cons_tl)
  from all_etran_from_fin[OF cpt cpt_Cons] have all_etran: ‹∀i. Suc i < length cpt ⟶ cpt ! i ─e→ cpt ! Suc i› .
  show ‹cpt ∈ commit (estran Γ) {fin} ?G ?P›
  proof(auto simp add: commit_def)
    fix i
    assume Suc_i_lt: ‹Suc i < length cpt›
    assume ctran: ‹(cpt ! i, cpt ! Suc i) ∈ estran Γ›
    from all_etran[rule_format, OF Suc_i_lt] have ‹cpt ! i ─e→ cpt ! Suc i› .
    from etran_imp_not_ctran[OF this] have ‹(cpt ! i, cpt ! Suc i) ∉ estran Γ› .
    with ctran show ‹(snd (cpt ! i), snd (cpt ! Suc i)) ∈ ?G› by blast
  next
    assume ‹fst (last cpt) = fin›
    have ‹∀i<length cpt. snd (cpt!i) ∈ ?P›
    proof(auto)
      fix i
      assume i_lt: ‹i < length cpt›
      show ‹snd (cpt ! i) ∈ ?P›
        using i_lt
      proof(induct i)
        case 0
        then show ?case
          apply(subst hd_conv_nth[symmetric])
           apply(rule ‹cpt≠[]›)
          using cpt_assume by (simp add: assume_def)
      next
        case (Suc i)
        then show ?case
        proof-
          assume 1: ‹i < length cpt ⟹ snd (cpt ! i) ∈ ?P›
          assume Suc_i_lt: ‹Suc i < length cpt›
          with 1 have ‹snd (cpt ! i) ∈ ?P› by simp
          from all_etran[rule_format, OF Suc_i_lt] have ‹cpt ! i ─e→ cpt ! Suc i› .
          with cpt_assume have ‹(snd (cpt ! i), snd (cpt ! Suc i)) ∈ ?R›
            apply(auto simp add: assume_def)
            using Suc_i_lt by blast
          with stable show ‹snd (cpt ! Suc i) ∈ ?P›
            apply(simp add: stable_def)
            using ‹snd (cpt ! i) ∈ ?P› by (simp add: lift_state_set_def lift_state_pair_set_def case_prod_unfold)
        qed
      qed
    qed
    then show ‹snd (last cpt) ∈ ?P› using ‹cpt≠[]›
      apply-
      apply(subst last_conv_nth)
       apply assumption
      by simp
  qed
qed

lemma Evt_react_list:
  ‹⟦ ∀i<length (rgfs::(('l,'k,'s,'prog) esys,'s) rgformula list). Γ ⊢ Com (rgfs!i) sat⇩e [Pre (rgfs!i), Rely (rgfs!i), Guar (rgfs!i), Post (rgfs!i)] ∧
   pre ⊆ Pre (rgfs!i) ∧ rely ⊆ Rely (rgfs!i) ∧
   Guar (rgfs!i) ⊆ guar ∧
   Post (rgfs!i) ⊆ pre; rgfs ≠ [];
   stable pre rely; ∀s. (s, s)∈guar ⟧ ⟹
   Γ ⊢ react_sys (map Com rgfs) sat⇩e [pre, rely, guar, pre]›
  apply (unfold react_sys_def)
  apply (rule Evt_While)
      apply assumption
     apply fast
    apply assumption
   apply (simp add: list_of_set_def)
   apply(rule Evt_OR_list)
    apply simp
   apply simp
   apply(rule allI)
   apply(rule impI)
   apply(rule_tac pre'=‹Pre (rgfs!i)› and rely'=‹Rely (rgfs!i)› and guar'=‹Guar (rgfs!i)› and post'=‹Post (rgfs!i)› in Evt_conseq)
       apply simp+
  done

lemma Evt_react_set:
  ‹⟦ ∀rgf ∈ (rgfs::(('l,'k,'s,'prog) esys,'s) rgformula set). Γ ⊢ Com rgf sat⇩e [Pre rgf, Rely rgf, Guar rgf, Post rgf] ∧
   pre ⊆ Pre rgf ∧ rely ⊆ Rely rgf ∧
   Guar rgf ⊆ guar ∧
   Post rgf ⊆ pre; rgfs ≠ {}; finite rgfs;
   stable pre rely; ∀s. (s, s)∈guar ⟧ ⟹
   Γ ⊢ react_sys (map Com (list_of_set rgfs)) sat⇩e [pre, rely, guar, pre]›
  apply(rule Evt_react_list)
     apply(simp add: list_of_set_def)
     apply (smt finite_list nth_mem tfl_some)
    apply(simp add: list_of_set_def)
    apply (metis (mono_tags, lifting) empty_set finite_list tfl_some)
   apply assumption
  apply assumption
  done

lemma Evt_react_set':
  ‹⟦ ∀rgf ∈ (rgfs::(('l,'k,'s,'prog) esys,'s) rgformula set). Γ ⊢ Com rgf sat⇩e [Pre rgf, Rely rgf, Guar rgf, Post rgf] ∧
   pre ⊆ Pre rgf ∧ rely ⊆ Rely rgf ∧
   Guar rgf ⊆ guar ∧
   Post rgf ⊆ pre; rgfs ≠ {}; finite rgfs;
   stable pre rely; ∀s. (s, s)∈guar; pre ⊆ post ⟧ ⟹
   Γ ⊢ react_sys (map Com (list_of_set rgfs)) sat⇩e [pre, rely, guar, post]›
  apply(subgoal_tac ‹Γ ⊢ react_sys (map Com (list_of_set rgfs)) sat⇩e [pre, rely, guar, pre]›)
  using Evt_conseq apply blast
  using Evt_react_set apply blast
  done

end (* context event_hoare *)

end