Theory Semantics

(* Title: RTS/Common/Semantics.thy *)
(* Author: Susannah Mansky, UIUC 2020 *)

section "Semantics model"

theory Semantics
imports Main
begin

text "General model for small-step semantics:"
locale Semantics =
 fixes
  small :: "'prog ⇒ 'state ⇒ 'state set" and
  endset :: "'state set"
 assumes
  endset_final: "σ ∈ endset ⟹ ∀P. small P σ = {}"

context Semantics begin

subsection "Extending @{term small} to multiple steps"

primrec small_nstep :: "'prog ⇒ 'state ⇒ nat ⇒ 'state set" where
small_nstep_base:
 "small_nstep P σ 0 = {σ}" |
small_nstep_Rec:
 "small_nstep P σ (Suc n) =
  { σ2. ∃σ1. σ1 ∈ small_nstep P σ n ∧ σ2 ∈ small P σ1 }"

lemma small_nstep_Rec2:
 "small_nstep P σ (Suc n) =
  { σ2. ∃σ1. σ1 ∈ small P σ ∧ σ2 ∈ small_nstep P σ1 n }"
proof(induct n arbitrary: σ)
  case (Suc n)
  have right: "⋀σ'. σ' ∈ small_nstep P σ (Suc(Suc n))
    ⟹ ∃σ1. σ1 ∈ small P σ ∧ σ' ∈ small_nstep P σ1 (Suc n)"
  proof -
    fix σ'
    assume "σ' ∈ small_nstep P σ (Suc(Suc n))"
    then obtain σ1 where Sucnstep: "σ1 ∈ small_nstep P σ (Suc n)" "σ' ∈ small P σ1" by fastforce
    obtain σ12 where nstep: "σ12 ∈ small P σ ∧ σ1 ∈ small_nstep P σ12 n"
      using Suc Sucnstep(1) by fastforce
    then show "∃σ1. σ1 ∈ small P σ ∧ σ' ∈ small_nstep P σ1 (Suc n)"
     using Sucnstep by fastforce
  qed
  have left: "⋀σ' . ∃σ1. σ1 ∈ small P σ ∧ σ' ∈ small_nstep P σ1 (Suc n)
    ⟹ σ' ∈ small_nstep P σ (Suc(Suc n))"
  proof -
    fix σ' 
    assume "∃σ1. σ1 ∈ small P σ ∧ σ' ∈ small_nstep P σ1 (Suc n)"
    then obtain σ1 where Sucnstep: "σ1 ∈ small P σ" "σ' ∈ small_nstep P σ1 (Suc n)"
      by fastforce
    obtain σ12 where nstep: "σ12 ∈ small_nstep P σ1 n ∧ σ' ∈ small P σ12"
      using Sucnstep(2) by auto
    then show "σ' ∈ small_nstep P σ (Suc(Suc n))" using Suc Sucnstep by fastforce
  qed
  show ?case using right left by fast
qed(simp)

lemma small_nstep_SucD:
assumes "σ' ∈ small_nstep P σ (Suc n)"
shows "∃σ1. σ1 ∈ small P σ ∧ σ' ∈ small_nstep P σ1 n"
  using small_nstep_Rec2 case_prodD assms by fastforce

lemma small_nstep_Suc_nend: "σ' ∈ small_nstep P σ (Suc n1) ⟹ σ ∉ endset"
  using endset_final small_nstep_SucD by fastforce

subsection "Extending @{term small} to a big-step semantics"

definition big :: "'prog ⇒ 'state ⇒ 'state set" where
"big P σ ≡ { σ'. ∃n. σ' ∈ small_nstep P σ n ∧ σ' ∈ endset }"

lemma bigI:
 "⟦ σ' ∈ small_nstep P σ n; σ' ∈ endset ⟧ ⟹ σ' ∈ big P σ"
by (fastforce simp add: big_def)

lemma bigD:
 "⟦ σ' ∈ big P σ ⟧ ⟹ ∃n. σ' ∈ small_nstep P σ n ∧ σ' ∈ endset"
by (simp add: big_def)

lemma big_def2:
 "σ' ∈ big P σ ⟷ (∃n. σ' ∈ small_nstep P σ n ∧ σ' ∈ endset)"
proof(rule iffI)
  assume "σ' ∈ big P σ"
  then show "∃n. σ' ∈ small_nstep P σ n ∧ σ' ∈ endset" using bigD big_def by auto
next
  assume "∃n. σ' ∈ small_nstep P σ n ∧ σ' ∈ endset"
  then show "σ' ∈ big P σ" using big_def big_def by auto
qed

lemma big_stepD:
assumes big: "σ' ∈ big P σ" and nend: "σ ∉ endset"
shows "∃σ1. σ1 ∈ small P σ ∧ σ' ∈ big P σ1"
proof -
  obtain n where n: "σ' ∈ small_nstep P σ n" "σ' ∈ endset"
    using big_def2 big by auto
  then show ?thesis using small_nstep_SucD nend big_def2 by(cases n, simp) blast
qed

(***)

lemma small_nstep_det_last_eq:
assumes det: "∀σ. small P σ = {} ∨ (∃σ'. small P σ = {σ'})"
shows "⟦ σ' ∈ big P σ; σ' ∈ small_nstep P σ n; σ' ∈ small_nstep P σ n' ⟧ ⟹ n = n'"
proof(induct n arbitrary: n' σ σ')
  case 0
  have "σ' = σ" using "0.prems"(2) small_nstep_base by blast
  then have endset: "σ ∈ endset" using "0.prems"(1) bigD by blast
  show ?case
  proof(cases n')
    case Suc then show ?thesis using "0.prems"(3) small_nstep_SucD endset_final[OF endset] by blast
  qed(simp)
next
  case (Suc n1)
  then have endset: "σ' ∈ endset" using Suc.prems(1) bigD by blast
  have nend: "σ ∉ endset" using small_nstep_Suc_nend[OF Suc.prems(2)] by simp
  then have neq: "σ' ≠ σ" using endset by auto
  obtain σ1 where σ1: "σ1 ∈ small P σ" "σ' ∈ small_nstep P σ1 n1"
    using small_nstep_SucD[OF Suc.prems(2)] by clarsimp
  then have big: "σ' ∈ big P σ1" using endset by(auto simp: big_def)
  show ?case
  proof(cases n')
    case 0 then show ?thesis using neq Suc.prems(3) using small_nstep_base by blast
  next
    case Suc': (Suc n1')
    then obtain σ1' where σ1': "σ1' ∈ small P σ" "σ' ∈ small_nstep P σ1' n1'"
      using small_nstep_SucD[where σ=σ and σ'=σ' and n=n1'] Suc.prems(3) by blast
    then have "σ1=σ1'" using σ1(1) det by auto
    then show ?thesis using Suc.hyps(1)[OF big σ1(2)] σ1'(2) Suc' by blast
  qed
qed

end ― ‹ Semantics ›


end