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