Theory picore_CSimpl

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

section ‹Integrating the CSimpl language into Picore›

theory picore_CSimpl
imports "CSimpl.LocalRG_HoareDef" "../picore/PiCore_RG_Invariant"
begin

type_synonym ('s,'p,'f,'e) configI = "('s,'p,'f,'e)com × ('s,'f) xstate"

type_synonym ('s,'p,'f,'e) confsI = "(('s,'p,'f,'e) configI) list"

type_synonym ('s,'p,'f,'e) Env = "('s,'p,'f,'e) body × ('s,'p,'f,'e) sextuple set"

type_synonym ('s,'p,'f,'e) confs' =  "('s,'p,'f,'e) Env ×(('s,'p,'f,'e) config) list"

(*
locale PicoreCSimpl =
fixes Env :: "('s,'p,'f,'e) Env"
assumes proc_sat: "∀(c,p,R,G,q,a)∈ snd Env. fst Env ⊨⇘/{}⇙ (Call c) sat [p, R, G, q,a]"
begin
*)

definition ptranI :: "('s,'p,'f,'e) Env ⇒ (('s,'p,'f,'e) configI × ('s,'p,'f,'e) configI) set"
where "ptranI Ψ ≡ {(P,Q). fst Ψ ⊢⇩c P → Q}"

definition ptranI' :: "('s,'p,'f,'e) Env ⇒ ('s,'p,'f,'e) configI ⇒ ('s,'p,'f,'e) configI ⇒ bool"
("_ ⊢⇩c⇩I _ → _" [81,81] 80)
where "Ψ ⊢⇩c⇩I P → Q ≡ (P,Q) ∈ ptranI Ψ"

lemma none_no_tranI': "((Q, s),(P,t)) ∈ ptranI Ψ ⟹ Q ≠ Skip"
  apply (simp add:ptranI_def) apply(rule stepc.cases)
  by simp+

lemma none_no_tranI: "((Skip, s),(P,t)) ∉ ptranI Ψ"
  using none_no_tranI' by fast

lemma ptran_neq': "((P, s),(Q,t)) ∈ ptranI Ψ ⟹ P ≠ Q"
  apply (simp add:ptranI_def)
  apply(rule stepc.cases) apply simp
    apply(rule stepc.cases) apply simp+
      using mod_env_not_component apply blast
      apply simp+
      using step_change_p_or_eq_s apply blast
      apply (simp add: step_change_p_or_eq_s)
      apply simp+
done

lemma ptran_neqI: "((P, s),(P,t)) ∉ ptranI Ψ"
  using ptran_neq' by fast

