# HG changeset patch
# User wenzelm
# Date 1009467919 -3600
# Node ID 30ec65eaaf5f1d14c3e5cff3822f3d0289d355b1
# Parent  8bc47cf91bf670bc03a1d74f643cc5efa244d57f
tuned;

diff -r 8bc47cf91bf6 -r 30ec65eaaf5f 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
diff -r 8bc47cf91bf6 -r 30ec65eaaf5f src/HOLCF/IMP/HoareEx.thy
--- a/src/HOLCF/IMP/HoareEx.thy	Thu Dec 27 16:44:43 2001 +0100
+++ b/src/HOLCF/IMP/HoareEx.thy	Thu Dec 27 16:45:19 2001 +0100
@@ -16,15 +16,16 @@
 
 types assn = "state => bool"
 
-constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
- "|= {A} c {B} == !s t. A s & D c $(Discr s) = Def t --> B t"
+constdefs
+  hoare_valid :: "[assn, com, assn] => bool"    ("|= {(1_)}/ (_)/ {(1_)}" 50)
+  "|= {A} c {B} == \<forall>s t. A s \<and> D c $(Discr s) = Def t --> B t"
 
 lemma WHILE_rule_sound:
-  "|= {A} c {A} ==> |= {A} \<WHILE> b \<DO> c {%s. A s & ~b s}"
+    "|= {A} c {A} ==> |= {A} \<WHILE> b \<DO> c {\<lambda>s. A s \<and> \<not> b s}"
   apply (unfold hoare_valid_def)
   apply (simp (no_asm))
   apply (rule fix_ind)
-    apply (simp (no_asm)) -- "simplifier with enhanced adm-tactic"
+    apply (simp (no_asm)) -- "simplifier with enhanced @{text adm}-tactic"
    apply (simp (no_asm))
   apply (simp (no_asm))
   apply blast
diff -r 8bc47cf91bf6 -r 30ec65eaaf5f src/HOLCF/IMP/ROOT.ML
--- a/src/HOLCF/IMP/ROOT.ML	Thu Dec 27 16:44:43 2001 +0100
+++ b/src/HOLCF/IMP/ROOT.ML	Thu Dec 27 16:45:19 2001 +0100
@@ -4,4 +4,6 @@
     Copyright   1997  TU Muenchen
 *)
 
-with_path "../../HOL/IMP" time_use_thy "HoareEx";
+with_path "../../HOL/IMP" (no_document time_use_thy) "Natural";
+time_use_thy "HoareEx";
+
diff -r 8bc47cf91bf6 -r 30ec65eaaf5f src/HOLCF/IMP/document/root.tex
--- a/src/HOLCF/IMP/document/root.tex	Thu Dec 27 16:44:43 2001 +0100
+++ b/src/HOLCF/IMP/document/root.tex	Thu Dec 27 16:45:19 2001 +0100
@@ -1,5 +1,6 @@
 
 \documentclass[11pt,a4paper]{article}
+\usepackage[latin1]{inputenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}