Theory picore_SIMP

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

section ‹Integrating the SIMP language into Picore›

theory picore_SIMP
imports "../picore/PiCore_RG_Invariant" "SIMP_plus" "../picore/PiCore_ext"
begin

abbreviation ptranI :: "'Env ⇒ ('a conf × 'a conf) set"
where "ptranI Γ ≡ ctran"

abbreviation prog_validityI :: "'Env ⇒ ('a com) option ⇒ 'a set ⇒ ('a × 'a) set ⇒ ('a × 'a) set ⇒ 'a set ⇒ bool"
where "prog_validityI Γ P ≡ prog_validity P"

abbreviation rghoare_pI :: "'Env ⇒ [('a com) option, 'a set, ('a × 'a) set, ('a × 'a) set, 'a set] ⇒ bool"
("_ ⊢⇩I _ sat⇩p [_, _, _, _]" [60,0,0,0,0] 45)
where "rghoare_pI Γ ≡ rghoare_p"

lemma none_no_tranI': "((Q, s),(P,t)) ∈ ptranI Γ ⟹ Q ≠ None"
  apply (simp) apply(rule ctran.cases)
  by simp+

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

lemma ptran_neqI: "((P, s),(P,t)) ∉ ptranI Γ"
  by (simp)

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

interpretation event ptranI None
  by(rule eventI)

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

interpretation event_comp ptranI None
  by(rule event_compI)

lemma rgsound_pI: "rghoare_pI Γ P pre rely guar post ⟹ prog_validityI Γ P pre rely guar post"
  using rgsound_p by blast

lemma cptn_equiv: ‹cptn = cpts ctran›
proof
  show ‹cptn ⊆ cpts ctran›
  proof
    fix cpt
    assume ‹cpt ∈ cptn›
    then show ‹cpt ∈ cpts ctran›
    proof(induct, auto)
      fix P s Q t xs
      assume ‹(P, s) -c→ (Q, t)›
      moreover assume ‹(Q, t) # xs ∈ cpts ctran›
      ultimately show ‹(P, s) # (Q, t) # xs ∈ cpts ctran›
        by (rule CptsComp)
    qed
  qed
next
  show ‹cpts ctran ⊆ cptn›
  proof
    fix cpt
    assume ‹cpt ∈ cpts ctran›
    then show ‹cpt ∈ cptn›
    proof(induct)
      case (CptsOne P s)
      then show ?case by (rule CptnOne)
    next
      case (CptsEnv P t cs s)
      then show ?case using CptnEnv by fast
    next
      case (CptsComp P s Q t cs)
      then show ?case
        apply -
        apply(rule CptnComp, assumption+)
        done
    qed
  qed
qed

lemma etran_equiv_aux: ‹(P,s) -e→ (Q,t) = (P,s) ─e→ (Q,t)›
  apply auto
   apply(erule etran.cases, auto)
  apply(rule Env)
  done

lemma etran_equiv: ‹c1 -e→ c2 = c1 ─e→ c2›
  using etran_equiv_aux surjective_pairing by metis

lemma cp_inter_assum_equiv: ‹cp P s ∩ assum (pre, rely) = {cpt ∈ cpts ctran. hd cpt = (P, s)} ∩ assume pre rely›
proof
  show ‹cp P s ∩ assum (pre, rely) ⊆ {cpt ∈ cpts ctran. hd cpt = (P, s)} ∩ assume pre rely›
  proof
    fix cpt
    assume ‹cpt ∈ cp P s ∩ assum (pre, rely)›
    then show ‹cpt ∈ {cpt ∈ cpts ctran. hd cpt = (P, s)} ∩ assume pre rely›
      apply(auto simp add: cp_def cptn_equiv assum_def assume_def etran_equiv)
      by (simp add: hd_conv_nth cpts_nonnil)+
  qed
next
  show ‹{cpt ∈ cpts ctran. hd cpt = (P, s)} ∩ assume pre rely ⊆ cp P s ∩ assum (pre, rely)›
  proof
    fix cpt
    assume ‹cpt ∈ {cpt ∈ cpts ctran. hd cpt = (P, s)} ∩ assume pre rely›
    then show ‹cpt ∈ cp P s ∩ assum (pre, rely)›
      apply(auto simp add: cp_def cptn_equiv assum_def assume_def etran_equiv)
      by (simp add: hd_conv_nth cpts_nonnil)+
  qed
qed

lemma comm_equiv: ‹comm (guar, post) = commit ctran {None} guar post›
  by (simp add: comm_def commit_def)

lemma prog_validity_defI: ‹⊨⇩I P sat⇩p [pre, rely, guar, post] ⟹ validity ctran {None} P pre rely guar post›
  by (simp add: prog_validity_def cp_inter_assum_equiv comm_equiv)

interpretation event_hoare ptranI None 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(erule prog_validity_defI)
  apply(rule event_hoare_axioms.intro)
  using rgsound_pI by blast

end