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