author | huffman |
Sat, 22 May 2010 16:45:46 -0700 | |
changeset 37085 | b2073920448f |
parent 35174 | e15040ae75d7 |
permissions | -rw-r--r-- |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
1 |
(* Title: HOLCF/IMP/Denotational.thy |
12600 | 2 |
Author: Tobias Nipkow and Robert Sandner, TUM |
2798 | 3 |
Copyright 1996 TUM |
4 |
*) |
|
5 |
||
12431 | 6 |
header "Denotational Semantics of Commands in HOLCF" |
7 |
||
26438 | 8 |
theory Denotational imports HOLCF "../../HOL/IMP/Natural" begin |
12431 | 9 |
|
37085 | 10 |
text {* Disable conflicting syntax from HOL Map theory. *} |
11 |
||
12 |
no_syntax |
|
13 |
"_maplet" :: "['a, 'a] => maplet" ("_ /|->/ _") |
|
14 |
"_maplets" :: "['a, 'a] => maplet" ("_ /[|->]/ _") |
|
15 |
"" :: "maplet => maplets" ("_") |
|
16 |
"_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _") |
|
17 |
"_MapUpd" :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900) |
|
18 |
"_Map" :: "maplets => 'a ~=> 'b" ("(1[_])") |
|
19 |
||
12431 | 20 |
subsection "Definition" |
2798 | 21 |
|
19737 | 22 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19737
diff
changeset
|
23 |
dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where |
19737 | 24 |
"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
|
25 |
|
27362 | 26 |
primrec D :: "com => state discr -> state lift" |
27 |
where |
|
12431 | 28 |
"D(\<SKIP>) = (LAM s. Def(undiscr s))" |
27362 | 29 |
| "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))" |
30 |
| "D(c0 ; c1) = (dlift(D c1) oo (D c0))" |
|
31 |
| "D(\<IF> b \<THEN> c1 \<ELSE> c2) = |
|
12600 | 32 |
(LAM s. if b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)" |
27362 | 33 |
| "D(\<WHILE> b \<DO> c) = |
12600 | 34 |
fix\<cdot>(LAM w s. if 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
|
35 |
else Def(undiscr s))" |
2798 | 36 |
|
12431 | 37 |
subsection |
38 |
"Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL" |
|
39 |
||
12600 | 40 |
lemma dlift_Def [simp]: "dlift f\<cdot>(Def x) = f\<cdot>(Discr x)" |
41 |
by (simp add: dlift_def) |
|
42 |
||
43 |
lemma cont_dlift [iff]: "cont (%f. dlift f)" |
|
44 |
by (simp add: dlift_def) |
|
12431 | 45 |
|
12600 | 46 |
lemma dlift_is_Def [simp]: |
47 |
"(dlift f\<cdot>l = Def y) = (\<exists>x. l = Def x \<and> f\<cdot>(Discr x) = Def y)" |
|
48 |
by (simp add: dlift_def split: lift.split) |
|
12431 | 49 |
|
12600 | 50 |
lemma eval_implies_D: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t ==> D c\<cdot>(Discr s) = (Def t)" |
51 |
apply (induct set: evalc) |
|
52 |
apply simp_all |
|
53 |
apply (subst fix_eq) |
|
54 |
apply simp |
|
55 |
apply (subst fix_eq) |
|
56 |
apply simp |
|
57 |
done |
|
12431 | 58 |
|
12600 | 59 |
lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" |
60 |
apply (induct c) |
|
61 |
apply simp |
|
62 |
apply simp |
|
12431 | 63 |
apply force |
12600 | 64 |
apply (simp (no_asm)) |
12431 | 65 |
apply force |
12600 | 66 |
apply (simp (no_asm)) |
67 |
apply (rule fix_ind) |
|
68 |
apply (fast intro!: adm_lemmas adm_chfindom ax_flat) |
|
69 |
apply (simp (no_asm)) |
|
70 |
apply (simp (no_asm)) |
|
71 |
apply safe |
|
72 |
apply fast |
|
73 |
done |
|
12431 | 74 |
|
12600 | 75 |
theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)" |
76 |
by (fast elim!: D_implies_eval [rule_format] eval_implies_D) |
|
12431 | 77 |
|
2798 | 78 |
end |