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