src/HOL/HOLCF/IMP/Denotational.thy
 author wenzelm Tue Sep 26 20:54:40 2017 +0200 (24 months ago) changeset 66695 91500c024c7f parent 66453 cc19f7ca2ed6 child 67613 ce654b0e6d69 permissions -rw-r--r--
tuned;
```     1 (*  Title:      HOL/HOLCF/IMP/Denotational.thy
```
```     2     Author:     Tobias Nipkow and Robert Sandner, TUM
```
```     3     Copyright   1996 TUM
```
```     4 *)
```
```     5
```
```     6 section "Denotational Semantics of Commands in HOLCF"
```
```     7
```
```     8 theory Denotational imports HOLCF "HOL-IMP.Big_Step" begin
```
```     9
```
```    10 subsection "Definition"
```
```    11
```
```    12 definition
```
```    13   dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where
```
```    14   "dlift f = (LAM x. case x of UU => UU | Def y => f\<cdot>(Discr y))"
```
```    15
```
```    16 primrec D :: "com => state discr -> state lift"
```
```    17 where
```
```    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
```
```    27 subsection
```
```    28   "Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL"
```
```    29
```
```    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)
```
```    35
```
```    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)
```
```    39
```
```    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
```
```    48
```
```    49 lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> (c,s) \<Rightarrow> t"
```
```    50 apply (induct c)
```
```    51     apply fastforce
```
```    52    apply fastforce
```
```    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
```
```    63
```
```    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)
```
```    66
```
```    67 end
```