1(*  Title:      HOL/HOLCF/IMP/Denotational.thy
2    Author:     Tobias Nipkow and Robert Sandner, TUM
3    Copyright   1996 TUM
4*)
5
6section "Denotational Semantics of Commands in HOLCF"
7
8theory Denotational imports HOLCF "HOL-IMP.Big_Step" begin
9
10subsection "Definition"
11
12definition
13  dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where
14  "dlift f = (LAM x. case x of UU \<Rightarrow> UU | Def y \<Rightarrow> f\<cdot>(Discr y))"
15
16primrec D :: "com \<Rightarrow> state discr \<rightarrow> state lift"
17where
18  "D(SKIP) = (LAM s. Def(undiscr s))"
19| "D(X ::= a) = (LAM s. Def((undiscr s)(X := aval a (undiscr s))))"
20| "D(c0 ;; c1) = (dlift(D c1) oo (D c0))"
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)
25                      else Def(undiscr s))"
26
27subsection
28  "Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL"
29
30lemma dlift_Def [simp]: "dlift f\<cdot>(Def x) = f\<cdot>(Discr x)"
31  by (simp add: dlift_def)
32
33lemma cont_dlift [iff]: "cont (%f. dlift f)"
34  by (simp add: dlift_def)
35
36lemma 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)
39
40lemma eval_implies_D: "(c,s) \<Rightarrow> t \<Longrightarrow> D c\<cdot>(Discr s) = (Def t)"
41apply (induct rule: big_step_induct)
42      apply (auto)
43 apply (subst fix_eq)
44 apply simp
45apply (subst fix_eq)
46apply simp
47done
48
49lemma D_implies_eval: "\<forall>s t. D c\<cdot>(Discr s) = (Def t) \<longrightarrow> (c,s) \<Rightarrow> t"
50apply (induct c)
51    apply fastforce
52   apply fastforce
53  apply force
54 apply (simp (no_asm))
55 apply force
56apply (simp (no_asm))
57apply (rule fix_ind)
58  apply (fast intro!: adm_lemmas adm_chfindom ax_flat)
59 apply (simp (no_asm))
60apply (simp (no_asm))
61apply force
62done
63
64theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = ((c,s) \<Rightarrow> t)"
65by (fast elim!: D_implies_eval [rule_format] eval_implies_D)
66
67end
68