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