src/HOL/IMP/Natural.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 23746 a455e69c31cc
child 27362 a6dc1769fdda
permissions -rw-r--r--
avoid rebinding of existing facts;
kleing@12431
     1
(*  Title:        HOL/IMP/Natural.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 "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
kleing@12431
    21
constdefs
kleing@12431
    22
  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
kleing@12431
    23
  "update == fun_upd"
kleing@12431
    24
kleing@12431
    25
syntax (xsymbols)
kleing@12431
    26
  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)
kleing@12431
    27
kleing@12431
    28
text {*
kleing@12431
    29
  The big-step execution relation @{text evalc} is defined inductively:
kleing@12431
    30
*}
berghofe@23746
    31
inductive
berghofe@23746
    32
  evalc :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
berghofe@23746
    33
where
kleing@12431
    34
  Skip:    "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
berghofe@23746
    35
| Assign:  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
kleing@12431
    36
berghofe@23746
    37
| 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
    38
berghofe@23746
    39
| 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
    40
| 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
    41
berghofe@23746
    42
| WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s"
berghofe@23746
    43
| 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
    44
               \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
    45
kleing@12431
    46
lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
kleing@12431
    47
kleing@12431
    48
text {*
kleing@12431
    49
The induction principle induced by this definition looks like this:
kleing@12431
    50
kleing@12431
    51
@{thm [display] evalc.induct [no_vars]}
kleing@12431
    52
kleing@12431
    53
wenzelm@18372
    54
(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
kleing@12431
    55
  meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
kleing@12431
    56
*}
kleing@12431
    57
kleing@12431
    58
kleing@12431
    59
text {*
kleing@12431
    60
  The rules of @{text evalc} are syntax directed, i.e.~for each
kleing@12431
    61
  syntactic category there is always only one rule applicable. That
kleing@12431
    62
  means we can use the rules in both directions. The proofs for this
kleing@12431
    63
  are all the same: one direction is trivial, the other one is shown
wenzelm@18372
    64
  by using the @{text evalc} rules backwards:
kleing@12431
    65
*}
wenzelm@18372
    66
lemma skip:
kleing@12431
    67
  "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
berghofe@23746
    68
  by (rule, erule evalc.cases) auto
kleing@12431
    69
wenzelm@18372
    70
lemma assign:
wenzelm@18372
    71
  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])"
berghofe@23746
    72
  by (rule, erule evalc.cases) auto
kleing@12431
    73
wenzelm@18372
    74
lemma semi:
kleing@12431
    75
  "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s' = (\<exists>s''. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s')"
berghofe@23746
    76
  by (rule, erule evalc.cases) auto
nipkow@1700
    77
wenzelm@18372
    78
lemma ifTrue:
wenzelm@18372
    79
  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"
berghofe@23746
    80
  by (rule, erule evalc.cases) auto
kleing@12431
    81
wenzelm@18372
    82
lemma ifFalse:
kleing@12431
    83
  "\<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'"
berghofe@23746
    84
  by (rule, erule evalc.cases) auto
kleing@12431
    85
wenzelm@18372
    86
lemma whileFalse:
kleing@12431
    87
  "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
berghofe@23746
    88
  by (rule, erule evalc.cases) auto
kleing@12431
    89
wenzelm@18372
    90
lemma whileTrue:
wenzelm@18372
    91
  "b s \<Longrightarrow>
wenzelm@18372
    92
  \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' =
