| author | haftmann |
| Mon, 07 Dec 2009 14:54:13 +0100 | |
| changeset 34022 | bb37c95f0b8e |
| parent 27362 | a6dc1769fdda |
| child 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 |
| 2798 | 2 |
ID: $Id$ |
| 12600 | 3 |
Author: Tobias Nipkow and Robert Sandner, TUM |
| 2798 | 4 |
Copyright 1996 TUM |
5 |
*) |
|
6 |
||
| 12431 | 7 |
header "Denotational Semantics of Commands in HOLCF" |
8 |
||
| 26438 | 9 |
theory Denotational imports HOLCF "../../HOL/IMP/Natural" begin |
| 12431 | 10 |
|
11 |
subsection "Definition" |
|
| 2798 | 12 |
|
| 19737 | 13 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19737
diff
changeset
|
14 |
dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where
|
| 19737 | 15 |
"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
|
16 |
|
| 27362 | 17 |
primrec D :: "com => state discr -> state lift" |
18 |
where |
|
| 12431 | 19 |
"D(\<SKIP>) = (LAM s. Def(undiscr s))" |
| 27362 | 20 |
| "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))" |
21 |
| "D(c0 ; c1) = (dlift(D c1) oo (D c0))" |
|
22 |
| "D(\<IF> b \<THEN> c1 \<ELSE> c2) = |
|
| 12600 | 23 |
(LAM s. if b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)" |
| 27362 | 24 |
| "D(\<WHILE> b \<DO> c) = |
| 12600 | 25 |
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
|
26 |
else Def(undiscr s))" |
| 2798 | 27 |
|
| 12431 | 28 |
subsection |
29 |
"Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL" |
|
30 |
||
| 12600 | 31 |
lemma dlift_Def [simp]: "dlift f\<cdot>(Def x) = f\<cdot>(Discr x)" |
32 |
by (simp add: dlift_def) |
|
33 |
||
34 |
lemma cont_dlift [iff]: "cont (%f. dlift f)" |
|
35 |
by (simp add: dlift_def) |
|
| 12431 | 36 |
|
| 12600 | 37 |
lemma dlift_is_Def [simp]: |
38 |
"(dlift f\<cdot>l = Def y) = (\<exists>x. l = Def x \<and> f\<cdot>(Discr x) = Def y)" |
|
39 |
by (simp add: dlift_def split: lift.split) |
|
| 12431 | 40 |
|
| 12600 | 41 |
lemma eval_implies_D: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t ==> D c\<cdot>(Discr s) = (Def t)" |
42 |
apply (induct set: evalc) |
|
43 |
apply simp_all |
|
44 |
apply (subst fix_eq) |
|
45 |
apply simp |
|
46 |
apply (subst fix_eq) |
|
47 |
apply simp |
|
48 |
done |
|
| 12431 | 49 |
|
| 12600 | 50 |
lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" |
51 |
apply (induct c) |
|
52 |
apply simp |
|
53 |
apply simp |
|
| 12431 | 54 |
apply force |
| 12600 | 55 |
apply (simp (no_asm)) |
| 12431 | 56 |
apply force |
| 12600 | 57 |
apply (simp (no_asm)) |
58 |
apply (rule fix_ind) |
|
59 |
apply (fast intro!: adm_lemmas adm_chfindom ax_flat) |
|
60 |
apply (simp (no_asm)) |
|
61 |
apply (simp (no_asm)) |
|
62 |
apply safe |
|
63 |
apply fast |
|
64 |
done |
|
| 12431 | 65 |
|
| 12600 | 66 |
theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)" |
67 |
by (fast elim!: D_implies_eval [rule_format] eval_implies_D) |
|
| 12431 | 68 |
|
| 2798 | 69 |
end |