--- 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
--- 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)
--- 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
--- 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",