equal
deleted
inserted
replaced
32 lemma Gamma_mono: "mono (Gamma b c)" |
32 lemma Gamma_mono: "mono (Gamma b c)" |
33 by (unfold Gamma_def mono_def) fast |
33 by (unfold Gamma_def mono_def) fast |
34 |
34 |
35 lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)" |
35 lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)" |
36 apply (simp (no_asm)) |
36 apply (simp (no_asm)) |
37 apply (subst lfp_unfold [OF Gamma_mono]) back back |
37 apply (subst lfp_unfold [OF Gamma_mono]) --{*lhs only*} |
38 apply (subst Gamma_def [THEN meta_eq_to_obj_eq, THEN fun_cong]) |
38 apply (simp add: Gamma_def) |
39 apply simp |
|
40 done |
39 done |
41 |
40 |
42 (* Operational Semantics implies Denotational Semantics *) |
41 (* Operational Semantics implies Denotational Semantics *) |
43 |
42 |
44 lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)" |
43 lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)" |
45 |
|
46 (* start with rule induction *) |
44 (* start with rule induction *) |
47 apply (erule evalc.induct) |
45 apply (erule evalc.induct) |
48 apply auto |
46 apply auto |
49 (* while *) |
47 (* while *) |
50 apply (unfold Gamma_def) |
48 apply (unfold Gamma_def) |