src/HOL/IMP/Big_Step.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45015 fdac1e9880eb
child 45321 b227989b6ee6
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
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
nipkow@44923
    40
values "{t. (SKIP, \<lambda>_. 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@44036
    45
values "{map t [''x''] |t. (SKIP, <''x'' := 42>) \<Rightarrow> t}"
nipkow@43141
    46
kleing@44036
    47
values "{map t [''x''] |t. (''x'' ::= N 2, <''x'' := 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@44036
    51
   <''x'' := 0, ''y'' := 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
kleing@44070
   116
(* Using rule inversion to prove simplification rules: *)
kleing@44070
   117
lemma assign_simp:
kleing@44070
   118
  "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
kleing@44070
   119
  by auto
nipkow@43141
   120
nipkow@43141
   121
subsection "Command Equivalence"
nipkow@43141
   122
nipkow@43141
   123
text {*
nipkow@43141
   124
  We call two statements @{text c} and @{text c'} equivalent wrt.\ the
nipkow@43141
   125
  big-step semantics when \emph{@{text c} started in @{text s} terminates
nipkow@43141
   126
  in @{text s'} iff @{text c'} started in the same @{text s} also terminates
nipkow@43141
   127
  in the same @{text s'}}. Formally:
nipkow@43141
   128
*}
nipkow@43141
   129
abbreviation
nipkow@43141
   130
  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
nipkow@43141
   131
  "c \<sim> c' == (\<forall>s t. (c,s) \<Rightarrow> t  =  (c',s) \<Rightarrow> t)"
nipkow@43141
   132
nipkow@43141
   133
text {*
nipkow@43141
   134
Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces).
nipkow@43141
   135
nipkow@43141
   136
  As an example, we show that loop unfolding is an equivalence
nipkow@43141
   137
  transformation on programs:
nipkow@43141
   138
*}
nipkow@43141
   139
lemma unfold_while:
nipkow@43141
   140
  "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
nipkow@43141
   141
proof -
nipkow@43141
   142
  -- "to show the equivalence, we look at the derivation tree for"
nipkow@43141
   143
  -- "each side and from that construct a derivation tree for the other side"
nipkow@43141
   144
  { fix s t assume "(?w, s) \<Rightarrow> t"
nipkow@43141
   145
    -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
nipkow@43141
   146
    -- "then both statements do nothing:"
nipkow@43141
   147
    { assume "\<not>bval b s"
nipkow@43141
   148
      hence "t = s" using `(?w,s) \<Rightarrow> t` by blast
nipkow@43141
   149
      hence "(?iw, s) \<Rightarrow> t" using `\<not>bval b s` by blast
nipkow@43141
   150
    }
nipkow@43141
   151
    moreover
nipkow@43141
   152
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
nipkow@43141
   153
    -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"} *}
nipkow@43141
   154
    { assume "bval b s"
nipkow@43141
   155
      with `(?w, s) \<Rightarrow> t` obtain s' where
nipkow@43141
   156
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
nipkow@43141
   157
      -- "now we can build a derivation tree for the @{text IF}"
nipkow@43141
   158
      -- "first, the body of the True-branch:"
nipkow@43141
   159
      hence "(c; ?w, s) \<Rightarrow> t" by (rule Semi)
nipkow@43141
   160
      -- "then the whole @{text IF}"
nipkow@43141
   161
      with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue)
nipkow@43141
   162
    }
nipkow@43141
   163
    ultimately
nipkow@43141
   164
    -- "both cases together give us what we want:"
nipkow@43141
   165
    have "(?iw, s) \<Rightarrow> t" by blast
nipkow@43141
   166
  }
nipkow@43141
   167
  moreover
nipkow@43141
   168
  -- "now the other direction:"
nipkow@43141
   169
  { fix s t assume "(?iw, s) \<Rightarrow> t"
nipkow@43141
   170
    -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
nipkow@43141
   171
    -- "of the @{text IF} is executed, and both statements do nothing:"
nipkow@43141
   172
    { assume "\<not>bval b s"
nipkow@43141
   173
      hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast
nipkow@43141
   174
      hence "(?w, s) \<Rightarrow> t" using `\<not>bval b s` by blast
nipkow@43141
   175
    }
nipkow@43141
   176
    moreover
nipkow@43141
   177
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
nipkow@43141
   178
    -- {* then this time only the @{text IfTrue} rule can have be used *}
nipkow@43141
   179
    { assume "bval b s"
nipkow@43141
   180
      with `(?iw, s) \<Rightarrow> t` have "(c; ?w, s) \<Rightarrow> t" by auto
nipkow@43141
   181
      -- "and for this, only the Semi-rule is applicable:"
nipkow@43141
   182
      then obtain s' where
nipkow@43141
   183
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
nipkow@43141
   184
      -- "with this information, we can build a derivation tree for the @{text WHILE}"
nipkow@43141
   185
      with `bval b s`
nipkow@43141
   186
      have "(?w, s) \<Rightarrow> t" by (rule WhileTrue)
nipkow@43141
   187
    }
nipkow@43141
   188
    ultimately
nipkow@43141
   189
    -- "both cases together again give us what we want:"
nipkow@43141
   190
    have "(?w, s) \<Rightarrow> t" by blast
nipkow@43141
   191
  }
nipkow@43141
   192
  ultimately
nipkow@43141
   193
  show ?thesis by blast
nipkow@43141
   194
qed
nipkow@43141
   195
nipkow@43141
   196
text {* Luckily, such lengthy proofs are seldom necessary.  Isabelle can
nipkow@43141
   197
prove many such facts automatically.  *}
nipkow@43141
   198
nipkow@43141
   199
lemma 
nipkow@43141
   200
  "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)"
nipkow@43141
   201
by blast
nipkow@43141
   202
nipkow@43141
   203
lemma triv_if:
nipkow@43141
   204
  "(IF b THEN c ELSE c) \<sim> c"
nipkow@43141
   205
by blast
nipkow@43141
   206
nipkow@43141
   207
lemma commute_if:
nipkow@43141
   208
  "(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2) 
nipkow@43141
   209
   \<sim> 
nipkow@43141
   210
   (IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
nipkow@43141
   211
by blast
nipkow@43141
   212
nipkow@43141
   213
nipkow@43141
   214
subsection "Execution is deterministic"
nipkow@43141
   215
nipkow@43141
   216
text {* This proof is automatic. *}
nipkow@43141
   217
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
nipkow@45015
   218
apply (induction arbitrary: u rule: big_step.induct)
nipkow@43141
   219
apply blast+
nipkow@43141
   220
done
nipkow@43141
   221
nipkow@43141
   222
text {*
nipkow@43141
   223
  This is the proof as you might present it in a lecture. The remaining
nipkow@43141
   224
  cases are simple enough to be proved automatically:
nipkow@43141
   225
*}
nipkow@43141
   226
theorem
nipkow@43141
   227
  "(c,s) \<Rightarrow> t  \<Longrightarrow>  (c,s) \<Rightarrow> t'  \<Longrightarrow>  t' = t"
nipkow@45015
   228
proof (induction arbitrary: t' rule: big_step.induct)
nipkow@43141
   229
  -- "the only interesting case, @{text WhileTrue}:"
nipkow@43141
   230
  fix b c s s1 t t'
nipkow@43141
   231
  -- "The assumptions of the rule:"
nipkow@43141
   232
  assume "bval b s" and "(c,s) \<Rightarrow> s1" and "(WHILE b DO c,s1) \<Rightarrow> t"
nipkow@43141
   233
  -- {* Ind.Hyp; note the @{text"\<And>"} because of arbitrary: *}
nipkow@43141
   234
  assume IHc: "\<And>t'. (c,s) \<Rightarrow> t' \<Longrightarrow> t' = s1"
nipkow@43141
   235
  assume IHw: "\<And>t'. (WHILE b DO c,s1) \<Rightarrow> t' \<Longrightarrow> t' = t"
nipkow@43141
   236
  -- "Premise of implication:"
nipkow@43141
   237
  assume "(WHILE b DO c,s) \<Rightarrow> t'"
nipkow@43141
   238
  with `bval b s` obtain s1' where
nipkow@43141
   239
      c: "(c,s) \<Rightarrow> s1'" and
nipkow@43141
   240
      w: "(WHILE b DO c,s1') \<Rightarrow> t'"
nipkow@43141
   241
    by auto
nipkow@43141
   242
  from c IHc have "s1' = s1" by blast
nipkow@43141
   243
  with w IHw show "t' = t" by blast
nipkow@43141
   244
qed blast+ -- "prove the rest automatically"
nipkow@43141
   245
nipkow@43141
   246
nipkow@43141
   247
end