# HG changeset patch
# User nipkow
# Date 1371542646 -7200
# Node ID b5b510c686cb32c46433fa2446539ef2b47e8650
# Parent  167dfa940c71e81f1f20121ef77ed27ee69d222c
improved defs and proofs

diff -r 167dfa940c71 -r b5b510c686cb src/HOL/IMP/Denotation.thy
--- 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