src/HOL/IMP/Transition.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 34990 81e8fdfeb849
child 41529 ba60efa2fd08
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
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
berghofe@34990
   208
    from `co = Some c2` and `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'''\<rangle>` and 1 n
berghofe@34990
   209
    have "?Q 1 n s'''" by simp
wenzelm@18372
   210
    thus ?thesis by blast
wenzelm@18372
   211
  next
berghofe@34990
   212
    case (Semi2 c1')
berghofe@34990
   213
    note c1 = `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'''\<rangle>`
berghofe@34990
   214
    with `co = Some (c1'; c2)` and n
berghofe@34990
   215
    have "\<langle>c1'; c2, s'''\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
wenzelm@18372
   216
    with Suc.hyps obtain i j s0 where
berghofe@34990
   217
        c1': "\<langle>c1',s'''\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
kleing@12431
   218
        c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
kleing@12431
   219
        i:   "n = i+j"
wenzelm@18372
   220
      by fast
wenzelm@18372
   221
wenzelm@18372
   222
    from c1 c1'
wenzelm@18372
   223
    have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2)
wenzelm@18372
   224
    with c2 i
wenzelm@18372
   225
    have "?Q (i+1) j s0" by simp
wenzelm@18372
   226
    thus ?thesis by blast
berghofe@34990
   227
  qed
kleing@12431
   228
qed
nipkow@1700
   229
nipkow@1700
   230
wenzelm@18372
   231
lemma semiI:
wenzelm@18372
   232
  "\<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
   233
proof (induct n arbitrary: c0 s s'')
wenzelm@18372
   234
  case 0
wenzelm@18372
   235
  from `\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
wenzelm@18372
   236
  have False by simp
wenzelm@18372
   237
  thus ?case ..
kleing@12431
   238
next
wenzelm@18372
   239
  case (Suc n)
wenzelm@18372
   240
  note c0 = `\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
wenzelm@18372
   241
  note c1 = `\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>`
wenzelm@18372
   242
  note IH = `\<And>c0 s s''.
wenzelm@18372
   243
    \<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
   244
  from c0 obtain y where
kleing@12431
   245
    1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
kleing@12431
   246
  from 1 obtain c0' s0' where
wenzelm@18372
   247
      "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>"
wenzelm@18372
   248
    by (cases y, cases "fst y") auto
kleing@12431
   249
  moreover
kleing@12431
   250
  { assume y: "y = \<langle>s0'\<rangle>"
kleing@12431
   251
    with n have "s'' = s0'" by simp
kleing@12431
   252
    with y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1, s''\<rangle>" by blast
kleing@12431
   253
    with c1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
kleing@12431
   254
  }
kleing@12431
   255
  moreover
kleing@12431
   256
  { assume y: "y = \<langle>c0', s0'\<rangle>"
kleing@12431
   257
    with n have "\<langle>c0', s0'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
kleing@12431
   258
    with IH c1 have "\<langle>c0'; c1,s0'\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
kleing@12431
   259
    moreover
kleing@12431
   260
    from y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0'; c1,s0'\<rangle>" by blast
kleing@12431
   261
    hence "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c0'; c1,s0'\<rangle>" by blast
kleing@12431
   262
    ultimately
kleing@12431
   263
    have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
kleing@12431
   264
  }
kleing@12431
   265
  ultimately
kleing@12431
   266
  show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
kleing@12431
   267
qed
kleing@12431
   268
kleing@12431
   269
text {*
kleing@12431
   270
  The easy direction of the equivalence proof:
kleing@12431
   271
*}
wenzelm@18372
   272
lemma evalc_imp_evalc1:
wenzelm@18372
   273
  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
wenzelm@18372
   274
  shows "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
wenzelm@18372
   275
  using prems
wenzelm@18372
   276
proof induct
wenzelm@18372
   277
  fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
wenzelm@18372
   278
next
wenzelm@18372
   279
  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
   280
next
wenzelm@18372
   281
  fix c0 c1 s s'' s'
wenzelm@18372
   282
  assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
wenzelm@18372
   283
  then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
wenzelm@18372
   284
  moreover
wenzelm@18372
   285
  assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
wenzelm@18372
   286
  ultimately
wenzelm@18372
   287
  show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
wenzelm@18372
   288
next
wenzelm@18372
   289
  fix s::state and b c0 c1 s'
wenzelm@18372
   290
  assume "b s"
wenzelm@18372
   291
  hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
wenzelm@18372
   292
  also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
wenzelm@18372
   293
  finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
wenzelm@18372
   294
next
wenzelm@18372
   295
  fix s::state and b c0 c1 s'
wenzelm@18372
   296
  assume "\<not>b s"
wenzelm@18372
   297
  hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
wenzelm@18372
   298
  also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
wenzelm@18372
   299
  finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
wenzelm@18372
   300
next
wenzelm@18372
   301
  fix b c and s::state
wenzelm@18372
   302
  assume b: "\<not>b s"
wenzelm@18372
   303
  let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
wenzelm@18372
   304
  have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
wenzelm@18372
   305
  also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
wenzelm@18372
   306
  also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
wenzelm@18372
   307
  finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
wenzelm@18372
   308
next
wenzelm@18372
   309
  fix b c s s'' s'
wenzelm@18372
   310
  let ?w  = "\<WHILE> b \<DO> c"
wenzelm@18372
   311
  let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
wenzelm@18372
   312
  assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
wenzelm@18372
   313
  assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
wenzelm@18372
   314
  assume b: "b s"
wenzelm@18372
   315
  have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
wenzelm@18372
   316
  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
wenzelm@18372
   317
  also
wenzelm@18372
   318
  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
   319
  with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
wenzelm@18372
   320
  finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
kleing@12431
   321
qed
kleing@12431
   322
kleing@12431
   323
text {*
kleing@12431
   324
  Finally, the equivalence theorem:
kleing@12431
   325
*}
kleing@12431
   326
theorem evalc_equiv_evalc1:
kleing@12431
   327
  "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
kleing@12431
   328
proof
kleing@12431
   329
  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
wenzelm@23373
   330
  then show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
wenzelm@18372
   331
next
kleing@12431
   332
  assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
kleing@12431
   333
  then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
kleing@12431
   334
  moreover
wenzelm@18372
   335
  have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
wenzelm@20503
   336
  proof (induct arbitrary: c s s' rule: less_induct)
kleing@12431
   337
    fix n
wenzelm@18372
   338
    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
   339
    fix c s s'
kleing@12431
   340
    assume c:  "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
kleing@12431
   341
    then obtain m where n: "n = Suc m" by (cases n) auto
wenzelm@18372
   342
    with c obtain y where
kleing@12431
   343
      c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast
wenzelm@18372
   344
    show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
   345
    proof (cases c)
kleing@12431
   346
      case SKIP
kleing@12431
   347
      with c n show ?thesis by auto
wenzelm@18372
   348
    next
kleing@12431
   349
      case Assign
kleing@12431
   350
      with c n show ?thesis by auto
kleing@12431
   351
    next
kleing@12431
   352
      fix c1 c2 assume semi: "c = (c1; c2)"
kleing@12431
   353
      with c obtain i j s'' where
wenzelm@18372
   354
          c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
wenzelm@18372
   355
          c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and
wenzelm@18372
   356
          ij: "n = i+j"
kleing@12431
   357
        by (blast dest: semiD)
wenzelm@18372
   358
      from c1 c2 obtain
kleing@12431
   359
        "0 < i" and "0 < j" by (cases i, auto, cases j, auto)
kleing@12431
   360
      with ij obtain
kleing@12431
   361
        i: "i < n" and j: "j < n" by simp
wenzelm@18372
   362
      from IH i c1
wenzelm@18372
   363
      have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" .
kleing@12431
   364
      moreover
wenzelm@18372
   365
      from IH j c2
wenzelm@18372
   366
      have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" .
kleing@12431
   367
      moreover
kleing@12431
   368
      note semi
kleing@12431
   369
      ultimately
kleing@12431
   370
      show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   371
    next
kleing@12431
   372
      fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2"
kleing@12431
   373
      { assume True: "b s = True"
kleing@12431
   374
        with If c n
wenzelm@18372
   375
        have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
kleing@12431
   376
        with n IH
kleing@12431
   377
        have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   378
        with If True
paulson@34055
   379
        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   380
      }
kleing@12431
   381
      moreover
kleing@12431
   382
      { assume False: "b s = False"
kleing@12431
   383
        with If c n
wenzelm@18372
   384
        have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
kleing@12431
   385
        with n IH
kleing@12431
   386
        have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   387
        with If False
paulson@34055
   388
        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   389
      }
kleing@12431
   390
      ultimately
kleing@12431
   391
      show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto
kleing@12431
   392
    next
kleing@12431
   393
      fix b c' assume w: "c = \<WHILE> b \<DO> c'"
wenzelm@18372
   394
      with c n
kleing@12431
   395
      have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
kleing@12431
   396
        (is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto
kleing@12431
   397
      with n IH
kleing@12431
   398
      have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   399
      moreover note unfold_while [of b c']
kleing@12431
   400
      -- {* @{thm unfold_while [of b c']} *}
wenzelm@18372
   401
      ultimately
kleing@12431
   402
      have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2)
kleing@12431
   403
      with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
kleing@12431
   404
    qed
kleing@12431
   405
  qed
kleing@12431
   406
  ultimately
kleing@12431
   407
  show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   408
qed
kleing@12431
   409
kleing@12431
   410
kleing@12431
   411
subsection "Winskel's Proof"
kleing@12431
   412
kleing@12431
   413
declare rel_pow_0_E [elim!]
kleing@12431
   414
kleing@12431
   415
text {*
wenzelm@18372
   416
  Winskel's small step rules are a bit different \cite{Winskel};
kleing@12431
   417
  we introduce their equivalents as derived rules:
kleing@12431
   418
*}
kleing@12431
   419
lemma whileFalse1 [intro]:
wenzelm@18372
   420
  "\<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
   421
proof -
kleing@12431
   422
  assume "\<not>b s"
kleing@12431
   423
  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
wenzelm@23373
   424
  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
   425
  also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" ..
kleing@12431
   426
  finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
kleing@12431
   427
qed
kleing@12431
   428
kleing@12431
   429
lemma whileTrue1 [intro]:
wenzelm@18372
   430
  "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>"
kleing@12431
   431
  (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>")
kleing@12431
   432
proof -
kleing@12431
   433
  assume "b s"
kleing@12431
   434
  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
wenzelm@23373
   435
  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
   436
  finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
kleing@12431
   437
qed
nipkow@1700
   438
wenzelm@18372
   439
inductive_cases evalc1_SEs:
berghofe@23746
   440
  "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
berghofe@23746
   441
  "\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
berghofe@23746
   442
  "\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
berghofe@23746
   443
  "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
berghofe@23746
   444
  "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
kleing@12431
   445
berghofe@23746
   446
inductive_cases evalc1_E: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
kleing@12431
   447
kleing@12431
   448
declare evalc1_SEs [elim!]
kleing@12431
   449
kleing@12431
   450
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
   451
apply (induct set: evalc)
kleing@12431
   452
wenzelm@18372
   453
-- SKIP
kleing@12431
   454
apply blast
kleing@12431
   455
wenzelm@18372
   456
-- ASSIGN
kleing@12431
   457
apply fast
kleing@12431
   458
wenzelm@18372
   459
-- SEMI
kleing@12431
   460
apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
kleing@12431
   461
wenzelm@18372
   462
-- IF
nipkow@12566
   463
apply (fast intro: converse_rtrancl_into_rtrancl)
nipkow@12566
   464
apply (fast intro: converse_rtrancl_into_rtrancl)
kleing@12431
   465
wenzelm@18372
   466
-- WHILE
paulson@34055
   467
apply blast
paulson@34055
   468
apply (blast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
kleing@12431
   469
kleing@12431
   470
done
kleing@12431
   471
kleing@12431
   472
wenzelm@18372
   473
lemma lemma2:
wenzelm@18372
   474
  "\<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
   475
apply (induct n arbitrary: c d s u)
kleing@12431
   476
 -- "case n = 0"
kleing@12431
   477
 apply fastsimp
kleing@12431
   478
-- "induction step"
wenzelm@18372
   479
apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2
nipkow@12566
   480
            elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
kleing@12431
   481
done
kleing@12431
   482
wenzelm@18372
   483
lemma evalc1_impl_evalc:
wenzelm@18372
   484
  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
wenzelm@20503
   485
apply (induct c arbitrary: s t)
kleing@12431
   486
apply (safe dest!: rtrancl_imp_UN_rel_pow)
kleing@12431
   487
kleing@12431
   488
-- SKIP
kleing@12431
   489
apply (simp add: SKIP_n)
kleing@12431
   490
wenzelm@18372
   491
-- ASSIGN
kleing@12431
   492
apply (fastsimp elim: rel_pow_E2)
kleing@12431
   493
kleing@12431
   494
-- SEMI
kleing@12431
   495
apply (fast dest!: rel_pow_imp_rtrancl lemma2)
kleing@12431
   496
wenzelm@18372
   497
-- IF
kleing@12431
   498
apply (erule rel_pow_E2)
kleing@12431
   499
apply simp
kleing@12431
   500
apply (fast dest!: rel_pow_imp_rtrancl)
kleing@12431
   501
kleing@12431
   502
-- "WHILE, induction on the length of the computation"
kleing@12431
   503
apply (rename_tac b c s t n)
kleing@12431
   504
apply (erule_tac P = "?X -n\<rightarrow>\<^sub>1 ?Y" in rev_mp)
kleing@12431
   505
apply (rule_tac x = "s" in spec)
wenzelm@18372
   506
apply (induct_tac n rule: nat_less_induct)
kleing@12431
   507
apply (intro strip)
kleing@12431
   508
apply (erule rel_pow_E2)
kleing@12431
   509
 apply simp
berghofe@23746
   510
apply (simp only: split_paired_all)
kleing@12431
   511
apply (erule evalc1_E)
kleing@12431
   512
kleing@12431
   513
apply simp
kleing@12431
   514
apply (case_tac "b x")
kleing@12431
   515
 -- WhileTrue
kleing@12431
   516
 apply (erule rel_pow_E2)
kleing@12431
   517
  apply simp
kleing@12431
   518
 apply (clarify dest!: lemma2)
wenzelm@18372
   519
 apply atomize
kleing@12431
   520
 apply (erule allE, erule allE, erule impE, assumption)
kleing@12431
   521
 apply (erule_tac x=mb in allE, erule impE, fastsimp)
kleing@12431
   522
 apply blast
wenzelm@18372
   523
-- WhileFalse
kleing@12431
   524
apply (erule rel_pow_E2)
kleing@12431
   525
 apply simp
kleing@12431
   526
apply (simp add: SKIP_n)
kleing@12431
   527
done
kleing@12431
   528
kleing@12431
   529
kleing@12431
   530
text {* proof of the equivalence of evalc and evalc1 *}
kleing@12431
   531
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
   532
  by (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
kleing@12431
   533
kleing@12431
   534
kleing@12431
   535
subsection "A proof without n"
kleing@12431
   536
kleing@12431
   537
text {*
kleing@12431
   538
  The inductions are a bit awkward to write in this section,
kleing@12431
   539
  because @{text None} as result statement in the small step
kleing@12431
   540
  semantics doesn't have a direct counterpart in the big step
wenzelm@18372
   541
  semantics.
nipkow@1700
   542
kleing@12431
   543
  Winskel's small step rule set (using the @{text "\<SKIP>"} statement
kleing@12431
   544
  to indicate termination) is better suited for this proof.
kleing@12431
   545
*}
kleing@12431
   546
wenzelm@18372
   547
lemma my_lemma1:
wenzelm@18372
   548
  assumes "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>"
wenzelm@18372
   549
    and "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
wenzelm@18372
   550
  shows "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
kleing@12431
   551
proof -
kleing@12431
   552
  -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
wenzelm@18372
   553
  from prems
wenzelm@18372
   554
  have "\<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
wenzelm@18372
   555
    apply (induct rule: converse_rtrancl_induct2)
kleing@12431
   556
     apply simp
kleing@12431
   557
    apply (rename_tac c s')
kleing@12431
   558
    apply simp
kleing@12431
   559
    apply (rule conjI)
wenzelm@18372
   560
     apply fast
kleing@12431
   561
    apply clarify
kleing@12431
   562
    apply (case_tac c)
nipkow@12566
   563
    apply (auto intro: converse_rtrancl_into_rtrancl)
kleing@12431
   564
    done
wenzelm@18372
   565
  then show ?thesis by simp
kleing@12431
   566
qed
kleing@12431
   567
wenzelm@13524
   568
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
   569
apply (induct set: evalc)
kleing@12431
   570
wenzelm@18372
   571
-- SKIP
kleing@12431
   572
apply fast
kleing@12431
   573
kleing@12431
   574
-- ASSIGN
kleing@12431
   575
apply fast
kleing@12431
   576
wenzelm@18372
   577
-- SEMI
kleing@12431
   578
apply (fast intro: my_lemma1)
kleing@12431
   579
kleing@12431
   580
-- IF
nipkow@12566
   581
apply (fast intro: converse_rtrancl_into_rtrancl)
wenzelm@18372
   582
apply (fast intro: converse_rtrancl_into_rtrancl)
kleing@12431
   583
wenzelm@18372
   584
-- WHILE
kleing@12431
   585
apply fast
nipkow@12566
   586
apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1)
kleing@12431
   587
kleing@12431
   588
done
kleing@12431
   589
kleing@12431
   590
text {*
kleing@12431
   591
  The opposite direction is based on a Coq proof done by Ranan Fraer and
kleing@12431
   592
  Yves Bertot. The following sketch is from an email by Ranan Fraer.
kleing@12431
   593
kleing@12431
   594
\begin{verbatim}
kleing@12431
   595
First we've broke it into 2 lemmas:
nipkow@1700
   596
kleing@12431
   597
Lemma 1
kleing@12431
   598
((c,s) --> (SKIP,t)) => (<c,s> -c-> t)
kleing@12431
   599
kleing@12431
   600
This is a quick one, dealing with the cases skip, assignment
kleing@12431
   601
and while_false.
kleing@12431
   602
kleing@12431
   603
Lemma 2
kleing@12431
   604
((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
wenzelm@18372
   605
  =>
kleing@12431
   606
<c,s> -c-> t
kleing@12431
   607
kleing@12431
   608
This is proved by rule induction on the  -*-> relation
wenzelm@18372
   609
and the induction step makes use of a third lemma:
kleing@12431
   610
kleing@12431
   611
Lemma 3
kleing@12431
   612
((c,s) --> (c',s')) /\ <c',s'> -c'-> t
wenzelm@18372
   613
  =>
kleing@12431
   614
<c,s> -c-> t
kleing@12431
   615
wenzelm@18372
   616
This captures the essence of the proof, as it shows that <c',s'>
kleing@12431
   617
behaves as the continuation of <c,s> with respect to the natural
kleing@12431
   618
semantics.
kleing@12431
   619
The proof of Lemma 3 goes by rule induction on the --> relation,
kleing@12431
   620
dealing with the cases sequence1, sequence2, if_true, if_false and
kleing@12431
   621
while_true. In particular in the case (sequence1) we make use again
kleing@12431
   622
of Lemma 1.
kleing@12431
   623
\end{verbatim}
kleing@12431
   624
*}
kleing@12431
   625
kleing@12431
   626
inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
kleing@12431
   627
wenzelm@18372
   628
lemma FB_lemma3:
wenzelm@18372
   629
  "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
wenzelm@18372
   630
  \<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
   631
  by (induct arbitrary: t set: evalc1)
wenzelm@18372
   632
    (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
kleing@12431
   633
wenzelm@18372
   634
lemma FB_lemma2:
wenzelm@18372
   635
  "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
wenzelm@18372
   636
   \<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
   637
  apply (induct rule: converse_rtrancl_induct2, force)
kleing@12434
   638
  apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
kleing@12431
   639
  done
kleing@12431
   640
wenzelm@13524
   641
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
   642
  by (fastsimp dest: FB_lemma2)
nipkow@1700
   643
nipkow@1700
   644
end