--- a/src/HOL/IMP/Denotation.thy Wed Jun 01 22:42:37 2011 +0200
+++ b/src/HOL/IMP/Denotation.thy Wed Jun 01 22:47:26 2011 +0200
@@ -20,8 +20,6 @@
"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
@@ -31,10 +29,9 @@
apply (simp add: Gamma_def)
done
-(* Operational Semantics implies Denotational Semantics *)
+text{* Equivalence of denotational and big-step semantics: *}
lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
-(* start with rule induction *)
apply (induct rule: big_step_induct)
apply auto
(* while *)
@@ -45,8 +42,6 @@
apply auto
done
-(* Denotational Semantics implies Operational Semantics *)
-
lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
apply (induct c arbitrary: s t)
apply auto
@@ -57,10 +52,7 @@
apply auto
done
-
-(**** Proof of Equivalence ****)
-
-lemma denotational_is_natural: "(s,t) \<in> C(c) = ((c,s) \<Rightarrow> t)"
+lemma denotational_is_big_step: "(s,t) \<in> C(c) = ((c,s) \<Rightarrow> t)"
by (fast elim: com2 dest: com1)
end