isabelle: src/HOL/HOLCF/IOA/Storage/Spec.thy@982e7128ce0f (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40945 diff changeset	1	(* Title: HOL/HOLCF/IOA/Storage/Spec.thy
40945 b8703f63bfb2 recoded latin1 as utf8; wenzelm parents: 40774 diff changeset	2	Author: Olaf Müller
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	3	*)
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	4
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 61032 diff changeset	5	section \<open>The specification of a memory\<close>
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	6
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	theory Spec
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 62009 diff changeset	8	imports IOA.IOA Action
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	10
27361 24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	11	definition
24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	12	spec_sig :: "action signature" where
67613 ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	13	"spec_sig = (\<Union>l.{Free l} \<union> {New},
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	14	\<Union>l.{Loc l},
27361 24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	15	{})"
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	16
27361 24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	17	definition
67613 ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	18	spec_trans :: "(action, nat set \<times> bool)transition set" where
27361 24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	19	"spec_trans =
24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	20	{tr. let s = fst(tr); used = fst s; c = snd s;
24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	21	t = snd(snd(tr)); used' = fst t; c' = snd t
24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	22	in
24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	23	case fst(snd(tr))
24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	24	of
67613 ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	25	New \<Rightarrow> used' = used \<and> c' \|
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	26	Loc l \<Rightarrow> c \<and> l \<notin> used \<and> used'= used \<union> {l} \<and> \<not>c' \|
ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	27	Free l \<Rightarrow> used'=used - {l} \<and> c'=c}"
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	28
27361 24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	29	definition
67613 ce654b0e6d69 more symbols; wenzelm parents: 66453 diff changeset	30	spec_ioa :: "(action, nat set \<times> bool)ioa" where
27361 24ec32bee347 modernized specifications; wenzelm parents: 19740 diff changeset	31	"spec_ioa = (spec_sig, {({},False)}, spec_trans,{},{})"
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	32
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	33	end

author	paulson <lp15@cam.ac.uk>
	Fri, 04 Jul 2025 15:08:09 +0100
changeset 82803	982e7128ce0f
parent 67613	ce654b0e6d69
permissions	-rw-r--r--