isabelle: src/HOL/HOLCF/IMP/Denotational.thy@e7d237c2ce93 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40774 diff changeset	1	(* Title: HOL/HOLCF/IMP/Denotational.thy
12600 30ec65eaaf5f tuned; wenzelm parents: 12431 diff changeset	2	Author: Tobias Nipkow and Robert Sandner, TUM
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	3	Copyright 1996 TUM
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	4	*)
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	5
58880 0baae4311a9f modernized header; wenzelm parents: 52047 diff changeset	6	section "Denotational Semantics of Commands in HOLCF"
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	7
43143 1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	8	theory Denotational imports HOLCF "~~/src/HOL/IMP/Big_Step" begin
37085 b2073920448f disambiguate some syntax huffman parents: 35174 diff changeset	9
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	10	subsection "Definition"
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	11
19737 3b8920131be2 tuned; wenzelm parents: 16417 diff changeset	12	definition
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19737 diff changeset	13	dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where
19737 3b8920131be2 tuned; wenzelm parents: 16417 diff changeset	14	"dlift f = (LAM x. case x of UU => UU \| Def y => f\<cdot>(Discr y))"
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	15
27362 a6dc1769fdda modernized specifications; wenzelm parents: 26438 diff changeset	16	primrec D :: "com => state discr -> state lift"
a6dc1769fdda modernized specifications; wenzelm parents: 26438 diff changeset	17	where
43143 1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	18	"D(SKIP) = (LAM s. Def(undiscr s))"
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	19	\| "D(X ::= a) = (LAM s. Def((undiscr s)(X := aval a (undiscr s))))"
52047 0476162187c4 repair after bc01725d7918; wenzelm parents: 44890 diff changeset	20	\| "D(c0 ;; c1) = (dlift(D c1) oo (D c0))"
43143 1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	21	\| "D(IF b THEN c1 ELSE c2) =
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	22	(LAM s. if bval b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	23	\| "D(WHILE b DO c) =
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	24	fix\<cdot>(LAM w s. if bval b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s)
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	25	else Def(undiscr s))"
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	26
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	27	subsection
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	28	"Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL"
07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	29
12600 30ec65eaaf5f tuned; wenzelm parents: 12431 diff changeset	30	lemma dlift_Def [simp]: "dlift f\<cdot>(Def x) = f\<cdot>(Discr x)"
30ec65eaaf5f tuned; wenzelm parents: 12431 diff changeset	31	by (simp add: dlift_def)
30ec65eaaf5f tuned; wenzelm parents: 12431 diff changeset	32
30ec65eaaf5f tuned; wenzelm parents: 12431 diff changeset	33	lemma cont_dlift [iff]: "cont (%f. dlift f)"
30ec65eaaf5f tuned; wenzelm parents: 12431 diff changeset	34	by (simp add: dlift_def)
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	35
12600 30ec65eaaf5f tuned; wenzelm parents: 12431 diff changeset	36	lemma dlift_is_Def [simp]:
30ec65eaaf5f tuned; wenzelm parents: 12431 diff changeset	37	"(dlift f\<cdot>l = Def y) = (\<exists>x. l = Def x \<and> f\<cdot>(Discr x) = Def y)"
30ec65eaaf5f tuned; wenzelm parents: 12431 diff changeset	38	by (simp add: dlift_def split: lift.split)
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	39
43143 1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	40	lemma eval_implies_D: "(c,s) \<Rightarrow> t ==> D c\<cdot>(Discr s) = (Def t)"
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	41	apply (induct rule: big_step_induct)
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	42	apply (auto)
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	43	apply (subst fix_eq)
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	44	apply simp
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	45	apply (subst fix_eq)
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	46	apply simp
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	47	done
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	48
43143 1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	49	lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> (c,s) \<Rightarrow> t"
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	50	apply (induct c)
44890 22f665a2e91c new fastforce replacing fastsimp - less confusing name nipkow parents: 43143 diff changeset	51	apply fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name nipkow parents: 43143 diff changeset	52	apply fastforce
43143 1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	53	apply force
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	54	apply (simp (no_asm))
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	55	apply force
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	56	apply (simp (no_asm))
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	57	apply (rule fix_ind)
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	58	apply (fast intro!: adm_lemmas adm_chfindom ax_flat)
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	59	apply (simp (no_asm))
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	60	apply (simp (no_asm))
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	61	apply force
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	62	done
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	63
43143 1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	64	theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = ((c,s) \<Rightarrow> t)"
1aeafba76f21 Fixed denotational semantics nipkow parents: 42151 diff changeset	65	by (fast elim!: D_implies_eval [rule_format] eval_implies_D)
12431 07ec657249e5 converted to Isar kleing parents: 12338 diff changeset	66
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	67	end

author	nipkow
	Fri, 16 Jan 2015 20:06:39 +0100
changeset 59380	e7d237c2ce93
parent 58880	0baae4311a9f
child 66453	cc19f7ca2ed6
permissions	-rw-r--r--