Theory CIMP_locales

(*<*)
theory CIMP_locales
imports
 "../CIMP"
begin

(*>*)
section‹ One locale per process ›

text‹

A sketch of what we're doing in ‹ConcurrentGC›, for quicker testing.

FIXME write some lemmas that further exercise the generated thms.

›

locale P1
begin

definition com :: "(unit, string, unit, nat) com" where
  "com = ⦃''A''⦄ WHILE ((<) 0) DO ⦃''B''⦄ ⌊λs. s - 1⌋ OD"

intern_com com_def
print_theorems (* P1.com_interned, P1.loc_defs *)

locset_definition "loop = {B}"
print_theorems (* P1.loop.memb, P1.loop_def *)
thm locset_cache (* the two facts in P1.loop.memb *)

definition "assertion = atS False loop"

end

thm locset_cache (* the two facts in P1.loop.memb *)

locale P2
begin

thm locset_cache (* the two facts in P1.loop.memb *)

definition com :: "(unit, string, unit, nat) com" where
  "com = ⦃''C''⦄ WHILE ((<) 0) DO ⦃''A''⦄ ⌊Suc⌋ OD"

intern_com com_def
locset_definition "loop = {A}"
print_theorems

end

thm locset_cache (* four facts: P1.loop.memb, P2.loop.memb *)

primrec coms :: "bool ⇒ (unit, string, unit, nat) com" where
  "coms False = P1.com"
| "coms True = P2.com"

(*<*)

end
(*>*)