Theory CollectionSemantics

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

section "Collection Semantics"

theory CollectionSemantics
imports Semantics
begin

text "General model for small step semantics instrumented
 with an information collection mechanism:"
locale CollectionSemantics = Semantics +
 constrains
  small :: "'prog ⇒ 'state ⇒ 'state set" and
  endset :: "'state set"
 fixes
  collect :: "'prog ⇒ 'state ⇒ 'state ⇒ 'coll" and
  combine :: "'coll ⇒ 'coll ⇒ 'coll" and
  collect_id :: "'coll"
 assumes
  combine_assoc: "combine (combine c1 c2) c3 = combine c1 (combine c2 c3)" and
  collect_idl[simp]: "combine collect_id c = c" and
  collect_idr[simp]: "combine c collect_id = c"

context CollectionSemantics begin

subsection "Small-Step Collection Semantics"

definition csmall :: "'prog ⇒ 'state ⇒ ('state × 'coll) set" where
"csmall P σ ≡ { (σ', coll). σ' ∈ small P σ ∧ collect P σ σ' = coll }"

lemma small_det_csmall_det:
assumes "∀σ. small P σ = {} ∨ (∃σ'. small P σ = {σ'})"
shows "∀σ. csmall P σ = {} ∨ (∃o'. csmall P σ = {o'})"
using assms by(fastforce simp: csmall_def)

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

primrec csmall_nstep :: "'prog ⇒ 'state ⇒ nat ⇒ ('state × 'coll) set" where
csmall_nstep_base:
 "csmall_nstep P σ 0 = {(σ, collect_id)}" |
csmall_nstep_Rec:
 "csmall_nstep P σ (Suc n) =
  { (σ2, coll). ∃σ1 coll1 coll2. (σ1, coll1) ∈ csmall_nstep P σ n
                      ∧ (σ2, coll2) ∈ csmall P σ1 ∧ combine coll1 coll2 = coll }"

lemma small_nstep_csmall_nstep_equiv:
 "small_nstep P σ n
       = { σ'. ∃coll. (σ', coll) ∈ csmall_nstep P σ n }"
proof (induct n) qed(simp_all add: csmall_def)

lemma csmall_nstep_exists:
 "σ' ∈ big P σ ⟹ ∃n coll. (σ', coll) ∈ csmall_nstep P σ n ∧ σ' ∈ endset"
proof(drule bigD) qed(clarsimp simp: small_nstep_csmall_nstep_equiv)

lemma csmall_det_csmall_nstep_det:
assumes "∀σ. csmall P σ = {} ∨ (∃o'. csmall P σ = {o'})"
shows "∀σ. csmall_nstep P σ n = {} ∨ (∃o'. csmall_nstep P σ n = {o'})"
using assms
proof(induct n)
  case (Suc n) then show ?case by fastforce
qed(simp)

lemma csmall_nstep_Rec2:
 "csmall_nstep P σ (Suc n) =
  { (σ2, coll). ∃σ1 coll1 coll2. (σ1, coll1) ∈ csmall P σ
                      ∧ (σ2, coll2) ∈ csmall_nstep P σ1 n ∧ combine coll1 coll2 = coll }"
