src/HOL/IMP/Big_Step.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 61337 4645502c3c64
child 64530 a720c3911308
permissions -rw-r--r--
Lots of new material for multivariate analysis
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
kleing@52370
     7
text {*
kleing@52370
     8
The big-step semantics is a straight-forward inductive definition
hoelzl@59451
     9
with concrete syntax. Note that the first parameter is a tuple,
kleing@52370
    10
so the syntax becomes @{text "(c,s) \<Rightarrow> s'"}.
kleing@52370
    11
*}
kleing@52370
    12
nipkow@49191
    13
text_raw{*\snip{BigStepdef}{0}{1}{% *}
nipkow@43141
    14
inductive
nipkow@43141
    15
  big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
nipkow@43141
    16
where
kleing@52391
    17
Skip: "(SKIP,s) \<Rightarrow> s" |
kleing@52391
    18
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
wenzelm@53015
    19
Seq: "\<lbrakk> (c\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2;  (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
wenzelm@53015
    20
IfTrue: "\<lbrakk> bval b s;  (c\<^sub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
wenzelm@53015
    21
IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^sub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
nipkow@43141
    22
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
kleing@52391
    23
WhileTrue:
wenzelm@53015
    24
"\<lbrakk> bval b s\<^sub>1;  (c,s\<^sub>1) \<Rightarrow> s\<^sub>2;  (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> 
wenzelm@53015
    25
\<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3"
nipkow@49191
    26
text_raw{*}%endsnip*}
nipkow@43141
    27
nipkow@49191
    28
text_raw{*\snip{BigStepEx}{1}{2}{% *}
wenzelm@61337
    29
schematic_goal ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
nipkow@47818
    30
apply(rule Seq)
nipkow@43141
    31
apply(rule Assign)
nipkow@43141
    32
apply simp
nipkow@43141
    33
apply(rule Assign)
nipkow@43141
    34
done
nipkow@49191
    35
text_raw{*}%endsnip*}
nipkow@43141
    36
nipkow@43141
    37
thm ex[simplified]
nipkow@43141
    38
nipkow@43141
    39
text{* We want to execute the big-step rules: *}
nipkow@43141
    40
nipkow@43141
    41
code_pred big_step .
nipkow@43141
    42
nipkow@43141
    43
text{* For inductive definitions we need command
nipkow@43141
    44
       \texttt{values} instead of \texttt{value}. *}
nipkow@43141
    45
nipkow@44923
    46
values "{t. (SKIP, \<lambda>_. 0) \<Rightarrow> t}"
nipkow@43141
    47
nipkow@43141
    48
text{* We need to translate the result state into a list
nipkow@43141
    49
to display it. *}
nipkow@43141
    50
kleing@44036
    51
values "{map t [''x''] |t. (SKIP, <''x'' := 42>) \<Rightarrow> t}"
nipkow@43141
    52
kleing@44036
    53
values "{map t [''x''] |t. (''x'' ::= N 2, <''x'' := 42>) \<Rightarrow> t}"
nipkow@43141
    54
nipkow@43141
    55
values "{map t [''x'',''y''] |t.
nipkow@43141
    56
  (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
kleing@44036
    57
   <''x'' := 0, ''y'' := 13>) \<Rightarrow> t}"
nipkow@43141
    58
nipkow@43141
    59
nipkow@43141
    60
text{* Proof automation: *}
nipkow@43141
    61
kleing@52370
    62
text {* The introduction rules are good for automatically
kleing@52370
    63
construction small program executions. The recursive cases
kleing@52370
    64
may require backtracking, so we declare the set as unsafe
kleing@52370
    65
intro rules. *}
nipkow@43141
    66
declare big_step.intros [intro]
nipkow@43141
    67
nipkow@43141
    68
text{* The standard induction rule 
nipkow@43141
    69
@{thm [display] big_step.induct [no_vars]} *}
nipkow@43141
    70
nipkow@43141
    71
thm big_step.induct
nipkow@43141
    72
kleing@52370
    73
text{*
kleing@52370
    74
This induction schema is almost perfect for our purposes, but
kleing@52370
    75
our trick for reusing the tuple syntax means that the induction
kleing@52370
    76
schema has two parameters instead of the @{text c}, @{text s},
kleing@52370
    77
and @{text s'} that we are likely to encounter. Splitting
kleing@52370
    78
the tuple parameter fixes this:
kleing@52370
    79
*}
nipkow@43141
    80
lemmas big_step_induct = big_step.induct[split_format(complete)]
nipkow@43141
    81
thm big_step_induct
nipkow@43141
    82
text {*
nipkow@43141
    83
@{thm [display] big_step_induct [no_vars]}
nipkow@43141
    84
*}
nipkow@43141
    85
nipkow@43141
    86
nipkow@43141
    87
subsection "Rule inversion"
nipkow@43141
    88
nipkow@43141
    89
text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ?
nipkow@43141
    90
That @{prop "s = t"}. This is how we can automatically prove it: *}
nipkow@43141
    91
