src/HOL/IMP/Natural.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 37736 2bf3a2cb5e58
child 41529 ba60efa2fd08
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
kleing@12431
     1
(*  Title:        HOL/IMP/Natural.thy
kleing@12431
     2
    ID:           $Id$
kleing@12431
     3
    Author:       Tobias Nipkow & Robert Sandner, TUM
paulson@34055
     4
    Isar Version: Gerwin Klein, 2001; additional proofs by Lawrence Paulson
kleing@12431
     5
    Copyright     1996 TUM
nipkow@1700
     6
*)
nipkow@1700
     7
kleing@12431
     8
header "Natural Semantics of Commands"
kleing@12431
     9
haftmann@16417
    10
theory Natural imports Com begin
kleing@12431
    11
kleing@12431
    12
subsection "Execution of commands"
nipkow@1700
    13
kleing@12431
    14
text {*
wenzelm@18372
    15
  We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
kleing@12431
    16
  in state @{text s}, terminates in state @{text s'}}. Formally,
kleing@12431
    17
  @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} is just another form of saying \emph{the tuple
kleing@12431
    18
  @{text "(c,s,s')"} is part of the relation @{text evalc}}:
kleing@12431
    19
*}
nipkow@1700
    20
wenzelm@27362
    21
definition
wenzelm@27362
    22
  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900) where
wenzelm@27362
    23
  "update = fun_upd"
kleing@12431
    24
wenzelm@27362
    25
notation (xsymbols)
wenzelm@27362
    26
  update  ("_/[_ \<mapsto> /_]" [900,0,0] 900)
kleing@12431
    27
huffman@37085
    28
text {* Disable conflicting syntax from HOL Map theory. *}
huffman@37085
    29
huffman@37085
    30
no_syntax
huffman@37085
    31
  "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
huffman@37085
    32
  "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
huffman@37085
    33
  ""         :: "maplet => maplets"             ("_")
huffman@37085
    34
  "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
huffman@37085
    35
  "_MapUpd"  :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
huffman@37085
    36
  "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
huffman@37085
    37
kleing@12431
    38
text {*
kleing@12431
    39
  The big-step execution relation @{text evalc} is defined inductively:
kleing@12431
    40
*}
berghofe@23746
    41
inductive
berghofe@23746
    42
  evalc :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
berghofe@23746
    43
where
kleing@12431
    44
  Skip:    "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
berghofe@23746
    45
| Assign:  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
kleing@12431
    46
berghofe@23746
    47
| Semi:    "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
    48
berghofe@23746
    49
| IfTrue:  "b s \<Longrightarrow> \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
berghofe@23746
    50
| IfFalse: "\<not>b s \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
    51
berghofe@23746
    52
| WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s"
berghofe@23746
    53
| WhileTrue:  "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'
kleing@12431
    54
               \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
    55
kleing@12431
    56
lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
kleing@12431
    57
kleing@12431
    58
