src/HOL/IMP/Transition.thy
author wenzelm
Tue Aug 27 11:03:05 2002 +0200 (2002-08-27)
changeset 13524 604d0f3622d6
parent 12566 fe20540bcf93
child 14565 c6dc17aab88a
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:        HOL/IMP/Transition.thy
     2     ID:           $Id$
     3     Author:       Tobias Nipkow & Robert Sandner, TUM
     4     Isar Version: Gerwin Klein, 2001
     5     Copyright     1996 TUM
     6 *)
     7 
     8 header "Transition Semantics of Commands"
     9 
    10 theory Transition = Natural:
    11 
    12 subsection "The transition relation"
    13 
    14 text {*
    15   We formalize the transition semantics as in \cite{Nielson}. This
    16   makes some of the rules a bit more intuitive, but also requires
    17   some more (internal) formal overhead.
    18   
    19   Since configurations that have terminated are written without 
    20   a statement, the transition relation is not 
    21   @{typ "((com \<times> state) \<times> (com \<times> state)) set"}
    22   but instead:
    23 *}
    24 consts evalc1 :: "((com option \<times> state) \<times> (com option \<times> state)) set"
    25 
    26 text {*
    27   Some syntactic sugar that we will use to hide the 
    28   @{text option} part in configurations:
    29 *}
    30 syntax
    31   "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
    32   "_angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
    33 
    34 syntax (xsymbols)
    35   "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
    36   "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
    37 
    38 translations
    39   "\<langle>c,s\<rangle>" == "(Some c, s)"
    40   "\<langle>s\<rangle>" == "(None, s)"
    41 
    42 text {*
    43   More syntactic sugar for the transition relation, and its
    44   iteration.
    45 *}
    46 syntax
    47   "_evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    48     ("_ -1-> _" [60,60] 60)
    49   "_evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    50     ("_ -_-> _" [60,60,60] 60)
    51   "_evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    52     ("_ -*-> _" [60,60] 60)
    53 
    54 syntax (xsymbols)
    55   "_evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    56     ("_ \<longrightarrow>\<^sub>1 _" [60,60] 61)
    57   "_evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    58     ("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60)
    59   "_evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    60     ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [60,60] 60)
    61 
    62 translations
    63   "cs \<longrightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1"
    64   "cs -n\<rightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1^n" 
    65   "cs \<longrightarrow>\<^sub>1\<^sup>* cs'" == "(cs,cs') \<in> evalc1^*" 
    66 
    67   -- {* Isabelle converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"}, 
    68         so we also include: *}
    69   "cs0 \<longrightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1"   
    70   "cs0 -n\<rightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^n"
    71   "cs0 \<longrightarrow>\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^*" 
    72 
    73 text {*
    74   Now, finally, we are set to write down the rules for our small step semantics:
    75 *}
    76 inductive evalc1
    77   intros
    78   Skip:    "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"  
    79   Assign:  "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> a s]\<rangle>"
    80 
    81   Semi1:   "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s'\<rangle>"
    82   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>"
    83 
    84   IfTrue:  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>"
    85   IfFalse: "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c2,s\<rangle>"
    86 
    87   While:   "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>,s\<rangle>"
    88 
    89 lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs"
    90 
    91 (*<*)
    92 (* fixme: move to Relation_Power.thy *)
    93 lemma rel_pow_Suc_E2 [elim!]:
    94   "[| (x, z) \<in> R ^ Suc n; !!y. [| (x, y) \<in> R; (y, z) \<in> R ^ n |] ==> P |] ==> P"
    95   by (drule rel_pow_Suc_D2) blast
    96 
    97 lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
    98 proof -
    99   assume "p \<in> R\<^sup>*"
   100   moreover obtain x y where p: "p = (x,y)" by (cases p)
   101   ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
   102   hence "\<exists>n. (x,y) \<in> R^n"
   103   proof induct
   104     fix a have "(a,a) \<in> R^0" by simp
   105     thus "\<exists>n. (a,a) \<in> R ^ n" ..
   106   next
   107     fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
   108     then obtain n where "(a,b) \<in> R^n" ..
   109     moreover assume "(b,c) \<in> R"
   110     ultimately have "(a,c) \<in> R^(Suc n)" by auto
   111     thus "\<exists>n. (a,c) \<in> R^n" ..
   112   qed
   113   with p show ?thesis by hypsubst
   114 qed  
   115 (*>*)    
   116 text {*
   117   As for the big step semantics you can read these rules in a 
   118   syntax directed way:
   119 *}
   120 lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)" 
   121   by (rule, cases set: evalc1, auto)      
   122 
   123 lemma Assign_1: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s[x \<mapsto> a s]\<rangle>)"
   124   by (rule, cases set: evalc1, auto)
   125 
   126 lemma Cond_1: 
   127   "\<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>))"
   128   by (rule, cases set: evalc1, auto)
   129 
   130 lemma While_1: 
   131   "\<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>)"
   132   by (rule, cases set: evalc1, auto)
   133 
   134 lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1
   135 
   136 
   137 subsection "Examples"
   138 
   139 lemma 
   140   "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>"
   141   (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _")
   142 proof -
   143   let ?c  = "x:== \<lambda>s. s x+1"
   144   let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
   145   assume [simp]: "s x = 0"
   146   have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
   147   also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp 
   148   also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1, simp)
   149   also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" ..
   150   also have "\<langle>?if, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle>" by (simp add: update_def)
   151   also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" ..
   152   finally show ?thesis ..
   153 qed
   154 
   155 lemma 
   156   "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'"
   157   (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'")
   158 proof -
   159   let ?c = "x:== \<lambda>s. s x+1"
   160   let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"  
   161   assume [simp]: "s x = 2"
   162   note update_def [simp]
   163   have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
   164   also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
   165   also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1, simp)
   166   also have "\<langle>?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 3]\<rangle>" ..
   167   also have "\<langle>?if, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 3]\<rangle>" by simp
   168   also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1, simp)
   169   also have "\<langle>?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 4]\<rangle>" ..
   170   also have "\<langle>?if, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 4]\<rangle>" by simp
   171   also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1, simp) 
   172   oops
   173 
   174 subsection "Basic properties"
   175 
   176 text {* 
   177   There are no \emph{stuck} programs:
   178 *}
   179 lemma no_stuck: "\<exists>y. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 y"
   180 proof (induct c)
   181   -- "case Semi:"
   182   fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" 
   183   then obtain y where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" ..
   184   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>"
   185     by (cases y, cases "fst y", auto)
   186   thus "\<exists>s'. \<langle>c1;c2,s\<rangle> \<longrightarrow>\<^sub>1 s'" by auto
   187 next
   188   -- "case If:"
   189   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"
   190   thus "\<exists>y. \<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y" by (cases "b s") auto
   191 qed auto -- "the rest is trivial"
   192 
   193 text {*
   194   If a configuration does not contain a statement, the program
   195   has terminated and there is no next configuration:
   196 *}
   197 lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P" 
   198   by (auto elim: evalc1.elims)
   199 
   200 lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>" 
   201   by (erule rtrancl_induct) auto 
   202 
   203 (*<*)
   204 (* fixme: relpow.simps don't work *)
   205 lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp
   206 lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp 
   207 lemmas [simp del] = relpow.simps
   208 (*>*)
   209 lemma evalc1_None_0 [simp, dest!]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
   210   by (cases n) auto
   211 
   212 lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1" 
   213   by (cases n) auto
   214 
   215 subsection "Equivalence to natural semantics (after Nielson and Nielson)"
   216 
   217 text {*
   218   We first need two lemmas about semicolon statements:
   219   decomposition and composition.
   220 *}
   221 lemma semiD:
   222   "\<And>c1 c2 s s''. \<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> 
   223   \<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"
   224   (is "PROP ?P n")
   225 proof (induct n)
   226   show "PROP ?P 0" by simp
   227 next
   228   fix n assume IH: "PROP ?P n"
   229   show "PROP ?P (Suc n)"
   230   proof -
   231     fix c1 c2 s s''
   232     assume "\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   233     then obtain y where
   234       1: "\<langle>c1; c2, s\<rangle> \<longrightarrow>\<^sub>1 y" and
   235       n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   236       by blast
   237 
   238     from 1
   239     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"
   240       (is "\<exists>i j s'. ?Q i j s'")
   241     proof (cases set: evalc1)
   242       case Semi1
   243       then obtain s' where
   244         "y = \<langle>c2, s'\<rangle>" and "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
   245         by auto
   246       with 1 n have "?Q 1 n s'" by simp
   247       thus ?thesis by blast
   248     next
   249       case Semi2
   250       then obtain c1' s' where
   251         y:  "y = \<langle>c1'; c2, s'\<rangle>" and
   252         c1: "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'\<rangle>"
   253         by auto
   254       with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp 
   255       with IH obtain i j s0 where 
   256         c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
   257         c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
   258         i:   "n = i+j"
   259         by fast
   260           
   261       from c1 c1'
   262       have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2)
   263       with c2 i
   264       have "?Q (i+1) j s0" by simp
   265       thus ?thesis by blast
   266     qed auto -- "the remaining cases cannot occur"
   267   qed
   268 qed
   269 
   270 
   271 lemma semiI: 
   272   "\<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>"
   273 proof (induct n)
   274   fix c0 s s'' assume "\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   275   hence False by simp
   276   thus "?thesis c0 s s''" ..
   277 next
   278   fix c0 s s'' n 
   279   assume c0: "\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   280   assume c1: "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   281   assume IH: "\<And>c0 s s''.
   282     \<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>"
   283   from c0 obtain y where 
   284     1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
   285   from 1 obtain c0' s0' where
   286     "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>" 
   287     by (cases y, cases "fst y", auto)
   288   moreover
   289   { assume y: "y = \<langle>s0'\<rangle>"
   290     with n have "s'' = s0'" by simp
   291     with y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1, s''\<rangle>" by blast
   292     with c1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
   293   }
   294   moreover
   295   { assume y: "y = \<langle>c0', s0'\<rangle>"
   296     with n have "\<langle>c0', s0'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
   297     with IH c1 have "\<langle>c0'; c1,s0'\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
   298     moreover
   299     from y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0'; c1,s0'\<rangle>" by blast
   300     hence "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c0'; c1,s0'\<rangle>" by blast
   301     ultimately
   302     have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
   303   }
   304   ultimately
   305   show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
   306 qed
   307 
   308 text {*
   309   The easy direction of the equivalence proof:
   310 *}
   311 lemma evalc_imp_evalc1: 
   312   "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   313 proof -
   314   assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   315   thus "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   316   proof induct
   317     fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
   318   next
   319     fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto
   320   next
   321     fix c0 c1 s s'' s'
   322     assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
   323     then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   324     moreover
   325     assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   326     ultimately
   327     show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
   328   next
   329     fix s::state and b c0 c1 s'
   330     assume "b s"
   331     hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
   332     also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" 
   333     finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
   334   next
   335     fix s::state and b c0 c1 s'
   336     assume "\<not>b s"
   337     hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
   338     also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   339     finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
   340   next
   341     fix b c and s::state
   342     assume b: "\<not>b s"
   343     let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
   344     have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
   345     also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
   346     also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
   347     finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
   348   next
   349     fix b c s s'' s'
   350     let ?w  = "\<WHILE> b \<DO> c"
   351     let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
   352     assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   353     assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
   354     assume b: "b s"
   355     have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
   356     also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
   357     also 
   358     from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   359     with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
   360     finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
   361   qed
   362 qed
   363 
   364 text {*
   365   Finally, the equivalence theorem:
   366 *}
   367 theorem evalc_equiv_evalc1:
   368   "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   369 proof
   370   assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   371   show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
   372 next  
   373   assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   374   then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   375   moreover
   376   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'" 
   377   proof (induct rule: nat_less_induct)
   378     fix n
   379     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')"
   380     fix c s s'
   381     assume c:  "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
   382     then obtain m where n: "n = Suc m" by (cases n) auto
   383     with c obtain y where 
   384       c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast
   385     show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" 
   386     proof (cases c)
   387       case SKIP
   388       with c n show ?thesis by auto
   389     next 
   390       case Assign
   391       with c n show ?thesis by auto
   392     next
   393       fix c1 c2 assume semi: "c = (c1; c2)"
   394       with c obtain i j s'' where
   395         c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
   396         c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and
   397         ij: "n = i+j"
   398         by (blast dest: semiD)
   399       from c1 c2 obtain 
   400         "0 < i" and "0 < j" by (cases i, auto, cases j, auto)
   401       with ij obtain
   402         i: "i < n" and j: "j < n" by simp
   403       from c1 i IH
   404       have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" by blast
   405       moreover
   406       from c2 j IH
   407       have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   408       moreover
   409       note semi
   410       ultimately
   411       show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   412     next
   413       fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2"
   414       { assume True: "b s = True"
   415         with If c n
   416         have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto      
   417         with n IH
   418         have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   419         with If True
   420         have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp        
   421       }
   422       moreover
   423       { assume False: "b s = False"
   424         with If c n
   425         have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto      
   426         with n IH
   427         have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   428         with If False
   429         have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp        
   430       }
   431       ultimately
   432       show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto
   433     next
   434       fix b c' assume w: "c = \<WHILE> b \<DO> c'"
   435       with c n 
   436       have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
   437         (is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto
   438       with n IH
   439       have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   440       moreover note unfold_while [of b c']
   441       -- {* @{thm unfold_while [of b c']} *}
   442       ultimately      
   443       have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2)
   444       with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
   445     qed
   446   qed
   447   ultimately
   448   show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   449 qed
   450 
   451 
   452 subsection "Winskel's Proof"
   453 
   454 declare rel_pow_0_E [elim!]
   455 
   456 text {*
   457   Winskel's small step rules are a bit different \cite{Winskel}; 
   458   we introduce their equivalents as derived rules:
   459 *}
   460 lemma whileFalse1 [intro]:
   461   "\<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>")  
   462 proof -
   463   assume "\<not>b s"
   464   have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
   465   also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
   466   also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" ..
   467   finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
   468 qed
   469 
   470 lemma whileTrue1 [intro]:
   471   "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>" 
   472   (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>")
   473 proof -
   474   assume "b s"
   475   have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
   476   also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
   477   finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
   478 qed
   479 
   480 inductive_cases evalc1_SEs: 
   481   "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 t" 
   482   "\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 t"
   483   "\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
   484   "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
   485   "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 t"
   486 
   487 inductive_cases evalc1_E: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 t"
   488 
   489 declare evalc1_SEs [elim!]
   490 
   491 lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
   492 apply (erule evalc.induct)
   493 
   494 -- SKIP 
   495 apply blast
   496 
   497 -- ASSIGN 
   498 apply fast
   499 
   500 -- SEMI 
   501 apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
   502 
   503 -- IF 
   504 apply (fast intro: converse_rtrancl_into_rtrancl)
   505 apply (fast intro: converse_rtrancl_into_rtrancl)
   506 
   507 -- WHILE 
   508 apply fast
   509 apply (fast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
   510 
   511 done
   512 
   513 
   514 lemma lemma2 [rule_format (no_asm)]: 
   515   "\<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)"
   516 apply (induct_tac "n")
   517  -- "case n = 0"
   518  apply fastsimp
   519 -- "induction step"
   520 apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2 
   521             elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
   522 done
   523 
   524 lemma evalc1_impl_evalc [rule_format (no_asm)]: 
   525   "\<forall>s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   526 apply (induct_tac "c")
   527 apply (safe dest!: rtrancl_imp_UN_rel_pow)
   528 
   529 -- SKIP
   530 apply (simp add: SKIP_n)
   531 
   532 -- ASSIGN 
   533 apply (fastsimp elim: rel_pow_E2)
   534 
   535 -- SEMI
   536 apply (fast dest!: rel_pow_imp_rtrancl lemma2)
   537 
   538 -- IF 
   539 apply (erule rel_pow_E2)
   540 apply simp
   541 apply (fast dest!: rel_pow_imp_rtrancl)
   542 
   543 -- "WHILE, induction on the length of the computation"
   544 apply (rename_tac b c s t n)
   545 apply (erule_tac P = "?X -n\<rightarrow>\<^sub>1 ?Y" in rev_mp)
   546 apply (rule_tac x = "s" in spec)
   547 apply (induct_tac "n" rule: nat_less_induct)
   548 apply (intro strip)
   549 apply (erule rel_pow_E2)
   550  apply simp
   551 apply (erule evalc1_E)
   552 
   553 apply simp
   554 apply (case_tac "b x")
   555  -- WhileTrue
   556  apply (erule rel_pow_E2)
   557   apply simp
   558  apply (clarify dest!: lemma2)
   559  apply (erule allE, erule allE, erule impE, assumption)
   560  apply (erule_tac x=mb in allE, erule impE, fastsimp)
   561  apply blast
   562 -- WhileFalse 
   563 apply (erule rel_pow_E2)
   564  apply simp
   565 apply (simp add: SKIP_n)
   566 done
   567 
   568 
   569 text {* proof of the equivalence of evalc and evalc1 *}
   570 lemma evalc1_eq_evalc: "(\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle>) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
   571 apply (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
   572 done
   573 
   574 
   575 subsection "A proof without n"
   576 
   577 text {*
   578   The inductions are a bit awkward to write in this section,
   579   because @{text None} as result statement in the small step
   580   semantics doesn't have a direct counterpart in the big step
   581   semantics. 
   582 
   583   Winskel's small step rule set (using the @{text "\<SKIP>"} statement
   584   to indicate termination) is better suited for this proof.
   585 *}
   586 
   587 lemma my_lemma1 [rule_format (no_asm)]: 
   588   "\<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"
   589 proof -
   590   -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
   591   have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<longrightarrow> 
   592        \<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
   593     apply (erule converse_rtrancl_induct2)
   594      apply simp
   595     apply (rename_tac c s')
   596     apply simp
   597     apply (rule conjI)
   598      apply fast 
   599     apply clarify
   600     apply (case_tac c)
   601     apply (auto intro: converse_rtrancl_into_rtrancl)
   602     done
   603   moreover assume "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
   604   ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
   605 qed
   606 
   607 lemma evalc_impl_evalc1': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
   608 apply (erule evalc.induct)
   609 
   610 -- SKIP 
   611 apply fast
   612 
   613 -- ASSIGN
   614 apply fast
   615 
   616 -- SEMI 
   617 apply (fast intro: my_lemma1)
   618 
   619 -- IF
   620 apply (fast intro: converse_rtrancl_into_rtrancl)
   621 apply (fast intro: converse_rtrancl_into_rtrancl) 
   622 
   623 -- WHILE 
   624 apply fast
   625 apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1)
   626 
   627 done
   628 
   629 text {*
   630   The opposite direction is based on a Coq proof done by Ranan Fraer and
   631   Yves Bertot. The following sketch is from an email by Ranan Fraer.
   632 
   633 \begin{verbatim}
   634 First we've broke it into 2 lemmas:
   635 
   636 Lemma 1
   637 ((c,s) --> (SKIP,t)) => (<c,s> -c-> t)
   638 
   639 This is a quick one, dealing with the cases skip, assignment
   640 and while_false.
   641 
   642 Lemma 2
   643 ((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
   644   => 
   645 <c,s> -c-> t
   646 
   647 This is proved by rule induction on the  -*-> relation
   648 and the induction step makes use of a third lemma: 
   649 
   650 Lemma 3
   651 ((c,s) --> (c',s')) /\ <c',s'> -c'-> t
   652   => 
   653 <c,s> -c-> t
   654 
   655 This captures the essence of the proof, as it shows that <c',s'> 
   656 behaves as the continuation of <c,s> with respect to the natural
   657 semantics.
   658 The proof of Lemma 3 goes by rule induction on the --> relation,
   659 dealing with the cases sequence1, sequence2, if_true, if_false and
   660 while_true. In particular in the case (sequence1) we make use again
   661 of Lemma 1.
   662 \end{verbatim}
   663 *}
   664 
   665 inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
   666 
   667 lemma FB_lemma3 [rule_format]:
   668   "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow>
   669   (\<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)"
   670   apply (erule evalc1.induct)
   671   apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
   672   done
   673 
   674 lemma FB_lemma2 [rule_format]:
   675   "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow> 
   676    \<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" 
   677   apply (erule converse_rtrancl_induct2)
   678    apply simp
   679   apply clarsimp
   680   apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
   681   done
   682 
   683 lemma evalc1_impl_evalc': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   684   apply (fastsimp dest: FB_lemma2)
   685   done
   686 
   687 end