src/HOL/IMP/Big_Step.thy
author kleing
Mon Jun 06 16:29:38 2011 +0200 (2011-06-06)
changeset 43158 686fa0a0696e
parent 43141 11fce8564415
child 44036 d03f9f28d01d
permissions -rw-r--r--
imported rest of new IMP
nipkow@43141
     1
(* Author: Gerwin Klein, Tobias Nipkow *)
nipkow@43141
     2
nipkow@43141
     3
theory Big_Step imports Com begin
nipkow@43141
     4
nipkow@43141
     5
subsection "Big-Step Semantics of Commands"
nipkow@43141
     6
nipkow@43141
     7
inductive
nipkow@43141
     8
  big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
nipkow@43141
     9
where
nipkow@43141
    10
Skip:    "(SKIP,s) \<Rightarrow> s" |
nipkow@43141
    11
Assign:  "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
nipkow@43141
    12
Semi:    "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
nipkow@43141
    13
          (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
nipkow@43141
    14
nipkow@43141
    15
IfTrue:  "\<lbrakk> bval b s;  (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
nipkow@43141
    16
         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
nipkow@43141
    17
IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
nipkow@43141
    18
         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
nipkow@43141
    19
nipkow@43141
    20
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
nipkow@43141
    21
WhileTrue:  "\<lbrakk> bval b s\<^isub>1;  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
nipkow@43141
    22
             (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
nipkow@43141
    23
nipkow@43141
    24
schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
nipkow@43141
    25
apply(rule Semi)
nipkow@43141
    26
apply(rule Assign)
nipkow@43141
    27
apply simp
nipkow@43141
    28
apply(rule Assign)
nipkow@43141
    29
done
nipkow@43141
    30
nipkow@43141
    31
thm ex[simplified]
nipkow@43141
    32
nipkow@43141
    33
text{* We want to execute the big-step rules: *}
nipkow@43141
    34
nipkow@43141
    35
code_pred big_step .
nipkow@43141
    36
nipkow@43141
    37
text{* For inductive definitions we need command
nipkow@43141
    38
       \texttt{values} instead of \texttt{value}. *}
nipkow@43141
    39
kleing@43158
    40
values "{t. (SKIP, %_. 0) \<Rightarrow> t}"
nipkow@43141
    41
nipkow@43141
    42
text{* We need to translate the result state into a list
nipkow@43141
    43
to display it. *}
nipkow@43141
    44
kleing@43158
    45
values "{map t [''x''] |t. (SKIP, [''x'' \<rightarrow> 42]) \<Rightarrow> t}"
nipkow@43141
    46
kleing@43158
    47
values "{map t [''x''] |t. (''x'' ::= N 2, [''x'' \<rightarrow> 42]) \<Rightarrow> t}"
nipkow@43141
    48
nipkow@43141
    49
values "{map t [''x'',''y''] |t.
nipkow@43141
    50
  (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
kleing@43158
    51
   [''x'' \<rightarrow> 0, ''y'' \<rightarrow> 13]) \<Rightarrow> t}"
nipkow@43141
    52
nipkow@43141
    53
nipkow@43141
    54
text{* Proof automation: *}
nipkow@43141
    55
nipkow@43141
    56
declare big_step.intros [intro]
nipkow@43141
    57
nipkow@43141
    58
text{* The standard induction rule 
nipkow@43141
    59
@{thm [display] big_step.induct [no_vars]} *}
nipkow@43141
    60
nipkow@43141
    61
thm big_step.induct
nipkow@43141
    62
nipkow@43141
    63
text{* A customized induction rule for (c,s) pairs: *}
nipkow@43141
    64
nipkow@43141
    65
lemmas big_step_induct = big_step.induct[split_format(complete)]
nipkow@43141
    66
thm big_step_induct
nipkow@43141
    67
text {*
nipkow@43141
    68
@{thm [display] big_step_induct [no_vars]}
nipkow@43141
    69
*}
nipkow@43141
    70
nipkow@43141
    71
nipkow@43141
    72
subsection "Rule inversion"
nipkow@43141
    73
nipkow@43141
    74
text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ?
nipkow@43141
    75
That @{prop "s = t"}. This is how we can automatically prove it: *}
nipkow@43141
    76
nipkow@43141
    77
inductive_cases skipE[elim!]: "(SKIP,s) \<Rightarrow> t"
nipkow@43141
    78
thm skipE
nipkow@43141
    79
nipkow@43141
    80
text{* This is an \emph{elimination rule}. The [elim] attribute tells auto,
nipkow@43141
    81
blast and friends (but not simp!) to use it automatically; [elim!] means that
nipkow@43141
    82
it is applied eagerly.
nipkow@43141
    83
nipkow@43141
    84
Similarly for the other commands: *}
nipkow@43141
    85
