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