nipkow@51513
    92
inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t"
nipkow@51513
    93
thm SkipE
nipkow@43141
    94
nipkow@43141
    95
text{* This is an \emph{elimination rule}. The [elim] attribute tells auto,
nipkow@43141
    96
blast and friends (but not simp!) to use it automatically; [elim!] means that
nipkow@43141
    97
it is applied eagerly.
nipkow@43141
    98
nipkow@43141
    99
Similarly for the other commands: *}
nipkow@43141
   100
nipkow@43141
   101
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
nipkow@43141
   102
thm AssignE
nipkow@52046
   103
inductive_cases SeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
nipkow@47818
   104
thm SeqE
nipkow@43141
   105
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
nipkow@43141
   106
thm IfE
nipkow@43141
   107
nipkow@43141
   108
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
nipkow@43141
   109
thm WhileE
nipkow@43141
   110
text{* Only [elim]: [elim!] would not terminate. *}
nipkow@43141
   111
nipkow@43141
   112
text{* An automatic example: *}
nipkow@43141
   113
nipkow@43141
   114
lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s"
nipkow@43141
   115
by blast
nipkow@43141
   116
nipkow@43141
   117
text{* Rule inversion by hand via the ``cases'' method: *}
nipkow@43141
   118
nipkow@43141
   119
lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t"
nipkow@43141
   120
shows "t = s"
nipkow@43141
   121
proof-
nipkow@43141
   122
  from assms show ?thesis
nipkow@43141
   123
  proof cases  --"inverting assms"
nipkow@43141
   124
    case IfTrue thm IfTrue
nipkow@43141
   125
    thus ?thesis by blast
nipkow@43141
   126
  next
nipkow@43141
   127
    case IfFalse thus ?thesis by blast
nipkow@43141
   128
  qed
nipkow@43141
   129
qed
nipkow@43141
   130
kleing@44070
   131
(* Using rule inversion to prove simplification rules: *)
kleing@44070
   132
lemma assign_simp:
kleing@44070
   133
  "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
kleing@44070
   134
  by auto
nipkow@43141
   135
kleing@52376
   136
text {* An example combining rule inversion and derivations *}
nipkow@52399
   137
lemma Seq_assoc:
kleing@52376
   138
  "(c1;; c2;; c3, s) \<Rightarrow> s' \<longleftrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> s'"
kleing@52376
   139
proof
kleing@52376
   140
  assume "(c1;; c2;; c3, s) \<Rightarrow> s'"
kleing@52376
   141
  then obtain s1 s2 where
kleing@52376
   142
    c1: "(c1, s) \<Rightarrow> s1" and
kleing@52376
   143
    c2: "(c2, s1) \<Rightarrow> s2" and
kleing@52376
   144
    c3: "(c3, s2) \<Rightarrow> s'" by auto
kleing@52376
   145
  from c2 c3
kleing@52376
   146
  have "(c2;; c3, s1) \<Rightarrow> s'" by (rule Seq)
kleing@52376
   147
  with c1
kleing@52376
   148
  show "(c1;; (c2;; c3), s) \<Rightarrow> s'" by (rule Seq)
kleing@52376
   149
next
kleing@52376
   150
  -- "The other direction is analogous"
kleing@52376
   151
  assume "(c1;; (c2;; c3), s) \<Rightarrow> s'"
kleing@52376
   152
  thus "(c1;; c2;; c3, s) \<Rightarrow> s'" by auto
kleing@52376
   153
qed
kleing@52376
   154
kleing@52376
   155
nipkow@43141
   156
subsection "Command Equivalence"
nipkow@43141
   157
nipkow@43141
   158
