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