--- a/src/HOL/IMP/Transition.thy Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,644 +0,0 @@
-(* Title: HOL/IMP/Transition.thy
- 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 \<times> state) \<times> (com \<times> state)) set"}
- but instead:
- @{typ "((com option \<times> state) \<times> (com option \<times> state)) set"}
-
- Some syntactic sugar that we will use to hide the
- @{text option} part in configurations:
-*}
-abbreviation
- angle :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>") where
- "<c,s> == (Some c, s)"
-abbreviation
- angle2 :: "state \<Rightarrow> com option \<times> state" ("<_>") where
- "<s> == (None, s)"
-
-notation (xsymbols)
- angle ("\<langle>_,_\<rangle>") and
- angle2 ("\<langle>_\<rangle>")
-
-notation (HTML output)
- angle ("\<langle>_,_\<rangle>") and
- angle2 ("\<langle>_\<rangle>")
-
-text {*
- Now, finally, we are set to write down the rules for our small step semantics:
-*}
-inductive_set
- evalc1 :: "((com option \<times> state) \<times> (com option \<times> state)) set"
- and evalc1' :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
- ("_ \<longrightarrow>\<^sub>1 _" [60,60] 61)
-where
- "cs \<longrightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1"
-| Skip: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"
-| Assign: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> a s]\<rangle>"
-
-| Semi1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s'\<rangle>"
-| Semi2: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0',s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0';c1,s'\<rangle>"
-
-| IfTrue: "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>"
-| IfFalse: "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c2,s\<rangle>"
-
-| While: "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>,s\<rangle>"
-
-lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs"
-
-text {*
- More syntactic sugar for the transition relation, and its
- iteration.
-*}
-abbreviation
- evalcn :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
- ("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60) where
- "cs -n\<rightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1^^n"
-
-abbreviation
- evalc' :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
- ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [60,60] 60) where
- "cs \<longrightarrow>\<^sub>1\<^sup>* cs' == (cs,cs') \<in> evalc1^*"
-
-(*<*)
-declare rel_pow_Suc_E2 [elim!]
-(*>*)
-
-text {*
- As for the big step semantics you can read these rules in a
- syntax directed way:
-*}
-lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)"
- by (induct y, rule, cases set: evalc1, auto)
-
-lemma Assign_1: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s[x \<mapsto> a s]\<rangle>)"
- by (induct y, rule, cases set: evalc1, auto)
-
-lemma Cond_1:
- "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y = ((b s \<longrightarrow> y = \<langle>c1, s\<rangle>) \<and> (\<not>b s \<longrightarrow> y = \<langle>c2, s\<rangle>))"
- by (induct y, rule, cases set: evalc1, auto)
-
-lemma While_1:
- "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>, s\<rangle>)"
- by (induct y, rule, cases set: evalc1, auto)
-
-lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1
-
-
-subsection "Examples"
-
-lemma
- "s x = 0 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x \<mapsto> 1]\<rangle>"
- (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _")
-proof -
- let ?c = "x:== \<lambda>s. s x+1"
- let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
- assume [simp]: "s x = 0"
- have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" ..
- also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
- also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1) simp
- also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" ..
- also have "\<langle>?if, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle>" by (simp add: update_def)
- also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" ..
- finally show ?thesis ..
-qed
-
-lemma
- "s x = 2 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'"
- (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'")
-proof -
- let ?c = "x:== \<lambda>s. s x+1"
- let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
- assume [simp]: "s x = 2"
- note update_def [simp]
- have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" ..
- also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
- also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1) simp
- also have "\<langle>?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 3]\<rangle>" ..
- also have "\<langle>?if, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s[x \<mapsto> 3]\<rangle>" by simp
- also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1) simp
- also have "\<langle>?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 4]\<rangle>" ..
- also have "\<langle>?if, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s[x \<mapsto> 4]\<rangle>" by simp
- also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1) simp
- oops
-
-subsection "Basic properties"
-
-text {*
- There are no \emph{stuck} programs:
-*}
-lemma no_stuck: "\<exists>y. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 y"
-proof (induct c)
- -- "case Semi:"
- fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y"
- then obtain y where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" ..
- then obtain c1' s' where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<or> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1',s'\<rangle>"
- by (cases y, cases "fst y") auto
- thus "\<exists>s'. \<langle>c1;c2,s\<rangle> \<longrightarrow>\<^sub>1 s'" by auto
-next
- -- "case If:"
- fix b c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" and "\<exists>y. \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>1 y"
- thus "\<exists>y. \<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>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!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P"
- by (induct y, auto elim: evalc1.cases)
-
-lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>"
- by (induct set: rtrancl) auto
-
-(*<*)
-(* FIXME: relpow.simps don't work *)
-lemmas [simp del] = relpow.simps
-lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R ^^ 0 = Id" by (simp add: relpow.simps)
-lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R ^^ Suc 0 = R" by (simp add: relpow.simps)
-
-(*>*)
-lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
- by (cases n) auto
-
-lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> 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:
- "\<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow>
- \<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> n = i+j"
-proof (induct n arbitrary: c1 c2 s s'')
- case 0
- then show ?case by simp
-next
- case (Suc n)
-
- from `\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
- obtain co s''' where
- 1: "\<langle>c1; c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s''')" and
- n: "(co, s''') -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
- by auto
-
- from 1
- show "\<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> Suc n = i+j"
- (is "\<exists>i j s'. ?Q i j s'")
- proof (cases set: evalc1)
- case Semi1
- from `co = Some c2` and `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'''\<rangle>` and 1 n
- have "?Q 1 n s'''" by simp
- thus ?thesis by blast
- next
- case (Semi2 c1')
- note c1 = `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'''\<rangle>`
- with `co = Some (c1'; c2)` and n
- have "\<langle>c1'; c2, s'''\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
- with Suc.hyps obtain i j s0 where
- c1': "\<langle>c1',s'''\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
- c2: "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
- i: "n = i+j"
- by fast
-
- from c1 c1'
- have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2)
- with c2 i
- have "?Q (i+1) j s0" by simp
- thus ?thesis by blast
- qed
-qed
-
-
-lemma semiI:
- "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-proof (induct n arbitrary: c0 s s'')
- case 0
- from `\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
- have False by simp
- thus ?case ..
-next
- case (Suc n)
- note c0 = `\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
- note c1 = `\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>`
- note IH = `\<And>c0 s s''.
- \<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>`
- from c0 obtain y where
- 1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
- from 1 obtain c0' s0' where
- "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>"
- by (cases y, cases "fst y") auto
- moreover
- { assume y: "y = \<langle>s0'\<rangle>"
- with n have "s'' = s0'" by simp
- with y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1, s''\<rangle>" by blast
- with c1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
- }
- moreover
- { assume y: "y = \<langle>c0', s0'\<rangle>"
- with n have "\<langle>c0', s0'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
- with IH c1 have "\<langle>c0'; c1,s0'\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
- moreover
- from y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0'; c1,s0'\<rangle>" by blast
- hence "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c0'; c1,s0'\<rangle>" by blast
- ultimately
- have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
- }
- ultimately
- show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
-qed
-
-text {*
- The easy direction of the equivalence proof:
-*}
-lemma evalc_imp_evalc1:
- assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- shows "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- using assms
-proof induct
- fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
-next
- fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto
-next
- fix c0 c1 s s'' s'
- assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
- then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
- moreover
- assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- ultimately
- show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
-next
- fix s::state and b c0 c1 s'
- assume "b s"
- hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
- also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
-next
- fix s::state and b c0 c1 s'
- assume "\<not>b s"
- hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
- also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
-next
- fix b c and s::state
- assume b: "\<not>b s"
- let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
- have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
- also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
- also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
- finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
-next
- fix b c s s'' s'
- let ?w = "\<WHILE> b \<DO> c"
- let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
- assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
- assume b: "b s"
- have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
- also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
- also
- from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
- with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
- finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
-qed
-
-text {*
- Finally, the equivalence theorem:
-*}
-theorem evalc_equiv_evalc1:
- "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-proof
- assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- then show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
-next
- assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
- moreover
- have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- proof (induct arbitrary: c s s' rule: less_induct)
- fix n
- assume IH: "\<And>m c s s'. m < n \<Longrightarrow> \<langle>c,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- fix c s s'
- assume c: "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
- then obtain m where n: "n = Suc m" by (cases n) auto
- with c obtain y where
- c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast
- show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>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: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
- c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" 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 IH i c1
- have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" .
- moreover
- from IH j c2
- have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" .
- moreover
- note semi
- ultimately
- show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>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 "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
- with n IH
- have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- with If True
- have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- }
- moreover
- { assume False: "b s = False"
- with If c n
- have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
- with n IH
- have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- with If False
- have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- }
- ultimately
- show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto
- next
- fix b c' assume w: "c = \<WHILE> b \<DO> c'"
- with c n
- have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
- (is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto
- with n IH
- have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- moreover note unfold_while [of b c']
- -- {* @{thm unfold_while [of b c']} *}
- ultimately
- have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2)
- with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
- qed
- qed
- ultimately
- show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>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]:
- "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>")
-proof -
- assume "\<not>b s"
- have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
- also from `\<not>b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
- also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" ..
- finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
-qed
-
-lemma whileTrue1 [intro]:
- "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>"
- (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>")
-proof -
- assume "b s"
- have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
- also from `b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
- finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
-qed
-
-inductive_cases evalc1_SEs:
- "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
- "\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
- "\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
- "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
- "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
-
-inductive_cases evalc1_E: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
-
-declare evalc1_SEs [elim!]
-
-lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
-apply (induct set: evalc)
-
--- 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 blast
-apply (blast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
-
-done
-
-
-lemma lemma2:
- "\<langle>c;d,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<Longrightarrow> \<exists>t m. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<and> \<langle>d,t\<rangle> -m\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<and> m \<le> n"
-apply (induct n arbitrary: c d s u)
- -- "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:
- "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-apply (induct c arbitrary: s t)
-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\<rightarrow>\<^sub>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 (simp only: split_paired_all)
-apply (erule evalc1_E)
-
-apply simp
-apply (case_tac "b x")
- -- WhileTrue
- apply (erule rel_pow_E2)
- apply simp
- apply (clarify dest!: lemma2)
- apply atomize
- 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: "(\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle>) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
- by (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
-
-
-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:
- assumes "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>"
- and "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
- shows "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
-proof -
- -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
- from assms
- have "\<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
- apply (induct rule: 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
- then show ?thesis by simp
-qed
-
-lemma evalc_impl_evalc1': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
-apply (induct set: evalc)
-
--- 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: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
-
-lemma FB_lemma3:
- "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
- \<langle>if c'=None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
- by (induct arbitrary: t set: evalc1)
- (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
-
-lemma FB_lemma2:
- "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
- \<langle>if c' = None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
- apply (induct rule: converse_rtrancl_induct2, force)
- apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
- done
-
-lemma evalc1_impl_evalc': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
- by (fastsimp dest: FB_lemma2)
-
-end