author | nipkow |
Mon, 12 Sep 2011 07:55:43 +0200 | |
changeset 44890 | 22f665a2e91c |
parent 43143 | 1aeafba76f21 |
child 52047 | 0476162187c4 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/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 |
||
43143 | 8 |
theory Denotational imports HOLCF "~~/src/HOL/IMP/Big_Step" begin |
37085 | 9 |
|
12431 | 10 |
subsection "Definition" |
2798 | 11 |
|
19737 | 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 | 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 | 16 |
primrec D :: "com => state discr -> state lift" |
17 |
where |
|
43143 | 18 |
"D(SKIP) = (LAM s. Def(undiscr s))" |
19 |
| "D(X ::= a) = (LAM s. Def((undiscr s)(X := aval a (undiscr s))))" |
|
27362 | 20 |
| "D(c0 ; c1) = (dlift(D c1) oo (D c0))" |
43143 | 21 |
| "D(IF b THEN c1 ELSE c2) = |
22 |
(LAM s. if bval b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)" |
|
23 |
| "D(WHILE b DO c) = |
|
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 | 26 |
|
12431 | 27 |
subsection |
28 |
"Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL" |
|
29 |
||
12600 | 30 |
lemma dlift_Def [simp]: "dlift f\<cdot>(Def x) = f\<cdot>(Discr x)" |
31 |
by (simp add: dlift_def) |
|
32 |
||
33 |
lemma cont_dlift [iff]: "cont (%f. dlift f)" |
|
34 |
by (simp add: dlift_def) |
|
12431 | 35 |
|
12600 | 36 |
lemma dlift_is_Def [simp]: |
37 |
"(dlift f\<cdot>l = Def y) = (\<exists>x. l = Def x \<and> f\<cdot>(Discr x) = Def y)" |
|
38 |
by (simp add: dlift_def split: lift.split) |
|
12431 | 39 |
|
43143 | 40 |
lemma eval_implies_D: "(c,s) \<Rightarrow> t ==> D c\<cdot>(Discr s) = (Def t)" |
41 |
apply (induct rule: big_step_induct) |
|
42 |
apply (auto) |
|
43 |
apply (subst fix_eq) |
|
44 |
apply simp |
|
45 |
apply (subst fix_eq) |
|
46 |
apply simp |
|
47 |
done |
|
12431 | 48 |
|
43143 | 49 |
lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> (c,s) \<Rightarrow> t" |
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 | 53 |
apply force |
54 |
apply (simp (no_asm)) |
|
55 |
apply force |
|
56 |
apply (simp (no_asm)) |
|
57 |
apply (rule fix_ind) |
|
58 |
apply (fast intro!: adm_lemmas adm_chfindom ax_flat) |
|
59 |
apply (simp (no_asm)) |
|
60 |
apply (simp (no_asm)) |
|
61 |
apply force |
|
62 |
done |
|
12431 | 63 |
|
43143 | 64 |
theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = ((c,s) \<Rightarrow> t)" |
65 |
by (fast elim!: D_implies_eval [rule_format] eval_implies_D) |
|
12431 | 66 |
|
2798 | 67 |
end |