| author | huffman |
| Sat, 04 Jun 2005 00:22:22 +0200 | |
| changeset 16222 | 613183ac1fa0 |
| parent 12600 | 30ec65eaaf5f |
| child 16417 | 9bc16273c2d4 |
| 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 |
||
9 |
theory Denotational = HOLCF + Natural: |
|
10 |
||
11 |
subsection "Definition" |
|
| 2798 | 12 |
|
|
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
13 |
constdefs |
| 12600 | 14 |
dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)"
|
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 |
|
|
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
17 |
consts D :: "com => state discr -> state lift" |
| 2798 | 18 |
|
| 5192 | 19 |
primrec |
| 12431 | 20 |
"D(\<SKIP>) = (LAM s. Def(undiscr s))" |
21 |
"D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))" |
|
|
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
22 |
"D(c0 ; c1) = (dlift(D c1) oo (D c0))" |
| 12431 | 23 |
"D(\<IF> b \<THEN> c1 \<ELSE> c2) = |
| 12600 | 24 |
(LAM s. if b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)" |
| 12431 | 25 |
"D(\<WHILE> b \<DO> c) = |
| 12600 | 26 |
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
|
27 |
else Def(undiscr s))" |
| 2798 | 28 |
|
| 12431 | 29 |
subsection |
30 |
"Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL" |
|
31 |
||
| 12600 | 32 |
lemma dlift_Def [simp]: "dlift f\<cdot>(Def x) = f\<cdot>(Discr x)" |
33 |
by (simp add: dlift_def) |
|
34 |
||
35 |
lemma cont_dlift [iff]: "cont (%f. dlift f)" |
|
36 |
by (simp add: dlift_def) |
|
| 12431 | 37 |
|
| 12600 | 38 |
lemma dlift_is_Def [simp]: |
39 |
"(dlift f\<cdot>l = Def y) = (\<exists>x. l = Def x \<and> f\<cdot>(Discr x) = Def y)" |
|
40 |
by (simp add: dlift_def split: lift.split) |
|
| 12431 | 41 |
|
| 12600 | 42 |
lemma eval_implies_D: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t ==> D c\<cdot>(Discr s) = (Def t)" |
43 |
apply (induct set: evalc) |
|
44 |
apply simp_all |
|
45 |
apply (subst fix_eq) |
|
46 |
apply simp |
|
47 |
apply (subst fix_eq) |
|
48 |
apply simp |
|
49 |
done |
|
| 12431 | 50 |
|
| 12600 | 51 |
lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" |
52 |
apply (induct c) |
|
53 |
apply simp |
|
54 |
apply simp |
|
| 12431 | 55 |
apply force |
| 12600 | 56 |
apply (simp (no_asm)) |
| 12431 | 57 |
apply force |
| 12600 | 58 |
apply (simp (no_asm)) |
59 |
apply (rule fix_ind) |
|
60 |
apply (fast intro!: adm_lemmas adm_chfindom ax_flat) |
|
61 |
apply (simp (no_asm)) |
|
62 |
apply (simp (no_asm)) |
|
63 |
apply safe |
|
64 |
apply fast |
|
65 |
done |
|
| 12431 | 66 |
|
| 12600 | 67 |
theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)" |
68 |
by (fast elim!: D_implies_eval [rule_format] eval_implies_D) |
|
| 12431 | 69 |
|
| 2798 | 70 |
end |