--- a/src/HOL/IMP/Denotation.thy Mon Jun 17 11:39:51 2013 -0700
+++ b/src/HOL/IMP/Denotation.thy Tue Jun 18 10:04:06 2013 +0200
@@ -6,53 +6,54 @@
type_synonym com_den = "(state \<times> state) set"
-definition
- 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})"
+definition W :: "bexp \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where
+"W b rc = (\<lambda>rw. {(s,t). if bval b s then (s,t) \<in> rc O rw else s=t})"
fun C :: "com \<Rightarrow> com_den" where
-"C SKIP = Id" |
+"C SKIP = {(s,t). s=t}" |
"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))"
-
+"C (c0;;c1) = C(c0) O C(c1)" |
+"C (IF b THEN c1 ELSE c2)
+ = {(s,t). if bval b s then (s,t) \<in> C c1 else (s,t) \<in> C c2}" |
+"C(WHILE b DO c) = lfp (W b (C c))"
-lemma Gamma_mono: "mono (Gamma b c)"
-by (unfold Gamma_def mono_def) fast
+lemma W_mono: "mono (W b r)"
+by (unfold W_def mono_def) auto
-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)
+apply (subst lfp_unfold [OF W_mono]) --{*lhs only*}
+apply (simp add: W_def)
done
text{* Equivalence of denotational and big-step semantics: *}
-lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
-apply (induction rule: big_step_induct)
-apply auto
-(* while *)
-apply (unfold Gamma_def)
-apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
-apply fast
-apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
-apply auto
-done
+lemma C_if_big_step: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
+proof (induction rule: big_step_induct)
+ case WhileFalse
+ with C_While_If show ?case by auto
+next
+ case WhileTrue
+ show ?case unfolding C_While_If using WhileTrue by auto
+qed auto
+
+abbreviation Big_step :: "com \<Rightarrow> com_den" where
+"Big_step c \<equiv> {(s,t). (c,s) \<Rightarrow> t}"
-lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
-apply (induction c arbitrary: s t)
-apply auto
-apply blast
-(* while *)
-apply (erule lfp_induct2 [OF _ Gamma_mono])
-apply (unfold Gamma_def)
-apply auto
-done
+lemma Big_step_if_C: "(s,t) \<in> C(c) \<Longrightarrow> (s,t) : Big_step c"
+proof (induction c arbitrary: s t)
+ case Seq thus ?case by fastforce
+next
+ case (While b c)
+ let ?B = "Big_step (WHILE b DO c)"
+ have "W b (C c) ?B <= ?B" using While.IH by (auto simp: W_def)
+ from lfp_lowerbound[where ?f = "W b (C c)", OF this] While.prems
+ show ?case by auto
+qed (auto split: if_splits)
-lemma denotational_is_big_step: "(s,t) \<in> C(c) = ((c,s) \<Rightarrow> t)"
-by (fast elim: com2 dest: com1)
+theorem denotational_is_big_step:
+ "(s,t) \<in> C(c) = ((c,s) \<Rightarrow> t)"
+by (metis C_if_big_step Big_step_if_C[simplified])
end