text {*
nipkow@43141
   159
  We call two statements @{text c} and @{text c'} equivalent wrt.\ the
nipkow@43141
   160
  big-step semantics when \emph{@{text c} started in @{text s} terminates
nipkow@43141
   161
  in @{text s'} iff @{text c'} started in the same @{text s} also terminates
nipkow@43141
   162
  in the same @{text s'}}. Formally:
nipkow@43141
   163
*}
nipkow@49191
   164
text_raw{*\snip{BigStepEquiv}{0}{1}{% *}
nipkow@43141
   165
abbreviation
nipkow@43141
   166
  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
kleing@52372
   167
  "c \<sim> c' \<equiv> (\<forall>s t. (c,s) \<Rightarrow> t  =  (c',s) \<Rightarrow> t)"
nipkow@49191
   168
text_raw{*}%endsnip*}
nipkow@43141
   169
nipkow@43141
   170
text {*
nipkow@43141
   171
Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces).
nipkow@43141
   172
nipkow@43141
   173
  As an example, we show that loop unfolding is an equivalence
nipkow@43141
   174
  transformation on programs:
nipkow@43141
   175
*}
nipkow@43141
   176
lemma unfold_while:
nipkow@52046
   177
  "(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
nipkow@43141
   178
proof -
nipkow@43141
   179
  -- "to show the equivalence, we look at the derivation tree for"
nipkow@43141
   180
  -- "each side and from that construct a derivation tree for the other side"
nipkow@43141
   181
  { fix s t assume "(?w, s) \<Rightarrow> t"
nipkow@43141
   182
    -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
nipkow@43141
   183
    -- "then both statements do nothing:"
nipkow@43141
   184
    { assume "\<not>bval b s"
nipkow@43141
   185
      hence "t = s" using `(?w,s) \<Rightarrow> t` by blast
nipkow@43141
   186
      hence "(?iw, s) \<Rightarrow> t" using `\<not>bval b s` by blast
nipkow@43141
   187
    }
nipkow@43141
   188
    moreover
nipkow@43141
   189
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
nipkow@43141
   190
    -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"} *}
nipkow@43141
   191
    { assume "bval b s"
nipkow@43141
   192
      with `(?w, s) \<Rightarrow> t` obtain s' where
nipkow@43141
   193
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
nipkow@43141
   194
      -- "now we can build a derivation tree for the @{text IF}"
nipkow@43141
   195
      -- "first, the body of the True-branch:"
nipkow@52046
   196
      hence "(c;; ?w, s) \<Rightarrow> t" by (rule Seq)
nipkow@43141
   197
      -- "then the whole @{text IF}"
nipkow@43141
   198
      with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue)
nipkow@43141
   199
    }
nipkow@43141
   200
    ultimately
nipkow@43141
   201
    -- "both cases together give us what we want:"
nipkow@43141
   202
    have "(?iw, s) \<Rightarrow> t" by blast
nipkow@43141
   203
  }
nipkow@43141
   204
  moreover
nipkow@43141
   205
  -- "now the other direction:"
nipkow@43141
   206
  { fix s t assume "(?iw, s) \<Rightarrow> t"
nipkow@43141
   207
    -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
nipkow@43141
   208
    -- "of the @{text IF} is executed, and both statements do nothing:"
nipkow@43141
   209
    { assume "\<not>bval b s"
nipkow@43141
   210
      hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast
nipkow@43141
   211
      hence "(?w, s) \<Rightarrow> t" using `\<not>bval b s` by blast
nipkow@43141
   212
    }
nipkow@43141
   213
    moreover
nipkow@43141
   214
    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
nipkow@43141
   215
    -- {* then this time only the @{text IfTrue} rule can have be used *}
nipkow@43141
   216
    { assume "bval b s"
nipkow@52046
   217
      with `(?iw, s) \<Rightarrow> t` have "(c;; ?w, s) \<Rightarrow> t" by auto
nipkow@47818
   218
      -- "and for this, only the Seq-rule is applicable:"
nipkow@43141
   219
      then obtain s' where
nipkow@43141
   220
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
nipkow@43141
   221
      -- "with this information, we can build a derivation tree for the @{text WHILE}"
nipkow@43141
   222
      with `bval b s`
nipkow@43141
   223
      have "(?w, s) \<Rightarrow> t" by (rule WhileTrue)
nipkow@43141
   224
    }
nipkow@43141
   225
    ultimately
nipkow@43141
   226
    -- "both cases together again give us what we want:"
nipkow@43141
   227
    have "(?w, s) \<Rightarrow> t" by blast
nipkow@43141
   228
  }
nipkow@43141
   229
  ultimately
nipkow@43141
   230
  show ?thesis by blast
nipkow@43141
   231
qed
nipkow@43141
   232
nipkow@43141
   233
text {* Luckily, such lengthy proofs are seldom necessary.  Isabelle can
nipkow@43141
   234
prove many such facts automatically.  *}
nipkow@43141
   235
kleing@45321
   236
lemma while_unfold:
nipkow@52046
   237
  "(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)"
nipkow@43141
   238
by blast
nipkow@43141
   239
nipkow@43141
   240
lemma triv_if:
nipkow@43141
   241
  "(IF b THEN c ELSE c) \<sim> c"
nipkow@43141
   242
by blast
nipkow@43141
   243
nipkow@43141
   244
lemma commute_if:
nipkow@43141
   245
  "(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2) 
nipkow@43141
   246
   \<sim> 
nipkow@43141
   247
   (IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
nipkow@43141
   248
by blast
nipkow@43141
   249
nipkow@51513
   250
lemma sim_while_cong_aux:
nipkow@51513
   251
  "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow> c \<sim> c' \<Longrightarrow>  (WHILE b DO c',s) \<Rightarrow> t"
nipkow@51513
   252
apply(induction "WHILE b DO c" s t arbitrary: b c rule: big_step_induct)
nipkow@51513
   253
 apply blast
nipkow@51513
   254
apply blast
nipkow@51513
   255
done
nipkow@51513
   256
nipkow@51513
   257
lemma sim_while_cong: "c \<sim> c' \<Longrightarrow> WHILE b DO c \<sim> WHILE b DO c'"
nipkow@51513
   258
by (metis sim_while_cong_aux)
nipkow@51513
   259
kleing@52021
   260
text {* Command equivalence is an equivalence relation, i.e.\ it is
kleing@52021
   261
reflexive, symmetric, and transitive. Because we used an abbreviation
kleing@52021
   262
above, Isabelle derives this automatically. *}
kleing@52021
   263
kleing@52021
   264
lemma sim_refl:  "c \<sim> c" by simp
kleing@52021
   265
lemma sim_sym:   "(c \<sim> c') = (c' \<sim> c)" by auto
kleing@52021
   266
lemma sim_trans: "c \<sim> c' \<Longrightarrow> c' \<sim> c'' \<Longrightarrow> c \<sim> c''" by auto
nipkow@43141
   267
nipkow@43141
   268
subsection "Execution is deterministic"
nipkow@43141
   269
nipkow@43141
   270
text {* This proof is automatic. *}
nipkow@54192
   271
nipkow@43141
   272
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
kleing@45321
   273
  by (induction arbitrary: u rule: big_step.induct) blast+
nipkow@43141
   274
nipkow@43141
   275
text {*
nipkow@43141
   276
  This is the proof as you might present it in a lecture. The remaining
nipkow@43141
   277
  cases are simple enough to be proved automatically:
nipkow@43141
   278
*}
nipkow@49191
   279
text_raw{*\snip{BigStepDetLong}{0}{2}{% *}
nipkow@43141
   280
theorem
nipkow@43141
   281
  "(c,s) \<Rightarrow> t  \<Longrightarrow>  (c,s) \<Rightarrow> t'  \<Longrightarrow>  t' = t"
nipkow@45015
   282
proof (induction arbitrary: t' rule: big_step.induct)
nipkow@43141
   283
  -- "the only interesting case, @{text WhileTrue}:"
wenzelm@53015
   284
  fix b c s s\<^sub>1 t t'
nipkow@43141
   285
  -- "The assumptions of the rule:"
wenzelm@53015
   286
  assume "bval b s" and "(c,s) \<Rightarrow> s\<^sub>1" and "(WHILE b DO c,s\<^sub>1) \<Rightarrow> t"
nipkow@43141
   287
  -- {* Ind.Hyp; note the @{text"\<And>"} because of arbitrary: *}
wenzelm@53015
   288
  assume IHc: "\<And>t'. (c,s) \<Rightarrow> t' \<Longrightarrow> t' = s\<^sub>1"
wenzelm@53015
   289
  assume IHw: "\<And>t'. (WHILE b DO c,s\<^sub>1) \<Rightarrow> t' \<Longrightarrow> t' = t"
nipkow@43141
   290
  -- "Premise of implication:"
nipkow@43141
   291
  assume "(WHILE b DO c,s) \<Rightarrow> t'"
wenzelm@53015
   292
  with `bval b s` obtain s\<^sub>1' where
wenzelm@53015
   293
      c: "(c,s) \<Rightarrow> s\<^sub>1'" and
wenzelm@53015
   294
      w: "(WHILE b DO c,s\<^sub>1') \<Rightarrow> t'"
nipkow@43141
   295
    by auto
wenzelm@53015
   296
  from c IHc have "s\<^sub>1' = s\<^sub>1" by blast
nipkow@43141
   297
  with w IHw show "t' = t" by blast
nipkow@43141
   298
qed blast+ -- "prove the rest automatically"
nipkow@49191
   299
text_raw{*}%endsnip*}
nipkow@43141
   300
nipkow@43141
   301
end