# HG changeset patch
# User nipkow
# Date 1306960957 -7200
# Node ID 1aeafba76f21dfb81fc3ece76f53ee2ed214acd1
# Parent  2a05c1f7c08c18ce2c383405c021f8c70b410b76
Fixed denotational semantics

diff -r 2a05c1f7c08c -r 1aeafba76f21 src/HOL/HOLCF/IMP/Denotational.thy
--- a/src/HOL/HOLCF/IMP/Denotational.thy	Wed Jun 01 21:50:49 2011 +0200
+++ b/src/HOL/HOLCF/IMP/Denotational.thy	Wed Jun 01 22:42:37 2011 +0200
@@ -5,17 +5,7 @@
 
 header "Denotational Semantics of Commands in HOLCF"
 
-theory Denotational imports HOLCF "~~/src/HOL/IMP/Natural" begin
-
-text {* Disable conflicting syntax from HOL Map theory. *}
-
-no_syntax
-  "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
-  "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
-  ""         :: "maplet => maplets"             ("_")
-  "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
-  "_MapUpd"  :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
-  "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
+theory Denotational imports HOLCF "~~/src/HOL/IMP/Big_Step" begin
 
 subsection "Definition"
 
@@ -25,13 +15,13 @@
 
 primrec D :: "com => state discr -> state lift"
 where
-  "D(\<SKIP>) = (LAM s. Def(undiscr s))"
-| "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))"
+  "D(SKIP) = (LAM s. Def(undiscr s))"
+| "D(X ::= a) = (LAM s. Def((undiscr s)(X := aval 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)\<cdot>s else (D c2)\<cdot>s)"
-| "D(\<WHILE> b \<DO> c) =
-        fix\<cdot>(LAM w s. if b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s)
+| "D(IF b THEN c1 ELSE c2) =
+        (LAM s. if bval b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
+| "D(WHILE b DO c) =
+        fix\<cdot>(LAM w s. if bval b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s)
                       else Def(undiscr s))"
 
 subsection
@@ -47,32 +37,31 @@
     "(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 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: "(c,s) \<Rightarrow> t ==> D c\<cdot>(Discr s) = (Def t)"
+apply (induct rule: big_step_induct)
+      apply (auto)
+ apply (subst fix_eq)
+ apply simp
+apply (subst fix_eq)
+apply simp
+done
 
-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 (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_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> (c,s) \<Rightarrow> t"
+apply (induct c)
+    apply fastsimp
+   apply fastsimp
+  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 force
+done
 
-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)
+theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = ((c,s) \<Rightarrow> t)"
+by (fast elim!: D_implies_eval [rule_format] eval_implies_D)
 
 end
diff -r 2a05c1f7c08c -r 1aeafba76f21 src/HOL/HOLCF/IMP/HoareEx.thy
--- a/src/HOL/HOLCF/IMP/HoareEx.thy	Wed Jun 01 21:50:49 2011 +0200
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Wed Jun 01 22:42:37 2011 +0200
@@ -8,7 +8,7 @@
 theory HoareEx imports Denotational begin
 
 text {*
-  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
+  An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch
   \cite{MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
   the correctness of the Hoare rule for while-loops.
 *}
@@ -17,10 +17,10 @@
 
 definition
   hoare_valid :: "[assn, com, assn] => bool"  ("|= {(1_)}/ (_)/ {(1_)}" 50) where
-  "|= {A} c {B} = (\<forall>s t. A s \<and> D c $(Discr s) = Def t --> B t)"
+  "|= {P} c {Q} = (\<forall>s t. P s \<and> D c $(Discr s) = Def t --> Q t)"
 
 lemma WHILE_rule_sound:
-    "|= {A} c {A} ==> |= {A} \<WHILE> b \<DO> c {\<lambda>s. A s \<and> \<not> b s}"
+    "|= {A} c {A} ==> |= {A} WHILE b DO c {\<lambda>s. A s \<and> \<not> bval b s}"
   apply (unfold hoare_valid_def)
   apply (simp (no_asm))
   apply (rule fix_ind)
diff -r 2a05c1f7c08c -r 1aeafba76f21 src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Wed Jun 01 21:50:49 2011 +0200
+++ b/src/HOL/IMP/Denotation.thy	Wed Jun 01 22:42:37 2011 +0200
@@ -1,34 +1,31 @@
-(*  Title:      HOL/IMP/Denotation.thy
-    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
-*)
+(* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *)
 
 header "Denotational Semantics of Commands"
 
-theory Denotation imports Natural begin
+theory Denotation imports Big_Step begin
 
 type_synonym com_den = "(state \<times> state) set"
 
 definition
-  Gamma :: "[bexp,com_den] => (com_den => com_den)" where
-  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> b s} \<union>
-                       {(s,t). s=t \<and> \<not>b s})"
+  Gamma :: "bexp \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where
+  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> bval b s} \<union>
+                       {(s,t). s=t \<and> \<not>bval b s})"
 
-primrec C :: "com => com_den"
-where
-  C_skip:   "C \<SKIP>   = Id"
-| C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
-| C_comp:   "C (c0;c1)   = C(c0) O C(c1)"
-| C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
-                                                {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
-| C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
+fun C :: "com \<Rightarrow> com_den" where
+"C SKIP   = Id" |
+"C (x ::= a) = {(s,t). t = s(x := aval a s)}" |
+"C (c0;c1)   = C(c0) O C(c1)" |
+"C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union>
+                            {(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" |
+"C(WHILE b DO c) = lfp (Gamma b (C c))"
 
 
 (**** mono (Gamma(b,c)) ****)
 
 lemma Gamma_mono: "mono (Gamma b c)"
-  by (unfold Gamma_def mono_def) fast
+by (unfold Gamma_def mono_def) fast
 
-lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
+lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"
 apply simp
 apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}
 apply (simp add: Gamma_def)
@@ -36,9 +33,9 @@
 
 (* Operational Semantics implies Denotational Semantics *)
 
-lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
+lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
 (* start with rule induction *)
-apply (induct set: evalc)
+apply (induct rule: big_step_induct)
 apply auto
 (* while *)
 apply (unfold Gamma_def)
@@ -50,11 +47,10 @@
 
 (* Denotational Semantics implies Operational Semantics *)
 
-lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
 apply (induct c arbitrary: s t)
 apply auto 
 apply blast
-
 (* while *)
 apply (erule lfp_induct2 [OF _ Gamma_mono])
 apply (unfold Gamma_def)
@@ -64,7 +60,7 @@
 
 (**** Proof of Equivalence ****)
 
-lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
-  by (fast elim: com2 dest: com1)
+lemma denotational_is_natural: "(s,t) \<in> C(c)  =  ((c,s) \<Rightarrow> t)"
+by (fast elim: com2 dest: com1)
 
 end
diff -r 2a05c1f7c08c -r 1aeafba76f21 src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Wed Jun 01 21:50:49 2011 +0200
+++ b/src/HOL/IMP/ROOT.ML	Wed Jun 01 22:42:37 2011 +0200
@@ -2,6 +2,7 @@
 ["BExp",
  "ASM",
  "Small_Step",
+ "Denotation",
  "Compiler"(*,
  "Poly_Types",
  "Sec_Typing",