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