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