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