kleing@12431
    93
  (\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')"
berghofe@23746
    94
  by (rule, erule evalc.cases) auto
kleing@12431
    95
kleing@12431
    96
text "Again, Isabelle may use these rules in automatic proofs:"
kleing@12431
    97
lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue
kleing@12431
    98
kleing@12431
    99
subsection "Equivalence of statements"
nipkow@1700
   100
kleing@12431
   101
text {*
kleing@12431
   102
  We call two statements @{text c} and @{text c'} equivalent wrt.~the
kleing@12431
   103
  big-step semantics when \emph{@{text c} started in @{text s} terminates
kleing@12431
   104
  in @{text s'} iff @{text c'} started in the same @{text s} also terminates
kleing@12431
   105
  in the same @{text s'}}. Formally:
wenzelm@18372
   106
*}
kleing@12431
   107
constdefs
kleing@12431
   108
  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
kleing@12431
   109
  "c \<sim> c' \<equiv> \<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
   110
kleing@12431
   111
text {*
kleing@12431
   112
  Proof rules telling Isabelle to unfold the definition
kleing@12431
   113
  if there is something to be proved about equivalent
wenzelm@18372
   114
  statements: *}
kleing@12431
   115
lemma equivI [intro!]:
kleing@12431
   116
  "(\<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
   117
  by (unfold equiv_c_def) blast
kleing@12431
   118
kleing@12431
   119
lemma equivD1:
kleing@12431
   120
  "c \<sim> c' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
   121
  by (unfold equiv_c_def) blast
kleing@12431
   122
kleing@12431
   123
lemma equivD2:
kleing@12431
   124
  "c \<sim> c' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
   125
  by (unfold equiv_c_def) blast
nipkow@1700
   126
kleing@12431
   127
text {*
kleing@12431
   128
  As an example, we show that loop unfolding is an equivalence
kleing@12431
   129
  transformation on programs:
kleing@12431
   130
*}
kleing@12431
   131
lemma unfold_while:
kleing@12431
   132
  "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w \<sim> ?if")
kleing@12431
   133
proof -
kleing@12431
   134
  -- "to show the equivalence, we look at the derivation tree for"
wenzelm@18372
   135
  -- "each side and from that construct a derivation tree for the other side"
kleing@12431
   136
  { fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
   137
    -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
kleing@12431
   138
    -- "then both statements do nothing:"
kleing@12431
   139
    hence "\<not>b s \<Longrightarrow> s = s'" by simp
kleing@12431
   140
    hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
kleing@12431
   141
    moreover
kleing@12431
   142
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
kleing@12431
   143
    -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"} *}
kleing@12431
   144
    { assume b: "b s"
kleing@12431
   145
      with w obtain s'' where
kleing@12431
   146
        "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
kleing@12431
   147
      -- "now we can build a derivation tree for the @{text \<IF>}"
kleing@12431
   148
      -- "first, the body of the True-branch:"
kleing@12431
   149
      hence "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule Semi)
kleing@12431
   150
      -- "then the whole @{text \<IF>}"
kleing@12431
   151
      with b have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule IfTrue)
kleing@12431
   152
    }
wenzelm@18372
   153
    ultimately
wenzelm@18372
   154
    -- "both cases together give us what we want:"
kleing@12431
   155
    have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   156
  }
kleing@12431
   157
  moreover
kleing@12431
   158
  -- "now the other direction:"
wenzelm@19796
   159
  { fix s s' assume "if": "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
kleing@12431
   160
    -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
kleing@12431
   161
    -- "of the @{text \<IF>} is executed, and both statements do nothing:"
kleing@12431
   162
    hence "\<not>b s \<Longrightarrow> s = s'" by simp
kleing@12431
   163
    hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
kleing@12431
   164
    moreover
kleing@12431
   165
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
kleing@12431
   166
    -- {* then this time only the @{text IfTrue} rule can have be used *}
kleing@12431
   167
    { assume b: "b s"
wenzelm@19796
   168
      with "if" have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
kleing@12431
   169
      -- "and for this, only the Semi-rule is applicable:"
kleing@12431
   170
      then obtain s'' where
kleing@12431
   171
        "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
kleing@12431
   172
      -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
kleing@12431
   173
      with b
wenzelm@18372
   174
      have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue)
kleing@12431
   175
    }
wenzelm@18372
   176
    ultimately
kleing@12431
   177
    -- "both cases together again give us what we want:"
kleing@12431
   178
    have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
kleing@12431
   179
  }
kleing@12431
   180
  ultimately
kleing@12431
   181
  show ?thesis by blast
kleing@12431
   182
qed
kleing@12431
   183
kleing@12431
   184
kleing@12431
   185
subsection "Execution is deterministic"
nipkow@1700
   186
kleing@12431
   187
text {*
kleing@12431
   188
The following proof presents all the details:
kleing@12431
   189
*}
wenzelm@18372
   190
theorem com_det:
wenzelm@18372
   191
  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   192
  shows "u = t"
wenzelm@18372
   193
  using prems
wenzelm@20503
   194
proof (induct arbitrary: u set: evalc)
wenzelm@18372
   195
  fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   196
  thus "u = s" by simp
wenzelm@18372
   197
next
wenzelm@18372
   198
  fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   199
  thus "u = s[x \<mapsto> a s]" by simp
wenzelm@18372
   200
next
wenzelm@18372
   201
  fix c0 c1 s s1 s2 u
wenzelm@18372
   202
  assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
wenzelm@18372
   203
  assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
kleing@12431
   204
wenzelm@18372
   205
  assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   206
  then obtain s' where
kleing@12431
   207
      c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and
wenzelm@18372
   208
      c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   209
    by auto
kleing@12431
   210
wenzelm@18372
   211
  from c0 IH0 have "s'=s2" by blast
wenzelm@18372
   212
  with c1 IH1 show "u=s1" by blast
wenzelm@18372
   213
next
wenzelm@18372
   214
  fix b c0 c1 s s1 u
wenzelm@18372
   215
  assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
kleing@12431
   216
wenzelm@18372
   217
  assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   218
  hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
wenzelm@18372
   219
  with IH show "u = s1" by blast
wenzelm@18372
   220
next
wenzelm@18372
   221
  fix b c0 c1 s s1 u
wenzelm@18372
   222
  assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
nipkow@1700
   223
wenzelm@18372
   224
  assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   225
  hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
wenzelm@18372
   226
  with IH show "u = s1" by blast
wenzelm@18372
   227
next
wenzelm@18372
   228
  fix b c s u
wenzelm@18372
   229
  assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   230
  thus "u = s" by simp
wenzelm@18372
   231
next
wenzelm@18372
   232
  fix b c s s1 s2 u
wenzelm@18372
   233
  assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
wenzelm@18372
   234
  assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
wenzelm@18372
   235
wenzelm@18372
   236
  assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   237
  then obtain s' where
kleing@12431
   238
      c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
wenzelm@18372
   239
      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   240
    by auto
wenzelm@18372
   241
wenzelm@18372
   242
  from c "IH\<^sub>c" have "s' = s2" by blast
wenzelm@18372
   243
  with w "IH\<^sub>w" show "u = s1" by blast
kleing@12431
   244
qed
kleing@12431
   245
nipkow@1700
   246
kleing@12431
   247
text {*
kleing@12431
   248
  This is the proof as you might present it in a lecture. The remaining
wenzelm@18372
   249
  cases are simple enough to be proved automatically:
wenzelm@18372
   250
*}
wenzelm@18372
   251
theorem
wenzelm@18372
   252
  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   253
  shows "u = t"
wenzelm@18372
   254
  using prems
wenzelm@20503
   255
proof (induct arbitrary: u)
wenzelm@18372
   256
  -- "the simple @{text \<SKIP>} case for demonstration:"
wenzelm@18372
   257
  fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   258
  thus "u = s" by simp
wenzelm@18372
   259
next
wenzelm@18372
   260
  -- "and the only really interesting case, @{text \<WHILE>}:"
wenzelm@18372
   261
  fix b c s s1 s2 u
wenzelm@18372
   262
  assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
wenzelm@18372
   263
  assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
wenzelm@18372
   264
wenzelm@18372
   265
  assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   266
  then obtain s' where
kleing@12431
   267
      c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
kleing@12431
   268
      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
wenzelm@18372
   269
    by auto
wenzelm@18372
   270
wenzelm@18372
   271
  from c "IH\<^sub>c" have "s' = s2" by blast
wenzelm@18372
   272
  with w "IH\<^sub>w" show "u = s1" by blast
wenzelm@18372
   273
qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
nipkow@1700
   274
nipkow@1700
   275
end