nipkow@43141
    86
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
nipkow@43141
    87
thm AssignE
nipkow@43141
    88
inductive_cases SemiE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"
nipkow@43141
    89
thm SemiE
nipkow@43141
    90
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
nipkow@43141
    91
thm IfE
nipkow@43141
    92
nipkow@43141
    93
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
nipkow@43141
    94
thm WhileE
nipkow@43141
    95
text{* Only [elim]: [elim!] would not terminate. *}
nipkow@43141
    96
nipkow@43141
    97
text{* An automatic example: *}
nipkow@43141
    98
nipkow@43141
    99
lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s"
nipkow@43141
   100
by blast
nipkow@43141
   101
nipkow@43141
   102
text{* Rule inversion by hand via the ``cases'' method: *}
nipkow@43141
   103
nipkow@43141
   104
lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t"
nipkow@43141
   105
shows "t = s"
nipkow@43141
   106
proof-
nipkow@43141
   107
  from assms show ?thesis
nipkow@43141
   108
  proof cases  --"inverting assms"
nipkow@43141
   109
    case IfTrue thm IfTrue
nipkow@43141
   110
    thus ?thesis by blast
nipkow@43141
   111
  next
nipkow@43141
   112
    case IfFalse thus ?thesis by blast
nipkow@43141
   113
  qed
nipkow@43141
   114
qed
nipkow@43141
   115
nipkow@43141
   116
nipkow@43141
   117
subsection "Command Equivalence"
nipkow@43141
   118
nipkow@43141
   119
