Theory PiCore_Semantics

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

section ‹Small-step Operational Semantics of PiCore Language›

theory PiCore_Semantics
  imports PiCore_Language
begin

subsection ‹Datatypes for Semantics›

datatype ('l,'s,'prog) act =
  Cmd |
  EvtEnt "('l,'s,'prog) event" |
  AtomEvt "('l,'s,'prog) event"

record ('l,'k,'s,'prog) actk =
  Act :: "('l,'s,'prog) act"
  K :: "'k"

abbreviation mk_actk :: "('l,'s,'prog) act ⇒ 'k ⇒ ('l,'k,'s,'prog) actk" ("_♯_" [91,91] 90)
  where "mk_actk a k ≡ ⦇Act=a, K=k⦈"

lemma actk_destruct:
  ‹a = Act a♯K a› by simp

type_synonym ('l,'k,'s,'prog) ectx = "'k ⇀ ('l,'s,'prog) event"

type_synonym ('s,'prog) pconf = "'prog × 's"

type_synonym ('s,'prog) pconfs = "('s,'prog) pconf list"

definition getspc_p :: "('s,'prog) pconf ⇒ 'prog" where
  "getspc_p conf ≡ fst conf"

definition gets_p :: "('s,'prog) pconf ⇒ 's" where
  "gets_p conf ≡ snd conf"

(*
type_synonym ('k,'s,'prog) econf = "(('s,'prog) event) × ('s × (('k,'s,'prog) ectx) )"
type_synonym ('k,'s,'prog) econfs = "('k,'s,'prog) econf list"

definition getspc_e :: "('k,'s,'prog) econf ⇒ ('s,'prog) event" where
  "getspc_e conf ≡ fst conf"

definition gets_e :: "('k,'s,'prog) econf ⇒ 's" where
  "gets_e conf ≡ fst (snd conf)"

definition getx_e :: "('k,'s,'prog) econf ⇒ ('k,'s,'prog) ectx" where
  "getx_e conf ≡ snd (snd conf)"
*)

type_synonym ('l,'k,'s,'prog) esconf = "('l,'k,'s,'prog) esys × ('s × ('l,'k,'s,'prog) ectx)"
type_synonym ('l,'k,'s,'prog) pesconf = "(('l,'k,'s,'prog) paresys) × ('s × ('l,'k,'s,'prog) ectx)"

(* 'Env: type of context, such as procedures defined in a system *)
locale event =
  fixes ptran :: "'Env ⇒ (('s,'prog) pconf × ('s,'prog) pconf) set"
  fixes fin_com :: "'prog" (* final command of imperative language, such as Skip in CSimpl and None in SIMP *)
    (*assumes EnvP: "Γ ⊢ (P, s) -pe→ (P, t)" *)
  assumes none_no_tran': "((fin_com, s),(P,t)) ∉ ptran Γ"
  assumes ptran_neq: "((P, s),(P,t)) ∉ ptran Γ"
begin

definition ptran' :: "'Env ⇒ ('s,'prog) pconf ⇒ ('s,'prog) pconf ⇒ bool"   ("_ ⊢ _ ─c→ _" [81,81] 80)
  where "Γ ⊢ P ─c→ Q ≡ (P,Q) ∈ ptran Γ"

declare ptran'_def[simp]

definition ptrans :: "'Env ⇒ ('s,'prog) pconf ⇒ ('s,'prog) pconf ⇒ bool"   ("_ ⊢ _ ─c*→ _" [81,81,81] 80)
  where "Γ ⊢ P ─c*→ Q ≡ (P,Q) ∈(ptran Γ)^*"

lemma none_no_tran: "¬(Γ ⊢ (fin_com,s) ─c→ (P,t))"
  using none_no_tran' by simp

lemma none_no_tran2: "¬(Γ ⊢ (fin_com,s) ─c→ Q)"
  using none_no_tran by (metis prod.collapse)

lemma ptran_not_none: "(Γ ⊢ (Q,s) ─c→ (P,t)) ⟹ Q ≠ fin_com"
  using none_no_tran apply simp by metis

subsection ‹Semantics of Event Systems›

abbreviation ‹fin ≡ EAnon fin_com›

inductive estran_p :: "'Env ⇒ ('l,'k,'s,'prog) esconf ⇒ ('l,'k,'s,'prog) actk ⇒ ('l,'k,'s,'prog) esconf ⇒ bool"
  ("_ ⊢ _ ─es[_]→ _" [81,81] 80)
  where
    EAnon: "⟦Γ ⊢ (P, s) ─c→ (Q, t); Q ≠ fin_com ⟧ ⟹
            Γ ⊢ (EAnon P, s,x) ─es[Cmd♯k]→ (EAnon Q, t,x)"
  | EAnon_fin: "⟦ Γ ⊢ (P, s) ─c→ (Q, t); Q = fin_com; y = x(k := None) ⟧ ⟹
            Γ ⊢ (EAnon P, s,x) ─es[Cmd♯k]→ (EAnon Q, t, y)"
  | EBasic: "⟦ P = body e; s ∈ guard e; y = x(k:=Some e) ⟧ ⟹
             Γ ⊢ (EBasic e, s,x) ─es[(EvtEnt e)♯k]→ ((EAnon P), s,y)"
  | EAtom:  "⟦ P = body e; s ∈ guard e; Γ ⊢ (P,s)─c*→(fin_com,t) ⟧ ⟹
             Γ ⊢ (EAtom e, s,x) ─es[(AtomEvt e)♯k]→ (fin, t,x)"
  | ESeq:  "⟦Γ ⊢ (es1, s,x) ─es[a]→(es1', t,y); es1' ≠ fin ⟧ ⟹
            Γ ⊢ (ESeq es1 es2, s,x) ─es[a]→ (ESeq es1' es2, t,y)"
  | ESeq_fin:  "⟦Γ ⊢ (es1, s,x) ─es[a]→(fin, t,y)⟧ ⟹
            Γ ⊢ (ESeq es1 es2, s,x) ─es[a]→ (es2, t,y)"

  | EChc1: "Γ ⊢ (es1,s,x) ─es[a]→ (es1',t,y) ⟹
            Γ ⊢ (EChc es1 es2, s,x) ─es[a]→ (es1', t,y)"
  | EChc2: "Γ ⊢ (es2,s,x) ─es[a]→ (es2',t,y) ⟹
            Γ ⊢ (EChc es1 es2, s,x) ─es[a]→ (es2', t,y)"

  | EJoin1: "Γ ⊢ (es1,s,x) ─es[a]→ (es1',t,y) ⟹
            Γ ⊢ (EJoin es1 es2, s,x) ─es[a]→ (EJoin es1' es2, t,y)"
  | EJoin2: "Γ ⊢ (es2,s,x) ─es[a]→ (es2',t,y) ⟹
            Γ ⊢ (EJoin es1 es2, s,x) ─es[a]→ (EJoin es1 es2', t,y)"
  | EJoin_fin: ‹Γ ⊢ (EJoin fin fin, s,x) ─es[Cmd♯k]→ (fin,s,x)›
  | EWhileT: "s∈b ⟹ P ≠ fin ⟹ Γ ⊢ (EWhile b P, s,x) ─es[Cmd♯k]→ (ESeq P (EWhile b P), s,x)"
  | EWhileF: "s∉b ⟹ Γ ⊢ (EWhile b P, s,x) ─es[Cmd♯k]→ (fin, s,x)"

primrec Choice_height :: "('l,'k,'s,'p) esys ⇒ nat" where
  "Choice_height (EAnon p) = 0" |
  "Choice_height (EBasic p) = 0" |
  "Choice_height (EAtom p) = 0" |
  "Choice_height (ESeq p q) = max (Choice_height p) (Choice_height q)" |
  "Choice_height (EChc p q) = Suc (max (Choice_height p) (Choice_height q))" |
  "Choice_height (EJoin p q) = max (Choice_height p) (Choice_height q)" |
  "Choice_height (EWhile _ p) = Choice_height p"

primrec Join_height :: "('l,'k,'s,'p) esys ⇒ nat" where
  "Join_height (EAnon p) = 0" |
  "Join_height (EBasic p) = 0" |
  "Join_height (EAtom p) = 0" |
  "Join_height (ESeq p q) = max (Join_height p) (Join_height q)" |
  "Join_height (EChc p q) = max (Join_height p) (Join_height q)" |
  "Join_height (EJoin p q) = Suc (max (Join_height p) (Join_height q))" |
  "Join_height (EWhile _ p) = Join_height p"

lemma chcneq_specneq: "Choice_height es1 ≠ Choice_height es2 ⟹ es1 ≠ es2"
  by auto

lemma allneq_specneq: "All_height es1 ≠ All_height es2 ⟹ es1 ≠ es2"
  by auto

inductive_cases estran_from_basic_cases: ‹Γ ⊢ (EBasic e, s) ─es[a]→ (es, t)›

lemma chc_hei_convg: "Γ ⊢ (es1,s) ─es[a]→ (es2,t) ⟹ Choice_height es1 ≥ Choice_height es2"
  apply(induct es1 arbitrary: es2 a s t; rule estran_p.cases, auto)
  by fastforce+

lemma join_hei_convg: "Γ ⊢ (es1,s) ─es[a]→ (es2,t) ⟹ Join_height es1 ≥ Join_height es2"
  apply (induct es1 arbitrary: es2 a s t; rule estran_p.cases, auto)
  by fastforce+

lemma "¬(∃es2 t a. Γ ⊢ (es1,s) ─es[a]→ (EChc es1 es2,t))"
  using chc_hei_convg by fastforce

lemma seq_neq2:
  ‹P NEXT Q ≠ Q›
proof
  assume ‹P  NEXT  Q = Q›
  then have ‹es_size (P  NEXT  Q) = es_size Q› by simp
  then show False by simp
qed

lemma join_neq1: ‹P⋈Q ≠ P› by (induct P) auto
lemma join_neq2: ‹P⋈Q ≠ Q› by (induct Q) auto

lemma spec_neq: "Γ ⊢ (es1,s,x)─es[a]→(es2,t,y) ⟹ es1 ≠ es2"
proof(induct es1 arbitrary: es2 s x t y a)
  case (EAnon x)
  then show ?case apply-
    apply(erule estran_p.cases, auto) using ptran_neq by simp+
next
  case (EBasic x)
  then show ?case using estran_p.cases by fast
next
  case (EAtom x)
  then show ?case using estran_p.cases by fast
next
  case (ESeq es11 es12)
  then show ?case apply-
    apply(erule estran_p.cases, auto)
    using seq_neq2 by blast+
next
  case (EChc es11 es12)
  then show ?case apply-
    apply(rule estran_p.cases, auto)
  proof-
    assume ‹Γ ⊢ (es11, s,x) ─es[a]→ (es11 OR es12, t,y)›
    with chc_hei_convg have ‹Choice_height (es11 OR es12) ≤ Choice_height es11› by blast
    then show False by force
  next
    assume ‹Γ ⊢ (es12, s,x) ─es[a]→ (es11 OR es12, t,y)›
    with chc_hei_convg have ‹Choice_height (es11 OR es12) ≤ Choice_height es12› by blast
    then show False by force
  qed
next
  case (EJoin es11 es12)
  then show ?case apply-
    apply(rule estran_p.cases, auto)
    using join_neq2 apply blast
    apply blast.
next
  case EWhile
  then show ?case using estran_p.cases by fast
qed

subsection ‹Semantics of Parallel Event Systems›

inductive
  pestran_p :: "'Env ⇒ ('l,'k,'s,'prog) pesconf ⇒ ('l,'k,'s,'prog) actk
                      ⇒ ('l,'k,'s,'prog) pesconf ⇒ bool"  ("_ ⊢ _ ─pes[_]→ _" [70,70] 60)
  where
    ParES: "Γ ⊢ (pes k, s,x) ─es[a♯k]→ (es', t,y) ⟹ Γ ⊢ (pes, s,x) ─pes[a♯k]→ (pes(k:=es'), t,y)"

subsection ‹Lemmas›

subsubsection ‹Programs›

lemma prog_not_eq_in_ctran_aux:
  assumes c: "Γ ⊢ (P,s) ─c→ (Q,t)"
  shows "P≠Q" using c
  using ptran_neq apply simp apply auto
  done

lemma prog_not_eq_in_ctran [simp]: "¬ Γ ⊢ (P,s) ─c→ (P,t)"
  apply clarify using ptran_neq apply simp
  done

subsubsection ‹Event systems›

lemma no_estran_to_self: ‹¬ Γ ⊢ (es, s,x) ─es[a]→ (es, t,y)›
  using spec_neq by blast

lemma no_estran_from_fin:
  ‹¬ Γ ⊢ (EAnon fin_com, s) ─es[a]→ c›
proof
  assume ‹Γ ⊢ (EAnon fin_com, s) ─es[a]→ c›
  then show False
    apply(rule estran_p.cases, auto)
    using none_no_tran by simp+
qed

lemma no_pestran_to_self: ‹¬ Γ ⊢ (Ps, S) ─pes[a]→ (Ps, T)›
proof(rule ccontr, simp)
  assume ‹Γ ⊢ (Ps, S) ─pes[a]→ (Ps, T)›
  then show False
  proof(cases)
    case ParES
    then show ?thesis using no_estran_to_self
      by (metis fun_upd_same)
  qed
qed

definition ‹estran Γ ≡ {(c,c'). ∃a. estran_p Γ c a c'}›
definition ‹pestran Γ ≡ {(c,c'). ∃a k. pestran_p Γ c (a♯k) c'}›

lemma no_estran_to_self': ‹¬((P,S),(P,T))∈estran Γ›
  apply(simp add: estran_def)
  using no_estran_to_self surjective_pairing[of S] surjective_pairing[of T] by metis

lemma no_estran_to_self'': ‹fst c1 = fst c2 ⟹ (c1,c2)∉estran Γ›
  apply(subst surjective_pairing[of c1])
  apply(subst surjective_pairing[of c2])
  using no_estran_to_self' by metis

lemma no_pestran_to_self': ‹¬((P,s),(P,t))∈pestran Γ›
  apply(simp add: pestran_def)
  using no_pestran_to_self by blast

end (* locale event *)

end