(* inductive_set cpts_p :: "'s imp_pconfs set"
where
  CptsPOne: "[(P,s)] ∈ cpts_p"
| CptsPEnv: "(P, t)#xs ∈ cpts_p ⟹ (P,s)#(P,t)#xs ∈ cpts_p"
| CptsPComp: "⟦(P,s) -impc→ (Q,t); (Q, t)#xs ∈ cpts_p⟧ ⟹ (P,s)#(Q,t)#xs ∈ cpts_p" *)
(* inductive_set cptn :: "(('s,'p,'f,'e) confs) set"
where
  CptnOne: " (Ψ, [(P,s)]) ∈ cptn"
| CptnEnv: "⟦Ψ⊢⇩c(P,s) →⇩e (P,t); (Ψ,(P, t)#xs) ∈ cptn ⟧ ⟹
             (Ψ,(P,s)#(P,t)#xs) ∈ cptn"
| CptnComp: "⟦Ψ⊢⇩c(P,s) → (Q,t); (Ψ,(Q, t)#xs) ∈ cptn ⟧ ⟹
              (Ψ,(P,s)#(Q,t)#xs) ∈ cptn" *)
inductive_set cptn' :: "(('s,'p,'f,'e) confs') set"
where
  CptnOne': " (Ψ, [(P,s)]) ∈ cptn'"
| CptnEnv': "(Ψ,(P, t)#xs) ∈ cptn' ⟹ (Ψ,(P,s)#(P,t)#xs) ∈ cptn'"
| CptnComp': "⟦Ψ⊢⇩c⇩I(P,s) → (Q,t); (Ψ,(Q, t)#xs) ∈ cptn' ⟧ ⟹
              (Ψ,(P,s)#(Q,t)#xs) ∈ cptn'"

lemma tl_in_cptn': "⟦ (Ψ,a#xs) ∈cptn'; xs≠[] ⟧ ⟹ (Ψ,xs)∈cptn'"
  by (force elim: cptn'.cases)

lemma ab_cptn'_c_or_eq: "(Ψ,a#b#l) ∈ cptn' ⟹ (Ψ⊢⇩c⇩I a → b) ∨ fst a = fst b"
  by (force elim: cptn'.cases)

lemma cptn_not_empty': "(Ψ,l) ∈ cptn ⟹ l ≠ []"
  by(force elim:cptn.cases)

lemma cptn'_not_empty': "(Ψ,l) ∈ cptn' ⟹ l ≠ []"
  by(force elim:cptn'.cases)


lemma cptn_in_cptn'_h: "((fst Ψ, l) ∈ cptn ⟹ (Ψ, l) ∈ cptn') ⟹ (fst Ψ, a # l) ∈ cptn ⟹ (Ψ, a # l) ∈ cptn'"
apply(rule cptn.cases[of "fst Ψ" "a#l"])
  apply simp
  using CptnOne' apply fast
  using CptnEnv' apply fast
  using CptnComp' apply(simp add:ptranI'_def ptranI_def) apply fast
done

lemma cptn_in_cptn': "(fst Ψ,l) ∈ cptn ⟹ (Ψ,l) ∈ cptn'"
apply(induct l) using cptn_not_empty' apply fast
using cptn_in_cptn'_h apply fast
done

definition cpts_pI :: "('s,'p,'f,'e) Env ⇒ (('s,'p,'f,'e) confsI) set"
where "cpts_pI Ψ ≡ {l. ∃l'. (Ψ,l') ∈ cptn' ∧ l = l'}"

(* assumes cpts_of_p_def: "cpts_of_p Ψ P s ≡ {l. l!0=(P,s) ∧ l ∈ cpts_p Ψ}"  *)
(* definition cp :: "('s,'p,'f,'e) body ⇒ ('s,'p,'f,'e) com ⇒
                  ('s,'f) xstate ⇒ (('s,'p,'f,'e) confs) set" where
  "cp Ψ P s ≡ {(Ψ1,l). l!0=(P,s) ∧ (Ψ,l) ∈ cptn ∧ Ψ1=Ψ}"  *)
definition cpts_of_pI :: "('s,'p,'f,'e) Env ⇒ (('s,'p,'f,'e) com) ⇒ ('s,'f) xstate ⇒ (('s,'p,'f,'e) confsI) set" where
  "cpts_of_pI Ψ P s ≡  {l. l!0=(P,s) ∧ l ∈ cpts_pI Ψ}"

lemma cptn_in_cpts_pI: "(Ψ,l') ∈ cptn' ∧ l = l'
      ⟹ l ∈ cpts_pI Ψ"
by (simp add:cpts_pI_def)


lemma cptn_not_emptyI:"[] ∉ cpts_pI Ψ"
  apply(simp add:cpts_pI_def) apply(force elim:cptn'.cases)
done

lemma cpts_of_pI_emptyI: "l ∈ cpts_of_pI Ψ P s ⟹ l ≠ []"
  apply(simp add:cpts_of_pI_def) using cptn_not_emptyI by fast

(*
lemma cpts_of_p_defI: "cpts_of_pI Ψ P s ≡ {l. l!0=(P,s) ∧ l ∈ cpts_pI Ψ}"
  by(simp add:cpts_of_pI_def)
*)
lemma cpts_of_p_defI: "l!0=(P,s) ∧ l ∈ cpts_pI Ψ ⟹ l ∈ cpts_of_pI Ψ P s"
  by(simp add:cpts_of_pI_def)

(* inductive
lrghoare :: "[('s,'p,'f,'e) body,
             ('s,'p,'f,'e) sextuple set,
              'f set,
              ('s,'p,'f,'e) com,
              ('s set),
              (('s,'f) tran) set, (('s,'f) tran) set,
              's set,
               's set] ⇒ bool"
    ("_,_ ⊢⇘'/_⇙ _ sat [_, _, _, _,_]" [61,61,60,60,0,0,0,0] 45) *)
(* Ψ ⊨⇘/F⇙ Pr sat [p, R, G, q,a] *)
(* lemma localRG_sound: "Ψ,Θ ⊢⇘/F⇙ c sat [p, R, G, q,a] ⟹ Ψ,Θ ⊨⇘/F⇙ c sat [p, R, G, q,a]" *)
definition rghoare_pI :: "('s,'p,'f,'e) Env ⇒ [('s,'p,'f,'e)com, ('s,'f) xstate set, (('s,'f) xstate × ('s,'f) xstate) set,
                            (('s,'f) xstate × ('s,'f) xstate) set, ('s,'f) xstate set] ⇒ bool"
("_ ⊢⇩I _ sat⇩p [_, _, _, _]" [60,0,0,0,0] 45)
where "rghoare_pI Ψ c p R G q
  ≡ (p ⊆ Normal ` UNIV) ∧ (q ⊆ Normal ` UNIV)
    ∧ (∀(c,p,R,G,q,a)∈ snd Ψ. fst Ψ,{} ⊢⇘/{}⇙ (Call c) sat [p, R, G, q,a])
    ∧ (fst Ψ,snd Ψ ⊢⇘/{}⇙ c sat [{s. Normal s ∈ p}, R, G, {s. Normal s ∈ q}, {}]) 
    ∧ (∀(s,t)∈R. s ∉ Normal ` UNIV ⟶ s = t)"

(* definition assum ::
  "('s set × ('s,'f) tran set) ⇒ (('s,'p,'f,'e) confs) set" where
  "assum ≡ λ(pre, rely).
             {c. snd((snd c)!0) ∈ Normal ` pre ∧
                 (∀i. Suc i<length (snd c) ⟶
                 (fst c)⊢⇩c((snd c)!i)  →⇩e ((snd c)!(Suc i)) ⟶
                   (snd((snd c)!i), snd((snd c)!(Suc i))) ∈  rely)}" *)
(* assume_p_def: "assume_p Ψ ≡ λ(pre, rely). {c. gets_p (c!0) ∈ pre ∧ (∀i. Suc i<length c ⟶
               Ψ ⊢ c!i -pe→ c!(Suc i) ⟶ (gets_p (c!i), gets_p (c!Suc i)) ∈ rely)}" *)

(* definition comm ::
  "(('s,'f) tran) set ×
   ('s set × 's set) ⇒
   'f set ⇒
     (('s,'p,'f,'e) confs) set" where
  "comm ≡ λ(guar, (q,a)) F.
            {c. snd (last (snd c)) ∉ Fault ` F  ⟶
                (∀i.
                 Suc i<length (snd c) ⟶
                 (fst c)⊢⇩c((snd c)!i)  → ((snd c)!(Suc i)) ⟶
                   (snd((snd c)!i), snd((snd c)!(Suc i))) ∈ guar) ∧
                 (final (last (snd c))  ⟶
                    ((fst (last (snd c)) = Skip ∧
                      snd (last (snd c)) ∈ Normal ` q)) ∨
                    (fst (last (snd c)) = Throw ∧
                      snd (last (snd c)) ∈ Normal ` a))}" *)
(* commit_p_def: "commit_p Ψ ≡ λ(guar, post). {c. (∀i. Suc i<length c ⟶
               Ψ ⊢ c!i -c→ c!(Suc i) ⟶ (gets_p (c!i), gets_p (c!Suc i)) ∈ guar) ∧
               (getspc_p (last c) = None ⟶ gets_p (last c) ∈ post)}" *)

definition prog_validityI :: "('s,'p,'f,'e) Env ⇒ ('s,'p,'f,'e)com ⇒ ('s,'f) xstate set
    ⇒ (('s,'f) xstate × ('s,'f) xstate) set
    ⇒ (('s,'f) xstate × ('s,'f) xstate) set ⇒ ('s,'f) xstate set ⇒ bool"
("_ ⊨⇩I _ sat⇩p [_, _, _, _]" [60,60,0,0,0,0] 45)
where "prog_validityI Ψ P pre rely guar post ≡
   ∀s. cpts_of_pI Ψ P s ∩ assume pre rely ⊆ commit (ptranI Ψ) {Skip} guar post"

(*
lemma prog_validity_defI: "prog_validityI Ψ P pre rely guar post ≡
   ∀s. cpts_of_pI Ψ P s ∩ assume_pI Ψ (pre, rely) ⊆ commit_pI Ψ (guar, post)"
  by(simp add:prog_validityI_def)
*)

lemma CptnComp_h: "⟦Ψ⊢⇩ca → b; (Ψ,b#xs) ∈ cptn ⟧ ⟹ (Ψ,a#b#xs) ∈ cptn"
  using CptnComp by (metis prod.collapse)

lemma rgsound_pI_h:
  "(Ψ, l) ∈ cptn' ⟹
    ∀(s, t)∈rely. s ∉ range Normal ⟶ s = t ⟹
    x = l ⟹
    ∀i. Suc i < length x ⟶ (x ! i ─e→ x ! Suc i) ⟶ (gets_p (x ! i), gets_p (x ! Suc i)) ∈ rely ⟹
    (fst Ψ, l) ∈ cptn"
proof(induct l arbitrary: x)
  case Nil
  then show ?case using cptn'_not_empty' by fast
next
  case (Cons a l)
  assume p0: "⋀x. (Ψ, l) ∈ cptn' ⟹
                  ∀(s, t)∈rely. s ∉ range Normal ⟶ s = t ⟹
                  x = l ⟹
                  ∀i. Suc i < length x ⟶ (x ! i ─e→ x ! Suc i) ⟶ (gets_p (x ! i), gets_p (x ! Suc i)) ∈ rely ⟹ (fst Ψ, l) ∈ cptn"
    and p1: "(Ψ, a # l) ∈ cptn'"
    and p2: "∀(s, t)∈rely. s ∉ range Normal ⟶ s = t"
    and p4: "x = (a # l)"
    and p3: "∀i. Suc i < length x ⟶ (x ! i ─e→ x ! Suc i) ⟶ (gets_p (x ! i), gets_p (x ! Suc i)) ∈ rely"
  show ?case
    proof(cases "l = []")
      assume l: "l = []"
      thus ?thesis using CptnOne by (metis prod.collapse)
    next
      assume l_ne_empty: "l ≠ []"
      then obtain b and l' where l: "l = b # l'"
        using list.exhaust by blast

      with p1 have l_in_cptn': "(Ψ, l) ∈ cptn'" using tl_in_cptn' by blast
      from p4 have len_x_l: "length x = length (a # l)"  by simp

      from p4 len_x_l obtain y where y: "y = tl x ∧ y = l"
        by simp

      from p3 y have y_pe_rely: "∀i. Suc i < length y ⟶ (y ! i ─e→ y ! Suc i) ⟶ (gets_p (y ! i), gets_p (y ! Suc i)) ∈ rely"
        by (metis (no_types, lifting) List.nth_tl Suc_lessD Suc_mono len_x_l length_Cons)


      from y_pe_rely y l_in_cptn' p0[of y] p2 have l_in_cptn: "(fst Ψ, l) ∈ cptn" by fast

      from p1 l have "Ψ⊢⇩c⇩I a → b ∨ fst a = fst b" using ab_cptn'_c_or_eq by simp

      thus ?thesis
        proof
          assume "Ψ⊢⇩c⇩I a → b"
          with l_in_cptn l show ?thesis using CptnComp_h[of "fst Ψ" a b l'] ptranI'_def[of Ψ a b] ptranI_def[of Ψ] by simp
        next
          assume ab_spec: "fst a = fst b"
          with l p4 len_x_l have "fst (x ! 0) = fst (x ! Suc 0)" by simp
          hence "x ! 0 ─e→ x ! Suc 0" by simp
          with p3 len_x_l l have "(gets_p (x ! 0), gets_p (x ! Suc 0)) ∈ rely" by simp
          moreover
          from p4 len_x_l have "gets_p (x ! 0) = snd a"
            by (simp add: gets_p_def)
          moreover
          from l_ne_empty p4 l len_x_l have "gets_p (x ! Suc 0) = snd b"
            by (simp add: gets_p_def)
          ultimately have "fst Ψ⊢⇩c a →⇩e b"
            apply(case_tac "∀t'. snd a ≠ Normal t'")
              using Env_n[of "snd a" "fst Ψ" "fst a"] p2 ab_spec surjective_pairing[of a] surjective_pairing[of b] apply auto[1]
              using Env[of "fst Ψ" "fst a" _ "snd b"] p2 ab_spec surjective_pairing[of a] surjective_pairing[of b] apply auto[1]
            done
          thus ?thesis using CptnEnv[of "fst Ψ" "fst a" "snd a" "snd b" l'] l l_in_cptn ab_spec surjective_pairing[of a] surjective_pairing[of b]
            by auto
        qed
    qed
qed


lemma rgsound_pI[rule_format]:
  "rghoare_pI Ψ P pre rely guar post ⟶ prog_validityI Ψ P pre rely guar post"
proof
  assume "rghoare_pI Ψ P pre rely guar post"
  hence a10: "pre ⊆ range Normal ∧ post ⊆ range Normal"
    and a11: "fst Ψ,snd Ψ ⊢⇘/{}⇙ P sat [{s. Normal s ∈ pre}, rely, guar, {s. Normal s ∈ post},{}]"
    and a12: "(∀(s,t)∈rely. s ∉ Normal ` UNIV ⟶ s = t)"
    and a13: "∀(c,p,R,G,q,a)∈ snd Ψ. fst Ψ,{} ⊢⇘/{}⇙ (Call c) sat [p, R, G, q,a]" apply auto
    apply (simp add:rghoare_pI_def, fast)+ apply (simp add:rghoare_pI_def)
    apply (simp add:rghoare_pI_def) apply auto[1] apply (simp add:rghoare_pI_def) by auto
  hence a1: "fst Ψ,snd Ψ ⊨⇘/{}⇙ P sat [{s. Normal s ∈ pre},rely, guar, {s. Normal s ∈ post},{}]"
    using localRG_sound com_cnvalid_to_cvalid by fast

  from a13 have "∀(c,p,R,G,q,a)∈ snd Ψ. fst Ψ,{} ⊨⇘/{}⇙ (Call c) sat [p, R, G, q,a]" using localRG_sound
    using com_cnvalid_to_cvalid by fastforce 
  hence "∀(c,p,R,G,q,a)∈ snd Ψ. fst Ψ ⊨⇘/{}⇙ (Call c) sat [p, R, G, q,a]" 
    by (simp add: com_cvalidity_def)
  
  with a1 have "∀s. cp (fst Ψ) P s ∩ assum ({s. Normal s ∈ pre}, rely) ⊆ comm (guar, {s. Normal s ∈ post}, {}) {}"
    by (simp add:com_cvalidity_def com_validity_def localRG_sound)
  hence a2: "∀s. {(Ψ1, l). l ! 0 = (P, s) ∧ (fst Ψ, l) ∈ cptn ∧ Ψ1 = fst Ψ} ∩
               {c. snd (snd c ! 0) ∈ Normal ` {s. Normal s ∈ pre} ∧
                   (∀i. Suc i < length (snd c) ⟶
                        fst c⊢⇩c snd c ! i →⇩e snd c ! Suc i ⟶ (snd (snd c ! i), snd (snd c ! Suc i)) ∈ rely)}
               ⊆ {c. (∀i. Suc i < length (snd c) ⟶
                           fst c⊢⇩c snd c ! i → snd c ! Suc i ⟶ (snd (snd c ! i), snd (snd c ! Suc i)) ∈ guar) ∧
                      (final (last (snd c)) ⟶
                       fst (last (snd c)) = Skip ∧ snd (last (snd c)) ∈ Normal ` {s. Normal s ∈ post} ∨
                       fst (last (snd c)) = Throw ∧ snd (last (snd c)) ∈ {})}"
    by (simp add: assum_def comm_def cp_def)

  {
    fix s x
    assume b0: "x ∈ cpts_of_pI Ψ P s ∩ assume pre rely"
    hence b1: "x ! 0 = (P, s) ∧
               (∃l'. (Ψ, l') ∈ cptn' ∧ x = l')"
      by(simp add:cpts_of_pI_def cpts_pI_def)
    then obtain l where b2:
        "(Ψ, l) ∈ cptn' ∧  x = l"
      by auto
    from b0 have x_not_empty: "x ≠ []" using cpts_of_pI_emptyI  by fast
    from x_not_empty b2 have l_not_empty: "l ≠ []" by fast
    from b0 have b3: "snd(x!0) ∈ pre ∧ (∀i. Suc i < length x ⟶ (x ! i ─e→ x ! Suc i)
                        ⟶ (gets_p (x ! i), gets_p (x ! Suc i)) ∈ rely)"
    proof (auto simp add: assume_def gets_p_def cpts_of_pI_def)
      assume ‹x ∈ cpts_pI Ψ›
      with cptn_not_emptyI have ‹x ≠ []› by fast
      assume 1: ‹x ! 0 = (P, s)›
      assume ‹snd (hd x) ∈ pre›
      with hd_conv_nth[OF ‹x≠[]›] 1 show ‹s∈pre› by simp
    qed

    from b1 b2 l_not_empty x_not_empty have l0: "l ! 0 = (P, s)" by fast
    from x_not_empty b2 l0 have x0_s: "snd (x!0) = s" by simp

    from l0 a10 b3 x0_s have l0_s: "snd (l ! 0) ∈ Normal ` {s. Normal s ∈ pre}" by auto

    from b2 have len_x_l: "length x = length l" by simp

    have l_rely: "∀i. Suc i < length l ⟶
                        (fst Ψ ⊢⇩c l ! i →⇩e l ! Suc i) ⟶ (snd (l ! i), snd (l ! Suc i)) ∈ rely"
    proof -
    {
      fix i
      assume c0: "Suc i < length l"
        and  c1: "fst Ψ ⊢⇩c l ! i →⇩e l ! Suc i"
      with b2 have "x ! i ─e→ x ! Suc i"
        apply-
        apply(erule step_e.cases)
         apply simp+
        done

      with b2 c0 b3 have "(gets_p (x ! i), gets_p (x ! Suc i)) ∈ rely"
         by auto
      moreover
      have "snd (l ! i) = gets_p (x ! i)" using b2 c0  gets_p_def by metis

      moreover
      have "snd (l ! Suc i) = gets_p (x ! Suc i)" using b2 c0 gets_p_def
        by (metis (mono_tags, lifting) length_map)
      ultimately have "(snd (l ! i), snd (l ! Suc i)) ∈ rely" by simp
    }
    then show ?thesis by auto qed

    (*from b2 b3 have "∀i. Suc i < length l ⟶ Ψ⊢⇩c (l ! i) →⇩e (l ! Suc i) ⟶ (snd (l ! i), snd (l ! Suc i)) ∈ rely"
      using stepe_imp_petranI[of x l] len_x_l using l_rely by blast *)
    from a12 b2 b3 have l_in_cptn: "(fst Ψ, l) ∈ cptn" using rgsound_pI_h by blast

    from a11 b2 b3 l0 a2[rule_format, of s] l0_s l_rely have g0: "(∀i. Suc i < length (l) ⟶
                           fst Ψ⊢⇩c l ! i → l ! Suc i ⟶ (snd (l ! i), snd (l ! Suc i)) ∈ guar) ∧
                      (SmallStepCon.final (last l) ⟶
                       fst (last l) = Skip ∧ snd (last l) ∈ Normal ` {s. Normal s ∈ post} ∨
                       fst (last l) = Throw ∧ snd (last l) ∈ {})" using l_in_cptn by auto

    {
      fix i
      assume c0: "Suc i < length x"
        and  c1: "fst Ψ ⊢⇩c x!i → x!(Suc i)"
      with b2 have "fst Ψ ⊢⇩c l ! i → l ! Suc i" by simp
      moreover have "snd (l ! i) = snd (x ! i)" using b2 c0 by metis
      moreover
      have "snd (l ! Suc i) = snd (x ! Suc i)" using b2 c0 by metis
      ultimately  have "(snd (x!i), snd (x!Suc i)) ∈ guar" using g0 c0 len_x_l by auto
    }
    moreover
    {
      assume "fst (last x) = Skip"
      with b2 have c1: "fst (last l) = Skip" using cptn'_not_empty'[of Ψ l] len_x_l by fast
      moreover
      from c1 have "final (last l)" by (simp add:final_def)
      moreover
      have "snd (last l) = snd (last x)" using b2 gets_p_def
        by (simp add: case_prod_unfold l_not_empty last_map)
      ultimately have "snd (last x) ∈ post" using cptn_not_empty'[of "fst Ψ" l] using b2 g0 by auto
    }
    ultimately have "x ∈ commit (ptranI Ψ) {Skip} guar post"
      by (simp add: commit_def ptranI_def)
  }
  hence "∀s. cpts_of_pI Ψ P s ∩ assume pre rely ⊆ commit (ptranI Ψ) {Skip} guar post" by auto

  thus "prog_validityI Ψ P pre rely guar post" by (simp add:prog_validityI_def)
qed

lemma eventI: ‹event ptranI Skip›
  apply(rule event.intro)
   apply(rule none_no_tranI)
  apply(rule ptran_neqI)
  done

interpretation event ptranI Skip
  by (rule eventI)

lemma event_compI: ‹event_comp ptranI Skip›
  apply(rule event_comp.intro)
  by (rule eventI)

interpretation event_comp ptranI Skip
  by (rule event_compI)

lemma cpts_equiv:
  ‹cpts_pI Γ = cpts (ptranI Γ)›
proof
  show ‹cpts_pI Γ ⊆ cpts (ptranI Γ)›
  proof
    fix cpt
    assume ‹cpt ∈ cpts_pI Γ›
    then have ‹(Γ, cpt) ∈ cptn'› by (simp add: cpts_pI_def)
    then show ‹cpt ∈ cpts (ptranI Γ)›
    proof(induct, auto)
      fix a b P s Q t xs
      assume 1: ‹(a, b) ⊢⇩c⇩I (P, s) → (Q, t)›
      assume 2: ‹(Q, t) # xs ∈ cpts (ptranI (a, b))›
      show ‹(P, s) # (Q, t) # xs ∈ cpts (ptranI (a, b))›
        apply(rule CptsComp)
         apply(simp add: ptranI_def)
        using 1 apply(simp add: ptranI'_def ptranI_def)
        by (rule 2)
    qed
  qed
next
  show ‹cpts (ptranI Γ) ⊆ cpts_pI Γ›
  proof
    fix cpt
    assume ‹cpt ∈ cpts (ptranI Γ)›
    then show ‹cpt ∈ cpts_pI Γ›
    proof(induct)
      case (CptsOne P s)
      then show ?case
        apply(simp add: cpts_pI_def)
        by (rule CptnOne')
    next
      case (CptsEnv P t cs s)
      then show ?case
        apply(simp add: cpts_pI_def)
        by (erule CptnEnv')
    next
      case (CptsComp P s Q t cs)
      then show ?case
        apply(simp add: cpts_pI_def ptranI_def ptranI'_def)
        apply(rule CptnComp')
         apply(simp add: ptranI'_def ptranI_def)
        by assumption
    qed
  qed
qed

lemma cpts_inter_assume_equiv:
  ‹cpts_of_pI Γ P s ∩ assume pre rely = {cpt ∈ cpts (ptranI Γ). hd cpt = (P, s)} ∩ assume pre rely›
  apply(simp add: cpts_of_pI_def)
  using cpts_equiv
  by (metis (no_types, lifting) cptn_not_emptyI hd_conv_nth)

lemma prog_validity_defI':
  ‹∀s. cpts_of_pI Γ P s ∩ assume pre rely ⊆ commit (ptranI Γ) {Skip} guar post ⟹
   validity (ptranI Γ) {LanguageCon.com.Skip} P pre rely guar post›
  by (simp add: cpts_inter_assume_equiv)

interpretation event_hoare ptranI Skip prog_validityI rghoare_pI
  apply(rule event_hoare.intro)
   apply(rule event_validity.intro)
    apply(rule event_compI)
   apply(rule event_validity_axioms.intro)
   apply(simp add: prog_validityI_def)
   apply(drule prog_validity_defI')
  apply simp
  apply(rule event_hoare_axioms.intro)
  apply(erule rgsound_pI)
  done

end