src/HOLCF/IMP/Denotational.thy

--- a/src/HOLCF/IMP/Denotational.thy	Thu Dec 27 16:44:43 2001 +0100
+++ b/src/HOLCF/IMP/Denotational.thy	Thu Dec 27 16:45:19 2001 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOLCF/IMP/Denotational.thy
     ID:         $Id$
-    Author:     Tobias Nipkow & Robert Sandner, TUM
+    Author:     Tobias Nipkow and Robert Sandner, TUM
     Copyright   1996 TUM
 *)
 
@@ -11,8 +11,8 @@
 subsection "Definition"
 
 constdefs
-   dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)"
-  "dlift f == (LAM x. case x of UU => UU | Def(y) => f$(Discr y))"
+  dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)"
+  "dlift f == (LAM x. case x of UU => UU | Def y => f\<cdot>(Discr y))"
 
 consts D :: "com => state discr -> state lift"
 
@@ -21,61 +21,50 @@
   "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))"
   "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
   "D(\<IF> b \<THEN> c1 \<ELSE> c2) =
-	(LAM s. if b(undiscr s) then (D c1)$s else (D c2)$s)"
+        (LAM s. if b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
   "D(\<WHILE> b \<DO> c) =
-	fix$(LAM w s. if b(undiscr s) then (dlift w)$((D c)$s)
+        fix\<cdot>(LAM w s. if b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s)
                       else Def(undiscr s))"
 
 subsection
   "Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL"
 
-lemma dlift_Def: "dlift f$(Def x) = f$(Discr x)"
-apply (unfold dlift_def)
-apply (simp (no_asm))
-done
-declare dlift_Def [simp]
+lemma dlift_Def [simp]: "dlift f\<cdot>(Def x) = f\<cdot>(Discr x)"
+  by (simp add: dlift_def)
+
+lemma cont_dlift [iff]: "cont (%f. dlift f)"
+  by (simp add: dlift_def)
 
-lemma cont_dlift: "cont(%f. dlift f)"
-apply (unfold dlift_def)
-apply (simp (no_asm))
-done
-declare cont_dlift [iff]
+lemma dlift_is_Def [simp]:
+    "(dlift f\<cdot>l = Def y) = (\<exists>x. l = Def x \<and> f\<cdot>(Discr x) = Def y)"
+  by (simp add: dlift_def split: lift.split)
 
-lemma dlift_is_Def: 
- "(dlift f$l = Def y) = (? x. l = Def x & f$(Discr x) = Def y)"
-apply (unfold dlift_def)
-apply (simp (no_asm) split add: lift.split)
-done
-declare dlift_is_Def [simp]
+lemma eval_implies_D: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t ==> D c\<cdot>(Discr s) = (Def t)"
+  apply (induct set: evalc)
+        apply simp_all
+   apply (subst fix_eq)
+   apply simp
+  apply (subst fix_eq)
+  apply simp
+  done
 
-lemma eval_implies_D [rule_format (no_asm)]: 
-  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t ==> D c$(Discr s) = (Def t)"
-apply (erule evalc.induct)
-      apply (simp_all (no_asm_simp))
- apply (subst fix_eq)
- apply simp
-apply (subst fix_eq)
-apply simp
-done
-
-lemma D_implies_eval [rule_format (no_asm)]: 
-  "!s t. D c$(Discr s) = (Def t) --> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-apply (induct_tac "c")
+lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+  apply (induct c)
+      apply simp
+     apply simp
     apply force
+   apply (simp (no_asm))
    apply force
-  apply force
- apply (simp (no_asm))
- apply force
-apply (simp (no_asm))
-apply (rule fix_ind)
-  apply (fast intro!: adm_lemmas adm_chfindom ax_flat)
- apply (simp (no_asm))
-apply (simp (no_asm))
-apply safe
-apply fast
-done
+  apply (simp (no_asm))
+  apply (rule fix_ind)
+    apply (fast intro!: adm_lemmas adm_chfindom ax_flat)
+   apply (simp (no_asm))
+  apply (simp (no_asm))
+  apply safe
+  apply fast
+  done
 
-lemma D_is_eval: "(D c$(Discr s) = (Def t)) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
-  by (fast elim!: D_implies_eval eval_implies_D)
+theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
+  by (fast elim!: D_implies_eval [rule_format] eval_implies_D)
 
 end