(* Title: HOL/IMP/Transition.thy ID: $Id: Transition.thy,v 1.17 2005/06/17 14:13:07 haftmann Exp $ Author: Tobias Nipkow & Robert Sandner, TUM Isar Version: Gerwin Klein, 2001 Copyright 1996 TUM *) header "Transition Semantics of Commands" theory Transition imports Natural begin subsection "The transition relation" text {* We formalize the transition semantics as in \cite{Nielson}. This makes some of the rules a bit more intuitive, but also requires some more (internal) formal overhead. Since configurations that have terminated are written without a statement, the transition relation is not @{typ "((com × state) × (com × state)) set"} but instead: *} consts evalc1 :: "((com option × state) × (com option × state)) set" text {* Some syntactic sugar that we will use to hide the @{text option} part in configurations: *} syntax "_angle" :: "[com, state] => com option × state" ("<_,_>") "_angle2" :: "state => com option × state" ("<_>") syntax (xsymbols) "_angle" :: "[com, state] => com option × state" ("〈_,_〉") "_angle2" :: "state => com option × state" ("〈_〉") syntax (HTML output) "_angle" :: "[com, state] => com option × state" ("〈_,_〉") "_angle2" :: "state => com option × state" ("〈_〉") translations "〈c,s〉" == "(Some c, s)" "〈s〉" == "(None, s)" text {* More syntactic sugar for the transition relation, and its iteration. *} syntax "_evalc1" :: "[(com option×state),(com option×state)] => bool" ("_ -1-> _" [60,60] 60) "_evalcn" :: "[(com option×state),nat,(com option×state)] => bool" ("_ -_-> _" [60,60,60] 60) "_evalc*" :: "[(com option×state),(com option×state)] => bool" ("_ -*-> _" [60,60] 60) syntax (xsymbols) "_evalc1" :: "[(com option×state),(com option×state)] => bool" ("_ -->1 _" [60,60] 61) "_evalcn" :: "[(com option×state),nat,(com option×state)] => bool" ("_ -_->1 _" [60,60,60] 60) "_evalc*" :: "[(com option×state),(com option×state)] => bool" ("_ -->1* _" [60,60] 60) translations "cs -->1 cs'" == "(cs,cs') ∈ evalc1" "cs -n->1 cs'" == "(cs,cs') ∈ evalc1^n" "cs -->1* cs'" == "(cs,cs') ∈ evalc1^*" -- {* Isabelle converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"}, so we also include: *} "cs0 -->1 (c1,s1)" == "(cs0,c1,s1) ∈ evalc1" "cs0 -n->1 (c1,s1)" == "(cs0,c1,s1) ∈ evalc1^n" "cs0 -->1* (c1,s1)" == "(cs0,c1,s1) ∈ evalc1^*" text {* Now, finally, we are set to write down the rules for our small step semantics: *} inductive evalc1 intros Skip: "〈\<SKIP>, s〉 -->1 〈s〉" Assign: "〈x :== a, s〉 -->1 〈s[x \<mapsto> a s]〉" Semi1: "〈c0,s〉 -->1 〈s'〉 ==> 〈c0;c1,s〉 -->1 〈c1,s'〉" Semi2: "〈c0,s〉 -->1 〈c0',s'〉 ==> 〈c0;c1,s〉 -->1 〈c0';c1,s'〉" IfTrue: "b s ==> 〈\<IF> b \<THEN> c1 \<ELSE> c2,s〉 -->1 〈c1,s〉" IfFalse: "¬b s ==> 〈\<IF> b \<THEN> c1 \<ELSE> c2,s〉 -->1 〈c2,s〉" While: "〈\<WHILE> b \<DO> c,s〉 -->1 〈\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>,s〉" lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs" (*<*) (* fixme: move to Relation_Power.thy *) lemma rel_pow_Suc_E2 [elim!]: "[| (x, z) ∈ R ^ Suc n; !!y. [| (x, y) ∈ R; (y, z) ∈ R ^ n |] ==> P |] ==> P" by (drule rel_pow_Suc_D2) blast lemma rtrancl_imp_rel_pow: "p ∈ R^* ==> ∃n. p ∈ R^n" proof - assume "p ∈ R*" moreover obtain x y where p: "p = (x,y)" by (cases p) ultimately have "(x,y) ∈ R*" by hypsubst hence "∃n. (x,y) ∈ R^n" proof induct fix a have "(a,a) ∈ R^0" by simp thus "∃n. (a,a) ∈ R ^ n" .. next fix a b c assume "∃n. (a,b) ∈ R ^ n" then obtain n where "(a,b) ∈ R^n" .. moreover assume "(b,c) ∈ R" ultimately have "(a,c) ∈ R^(Suc n)" by auto thus "∃n. (a,c) ∈ R^n" .. qed with p show ?thesis by hypsubst qed (*>*) text {* As for the big step semantics you can read these rules in a syntax directed way: *} lemma SKIP_1: "〈\<SKIP>, s〉 -->1 y = (y = 〈s〉)" by (rule, cases set: evalc1, auto) lemma Assign_1: "〈x :== a, s〉 -->1 y = (y = 〈s[x \<mapsto> a s]〉)" by (rule, cases set: evalc1, auto) lemma Cond_1: "〈\<IF> b \<THEN> c1 \<ELSE> c2, s〉 -->1 y = ((b s --> y = 〈c1, s〉) ∧ (¬b s --> y = 〈c2, s〉))" by (rule, cases set: evalc1, auto) lemma While_1: "〈\<WHILE> b \<DO> c, s〉 -->1 y = (y = 〈\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>, s〉)" by (rule, cases set: evalc1, auto) lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1 subsection "Examples" lemma "s x = 0 ==> 〈\<WHILE> λs. s x ≠ 1 \<DO> (x:== λs. s x+1), s〉 -->1* 〈s[x \<mapsto> 1]〉" (is "_ ==> 〈?w, _〉 -->1* _") proof - let ?c = "x:== λs. s x+1" let ?if = "\<IF> λs. s x ≠ 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>" assume [simp]: "s x = 0" have "〈?w, s〉 -->1 〈?if, s〉" .. also have "〈?if, s〉 -->1 〈?c; ?w, s〉" by simp also have "〈?c; ?w, s〉 -->1 〈?w, s[x \<mapsto> 1]〉" by (rule Semi1, simp) also have "〈?w, s[x \<mapsto> 1]〉 -->1 〈?if, s[x \<mapsto> 1]〉" .. also have "〈?if, s[x \<mapsto> 1]〉 -->1 〈\<SKIP>, s[x \<mapsto> 1]〉" by (simp add: update_def) also have "〈\<SKIP>, s[x \<mapsto> 1]〉 -->1 〈s[x \<mapsto> 1]〉" .. finally show ?thesis .. qed lemma "s x = 2 ==> 〈\<WHILE> λs. s x ≠ 1 \<DO> (x:== λs. s x+1), s〉 -->1* s'" (is "_ ==> 〈?w, _〉 -->1* s'") proof - let ?c = "x:== λs. s x+1" let ?if = "\<IF> λs. s x ≠ 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>" assume [simp]: "s x = 2" note update_def [simp] have "〈?w, s〉 -->1 〈?if, s〉" .. also have "〈?if, s〉 -->1 〈?c; ?w, s〉" by simp also have "〈?c; ?w, s〉 -->1 〈?w, s[x \<mapsto> 3]〉" by (rule Semi1, simp) also have "〈?w, s[x \<mapsto> 3]〉 -->1 〈?if, s[x \<mapsto> 3]〉" .. also have "〈?if, s[x \<mapsto> 3]〉 -->1 〈?c; ?w, s[x \<mapsto> 3]〉" by simp also have "〈?c; ?w, s[x \<mapsto> 3]〉 -->1 〈?w, s[x \<mapsto> 4]〉" by (rule Semi1, simp) also have "〈?w, s[x \<mapsto> 4]〉 -->1 〈?if, s[x \<mapsto> 4]〉" .. also have "〈?if, s[x \<mapsto> 4]〉 -->1 〈?c; ?w, s[x \<mapsto> 4]〉" by simp also have "〈?c; ?w, s[x \<mapsto> 4]〉 -->1 〈?w, s[x \<mapsto> 5]〉" by (rule Semi1, simp) oops subsection "Basic properties" text {* There are no \emph{stuck} programs: *} lemma no_stuck: "∃y. 〈c,s〉 -->1 y" proof (induct c) -- "case Semi:" fix c1 c2 assume "∃y. 〈c1,s〉 -->1 y" then obtain y where "〈c1,s〉 -->1 y" .. then obtain c1' s' where "〈c1,s〉 -->1 〈s'〉 ∨ 〈c1,s〉 -->1 〈c1',s'〉" by (cases y, cases "fst y", auto) thus "∃s'. 〈c1;c2,s〉 -->1 s'" by auto next -- "case If:" fix b c1 c2 assume "∃y. 〈c1,s〉 -->1 y" and "∃y. 〈c2,s〉 -->1 y" thus "∃y. 〈\<IF> b \<THEN> c1 \<ELSE> c2, s〉 -->1 y" by (cases "b s") auto qed auto -- "the rest is trivial" text {* If a configuration does not contain a statement, the program has terminated and there is no next configuration: *} lemma stuck [elim!]: "〈s〉 -->1 y ==> P" by (auto elim: evalc1.elims) lemma evalc_None_retrancl [simp, dest!]: "〈s〉 -->1* s' ==> s' = 〈s〉" by (erule rtrancl_induct) auto (*<*) (* fixme: relpow.simps don't work *) lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp lemmas [simp del] = relpow.simps (*>*) lemma evalc1_None_0 [simp, dest!]: "〈s〉 -n->1 y = (n = 0 ∧ y = 〈s〉)" by (cases n) auto lemma SKIP_n: "〈\<SKIP>, s〉 -n->1 〈s'〉 ==> s' = s ∧ n=1" by (cases n) auto subsection "Equivalence to natural semantics (after Nielson and Nielson)" text {* We first need two lemmas about semicolon statements: decomposition and composition. *} lemma semiD: "!!c1 c2 s s''. 〈c1; c2, s〉 -n->1 〈s''〉 ==> ∃i j s'. 〈c1, s〉 -i->1 〈s'〉 ∧ 〈c2, s'〉 -j->1 〈s''〉 ∧ n = i+j" (is "PROP ?P n") proof (induct n) show "PROP ?P 0" by simp next fix n assume IH: "PROP ?P n" show "PROP ?P (Suc n)" proof - fix c1 c2 s s'' assume "〈c1; c2, s〉 -Suc n->1 〈s''〉" then obtain y where 1: "〈c1; c2, s〉 -->1 y" and n: "y -n->1 〈s''〉" by blast from 1 show "∃i j s'. 〈c1, s〉 -i->1 〈s'〉 ∧ 〈c2, s'〉 -j->1 〈s''〉 ∧ Suc n = i+j" (is "∃i j s'. ?Q i j s'") proof (cases set: evalc1) case Semi1 then obtain s' where "y = 〈c2, s'〉" and "〈c1, s〉 -->1 〈s'〉" by auto with 1 n have "?Q 1 n s'" by simp thus ?thesis by blast next case Semi2 then obtain c1' s' where y: "y = 〈c1'; c2, s'〉" and c1: "〈c1, s〉 -->1 〈c1', s'〉" by auto with n have "〈c1'; c2, s'〉 -n->1 〈s''〉" by simp with IH obtain i j s0 where c1': "〈c1',s'〉 -i->1 〈s0〉" and c2: "〈c2,s0〉 -j->1 〈s''〉" and i: "n = i+j" by fast from c1 c1' have "〈c1,s〉 -(i+1)->1 〈s0〉" by (auto intro: rel_pow_Suc_I2) with c2 i have "?Q (i+1) j s0" by simp thus ?thesis by blast qed auto -- "the remaining cases cannot occur" qed qed lemma semiI: "!!c0 s s''. 〈c0,s〉 -n->1 〈s''〉 ==> 〈c1,s''〉 -->1* 〈s'〉 ==> 〈c0; c1, s〉 -->1* 〈s'〉" proof (induct n) fix c0 s s'' assume "〈c0,s〉 -(0::nat)->1 〈s''〉" hence False by simp thus "?thesis c0 s s''" .. next fix c0 s s'' n assume c0: "〈c0,s〉 -Suc n->1 〈s''〉" assume c1: "〈c1,s''〉 -->1* 〈s'〉" assume IH: "!!c0 s s''. 〈c0,s〉 -n->1 〈s''〉 ==> 〈c1,s''〉 -->1* 〈s'〉 ==> 〈c0; c1,s〉 -->1* 〈s'〉" from c0 obtain y where 1: "〈c0,s〉 -->1 y" and n: "y -n->1 〈s''〉" by blast from 1 obtain c0' s0' where "y = 〈s0'〉 ∨ y = 〈c0', s0'〉" by (cases y, cases "fst y", auto) moreover { assume y: "y = 〈s0'〉" with n have "s'' = s0'" by simp with y 1 have "〈c0; c1,s〉 -->1 〈c1, s''〉" by blast with c1 have "〈c0; c1,s〉 -->1* 〈s'〉" by (blast intro: rtrancl_trans) } moreover { assume y: "y = 〈c0', s0'〉" with n have "〈c0', s0'〉 -n->1 〈s''〉" by blast with IH c1 have "〈c0'; c1,s0'〉 -->1* 〈s'〉" by blast moreover from y 1 have "〈c0; c1,s〉 -->1 〈c0'; c1,s0'〉" by blast hence "〈c0; c1,s〉 -->1* 〈c0'; c1,s0'〉" by blast ultimately have "〈c0; c1,s〉 -->1* 〈s'〉" by (blast intro: rtrancl_trans) } ultimately show "〈c0; c1,s〉 -->1* 〈s'〉" by blast qed text {* The easy direction of the equivalence proof: *} lemma evalc_imp_evalc1: "〈c,s〉 -->c s' ==> 〈c, s〉 -->1* 〈s'〉" proof - assume "〈c,s〉 -->c s'" thus "〈c, s〉 -->1* 〈s'〉" proof induct fix s show "〈\<SKIP>,s〉 -->1* 〈s〉" by auto next fix x a s show "〈x :== a ,s〉 -->1* 〈s[x\<mapsto>a s]〉" by auto next fix c0 c1 s s'' s' assume "〈c0,s〉 -->1* 〈s''〉" then obtain n where "〈c0,s〉 -n->1 〈s''〉" by (blast dest: rtrancl_imp_rel_pow) moreover assume "〈c1,s''〉 -->1* 〈s'〉" ultimately show "〈c0; c1,s〉 -->1* 〈s'〉" by (rule semiI) next fix s::state and b c0 c1 s' assume "b s" hence "〈\<IF> b \<THEN> c0 \<ELSE> c1,s〉 -->1 〈c0,s〉" by simp also assume "〈c0,s〉 -->1* 〈s'〉" finally show "〈\<IF> b \<THEN> c0 \<ELSE> c1,s〉 -->1* 〈s'〉" . next fix s::state and b c0 c1 s' assume "¬b s" hence "〈\<IF> b \<THEN> c0 \<ELSE> c1,s〉 -->1 〈c1,s〉" by simp also assume "〈c1,s〉 -->1* 〈s'〉" finally show "〈\<IF> b \<THEN> c0 \<ELSE> c1,s〉 -->1* 〈s'〉" . next fix b c and s::state assume b: "¬b s" let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>" have "〈\<WHILE> b \<DO> c,s〉 -->1 〈?if, s〉" by blast also have "〈?if,s〉 -->1 〈\<SKIP>, s〉" by (simp add: b) also have "〈\<SKIP>, s〉 -->1 〈s〉" by blast finally show "〈\<WHILE> b \<DO> c,s〉 -->1* 〈s〉" .. next fix b c s s'' s' let ?w = "\<WHILE> b \<DO> c" let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>" assume w: "〈?w,s''〉 -->1* 〈s'〉" assume c: "〈c,s〉 -->1* 〈s''〉" assume b: "b s" have "〈?w,s〉 -->1 〈?if, s〉" by blast also have "〈?if, s〉 -->1 〈c; ?w, s〉" by (simp add: b) also from c obtain n where "〈c,s〉 -n->1 〈s''〉" by (blast dest: rtrancl_imp_rel_pow) with w have "〈c; ?w,s〉 -->1* 〈s'〉" by - (rule semiI) finally show "〈\<WHILE> b \<DO> c,s〉 -->1* 〈s'〉" .. qed qed text {* Finally, the equivalence theorem: *} theorem evalc_equiv_evalc1: "〈c, s〉 -->c s' = 〈c,s〉 -->1* 〈s'〉" proof assume "〈c,s〉 -->c s'" show "〈c, s〉 -->1* 〈s'〉" by (rule evalc_imp_evalc1) next assume "〈c, s〉 -->1* 〈s'〉" then obtain n where "〈c, s〉 -n->1 〈s'〉" by (blast dest: rtrancl_imp_rel_pow) moreover have "!!c s s'. 〈c, s〉 -n->1 〈s'〉 ==> 〈c,s〉 -->c s'" proof (induct rule: nat_less_induct) fix n assume IH: "∀m. m < n --> (∀c s s'. 〈c, s〉 -m->1 〈s'〉 --> 〈c,s〉 -->c s')" fix c s s' assume c: "〈c, s〉 -n->1 〈s'〉" then obtain m where n: "n = Suc m" by (cases n) auto with c obtain y where c': "〈c, s〉 -->1 y" and m: "y -m->1 〈s'〉" by blast show "〈c,s〉 -->c s'" proof (cases c) case SKIP with c n show ?thesis by auto next case Assign with c n show ?thesis by auto next fix c1 c2 assume semi: "c = (c1; c2)" with c obtain i j s'' where c1: "〈c1, s〉 -i->1 〈s''〉" and c2: "〈c2, s''〉 -j->1 〈s'〉" and ij: "n = i+j" by (blast dest: semiD) from c1 c2 obtain "0 < i" and "0 < j" by (cases i, auto, cases j, auto) with ij obtain i: "i < n" and j: "j < n" by simp from c1 i IH have "〈c1,s〉 -->c s''" by blast moreover from c2 j IH have "〈c2,s''〉 -->c s'" by blast moreover note semi ultimately show "〈c,s〉 -->c s'" by blast next fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2" { assume True: "b s = True" with If c n have "〈c1,s〉 -m->1 〈s'〉" by auto with n IH have "〈c1,s〉 -->c s'" by blast with If True have "〈c,s〉 -->c s'" by simp } moreover { assume False: "b s = False" with If c n have "〈c2,s〉 -m->1 〈s'〉" by auto with n IH have "〈c2,s〉 -->c s'" by blast with If False have "〈c,s〉 -->c s'" by simp } ultimately show "〈c,s〉 -->c s'" by (cases "b s") auto next fix b c' assume w: "c = \<WHILE> b \<DO> c'" with c n have "〈\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s〉 -m->1 〈s'〉" (is "〈?if,_〉 -m->1 _") by auto with n IH have "〈\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s〉 -->c s'" by blast moreover note unfold_while [of b c'] -- {* @{thm unfold_while [of b c']} *} ultimately have "〈\<WHILE> b \<DO> c',s〉 -->c s'" by (blast dest: equivD2) with w show "〈c,s〉 -->c s'" by simp qed qed ultimately show "〈c,s〉 -->c s'" by blast qed subsection "Winskel's Proof" declare rel_pow_0_E [elim!] text {* Winskel's small step rules are a bit different \cite{Winskel}; we introduce their equivalents as derived rules: *} lemma whileFalse1 [intro]: "¬ b s ==> 〈\<WHILE> b \<DO> c,s〉 -->1* 〈s〉" (is "_ ==> 〈?w, s〉 -->1* 〈s〉") proof - assume "¬b s" have "〈?w, s〉 -->1 〈\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s〉" .. also have "〈\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s〉 -->1 〈\<SKIP>, s〉" .. also have "〈\<SKIP>, s〉 -->1 〈s〉" .. finally show "〈?w, s〉 -->1* 〈s〉" .. qed lemma whileTrue1 [intro]: "b s ==> 〈\<WHILE> b \<DO> c,s〉 -->1* 〈c;\<WHILE> b \<DO> c, s〉" (is "_ ==> 〈?w, s〉 -->1* 〈c;?w,s〉") proof - assume "b s" have "〈?w, s〉 -->1 〈\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s〉" .. also have "〈\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s〉 -->1 〈c;?w, s〉" .. finally show "〈?w, s〉 -->1* 〈c;?w,s〉" .. qed inductive_cases evalc1_SEs: "〈\<SKIP>,s〉 -->1 t" "〈x:==a,s〉 -->1 t" "〈c1;c2, s〉 -->1 t" "〈\<IF> b \<THEN> c1 \<ELSE> c2, s〉 -->1 t" "〈\<WHILE> b \<DO> c, s〉 -->1 t" inductive_cases evalc1_E: "〈\<WHILE> b \<DO> c, s〉 -->1 t" declare evalc1_SEs [elim!] lemma evalc_impl_evalc1: "〈c,s〉 -->c s1 ==> 〈c,s〉 -->1* 〈s1〉" apply (erule evalc.induct) -- SKIP apply blast -- ASSIGN apply fast -- SEMI apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI) -- IF apply (fast intro: converse_rtrancl_into_rtrancl) apply (fast intro: converse_rtrancl_into_rtrancl) -- WHILE apply fast apply (fast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI) done lemma lemma2 [rule_format (no_asm)]: "∀c d s u. 〈c;d,s〉 -n->1 〈u〉 --> (∃t m. 〈c,s〉 -->1* 〈t〉 ∧ 〈d,t〉 -m->1 〈u〉 ∧ m ≤ n)" apply (induct_tac "n") -- "case n = 0" apply fastsimp -- "induction step" apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2 elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl) done lemma evalc1_impl_evalc [rule_format (no_asm)]: "∀s t. 〈c,s〉 -->1* 〈t〉 --> 〈c,s〉 -->c t" apply (induct_tac "c") apply (safe dest!: rtrancl_imp_UN_rel_pow) -- SKIP apply (simp add: SKIP_n) -- ASSIGN apply (fastsimp elim: rel_pow_E2) -- SEMI apply (fast dest!: rel_pow_imp_rtrancl lemma2) -- IF apply (erule rel_pow_E2) apply simp apply (fast dest!: rel_pow_imp_rtrancl) -- "WHILE, induction on the length of the computation" apply (rename_tac b c s t n) apply (erule_tac P = "?X -n->1 ?Y" in rev_mp) apply (rule_tac x = "s" in spec) apply (induct_tac "n" rule: nat_less_induct) apply (intro strip) apply (erule rel_pow_E2) apply simp apply (erule evalc1_E) apply simp apply (case_tac "b x") -- WhileTrue apply (erule rel_pow_E2) apply simp apply (clarify dest!: lemma2) apply (erule allE, erule allE, erule impE, assumption) apply (erule_tac x=mb in allE, erule impE, fastsimp) apply blast -- WhileFalse apply (erule rel_pow_E2) apply simp apply (simp add: SKIP_n) done text {* proof of the equivalence of evalc and evalc1 *} lemma evalc1_eq_evalc: "(〈c, s〉 -->1* 〈t〉) = (〈c,s〉 -->c t)" apply (fast elim!: evalc1_impl_evalc evalc_impl_evalc1) done subsection "A proof without n" text {* The inductions are a bit awkward to write in this section, because @{text None} as result statement in the small step semantics doesn't have a direct counterpart in the big step semantics. Winskel's small step rule set (using the @{text "\<SKIP>"} statement to indicate termination) is better suited for this proof. *} lemma my_lemma1 [rule_format (no_asm)]: "〈c1,s1〉 -->1* 〈s2〉 ==> 〈c2,s2〉 -->1* cs3 ==> 〈c1;c2,s1〉 -->1* cs3" proof - -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *} have "〈c1,s1〉 -->1* 〈s2〉 ==> 〈c2,s2〉 -->1* cs3 --> 〈(λc. if c = None then c2 else the c; c2) (Some c1),s1〉 -->1* cs3" apply (erule converse_rtrancl_induct2) apply simp apply (rename_tac c s') apply simp apply (rule conjI) apply fast apply clarify apply (case_tac c) apply (auto intro: converse_rtrancl_into_rtrancl) done moreover assume "〈c1,s1〉 -->1* 〈s2〉" "〈c2,s2〉 -->1* cs3" ultimately show "〈c1;c2,s1〉 -->1* cs3" by simp qed lemma evalc_impl_evalc1': "〈c,s〉 -->c s1 ==> 〈c,s〉 -->1* 〈s1〉" apply (erule evalc.induct) -- SKIP apply fast -- ASSIGN apply fast -- SEMI apply (fast intro: my_lemma1) -- IF apply (fast intro: converse_rtrancl_into_rtrancl) apply (fast intro: converse_rtrancl_into_rtrancl) -- WHILE apply fast apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1) done text {* The opposite direction is based on a Coq proof done by Ranan Fraer and Yves Bertot. The following sketch is from an email by Ranan Fraer. \begin{verbatim} First we've broke it into 2 lemmas: Lemma 1 ((c,s) --> (SKIP,t)) => (<c,s> -c-> t) This is a quick one, dealing with the cases skip, assignment and while_false. Lemma 2 ((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t => <c,s> -c-> t This is proved by rule induction on the -*-> relation and the induction step makes use of a third lemma: Lemma 3 ((c,s) --> (c',s')) /\ <c',s'> -c'-> t => <c,s> -c-> t This captures the essence of the proof, as it shows that <c',s'> behaves as the continuation of <c,s> with respect to the natural semantics. The proof of Lemma 3 goes by rule induction on the --> relation, dealing with the cases sequence1, sequence2, if_true, if_false and while_true. In particular in the case (sequence1) we make use again of Lemma 1. \end{verbatim} *} inductive_cases evalc1_term_cases: "〈c,s〉 -->1 〈s'〉" lemma FB_lemma3 [rule_format]: "(c,s) -->1 (c',s') ==> c ≠ None --> (∀t. 〈if c'=None then \<SKIP> else the c',s'〉 -->c t --> 〈the c,s〉 -->c t)" apply (erule evalc1.induct) apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while]) done lemma FB_lemma2 [rule_format]: "(c,s) -->1* (c',s') ==> c ≠ None --> 〈if c' = None then \<SKIP> else the c',s'〉 -->c t --> 〈the c,s〉 -->c t" apply (erule converse_rtrancl_induct2) apply simp apply clarsimp apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3) done lemma evalc1_impl_evalc': "〈c,s〉 -->1* 〈t〉 ==> 〈c,s〉 -->c t" apply (fastsimp dest: FB_lemma2) done end
lemmas
〈SKIP,s〉 -1-> 〈s〉
〈x :== a ,s〉 -1-> 〈s[x ::= a s]〉
〈c0.0,s〉 -1-> 〈s'〉 ==> 〈c0.0; c1.0,s〉 -1-> 〈c1.0,s'〉
〈c0.0,s〉 -1-> 〈c0',s'〉 ==> 〈c0.0; c1.0,s〉 -1-> 〈c0'; c1.0,s'〉
b s ==> 〈IF b THEN c1.0 ELSE c2.0,s〉 -1-> 〈c1.0,s〉
¬ b s ==> 〈IF b THEN c1.0 ELSE c2.0,s〉 -1-> 〈c2.0,s〉
〈WHILE b DO c,s〉 -1-> 〈IF b THEN c; WHILE b DO c ELSE SKIP,s〉
lemmas
〈SKIP,s〉 -1-> 〈s〉
〈x :== a ,s〉 -1-> 〈s[x ::= a s]〉
〈c0.0,s〉 -1-> 〈s'〉 ==> 〈c0.0; c1.0,s〉 -1-> 〈c1.0,s'〉
〈c0.0,s〉 -1-> 〈c0',s'〉 ==> 〈c0.0; c1.0,s〉 -1-> 〈c0'; c1.0,s'〉
b s ==> 〈IF b THEN c1.0 ELSE c2.0,s〉 -1-> 〈c1.0,s〉
¬ b s ==> 〈IF b THEN c1.0 ELSE c2.0,s〉 -1-> 〈c2.0,s〉
〈WHILE b DO c,s〉 -1-> 〈IF b THEN c; WHILE b DO c ELSE SKIP,s〉
lemma rel_pow_Suc_E2:
[| (x, z) ∈ R ^ Suc n; !!y. [| (x, y) ∈ R; (y, z) ∈ R ^ n |] ==> P |] ==> P
lemma rtrancl_imp_rel_pow:
p ∈ R* ==> ∃n. p ∈ R ^ n
lemma SKIP_1:
〈SKIP,s〉 -1-> y = (y = 〈s〉)
lemma Assign_1:
〈x :== a ,s〉 -1-> y = (y = 〈s[x ::= a s]〉)
lemma Cond_1:
〈IF b THEN c1.0 ELSE c2.0,s〉 -1-> y = ((b s --> y = 〈c1.0,s〉) ∧ (¬ b s --> y = 〈c2.0,s〉))
lemma While_1:
〈WHILE b DO c,s〉 -1-> y = (y = 〈IF b THEN c; WHILE b DO c ELSE SKIP,s〉)
lemmas
〈SKIP,s〉 -1-> y = (y = 〈s〉)
〈x :== a ,s〉 -1-> y = (y = 〈s[x ::= a s]〉)
〈IF b THEN c1.0 ELSE c2.0,s〉 -1-> y = ((b s --> y = 〈c1.0,s〉) ∧ (¬ b s --> y = 〈c2.0,s〉))
〈WHILE b DO c,s〉 -1-> y = (y = 〈IF b THEN c; WHILE b DO c ELSE SKIP,s〉)
lemmas
〈SKIP,s〉 -1-> y = (y = 〈s〉)
〈x :== a ,s〉 -1-> y = (y = 〈s[x ::= a s]〉)
〈IF b THEN c1.0 ELSE c2.0,s〉 -1-> y = ((b s --> y = 〈c1.0,s〉) ∧ (¬ b s --> y = 〈c2.0,s〉))
〈WHILE b DO c,s〉 -1-> y = (y = 〈IF b THEN c; WHILE b DO c ELSE SKIP,s〉)
lemma
s x = 0 ==> 〈WHILE %s. s x ≠ 1 DO x :== %s. s x + 1 ,s〉 -*-> 〈s[x ::= 1]〉
lemma no_stuck:
∃y. 〈c,s〉 -1-> y
lemma stuck:
〈s〉 -1-> y ==> P
lemma evalc_None_retrancl:
〈s〉 -*-> s' ==> s' = 〈s〉
lemma rel_pow_0:
R ^ 0 = Id
lemma rel_pow_Suc_0:
R ^ Suc 0 = R
lemmas
R ^ 0 = Id
R ^ Suc n = R O R ^ n
lemmas
R ^ 0 = Id
R ^ Suc n = R O R ^ n
lemma evalc1_None_0:
〈s〉 -n-> y = (n = 0 ∧ y = 〈s〉)
lemma SKIP_n:
〈SKIP,s〉 -n-> 〈s'〉 ==> s' = s ∧ n = 1
lemma semiD:
〈c1.0; c2.0,s〉 -n-> 〈s''〉 ==> ∃i j s'. 〈c1.0,s〉 -i-> 〈s'〉 ∧ 〈c2.0,s'〉 -j-> 〈s''〉 ∧ n = i + j
lemma semiI:
[| 〈c0.0,s〉 -n-> 〈s''〉; 〈c1.0,s''〉 -*-> 〈s'〉 |] ==> 〈c0.0; c1.0,s〉 -*-> 〈s'〉
lemma evalc_imp_evalc1:
〈c,s〉 -->c s' ==> 〈c,s〉 -*-> 〈s'〉
theorem evalc_equiv_evalc1:
〈c,s〉 -->c s' = 〈c,s〉 -*-> 〈s'〉
lemma whileFalse1:
¬ b s ==> 〈WHILE b DO c,s〉 -*-> 〈s〉
lemma whileTrue1:
b s ==> 〈WHILE b DO c,s〉 -*-> 〈c; WHILE b DO c,s〉
lemmas evalc1_SEs:
[| 〈SKIP,s〉 -1-> t; t = 〈s〉 ==> P |] ==> P
[| 〈x :== a ,s〉 -1-> t; t = 〈s[x ::= a s]〉 ==> P |] ==> P
[| 〈c1.0; c2.0,s〉 -1-> t; !!s'. [| 〈c1.0,s〉 -1-> 〈s'〉; t = 〈c2.0,s'〉 |] ==> P; !!c0' s'. [| 〈c1.0,s〉 -1-> 〈c0',s'〉; t = 〈c0'; c2.0,s'〉 |] ==> P |] ==> P
[| 〈IF b THEN c1.0 ELSE c2.0,s〉 -1-> t; [| b s; t = 〈c1.0,s〉 |] ==> P; [| ¬ b s; t = 〈c2.0,s〉 |] ==> P |] ==> P
[| 〈WHILE b DO c,s〉 -1-> t; t = 〈IF b THEN c; WHILE b DO c ELSE SKIP,s〉 ==> P |] ==> P
lemmas evalc1_E:
[| 〈WHILE b DO c,s〉 -1-> t; t = 〈IF b THEN c; WHILE b DO c ELSE SKIP,s〉 ==> P |] ==> P
lemma evalc_impl_evalc1:
〈c,s〉 -->c s1.0 ==> 〈c,s〉 -*-> 〈s1.0〉
lemma lemma2:
〈c; d,s〉 -n-> 〈u〉 ==> ∃t m. 〈c,s〉 -*-> 〈t〉 ∧ 〈d,t〉 -m-> 〈u〉 ∧ m ≤ n
lemma evalc1_impl_evalc:
〈c,s〉 -*-> 〈t〉 ==> 〈c,s〉 -->c t
lemma evalc1_eq_evalc:
〈c,s〉 -*-> 〈t〉 = 〈c,s〉 -->c t
lemma my_lemma1:
[| 〈c1.0,s1.0〉 -*-> 〈s2.0〉; 〈c2.0,s2.0〉 -*-> cs3.0 |] ==> 〈c1.0; c2.0,s1.0〉 -*-> cs3.0
lemma evalc_impl_evalc1':
〈c,s〉 -->c s1.0 ==> 〈c,s〉 -*-> 〈s1.0〉
lemmas evalc1_term_cases:
[| 〈c,s〉 -1-> 〈s'〉; [| c = SKIP; s' = s |] ==> P; !!a x. [| c = x :== a ; s' = s[x ::= a s] |] ==> P |] ==> P
lemma FB_lemma3:
[| (c, s) -1-> (c', s'); c ≠ None; 〈if c' = None then SKIP else the c',s'〉 -->c t |] ==> 〈the c,s〉 -->c t
lemma FB_lemma2:
[| (c, s) -*-> (c', s'); c ≠ None; 〈if c' = None then SKIP else the c',s'〉 -->c t |] ==> 〈the c,s〉 -->c t
lemma evalc1_impl_evalc':
〈c,s〉 -*-> 〈t〉 ==> 〈c,s〉 -->c t