src/HOL/IMP/Denotation.thy
 changeset 43144 631dd866b284 parent 43143 1aeafba76f21 child 45015 fdac1e9880eb
```--- 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 @@
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)"
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```