proof(induct n arbitrary: σ)
  case (Suc n)
  have right: "⋀σ' coll'. (σ', coll') ∈ csmall_nstep P σ (Suc(Suc n))
    ⟹ ∃σ1 coll1 coll2. (σ1, coll1) ∈ csmall P σ
                      ∧ (σ', coll2) ∈ csmall_nstep P σ1 (Suc n) ∧ combine coll1 coll2 = coll'"
  proof -
    fix σ' coll'
    assume "(σ', coll') ∈ csmall_nstep P σ (Suc(Suc n))"
    then obtain σ1 coll1 coll2 where Sucnstep: "(σ1, coll1) ∈ csmall_nstep P σ (Suc n)"
                        "(σ', coll2) ∈ csmall P σ1" "combine coll1 coll2 = coll'" by fastforce
    obtain σ12 coll12 coll22 where nstep: "(σ12, coll12) ∈ csmall P σ
                        ∧ (σ1, coll22) ∈ csmall_nstep P σ12 n ∧ combine coll12 coll22 = coll1"
      using Suc Sucnstep(1) by fastforce
    then show "∃σ1 coll1 coll2. (σ1, coll1) ∈ csmall P σ
                      ∧ (σ', coll2) ∈ csmall_nstep P σ1 (Suc n) ∧ combine coll1 coll2 = coll'"
     using combine_assoc[of coll12 coll22 coll2] Sucnstep by fastforce
  qed
  have left: "⋀σ' coll'. ∃σ1 coll1 coll2. (σ1, coll1) ∈ csmall P σ
                      ∧ (σ', coll2) ∈ csmall_nstep P σ1 (Suc n) ∧ combine coll1 coll2 = coll'
    ⟹ (σ', coll') ∈ csmall_nstep P σ (Suc(Suc n))"
  proof -
    fix σ' coll'
    assume "∃σ1 coll1 coll2. (σ1, coll1) ∈ csmall P σ
                      ∧ (σ', coll2) ∈ csmall_nstep P σ1 (Suc n) ∧ combine coll1 coll2 = coll'"
    then obtain σ1 coll1 coll2 where Sucnstep: "(σ1, coll1) ∈ csmall P σ"
                      "(σ', coll2) ∈ csmall_nstep P σ1 (Suc n)" "combine coll1 coll2 = coll'"
      by fastforce
    obtain σ12 coll12 coll22 where nstep: "(σ12, coll12) ∈ csmall_nstep P σ1 n
                        ∧ (σ', coll22) ∈ csmall P σ12 ∧ combine coll12 coll22 = coll2"
      using Sucnstep(2) by auto
    then show "(σ', coll') ∈ csmall_nstep P σ (Suc(Suc n))"
      using combine_assoc[of coll1 coll12 coll22] Suc Sucnstep by fastforce
  qed
  show ?case using right left by fast
qed(simp)

lemma csmall_nstep_SucD:
assumes "(σ',coll') ∈ csmall_nstep P σ (Suc n)"
shows "∃σ1 coll1. (σ1, coll1) ∈ csmall P σ
   ∧ (∃coll. coll' = combine coll1 coll ∧ (σ',coll) ∈ csmall_nstep P σ1 n)"
  using csmall_nstep_Rec2 CollectionSemantics_axioms case_prodD assms by fastforce

lemma csmall_nstep_Suc_nend: "o' ∈ csmall_nstep P σ (Suc n1) ⟹ σ ∉ endset"
  using endset_final csmall_nstep_SucD CollectionSemantics.csmall_def CollectionSemantics_axioms
  by fastforce

lemma small_to_csmall_nstep_pres:
assumes Qpres: "⋀P σ σ'. Q P σ ⟹ σ' ∈ small P σ ⟹ Q P σ'"
shows "Q P σ ⟹ (σ', coll) ∈ csmall_nstep P σ n ⟹ Q P σ'"
proof(induct n arbitrary: σ σ' coll)
  case (Suc n)
  then obtain σ1 coll1 coll2 where nstep: "(σ1, coll1) ∈ csmall_nstep P σ n
                      ∧ (σ', coll2) ∈ csmall P σ1 ∧ combine coll1 coll2 = coll" by clarsimp
  then show ?case using Suc Qpres[where P=P and σ=σ1 and σ'=σ'] by(auto simp: csmall_def)
qed(simp)

lemma csmall_to_csmall_nstep_prop:
assumes cond: "⋀P σ σ' coll. (σ', coll) ∈ csmall P σ ⟹ R P coll ⟹ Q P σ ⟹ R' P σ σ' coll"
  and Rcomb: "⋀P coll1 coll2. R P (combine coll1 coll2) = (R P coll1 ∧ R P coll2)"
  and Qpres: "⋀P σ σ'. Q P σ ⟹ σ' ∈ small P σ ⟹ Q P σ'"
  and Rtrans': "⋀P σ σ1 σ' coll1 coll2.
                        R' P σ σ1 coll1 ∧ R' P σ1 σ' coll2 ⟹ R' P σ σ' (combine coll1 coll2)"
  and base: "⋀σ. R' P σ σ collect_id"
shows "(σ', coll) ∈ csmall_nstep P σ n ⟹ R P coll ⟹ Q P σ ⟹ R' P σ σ' coll"
proof(induct n arbitrary: σ σ' coll)
  case (Suc n)
  then obtain σ1 coll1 coll2 where nstep: "(σ1, coll1) ∈ csmall_nstep P σ n
                      ∧ (σ', coll2) ∈ csmall P σ1 ∧ combine coll1 coll2 = coll" by clarsimp
  then have "Q P σ1" using small_to_csmall_nstep_pres[where Q=Q] Qpres Suc by blast
  then show ?case using nstep assms Suc by auto blast
qed(simp add: base)

lemma csmall_to_csmall_nstep_prop2:
assumes cond: "⋀P P' σ σ' coll. (σ', coll) ∈ csmall P σ
             ⟹ R P P' coll ⟹ Q σ ⟹ (σ', coll) ∈ csmall P' σ"
  and Rcomb: "⋀P P' coll1 coll2. R P P' (combine coll1 coll2) = (R P P' coll1 ∧ R P P' coll2)"
  and Qpres: "⋀P σ σ'. Q σ ⟹ σ' ∈ small P σ ⟹ Q σ'"
shows "(σ', coll) ∈ csmall_nstep P σ n ⟹ R P P' coll ⟹ Q σ ⟹ (σ', coll) ∈ csmall_nstep P' σ n"
proof(induct n arbitrary: σ σ' coll)
  case (Suc n)
  then obtain σ1 coll1 coll2 where nstep: "(σ1, coll1) ∈ csmall_nstep P σ n
                      ∧ (σ', coll2) ∈ csmall P σ1 ∧ combine coll1 coll2 = coll" by clarsimp
  then have "Q σ1" using small_to_csmall_nstep_pres[where Q="λP. Q"] Qpres Suc by blast
  then show ?case using nstep assms Suc by auto blast
qed(simp)

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

definition cbig :: "'prog ⇒ 'state ⇒ ('state × 'coll) set" where
"cbig P σ ≡
  { (σ', coll). ∃n. (σ', coll) ∈ csmall_nstep P σ n ∧ σ' ∈ endset }"

lemma cbigD:
 "⟦ (σ',coll') ∈ cbig P σ ⟧ ⟹ ∃n. (σ',coll') ∈ csmall_nstep P σ n ∧ σ' ∈ endset"
  by(simp add: cbig_def)

lemma cbigD':
 "⟦ o' ∈ cbig P σ ⟧ ⟹ ∃n. o' ∈ csmall_nstep P σ n ∧ fst o' ∈ endset"
  by(cases o', simp add: cbig_def)

lemma cbig_def2:
 "(σ', coll) ∈ cbig P σ ⟷ (∃n. (σ', coll) ∈ csmall_nstep P σ n ∧ σ' ∈ endset)"
proof(rule iffI)
  assume "(σ', coll) ∈ cbig P σ"
  then show "∃n. (σ', coll) ∈ csmall_nstep P σ n ∧ σ' ∈ endset" using bigD cbig_def by auto
next
  assume "∃n. (σ', coll) ∈ csmall_nstep P σ n ∧ σ' ∈ endset"
  then show "(σ', coll) ∈ cbig P σ" using big_def cbig_def small_nstep_csmall_nstep_equiv by auto
qed

lemma cbig_big_equiv:
 "(∃coll. (σ', coll) ∈ cbig P σ) ⟷ σ' ∈ big P σ"
proof(rule iffI)
  assume "∃coll. (σ', coll) ∈ cbig P σ"
  then show "σ' ∈ big P σ" by (auto simp: big_def cbig_def small_nstep_csmall_nstep_equiv)
next
  assume "σ' ∈ big P σ"
  then show "∃coll. (σ', coll) ∈ cbig P σ" by (fastforce simp: cbig_def dest: csmall_nstep_exists)
qed

lemma cbig_big_implies:
 "(σ', coll) ∈ cbig P σ ⟹ σ' ∈ big P σ"
using cbig_big_equiv by blast

lemma csmall_to_cbig_prop:
assumes "⋀P σ σ' coll. (σ', coll) ∈ csmall P σ ⟹ R P coll ⟹ Q P σ ⟹ R' P σ σ' coll"
  and "⋀P coll1 coll2. R P (combine coll1 coll2) = (R P coll1 ∧ R P coll2)"
  and "⋀P σ σ'. Q P σ ⟹ σ' ∈ small P σ ⟹ Q P σ'"
  and "⋀P σ σ1 σ' coll1 coll2.
                        R' P σ σ1 coll1 ∧ R' P σ1 σ' coll2 ⟹ R' P σ σ' (combine coll1 coll2)"
  and "⋀σ. R' P σ σ collect_id"
shows "(σ', coll) ∈ cbig P σ ⟹ R P coll ⟹ Q P σ ⟹ R' P σ σ' coll"
using assms csmall_to_csmall_nstep_prop[where R=R and Q=Q and R'=R' and σ=σ]
  by(auto simp: cbig_def2)

lemma csmall_to_cbig_prop2:
assumes "⋀P P' σ σ' coll. (σ', coll) ∈ csmall P σ ⟹ R P P' coll ⟹ Q σ ⟹ (σ', coll) ∈ csmall P' σ"
  and "⋀P P' coll1 coll2. R P P' (combine coll1 coll2) = (R P P' coll1 ∧ R P P' coll2)"
  and Qpres: "⋀P σ σ'. Q σ ⟹ σ' ∈ small P σ ⟹ Q σ'"
shows "(σ', coll) ∈ cbig P σ ⟹ R P P' coll ⟹ Q σ ⟹ (σ', coll) ∈ cbig P' σ"
using assms csmall_to_csmall_nstep_prop2[where R=R and Q=Q] by(auto simp: cbig_def2) blast

lemma cbig_stepD:
assumes cbig: "(σ',coll') ∈ cbig P σ" and nend: "σ ∉ endset"
shows "∃σ1 coll1. (σ1, coll1) ∈ csmall P σ
   ∧ (∃coll. coll' = combine coll1 coll ∧ (σ',coll) ∈ cbig P σ1)"
proof -
  obtain n where n: "(σ', coll') ∈ csmall_nstep P σ n" "σ' ∈ endset"
    using cbig_def2 cbig by auto
  then show ?thesis using csmall_nstep_SucD nend cbig_def2 by(cases n, simp) blast
qed

(****)

lemma csmall_nstep_det_last_eq:
assumes det: "∀σ. small P σ = {} ∨ (∃σ'. small P σ = {σ'})"
shows "⟦ (σ',coll') ∈ cbig P σ; (σ',coll') ∈ csmall_nstep P σ n; (σ',coll'') ∈ csmall_nstep P σ n' ⟧
 ⟹ n = n'"
proof(induct n arbitrary: n' σ σ' coll' coll'')
  case 0
  have "σ' = σ" using "0.prems"(2) csmall_nstep_base by blast
  then have endset: "σ ∈ endset" using "0.prems"(1) cbigD by blast
  show ?case
  proof(cases n')
    case Suc then show ?thesis using "0.prems"(3) csmall_nstep_Suc_nend endset by blast
  qed(simp)
next
  case (Suc n1)
  then have endset: "σ' ∈ endset" using Suc.prems(1) cbigD by blast
  have nend: "σ ∉ endset" using csmall_nstep_Suc_nend[OF Suc.prems(2)] by simp
  then have neq: "σ' ≠ σ" using endset by auto
  obtain σ1 coll coll1 where σ1: "(σ1,coll1) ∈ csmall P σ" "coll' = combine coll1 coll"
     "(σ',coll) ∈ csmall_nstep P σ1 n1"
    using csmall_nstep_SucD[OF Suc.prems(2)] by clarsimp
  then have cbig: "(σ',coll) ∈ cbig P σ1" using endset by(auto simp: cbig_def)
  show ?case
  proof(cases n')
    case 0 then show ?thesis using neq Suc.prems(3) using csmall_nstep_base by simp
  next
    case Suc': (Suc n1')
    then obtain σ1' coll2 coll1' where σ1': "(σ1',coll1') ∈ csmall P σ" "coll'' = combine coll1' coll2"
      "(σ',coll2) ∈ csmall_nstep P σ1' n1'"
      using csmall_nstep_SucD[where σ=σ and σ'=σ' and coll'=coll'' and n=n1'] Suc.prems(3) by blast
    then have "σ1=σ1'" using σ1 det csmall_def by auto
    then show ?thesis using Suc.hyps(1)[OF cbig σ1(3)] σ1'(3) Suc' by blast
  qed
qed

end ― ‹ CollectionSemantics ›

end