diff -r 1aeafba76f21 -r 631dd866b284 src/HOL/IMP/Denotation.thy --- 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) \ t \ (s,t) \ 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) \ C(c) \ (c,s) \ 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) \ C(c) = ((c,s) \ t)" +lemma denotational_is_big_step: "(s,t) \ C(c) = ((c,s) \ t)" by (fast elim: com2 dest: com1) end