text {*
kleing@12431
    59
The induction principle induced by this definition looks like this:
kleing@12431
    60
kleing@12431
    61
@{thm [display] evalc.induct [no_vars]}
kleing@12431
    62
kleing@12431
    63
wenzelm@18372
    64
(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
kleing@12431
    65
  meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
kleing@12431
    66
*}
kleing@12431
    67
kleing@12431
    68
text {*
kleing@12431
    69
  The rules of @{text evalc} are syntax directed, i.e.~for each
kleing@12431
    70
  syntactic category there is always only one rule applicable. That
paulson@34055
    71
  means we can use the rules in both directions.  This property is called rule inversion.
kleing@12431
    72
*}
paulson@34055
    73
inductive_cases skipE [elim!]:   "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'"
paulson@34055
    74
inductive_cases semiE [elim!]:   "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
paulson@34055
    75
inductive_cases assignE [elim!]: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'"
paulson@34055
    76
inductive_cases ifE [elim!]:     "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
paulson@34055
    77
inductive_cases whileE [elim]:  "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s'"
paulson@34055
    78
paulson@34055
    79
text {* The next proofs are all trivial by rule inversion.
paulson@34055
    80
*}
paulson@34055
    81
bulwahn@37736
    82
inductive_simps
bulwahn@37736
    83
  skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'"
bulwahn@37736
    84
  and assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'"
bulwahn@37736
    85
  and semi: "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
nipkow@1700
    86
wenzelm@18372
    87
lemma ifTrue:
wenzelm@18372
    88
  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"
paulson@34055
    89
  by auto
kleing@12431
    90
wenzelm@18372
    91
lemma ifFalse:
kleing@12431
    92
  "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'"
paulson@34055
    93
  by auto
kleing@12431
    94
wenzelm@18372
    95
lemma whileFalse:
kleing@12431
    96
  "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
paulson@34055
    97
  by auto
kleing@12431
    98
wenzelm@18372
    99
lemma whileTrue:
wenzelm@18372
   100
  "b s \<Longrightarrow>
wenzelm@18372
   101
  \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' =
kleing@12431
   102
  (\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')"
paulson@34055
   103
  by auto
kleing@12431
   104
kleing@12431
   105
text "Again, Isabelle may use these rules in automatic proofs:"
kleing@12431
   106
lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue
kleing@12431
   107
kleing@12431
   108
subsection "Equivalence of statements"
nipkow@1700
   109
kleing@12431
   110
text {*
kleing@12431
   111
  We call two statements @{text c} and @{text c'} equivalent wrt.~the
kleing@12431
   112
  big-step semantics when \emph{@{text c} started in @{text s} terminates
kleing@12431
   113
  in @{text s'} iff @{text c'} started in the same @{text s} also terminates
kleing@12431
   114
  in the same @{text s'}}. Formally:
wenzelm@18372
   115
*}
wenzelm@27362
   116
definition
huffman@37085
   117
  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _" [56, 56] 55) where
wenzelm@27362
   118
  "c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')"
kleing@12431
   119
kleing@12431
   120
text {*
kleing@12431
   121
  Proof rules telling Isabelle to unfold the definition
kleing@12431
   122
  if there is something to be proved about equivalent
wenzelm@18372
   123
  statements: *}
kleing@12431
   124
lemma equivI [intro!]:
kleing@12431
   125
  "(\<And>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s') \<Longrightarrow> c \<sim> c'"
kleing@12431
   126
  by (unfold equiv_c_def) blast
kleing@12431
   127
kleing@12431
   128
lemma equivD1:
kleing@12431
   129
  "c \<sim> c' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
   130
  by (unfold equiv_c_def) blast
kleing@12431
   131
kleing@12431
   132
lemma equivD2:
kleing@12431
   133
  "c \<sim> c' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
   134
  by (unfold equiv_c_def) blast
nipkow@1700
   135
kleing@12431
   136
text {*
kleing@12431
   137
  As an example, we show that loop unfolding is an equivalence
kleing@12431
   138
  transformation on programs:
kleing@12431
   139
*}
kleing@12431
   140
lemma unfold_while:
kleing@12431
   141
  "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w \<sim> ?if")
kleing@12431
   142
proof -
kleing@12431
   143
  -- "to show the equivalence, we look at the derivation tree for"
wenzelm@18372
   144
  -- "each side and from that construct a derivation tree for the other side"
kleing@12431
   145
  { fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
   146
    -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
kleing@12431
   147
    -- "then both statements do nothing:"
paulson@34055
   148
    hence "\<not>b s \<Longrightarrow> s = s'" by blast
paulson@34055
   149
    hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   150
    moreover
kleing@12431
   151
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
kleing@12431
   152
    -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"} *}
kleing@12431
   153
    { assume b: "b s"
kleing@12431
   154
      with w obtain s'' where
kleing@12431
   155
        "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
kleing@12431
   156
      -- "now we can build a derivation tree for the @{text \<IF>}"
kleing@12431
   157
      -- "first, the body of the True-branch:"
kleing@12431
   158
      hence "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule Semi)
kleing@12431
   159
      -- "then the whole @{text \<IF>}"
kleing@12431
   160
      with b have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule IfTrue)
kleing@12431
   161
    }
wenzelm@18372
   162
    ultimately
wenzelm@18372
   163
    -- "both cases together give us what we want:"
kleing@12431
   164
    have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   165
  }
kleing@12431
   166
  moreover
kleing@12431
   167
  -- "now the other direction:"
wenzelm@19796
   168
  { fix s s' assume "if": "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
   169
    -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
kleing@12431
   170
    -- "of the @{text \<IF>} is executed, and both statements do nothing:"
paulson@34055
   171
    hence "\<not>b s \<Longrightarrow> s = s'" by blast
paulson@34055
   172
    hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   173
    moreover
kleing@12431
   174
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
kleing@12431
   175
    -- {* then this time only the @{text IfTrue} rule can have be used *}
kleing@12431
   176
    { assume b: "b s"
wenzelm@19796
   177
      with "if" have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
kleing@12431
   178
      -- "and for this, only the Semi-rule is applicable:"
kleing@12431
   179
      then obtain s'' where
kleing@12431
   180
        "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
kleing@12431
   181
      -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
kleing@12431
   182
      with b
wenzelm@18372
   183
      have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue)
kleing@12431
   184
    }
wenzelm@18372
   185
    ultimately
kleing@12431
   186
    -- "both cases together again give us what we want:"
kleing@12431
   187
    have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   188
  }
kleing@12431
   189
  ultimately
kleing@12431
   190
  show ?thesis by blast
kleing@12431
   191
qed
kleing@12431
   192
paulson@34055
   193
text {*
paulson@34055
   194
   Happily, such lengthy proofs are seldom necessary.  Isabelle can prove many such facts automatically.
paulson@34055
   195
*}
paulson@34055
   196
paulson@34055
   197
lemma 
paulson@34055
   198
  "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
paulson@34055
   199
by blast
paulson@34055
   200
paulson@34055
   201
lemma triv_if:
paulson@34055
   202
  "(\<IF> b \<THEN> c \<ELSE> c) \<sim> c"
paulson@34055
   203
by blast
paulson@34055
   204
paulson@34055
   205
lemma commute_if:
paulson@34055
   206
  "(\<IF> b1 \<THEN> (\<IF> b2 \<THEN> c11 \<ELSE> c12) \<ELSE> c2) 
paulson@34055
   207
   \<sim> 
paulson@34055
   208
   (\<IF> b2 \<THEN> (\<IF> b1 \<THEN> c11 \<ELSE> c2) \<ELSE> (\<IF> b1 \<THEN> c12 \<ELSE> c2))"
paulson@34055
   209
by blast
paulson@34055
   210
paulson@34055
   211
lemma while_equiv:
paulson@34055
   212
  "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<sim> c' \<Longrightarrow> (c0 = \<WHILE> b \<DO> c) \<Longrightarrow> \<langle>\<WHILE> b \<DO> c', s\<rangle> \<longrightarrow>\<^sub>c u" 
paulson@34055
   213
by (induct rule: evalc.induct) (auto simp add: equiv_c_def) 
paulson@34055
   214
paulson@34055
   215
lemma equiv_while:
paulson@34055
   216
  "c \<sim> c' \<Longrightarrow> (\<WHILE> b \<DO> c) \<sim> (\<WHILE> b \<DO> c')"
paulson@34055
   217
by (simp add: equiv_c_def) (metis equiv_c_def while_equiv) 
paulson@34055
   218
paulson@34055
   219
paulson@34055
   220
text {*
paulson@34055
   221
    Program equivalence is an equivalence relation.
paulson@34055
   222
*}
paulson@34055
   223
paulson@34055
   224
lemma equiv_refl:
paulson@34055
   225
  "c \<sim> c"
paulson@34055
   226
by blast
paulson@34055
   227
paulson@34055
   228
lemma equiv_sym:
paulson@34055
   229
  "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c1"
paulson@34055
   230
by (auto simp add: equiv_c_def) 
paulson@34055
   231
paulson@34055
   232
lemma equiv_trans:
paulson@34055
   233
  "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c3 \<Longrightarrow> c1 \<sim> c3"
paulson@34055
   234
by (auto simp add: equiv_c_def) 
paulson@34055
   235
paulson@34055
   236
text {*
paulson@34055
   237
    Program constructions preserve equivalence.
paulson@34055
   238
*}
paulson@34055
   239
paulson@34055
   240
lemma equiv_semi:
paulson@34055
   241
  "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (c1; c2) \<sim> (c1'; c2')"
paulson@34055
   242
by (force simp add: equiv_c_def) 
paulson@34055
   243
paulson@34055
   244
lemma equiv_if:
paulson@34055
   245
  "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (\<IF> b \<THEN> c1 \<ELSE> c2) \<sim> (\<IF> b \<THEN> c1' \<ELSE> c2')"
paulson@34055
   246
by (force simp add: equiv_c_def) 
paulson@34055
   247
paulson@34055
   248
lemma while_never: "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<noteq> \<WHILE> (\<lambda>s. True) \<DO> c1"
paulson@34055
   249
apply (induct rule: evalc.induct)
paulson@34055
   250
apply auto
paulson@34055
   251
done
paulson@34055
   252
paulson@34055
   253
lemma equiv_while_True:
paulson@34055
   254
  "(\<WHILE> (\<lambda>s. True) \<DO> c1) \<sim> (\<WHILE> (\<lambda>s. True) \<DO> c2)" 
paulson@34055
   255
by (blast dest: while_never) 
paulson@34055
   256
kleing@12431
   257
kleing@12431
   258
subsection "Execution is deterministic"
nipkow@1700
   259
kleing@12431
   260
text {*
paulson@34055
   261
This proof is automatic.
paulson@34055
   262
*}
paulson@34055
   263
theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = t"
paulson@34055
   264
by (induct arbitrary: u rule: evalc.induct) blast+
paulson@34055
   265
paulson@34055
   266
paulson@34055
   267
text {*
kleing@12431
   268
The following proof presents all the details:
kleing@12431
   269
*}
wenzelm@18372
   270
theorem com_det:
wenzelm@18372
   271
  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   272
  shows "u = t"
wenzelm@18372
   273
  using prems
wenzelm@20503
   274
proof (induct arbitrary: u set: evalc)
wenzelm@18372
   275
  fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
paulson@34055
   276
  thus "u = s" by blast
wenzelm@18372
   277
next
wenzelm@18372
   278
  fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
paulson@34055
   279
  thus "u = s[x \<mapsto> a s]" by blast
wenzelm@18372
   280
next
wenzelm@18372
   281
  fix c0 c1 s s1 s2 u
wenzelm@18372
   282
  assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
wenzelm@18372
   283
  assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
kleing@12431
   284
wenzelm@18372
   285
  assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   286
  then obtain s' where
kleing@12431
   287
      c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and
wenzelm@18372
   288
      c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   289
    by auto
kleing@12431
   290
wenzelm@18372
   291
  from c0 IH0 have "s'=s2" by blast
wenzelm@18372
   292
  with c1 IH1 show "u=s1" by blast
wenzelm@18372
   293
next
wenzelm@18372
   294
  fix b c0 c1 s s1 u
wenzelm@18372
   295
  assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
kleing@12431
   296
wenzelm@18372
   297
  assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
paulson@34055
   298
  hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by blast
wenzelm@18372
   299
  with IH show "u = s1" by blast
wenzelm@18372
   300
next
wenzelm@18372
   301
  fix b c0 c1 s s1 u
wenzelm@18372
   302
  assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
nipkow@1700
   303
wenzelm@18372
   304
  assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
paulson@34055
   305
  hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by blast
wenzelm@18372
   306
  with IH show "u = s1" by blast
wenzelm@18372
   307
next
wenzelm@18372
   308
  fix b c s u
wenzelm@18372
   309
  assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
paulson@34055
   310
  thus "u = s" by blast
wenzelm@18372
   311
next
wenzelm@18372
   312
  fix b c s s1 s2 u
wenzelm@18372
   313
  assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
wenzelm@18372
   314
  assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
wenzelm@18372
   315
wenzelm@18372
   316
  assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   317
  then obtain s' where
kleing@12431
   318
      c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
wenzelm@18372
   319
      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   320
    by auto
wenzelm@18372
   321
wenzelm@18372
   322
  from c "IH\<^sub>c" have "s' = s2" by blast
wenzelm@18372
   323
  with w "IH\<^sub>w" show "u = s1" by blast
kleing@12431
   324
qed
kleing@12431
   325
nipkow@1700
   326
kleing@12431
   327
text {*
kleing@12431
   328
  This is the proof as you might present it in a lecture. The remaining
wenzelm@18372
   329
  cases are simple enough to be proved automatically:
wenzelm@18372
   330
*}
wenzelm@18372
   331
theorem
wenzelm@18372
   332
  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   333
  shows "u = t"
wenzelm@18372
   334
  using prems
wenzelm@20503
   335
proof (induct arbitrary: u)
wenzelm@18372
   336
  -- "the simple @{text \<SKIP>} case for demonstration:"
wenzelm@18372
   337
  fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
paulson@34055
   338
  thus "u = s" by blast
wenzelm@18372
   339
next
wenzelm@18372
   340
  -- "and the only really interesting case, @{text \<WHILE>}:"
wenzelm@18372
   341
  fix b c s s1 s2 u
wenzelm@18372
   342
  assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
wenzelm@18372
   343
  assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
wenzelm@18372
   344
wenzelm@18372
   345
  assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   346
  then obtain s' where
kleing@12431
   347
      c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
kleing@12431
   348
      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   349
    by auto
wenzelm@18372
   350
wenzelm@18372
   351
  from c "IH\<^sub>c" have "s' = s2" by blast
wenzelm@18372
   352
  with w "IH\<^sub>w" show "u = s1" by blast
paulson@34055
   353
qed blast+ -- "prove the rest automatically"
nipkow@1700
   354
nipkow@1700
   355
end