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