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