text {*
nipkow@43141
   120
  We call two statements @{text c} and @{text c'} equivalent wrt.\ the
nipkow@43141
   121
  big-step semantics when \emph{@{text c} started in @{text s} terminates
nipkow@43141
   122
  in @{text s'} iff @{text c'} started in the same @{text s} also terminates
nipkow@43141
   123
  in the same @{text s'}}. Formally:
nipkow@43141
   124
*}
nipkow@43141
   125
abbreviation
nipkow@43141
   126
  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
nipkow@43141
   127
  "c \<sim> c' == (\<forall>s t. (c,s) \<Rightarrow> t  =  (c',s) \<Rightarrow> t)"
nipkow@43141
   128
nipkow@43141
   129
text {*
nipkow@43141
   130
Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces).
nipkow@43141
   131
nipkow@43141
   132
  As an example, we show that loop unfolding is an equivalence
nipkow@43141
   133
  transformation on programs:
nipkow@43141
   134
*}
nipkow@43141
   135
lemma unfold_while:
nipkow@43141
   136
  "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
nipkow@43141
   137
proof -
nipkow@43141
   138
  -- "to show the equivalence, we look at the derivation tree for"
nipkow@43141
   139
  -- "each side and from that construct a derivation tree for the other side"
nipkow@43141
   140
  { fix s t assume "(?w, s) \<Rightarrow> t"
nipkow@43141
   141
    -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
nipkow@43141
   142
    -- "then both statements do nothing:"
nipkow@43141
   143
    { assume "\<not>bval b s"
nipkow@43141
   144
      hence "t = s" using `(?w,s) \<Rightarrow> t` by blast
nipkow@43141
   145
      hence "(?iw, s) \<Rightarrow> t" using `\<not>bval b s` by blast
nipkow@43141
   146
    }
nipkow@43141
   147
    moreover
nipkow@43141
   148
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
nipkow@43141
   149
    -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"} *}
nipkow@43141
   150
    { assume "bval b s"
nipkow@43141
   151
      with `(?w, s) \<Rightarrow> t` obtain s' where
nipkow@43141
   152
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
nipkow@43141
   153
      -- "now we can build a derivation tree for the @{text IF}"
nipkow@43141
   154
      -- "first, the body of the True-branch:"
nipkow@43141
   155
      hence "(c; ?w, s) \<Rightarrow> t" by (rule Semi)
nipkow@43141
   156
      -- "then the whole @{text IF}"
nipkow@43141
   157
      with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue)
nipkow@43141
   158
    }
nipkow@43141
   159
    ultimately
nipkow@43141
   160
    -- "both cases together give us what we want:"
nipkow@43141
   161
    have "(?iw, s) \<Rightarrow> t" by blast
nipkow@43141
   162
  }
nipkow@43141
   163
  moreover
nipkow@43141
   164
  -- "now the other direction:"
nipkow@43141
   165
  { fix s t assume "(?iw, s) \<Rightarrow> t"
nipkow@43141
   166
    -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
nipkow@43141
   167
    -- "of the @{text IF} is executed, and both statements do nothing:"
nipkow@43141
   168
    { assume "\<not>bval b s"
nipkow@43141
   169
      hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast
nipkow@43141
   170
      hence "(?w, s) \<Rightarrow> t" using `\<not>bval b s` by blast
nipkow@43141
   171
    }
nipkow@43141
   172
    moreover
nipkow@43141
   173
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
nipkow@43141
   174
    -- {* then this time only the @{text IfTrue} rule can have be used *}
nipkow@43141
   175
    { assume "bval b s"
nipkow@43141
   176
      with `(?iw, s) \<Rightarrow> t` have "(c; ?w, s) \<Rightarrow> t" by auto
nipkow@43141
   177
      -- "and for this, only the Semi-rule is applicable:"
nipkow@43141
   178
      then obtain s' where
nipkow@43141
   179
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
nipkow@43141
   180
      -- "with this information, we can build a derivation tree for the @{text WHILE}"
nipkow@43141
   181
      with `bval b s`
nipkow@43141
   182
      have "(?w, s) \<Rightarrow> t" by (rule WhileTrue)
nipkow@43141
   183
    }
nipkow@43141
   184
    ultimately
nipkow@43141
   185
    -- "both cases together again give us what we want:"
nipkow@43141
   186
    have "(?w, s) \<Rightarrow> t" by blast
nipkow@43141
   187
  }
nipkow@43141
   188
  ultimately
nipkow@43141
   189
  show ?thesis by blast
nipkow@43141
   190
qed
nipkow@43141
   191
nipkow@43141
   192
text {* Luckily, such lengthy proofs are seldom necessary.  Isabelle can
nipkow@43141
   193
prove many such facts automatically.  *}
nipkow@43141
   194
nipkow@43141
   195
lemma 
nipkow@43141
   196
  "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)"
nipkow@43141
   197
by blast
nipkow@43141
   198
nipkow@43141
   199
lemma triv_if:
nipkow@43141
   200
  "(IF b THEN c ELSE c) \<sim> c"
nipkow@43141
   201
by blast
nipkow@43141
   202
nipkow@43141
   203
lemma commute_if:
nipkow@43141
   204
  "(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2) 
nipkow@43141
   205
   \<sim> 
nipkow@43141
   206
   (IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
nipkow@43141
   207
by blast
nipkow@43141
   208
nipkow@43141
   209
nipkow@43141
   210
subsection "Execution is deterministic"
nipkow@43141
   211
nipkow@43141
   212
text {* This proof is automatic. *}
nipkow@43141
   213
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
nipkow@43141
   214
apply (induct arbitrary: u rule: big_step.induct)
nipkow@43141
   215
apply blast+
nipkow@43141
   216
done
nipkow@43141
   217
nipkow@43141
   218
text {*
nipkow@43141
   219
  This is the proof as you might present it in a lecture. The remaining
nipkow@43141
   220
  cases are simple enough to be proved automatically:
nipkow@43141
   221
*}
nipkow@43141
   222
theorem
nipkow@43141
   223
  "(c,s) \<Rightarrow> t  \<Longrightarrow>  (c,s) \<Rightarrow> t'  \<Longrightarrow>  t' = t"
nipkow@43141
   224
proof (induct arbitrary: t' rule: big_step.induct)
nipkow@43141
   225
  -- "the only interesting case, @{text WhileTrue}:"
nipkow@43141
   226
  fix b c s s1 t t'
nipkow@43141
   227
  -- "The assumptions of the rule:"
nipkow@43141
   228
  assume "bval b s" and "(c,s) \<Rightarrow> s1" and "(WHILE b DO c,s1) \<Rightarrow> t"
nipkow@43141
   229
  -- {* Ind.Hyp; note the @{text"\<And>"} because of arbitrary: *}
nipkow@43141
   230
  assume IHc: "\<And>t'. (c,s) \<Rightarrow> t' \<Longrightarrow> t' = s1"
nipkow@43141
   231
  assume IHw: "\<And>t'. (WHILE b DO c,s1) \<Rightarrow> t' \<Longrightarrow> t' = t"
nipkow@43141
   232
  -- "Premise of implication:"
nipkow@43141
   233
  assume "(WHILE b DO c,s) \<Rightarrow> t'"
nipkow@43141
   234
  with `bval b s` obtain s1' where
nipkow@43141
   235
      c: "(c,s) \<Rightarrow> s1'" and
nipkow@43141
   236
      w: "(WHILE b DO c,s1') \<Rightarrow> t'"
nipkow@43141
   237
    by auto
nipkow@43141
   238
  from c IHc have "s1' = s1" by blast
nipkow@43141
   239
  with w IHw show "t' = t" by blast
nipkow@43141
   240
qed blast+ -- "prove the rest automatically"
nipkow@43141
   241
nipkow@43141
   242
nipkow@43141
   243
end