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