src/HOL/IMP/Transition.thy
changeset 12431 07ec657249e5
parent 9364 e783491b9a1f
child 12434 ff2efde4574d
     1.1 --- a/src/HOL/IMP/Transition.thy	Sun Dec 09 14:35:11 2001 +0100
     1.2 +++ b/src/HOL/IMP/Transition.thy	Sun Dec 09 14:35:36 2001 +0100
     1.3 @@ -1,45 +1,686 @@
     1.4 -(*  Title:      HOL/IMP/Transition.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow & Robert Sandner, TUM
     1.7 -    Copyright   1996 TUM
     1.8 -
     1.9 -Transition semantics of commands
    1.10 +(*  Title:        HOL/IMP/Transition.thy
    1.11 +    ID:           $Id$
    1.12 +    Author:       Tobias Nipkow & Robert Sandner, TUM
    1.13 +    Isar Version: Gerwin Klein, 2001
    1.14 +    Copyright     1996 TUM
    1.15  *)
    1.16  
    1.17 -Transition = Natural +
    1.18 +header "Transition Semantics of Commands"
    1.19 +
    1.20 +theory Transition = Natural:
    1.21 +
    1.22 +subsection "The transition relation"
    1.23  
    1.24 -consts  evalc1    :: "((com*state)*(com*state))set"
    1.25 +text {*
    1.26 +  We formalize the transition semantics as in \cite{Nielson}. This
    1.27 +  makes some of the rules a bit more intuitive, but also requires
    1.28 +  some more (internal) formal overhead.
    1.29 +  
    1.30 +  Since configurations that have terminated are written without 
    1.31 +  a statement, the transition relation is not 
    1.32 +  @{typ "((com \<times> state) \<times> (com \<times> state)) set"}
    1.33 +  but instead:
    1.34 +*}
    1.35 +consts evalc1 :: "((com option \<times> state) \<times> (com option \<times> state)) set"
    1.36  
    1.37 +text {*
    1.38 +  Some syntactic sugar that we will use to hide the 
    1.39 +  @{text option} part in configurations:
    1.40 +*}
    1.41  syntax
    1.42 -        "@evalc1" :: "[(com*state),(com*state)] => bool"
    1.43 -                                ("_ -1-> _" [81,81] 100)
    1.44 -        "@evalcn" :: "[(com*state),nat,(com*state)] => bool"
    1.45 -                                ("_ -_-> _" [81,81] 100)
    1.46 -        "@evalc*" :: "[(com*state),(com*state)] => bool"
    1.47 -                                ("_ -*-> _" [81,81] 100)
    1.48 +  "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
    1.49 +  "@angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
    1.50 +
    1.51 +syntax (xsymbols)
    1.52 +  "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
    1.53 +  "@angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
    1.54 +
    1.55 +translations
    1.56 +  "\<langle>c,s\<rangle>" == "(Some c, s)"
    1.57 +  "\<langle>s\<rangle>" == "(None, s)"
    1.58 +
    1.59 +text {*
    1.60 +  More syntactic sugar for the transition relation, and its
    1.61 +  iteration.
    1.62 +*}
    1.63 +syntax
    1.64 +  "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.65 +    ("_ -1-> _" [81,81] 100)
    1.66 +  "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    1.67 +    ("_ -_-> _" [81,81] 100)
    1.68 +  "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.69 +    ("_ -*-> _" [81,81] 100)
    1.70 +
    1.71 +syntax (xsymbols)
    1.72 +  "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.73 +    ("_ \<longrightarrow>\<^sub>1 _" [81,81] 100)
    1.74 +  "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    1.75 +    ("_ -_\<rightarrow>\<^sub>1 _" [81,81] 100)
    1.76 +  "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.77 +    ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [81,81] 100)
    1.78  
    1.79  translations
    1.80 -  "cs0 -1-> cs1"	== "(cs0,cs1) : evalc1"
    1.81 -  "cs0 -1-> (c1,s1)"	== "(cs0,c1,s1) : evalc1"
    1.82 +  "cs \<longrightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1"
    1.83 +  "cs -n\<rightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1^n" 
    1.84 +  "cs \<longrightarrow>\<^sub>1\<^sup>* cs'" == "(cs,cs') \<in> evalc1^*" 
    1.85 +
    1.86 +  -- {* Isabelle converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"}, 
    1.87 +        so we also include: *}
    1.88 +  "cs0 \<longrightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1"   
    1.89 +  "cs0 -n\<rightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^n"
    1.90 +  "cs0 \<longrightarrow>\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^*" 
    1.91 +
    1.92 +text {*
    1.93 +  Now, finally, we are set to write down the rules for our small step semantics:
    1.94 +*}
    1.95 +inductive evalc1
    1.96 +  intros
    1.97 +  Skip:    "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"  
    1.98 +  Assign:  "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> a s]\<rangle>"
    1.99 +
   1.100 +  Semi1:   "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s'\<rangle>"
   1.101 +  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>"
   1.102 +
   1.103 +  IfTrue:  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>"
   1.104 +  IfFalse: "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c2,s\<rangle>"
   1.105 +
   1.106 +  While:   "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>,s\<rangle>"
   1.107 +
   1.108 +lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs"
   1.109 +
   1.110 +(*<*)
   1.111 +(* fixme: move to Relation_Power.thy *)
   1.112 +lemma rel_pow_Suc_E2 [elim!]:
   1.113 +  "[| (x, z) \<in> R ^ Suc n; !!y. [| (x, y) \<in> R; (y, z) \<in> R ^ n |] ==> P |] ==> P"
   1.114 +  by (drule rel_pow_Suc_D2) blast
   1.115 +
   1.116 +lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
   1.117 +proof -
   1.118 +  assume "p \<in> R\<^sup>*"
   1.119 +  moreover obtain x y where p: "p = (x,y)" by (cases p)
   1.120 +  ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
   1.121 +  hence "\<exists>n. (x,y) \<in> R^n"
   1.122 +  proof induct
   1.123 +    fix a have "(a,a) \<in> R^0" by simp
   1.124 +    thus "\<exists>n. (a,a) \<in> R ^ n" ..
   1.125 +  next
   1.126 +    fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
   1.127 +    then obtain n where "(a,b) \<in> R^n" ..
   1.128 +    moreover assume "(b,c) \<in> R"
   1.129 +    ultimately have "(a,c) \<in> R^(Suc n)" by auto
   1.130 +    thus "\<exists>n. (a,c) \<in> R^n" ..
   1.131 +  qed
   1.132 +  with p show ?thesis by hypsubst
   1.133 +qed  
   1.134 +(*>*)    
   1.135 +text {*
   1.136 +  As for the big step semantics you can read these rules in a 
   1.137 +  syntax directed way:
   1.138 +*}
   1.139 +lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)" 
   1.140 +  by (rule, cases set: evalc1, auto)      
   1.141 +
   1.142 +lemma Assign_1: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s[x \<mapsto> a s]\<rangle>)"
   1.143 +  by (rule, cases set: evalc1, auto)
   1.144 +
   1.145 +lemma Cond_1: 
   1.146 +  "\<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>))"
   1.147 +  by (rule, cases set: evalc1, auto)
   1.148 +
   1.149 +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>)"
   1.150 +  by (rule, cases set: evalc1, auto)
   1.151 +
   1.152 +lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1
   1.153 +
   1.154 +
   1.155 +subsection "Examples"
   1.156 +
   1.157 +lemma 
   1.158 +  "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>"
   1.159 +  (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _")
   1.160 +proof -
   1.161 +  let ?x  = "x:== \<lambda>s. s x+1"
   1.162 +  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?x; ?w \<ELSE> \<SKIP>"
   1.163 +  assume [simp]: "s x = 0"
   1.164 +  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
   1.165 +  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?x; ?w, s\<rangle>" by simp 
   1.166 +  also have "\<langle>?x; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1, simp)
   1.167 +  also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" ..
   1.168 +  also have "\<langle>?if, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle>" by (simp add: update_def)
   1.169 +  also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" ..
   1.170 +  finally show ?thesis ..
   1.171 +qed
   1.172  
   1.173 -  "cs0 -n-> cs1" 	== "(cs0,cs1) : evalc1^n"
   1.174 -  "cs0 -n-> (c1,s1)" 	== "(cs0,c1,s1) : evalc1^n"
   1.175 +lemma 
   1.176 +  "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'"
   1.177 +  (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'")
   1.178 +proof -
   1.179 +  let ?c = "x:== \<lambda>s. s x+1"
   1.180 +  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"  
   1.181 +  assume [simp]: "s x = 2"
   1.182 +  note update_def [simp]
   1.183 +  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
   1.184 +  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
   1.185 +  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1, simp)
   1.186 +  also have "\<langle>?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 3]\<rangle>" ..
   1.187 +  also have "\<langle>?if, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 3]\<rangle>" by simp
   1.188 +  also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1, simp)
   1.189 +  also have "\<langle>?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 4]\<rangle>" ..
   1.190 +  also have "\<langle>?if, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 4]\<rangle>" by simp
   1.191 +  also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1, simp) 
   1.192 +  oops
   1.193 +
   1.194 +subsection "Basic properties"
   1.195 +
   1.196 +text {* 
   1.197 +  There are no \emph{stuck} programs:
   1.198 +*}
   1.199 +lemma no_stuck: "\<exists>y. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 y"
   1.200 +proof (induct c)
   1.201 +  -- "case Semi:"
   1.202 +  fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" 
   1.203 +  then obtain y where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" ..
   1.204 +  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>"
   1.205 +    by (cases y, cases "fst y", auto)
   1.206 +  thus "\<exists>s'. \<langle>c1;c2,s\<rangle> \<longrightarrow>\<^sub>1 s'" by auto
   1.207 +next
   1.208 +  -- "case If:"
   1.209 +  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"
   1.210 +  thus "\<exists>y. \<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y" by (cases "b s") auto
   1.211 +qed auto -- "the rest is trivial"
   1.212 +
   1.213 +text {*
   1.214 +  If a configuration does not contain a statement, the program
   1.215 +  has terminated and there is no next configuration:
   1.216 +*}
   1.217 +lemma stuck [dest]: "(None, s) \<longrightarrow>\<^sub>1 y \<Longrightarrow> False" by (auto elim: evalc1.elims)
   1.218 +
   1.219 +(*<*)
   1.220 +(* fixme: relpow.simps don't work *)
   1.221 +lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp
   1.222 +lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp 
   1.223 +lemmas [simp del] = relpow.simps
   1.224 +(*>*)
   1.225 +
   1.226 +lemma evalc_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
   1.227 +  by (cases n) auto
   1.228  
   1.229 -  "cs0 -*-> cs1" 	== "(cs0,cs1) : evalc1^*"
   1.230 -  "cs0 -*-> (c1,s1)" 	== "(cs0,c1,s1) : evalc1^*"
   1.231 +lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1" 
   1.232 +  by (cases n) auto
   1.233 +
   1.234 +subsection "Equivalence to natural semantics (after Nielson and Nielson)"
   1.235 +
   1.236 +text {*
   1.237 +  We first need two lemmas about semicolon statements:
   1.238 +  decomposition and composition.
   1.239 +*}
   1.240 +lemma semiD:
   1.241 +  "\<And>c1 c2 s s''. \<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> 
   1.242 +  \<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"
   1.243 +  (is "PROP ?P n")
   1.244 +proof (induct n)
   1.245 +  show "PROP ?P 0" by simp
   1.246 +next
   1.247 +  fix n assume IH: "PROP ?P n"
   1.248 +  show "PROP ?P (Suc n)"
   1.249 +  proof -
   1.250 +    fix c1 c2 s s''
   1.251 +    assume "\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   1.252 +    then obtain y where
   1.253 +      1: "\<langle>c1; c2, s\<rangle> \<longrightarrow>\<^sub>1 y" and
   1.254 +      n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   1.255 +      by blast
   1.256 +
   1.257 +    from 1
   1.258 +    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"
   1.259 +      (is "\<exists>i j s'. ?Q i j s'")
   1.260 +    proof (cases set: evalc1)
   1.261 +      case Semi1
   1.262 +      then obtain s' where
   1.263 +        "y = \<langle>c2, s'\<rangle>" and "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
   1.264 +        by auto
   1.265 +      with 1 n have "?Q 1 n s'" by simp
   1.266 +      thus ?thesis by blast
   1.267 +    next
   1.268 +      case Semi2
   1.269 +      then obtain c1' s' where
   1.270 +        y:  "y = \<langle>c1'; c2, s'\<rangle>" and
   1.271 +        c1: "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'\<rangle>"
   1.272 +        by auto
   1.273 +      with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp 
   1.274 +      with IH obtain i j s0 where 
   1.275 +        c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
   1.276 +        c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
   1.277 +        i:   "n = i+j"
   1.278 +        by blast
   1.279 +          
   1.280 +      from c1 c1'
   1.281 +      have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto simp del: relpow.simps intro: rel_pow_Suc_I2)
   1.282 +      with c2 i
   1.283 +      have "?Q (i+1) j s0" by simp
   1.284 +      thus ?thesis by blast
   1.285 +    qed auto -- "the remaining cases cannot occur"
   1.286 +  qed
   1.287 +qed
   1.288  
   1.289  
   1.290 -inductive evalc1
   1.291 -  intrs
   1.292 -    Assign "(x :== a,s) -1-> (SKIP,s[x ::= a s])"
   1.293 +lemma semiI: 
   1.294 +  "\<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>"
   1.295 +proof (induct n)
   1.296 +  fix c0 s s'' assume "\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   1.297 +  hence False by simp
   1.298 +  thus "?thesis c0 s s''" ..
   1.299 +next
   1.300 +  fix c0 s s'' n 
   1.301 +  assume c0: "\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   1.302 +  assume c1: "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   1.303 +  assume IH: "\<And>c0 s s''.
   1.304 +    \<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>"
   1.305 +  from c0 obtain y where 
   1.306 +    1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
   1.307 +  from 1 obtain c0' s0' where
   1.308 +    "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>" 
   1.309 +    by (cases y, cases "fst y", auto)
   1.310 +  moreover
   1.311 +  { assume y: "y = \<langle>s0'\<rangle>"
   1.312 +    with n have "s'' = s0'" by simp
   1.313 +    with y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1, s''\<rangle>" by blast
   1.314 +    with c1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
   1.315 +  }
   1.316 +  moreover
   1.317 +  { assume y: "y = \<langle>c0', s0'\<rangle>"
   1.318 +    with n have "\<langle>c0', s0'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
   1.319 +    with IH c1 have "\<langle>c0'; c1,s0'\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
   1.320 +    moreover
   1.321 +    from y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0'; c1,s0'\<rangle>" by blast
   1.322 +    hence "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c0'; c1,s0'\<rangle>" by blast
   1.323 +    ultimately
   1.324 +    have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
   1.325 +  }
   1.326 +  ultimately
   1.327 +  show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
   1.328 +qed
   1.329 +
   1.330 +text {*
   1.331 +  The easy direction of the equivalence proof:
   1.332 +*}
   1.333 +lemma evalc_imp_evalc1: 
   1.334 +  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   1.335 +proof -
   1.336 +  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   1.337 +  thus "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   1.338 +  proof induct
   1.339 +    fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
   1.340 +  next
   1.341 +    fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto
   1.342 +  next
   1.343 +    fix c0 c1 s s'' s'
   1.344 +    assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
   1.345 +    then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   1.346 +    moreover
   1.347 +    assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   1.348 +    ultimately
   1.349 +    show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
   1.350 +  next
   1.351 +    fix s::state and b c0 c1 s'
   1.352 +    assume "b s"
   1.353 +    hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
   1.354 +    also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" 
   1.355 +    finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
   1.356 +  next
   1.357 +    fix s::state and b c0 c1 s'
   1.358 +    assume "\<not>b s"
   1.359 +    hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
   1.360 +    also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   1.361 +    finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
   1.362 +  next
   1.363 +    fix b c and s::state
   1.364 +    assume b: "\<not>b s"
   1.365 +    let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
   1.366 +    have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
   1.367 +    also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
   1.368 +    also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
   1.369 +    finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
   1.370 +  next
   1.371 +    fix b c s s'' s'
   1.372 +    let ?w  = "\<WHILE> b \<DO> c"
   1.373 +    let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
   1.374 +    assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   1.375 +    assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
   1.376 +    assume b: "b s"
   1.377 +    have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
   1.378 +    also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
   1.379 +    also 
   1.380 +    from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   1.381 +    with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
   1.382 +    finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
   1.383 +  qed
   1.384 +qed
   1.385 +
   1.386 +text {*
   1.387 +  Finally, the equivalence theorem:
   1.388 +*}
   1.389 +theorem evalc_equiv_evalc1:
   1.390 +  "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   1.391 +proof
   1.392 +  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   1.393 +  show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
   1.394 +next  
   1.395 +  assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   1.396 +  then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   1.397 +  moreover
   1.398 +  have "\<And>c s s'. \<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" 
   1.399 +  proof (induct rule: nat_less_induct)
   1.400 +    fix n
   1.401 +    assume IH: "\<forall>m. m < n \<longrightarrow> (\<forall>c s s'. \<langle>c, s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s')"
   1.402 +    fix c s s'
   1.403 +    assume c:  "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
   1.404 +    then obtain m where n: "n = Suc m" by (cases n) auto
   1.405 +    with c obtain y where 
   1.406 +      c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast
   1.407 +    show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" 
   1.408 +    proof (cases c)
   1.409 +      case SKIP
   1.410 +      with c n show ?thesis by auto
   1.411 +    next 
   1.412 +      case Assign
   1.413 +      with c n show ?thesis by auto
   1.414 +    next
   1.415 +      fix c1 c2 assume semi: "c = (c1; c2)"
   1.416 +      with c obtain i j s'' where
   1.417 +        c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
   1.418 +        c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and
   1.419 +        ij: "n = i+j"
   1.420 +        by (blast dest: semiD)
   1.421 +      from c1 c2 obtain 
   1.422 +        "0 < i" and "0 < j" by (cases i, auto, cases j, auto)
   1.423 +      with ij obtain
   1.424 +        i: "i < n" and j: "j < n" by simp
   1.425 +      from c1 i IH
   1.426 +      have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" by blast
   1.427 +      moreover
   1.428 +      from c2 j IH
   1.429 +      have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   1.430 +      moreover
   1.431 +      note semi
   1.432 +      ultimately
   1.433 +      show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   1.434 +    next
   1.435 +      fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2"
   1.436 +      { assume True: "b s = True"
   1.437 +        with If c n
   1.438 +        have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto      
   1.439 +        with n IH
   1.440 +        have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   1.441 +        with If True
   1.442 +        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp        
   1.443 +      }
   1.444 +      moreover
   1.445 +      { assume False: "b s = False"
   1.446 +        with If c n
   1.447 +        have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto      
   1.448 +        with n IH
   1.449 +        have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   1.450 +        with If False
   1.451 +        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp        
   1.452 +      }
   1.453 +      ultimately
   1.454 +      show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto
   1.455 +    next
   1.456 +      fix b c' assume w: "c = \<WHILE> b \<DO> c'"
   1.457 +      with c n 
   1.458 +      have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
   1.459 +        (is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto
   1.460 +      with n IH
   1.461 +      have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   1.462 +      moreover note unfold_while [of b c']
   1.463 +      -- {* @{thm unfold_while [of b c']} *}
   1.464 +      ultimately      
   1.465 +      have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2)
   1.466 +      with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
   1.467 +    qed
   1.468 +  qed
   1.469 +  ultimately
   1.470 +  show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   1.471 +qed
   1.472 +
   1.473 +
   1.474 +subsection "Winskel's Proof"
   1.475 +
   1.476 +declare rel_pow_0_E [elim!]
   1.477 +
   1.478 +text {*
   1.479 +  Winskel's small step rules are a bit different \cite{Winskel}; 
   1.480 +  we introduce their equivalents as derived rules:
   1.481 +*}
   1.482 +lemma whileFalse1 [intro]:
   1.483 +  "\<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>")  
   1.484 +proof -
   1.485 +  assume "\<not>b s"
   1.486 +  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
   1.487 +  also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
   1.488 +  also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" ..
   1.489 +  finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
   1.490 +qed
   1.491 +
   1.492 +lemma whileTrue1 [intro]:
   1.493 +  "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>" 
   1.494 +  (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>")
   1.495 +proof -
   1.496 +  assume "b s"
   1.497 +  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
   1.498 +  also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
   1.499 +  finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
   1.500 +qed
   1.501  
   1.502 -    Semi1   "(SKIP;c,s) -1-> (c,s)"     
   1.503 -    Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
   1.504 +inductive_cases evalc1_SEs: 
   1.505 +  "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 t" 
   1.506 +  "\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 t"
   1.507 +  "\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
   1.508 +  "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
   1.509 +  "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 t"
   1.510 +
   1.511 +inductive_cases evalc1_E: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 t"
   1.512 +
   1.513 +declare evalc1_SEs [elim!]
   1.514 +
   1.515 +lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
   1.516 +apply (erule evalc.induct)
   1.517 +
   1.518 +-- SKIP 
   1.519 +apply blast
   1.520 +
   1.521 +-- ASSIGN 
   1.522 +apply fast
   1.523 +
   1.524 +-- SEMI 
   1.525 +apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
   1.526 +
   1.527 +-- IF 
   1.528 +apply (fast intro: rtrancl_into_rtrancl2)
   1.529 +apply (fast intro: rtrancl_into_rtrancl2)
   1.530 +
   1.531 +-- WHILE 
   1.532 +apply fast
   1.533 +apply (fast dest: rtrancl_imp_UN_rel_pow intro: rtrancl_into_rtrancl2 semiI)
   1.534 +
   1.535 +done
   1.536 +
   1.537 +
   1.538 +lemma lemma2 [rule_format (no_asm)]: 
   1.539 +  "\<forall>c d s u. \<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)"
   1.540 +apply (induct_tac "n")
   1.541 + -- "case n = 0"
   1.542 + apply fastsimp
   1.543 +-- "induction step"
   1.544 +apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2 
   1.545 +            elim!: rel_pow_imp_rtrancl rtrancl_into_rtrancl2)
   1.546 +done
   1.547 +
   1.548 +lemma evalc1_impl_evalc [rule_format (no_asm)]: 
   1.549 +  "\<forall>s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   1.550 +apply (induct_tac "c")
   1.551 +apply (safe dest!: rtrancl_imp_UN_rel_pow)
   1.552 +
   1.553 +-- SKIP
   1.554 +apply (simp add: SKIP_n)
   1.555 +
   1.556 +-- ASSIGN 
   1.557 +apply (fastsimp elim: rel_pow_E2)
   1.558 +
   1.559 +-- SEMI
   1.560 +apply (fast dest!: rel_pow_imp_rtrancl lemma2)
   1.561 +
   1.562 +-- IF 
   1.563 +apply (erule rel_pow_E2)
   1.564 +apply simp
   1.565 +apply (fast dest!: rel_pow_imp_rtrancl)
   1.566 +
   1.567 +-- "WHILE, induction on the length of the computation"
   1.568 +apply (rename_tac b c s t n)
   1.569 +apply (erule_tac P = "?X -n\<rightarrow>\<^sub>1 ?Y" in rev_mp)
   1.570 +apply (rule_tac x = "s" in spec)
   1.571 +apply (induct_tac "n" rule: nat_less_induct)
   1.572 +apply (intro strip)
   1.573 +apply (erule rel_pow_E2)
   1.574 + apply simp
   1.575 +apply (erule evalc1_E)
   1.576 +
   1.577 +apply simp
   1.578 +apply (case_tac "b x")
   1.579 + -- WhileTrue
   1.580 + apply (erule rel_pow_E2)
   1.581 +  apply simp
   1.582 + apply (clarify dest!: lemma2)
   1.583 + apply (erule allE, erule allE, erule impE, assumption)
   1.584 + apply (erule_tac x=mb in allE, erule impE, fastsimp)
   1.585 + apply blast
   1.586 +-- WhileFalse 
   1.587 +apply (erule rel_pow_E2)
   1.588 + apply simp
   1.589 +apply (simp add: SKIP_n)
   1.590 +done
   1.591 +
   1.592 +
   1.593 +text {* proof of the equivalence of evalc and evalc1 *}
   1.594 +lemma evalc1_eq_evalc: "(\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle>) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
   1.595 +apply (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
   1.596 +done
   1.597 +
   1.598 +
   1.599 +subsection "A proof without n"
   1.600 +
   1.601 +text {*
   1.602 +  The inductions are a bit awkward to write in this section,
   1.603 +  because @{text None} as result statement in the small step
   1.604 +  semantics doesn't have a direct counterpart in the big step
   1.605 +  semantics. 
   1.606  
   1.607 -    IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
   1.608 -    IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
   1.609 +  Winskel's small step rule set (using the @{text "\<SKIP>"} statement
   1.610 +  to indicate termination) is better suited for this proof.
   1.611 +*}
   1.612 +
   1.613 +lemma my_lemma1 [rule_format (no_asm)]: 
   1.614 +  "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<Longrightarrow> \<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
   1.615 +proof -
   1.616 +  -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
   1.617 +  have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<longrightarrow> 
   1.618 +       \<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
   1.619 +    apply (erule converse_rtrancl_induct2)
   1.620 +     apply simp
   1.621 +    apply (rename_tac c s')
   1.622 +    apply simp
   1.623 +    apply (rule conjI)
   1.624 +     apply (fast dest: stuck)
   1.625 +    apply clarify
   1.626 +    apply (case_tac c)
   1.627 +    apply (auto intro: rtrancl_into_rtrancl2)
   1.628 +    done
   1.629 +  moreover assume "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
   1.630 +  ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
   1.631 +qed
   1.632 +
   1.633 +lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
   1.634 +apply (erule evalc.induct)
   1.635 +
   1.636 +-- SKIP 
   1.637 +apply fast
   1.638 +
   1.639 +-- ASSIGN
   1.640 +apply fast
   1.641 +
   1.642 +-- SEMI 
   1.643 +apply (fast intro: my_lemma1)
   1.644 +
   1.645 +-- IF
   1.646 +apply (fast intro: rtrancl_into_rtrancl2)
   1.647 +apply (fast intro: rtrancl_into_rtrancl2) 
   1.648 +
   1.649 +-- WHILE 
   1.650 +apply fast
   1.651 +apply (fast intro: rtrancl_into_rtrancl2 my_lemma1)
   1.652 +
   1.653 +done
   1.654 +
   1.655 +text {*
   1.656 +  The opposite direction is based on a Coq proof done by Ranan Fraer and
   1.657 +  Yves Bertot. The following sketch is from an email by Ranan Fraer.
   1.658 +
   1.659 +\begin{verbatim}
   1.660 +First we've broke it into 2 lemmas:
   1.661  
   1.662 -    WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
   1.663 -    WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
   1.664 +Lemma 1
   1.665 +((c,s) --> (SKIP,t)) => (<c,s> -c-> t)
   1.666 +
   1.667 +This is a quick one, dealing with the cases skip, assignment
   1.668 +and while_false.
   1.669 +
   1.670 +Lemma 2
   1.671 +((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
   1.672 +  => 
   1.673 +<c,s> -c-> t
   1.674 +
   1.675 +This is proved by rule induction on the  -*-> relation
   1.676 +and the induction step makes use of a third lemma: 
   1.677 +
   1.678 +Lemma 3
   1.679 +((c,s) --> (c',s')) /\ <c',s'> -c'-> t
   1.680 +  => 
   1.681 +<c,s> -c-> t
   1.682 +
   1.683 +This captures the essence of the proof, as it shows that <c',s'> 
   1.684 +behaves as the continuation of <c,s> with respect to the natural
   1.685 +semantics.
   1.686 +The proof of Lemma 3 goes by rule induction on the --> relation,
   1.687 +dealing with the cases sequence1, sequence2, if_true, if_false and
   1.688 +while_true. In particular in the case (sequence1) we make use again
   1.689 +of Lemma 1.
   1.690 +\end{verbatim}
   1.691 +*}
   1.692 +
   1.693 +inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
   1.694 +
   1.695 +lemma FB_lemma3 [rule_format]:
   1.696 +  "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow>
   1.697 +  (\<forall>t. \<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)"
   1.698 +  apply (erule evalc1.induct)
   1.699 +  apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
   1.700 +  done
   1.701 +
   1.702 +lemma rtrancl_stuck: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = (None, s)"
   1.703 +  by (erule rtrancl_induct) (auto dest: stuck)
   1.704 +
   1.705 +lemma FB_lemma2 [rule_format]:
   1.706 +  "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow> 
   1.707 +   \<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" 
   1.708 +  apply (erule converse_rtrancl_induct2)
   1.709 +   apply simp
   1.710 +  apply clarsimp
   1.711 +  apply (fastsimp elim!: evalc1_term_cases dest: rtrancl_stuck intro: FB_lemma3)
   1.712 +  done
   1.713 +
   1.714 +lemma evalc1_impl_evalc: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   1.715 +  apply (fastsimp dest: FB_lemma2)
   1.716 +  done
   1.717  
   1.718  end