src/HOL/IMP/Natural.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 37736 2bf3a2cb5e58
child 41529 ba60efa2fd08
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     1 (*  Title:        HOL/IMP/Natural.thy
     2     ID:           $Id$
     3     Author:       Tobias Nipkow & Robert Sandner, TUM
     4     Isar Version: Gerwin Klein, 2001; additional proofs by Lawrence Paulson
     5     Copyright     1996 TUM
     6 *)
     7 
     8 header "Natural Semantics of Commands"
     9 
    10 theory Natural imports Com begin
    11 
    12 subsection "Execution of commands"
    13 
    14 text {*
    15   We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
    16   in state @{text s}, terminates in state @{text s'}}. Formally,
    17   @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} is just another form of saying \emph{the tuple
    18   @{text "(c,s,s')"} is part of the relation @{text evalc}}:
    19 *}
    20 
    21 definition
    22   update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900) where
    23   "update = fun_upd"
    24 
    25 notation (xsymbols)
    26   update  ("_/[_ \<mapsto> /_]" [900,0,0] 900)
    27 
    28 text {* Disable conflicting syntax from HOL Map theory. *}
    29 
    30 no_syntax
    31   "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
    32   "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
    33   ""         :: "maplet => maplets"             ("_")
    34   "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
    35   "_MapUpd"  :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
    36   "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
    37 
    38 text {*
    39   The big-step execution relation @{text evalc} is defined inductively:
    40 *}
    41 inductive
    42   evalc :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
    43 where
    44   Skip:    "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
    45 | Assign:  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
    46 
    47 | Semi:    "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
    48 
    49 | IfTrue:  "b s \<Longrightarrow> \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
    50 | IfFalse: "\<not>b s \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
    51 
    52 | WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s"
    53 | WhileTrue:  "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'
    54                \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'"
    55 
    56 lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
    57 
    58 text {*
    59 The induction principle induced by this definition looks like this:
    60 
    61 @{thm [display] evalc.induct [no_vars]}
    62 
    63 
    64 (@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
    65   meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
    66 *}
    67 
    68 text {*
    69   The rules of @{text evalc} are syntax directed, i.e.~for each
    70   syntactic category there is always only one rule applicable. That
    71   means we can use the rules in both directions.  This property is called rule inversion.
    72 *}
    73 inductive_cases skipE [elim!]:   "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'"
    74 inductive_cases semiE [elim!]:   "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
    75 inductive_cases assignE [elim!]: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'"
    76 inductive_cases ifE [elim!]:     "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
    77 inductive_cases whileE [elim]:  "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s'"
    78 
    79 text {* The next proofs are all trivial by rule inversion.
    80 *}
    81 
    82 inductive_simps
    83   skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'"
    84   and assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'"
    85   and semi: "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
    86 
    87 lemma ifTrue:
    88   "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"
    89   by auto
    90 
    91 lemma ifFalse:
    92   "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'"
    93   by auto
    94 
    95 lemma whileFalse:
    96   "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
    97   by auto
    98 
    99 lemma whileTrue:
   100   "b s \<Longrightarrow>
   101   \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' =
   102   (\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')"
   103   by auto
   104 
   105 text "Again, Isabelle may use these rules in automatic proofs:"
   106 lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue
   107 
   108 subsection "Equivalence of statements"
   109 
   110 text {*
   111   We call two statements @{text c} and @{text c'} equivalent wrt.~the
   112   big-step semantics when \emph{@{text c} started in @{text s} terminates
   113   in @{text s'} iff @{text c'} started in the same @{text s} also terminates
   114   in the same @{text s'}}. Formally:
   115 *}
   116 definition
   117   equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _" [56, 56] 55) where
   118   "c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')"
   119 
   120 text {*
   121   Proof rules telling Isabelle to unfold the definition
   122   if there is something to be proved about equivalent
   123   statements: *}
   124 lemma equivI [intro!]:
   125   "(\<And>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s') \<Longrightarrow> c \<sim> c'"
   126   by (unfold equiv_c_def) blast
   127 
   128 lemma equivD1:
   129   "c \<sim> c' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
   130   by (unfold equiv_c_def) blast
   131 
   132 lemma equivD2:
   133   "c \<sim> c' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s'"
   134   by (unfold equiv_c_def) blast
   135 
   136 text {*
   137   As an example, we show that loop unfolding is an equivalence
   138   transformation on programs:
   139 *}
   140 lemma unfold_while:
   141   "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w \<sim> ?if")
   142 proof -
   143   -- "to show the equivalence, we look at the derivation tree for"
   144   -- "each side and from that construct a derivation tree for the other side"
   145   { fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"
   146     -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
   147     -- "then both statements do nothing:"
   148     hence "\<not>b s \<Longrightarrow> s = s'" by blast
   149     hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   150     moreover
   151     -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
   152     -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"} *}
   153     { assume b: "b s"
   154       with w obtain s'' where
   155         "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
   156       -- "now we can build a derivation tree for the @{text \<IF>}"
   157       -- "first, the body of the True-branch:"
   158       hence "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule Semi)
   159       -- "then the whole @{text \<IF>}"
   160       with b have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule IfTrue)
   161     }
   162     ultimately
   163     -- "both cases together give us what we want:"
   164     have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   165   }
   166   moreover
   167   -- "now the other direction:"
   168   { fix s s' assume "if": "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
   169     -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
   170     -- "of the @{text \<IF>} is executed, and both statements do nothing:"
   171     hence "\<not>b s \<Longrightarrow> s = s'" by blast
   172     hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   173     moreover
   174     -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
   175     -- {* then this time only the @{text IfTrue} rule can have be used *}
   176     { assume b: "b s"
   177       with "if" have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
   178       -- "and for this, only the Semi-rule is applicable:"
   179       then obtain s'' where
   180         "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
   181       -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
   182       with b
   183       have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue)
   184     }
   185     ultimately
   186     -- "both cases together again give us what we want:"
   187     have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   188   }
   189   ultimately
   190   show ?thesis by blast
   191 qed
   192 
   193 text {*
   194    Happily, such lengthy proofs are seldom necessary.  Isabelle can prove many such facts automatically.
   195 *}
   196 
   197 lemma 
   198   "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
   199 by blast
   200 
   201 lemma triv_if:
   202   "(\<IF> b \<THEN> c \<ELSE> c) \<sim> c"
   203 by blast
   204 
   205 lemma commute_if:
   206   "(\<IF> b1 \<THEN> (\<IF> b2 \<THEN> c11 \<ELSE> c12) \<ELSE> c2) 
   207    \<sim> 
   208    (\<IF> b2 \<THEN> (\<IF> b1 \<THEN> c11 \<ELSE> c2) \<ELSE> (\<IF> b1 \<THEN> c12 \<ELSE> c2))"
   209 by blast
   210 
   211 lemma while_equiv:
   212   "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<sim> c' \<Longrightarrow> (c0 = \<WHILE> b \<DO> c) \<Longrightarrow> \<langle>\<WHILE> b \<DO> c', s\<rangle> \<longrightarrow>\<^sub>c u" 
   213 by (induct rule: evalc.induct) (auto simp add: equiv_c_def) 
   214 
   215 lemma equiv_while:
   216   "c \<sim> c' \<Longrightarrow> (\<WHILE> b \<DO> c) \<sim> (\<WHILE> b \<DO> c')"
   217 by (simp add: equiv_c_def) (metis equiv_c_def while_equiv) 
   218 
   219 
   220 text {*
   221     Program equivalence is an equivalence relation.
   222 *}
   223 
   224 lemma equiv_refl:
   225   "c \<sim> c"
   226 by blast
   227 
   228 lemma equiv_sym:
   229   "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c1"
   230 by (auto simp add: equiv_c_def) 
   231 
   232 lemma equiv_trans:
   233   "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c3 \<Longrightarrow> c1 \<sim> c3"
   234 by (auto simp add: equiv_c_def) 
   235 
   236 text {*
   237     Program constructions preserve equivalence.
   238 *}
   239 
   240 lemma equiv_semi:
   241   "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (c1; c2) \<sim> (c1'; c2')"
   242 by (force simp add: equiv_c_def) 
   243 
   244 lemma equiv_if:
   245   "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (\<IF> b \<THEN> c1 \<ELSE> c2) \<sim> (\<IF> b \<THEN> c1' \<ELSE> c2')"
   246 by (force simp add: equiv_c_def) 
   247 
   248 lemma while_never: "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<noteq> \<WHILE> (\<lambda>s. True) \<DO> c1"
   249 apply (induct rule: evalc.induct)
   250 apply auto
   251 done
   252 
   253 lemma equiv_while_True:
   254   "(\<WHILE> (\<lambda>s. True) \<DO> c1) \<sim> (\<WHILE> (\<lambda>s. True) \<DO> c2)" 
   255 by (blast dest: while_never) 
   256 
   257 
   258 subsection "Execution is deterministic"
   259 
   260 text {*
   261 This proof is automatic.
   262 *}
   263 theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = t"
   264 by (induct arbitrary: u rule: evalc.induct) blast+
   265 
   266 
   267 text {*
   268 The following proof presents all the details:
   269 *}
   270 theorem com_det:
   271   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   272   shows "u = t"
   273   using prems
   274 proof (induct arbitrary: u set: evalc)
   275   fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   276   thus "u = s" by blast
   277 next
   278   fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
   279   thus "u = s[x \<mapsto> a s]" by blast
   280 next
   281   fix c0 c1 s s1 s2 u
   282   assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   283   assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   284 
   285   assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
   286   then obtain s' where
   287       c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   288       c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u"
   289     by auto
   290 
   291   from c0 IH0 have "s'=s2" by blast
   292   with c1 IH1 show "u=s1" by blast
   293 next
   294   fix b c0 c1 s s1 u
   295   assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   296 
   297   assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
   298   hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by blast
   299   with IH show "u = s1" by blast
   300 next
   301   fix b c0 c1 s s1 u
   302   assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   303 
   304   assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
   305   hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by blast
   306   with IH show "u = s1" by blast
   307 next
   308   fix b c s u
   309   assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   310   thus "u = s" by blast
   311 next
   312   fix b c s s1 s2 u
   313   assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   314   assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   315 
   316   assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   317   then obtain s' where
   318       c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   319       w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
   320     by auto
   321 
   322   from c "IH\<^sub>c" have "s' = s2" by blast
   323   with w "IH\<^sub>w" show "u = s1" by blast
   324 qed
   325 
   326 
   327 text {*
   328   This is the proof as you might present it in a lecture. The remaining
   329   cases are simple enough to be proved automatically:
   330 *}
   331 theorem
   332   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   333   shows "u = t"
   334   using prems
   335 proof (induct arbitrary: u)
   336   -- "the simple @{text \<SKIP>} case for demonstration:"
   337   fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   338   thus "u = s" by blast
   339 next
   340   -- "and the only really interesting case, @{text \<WHILE>}:"
   341   fix b c s s1 s2 u
   342   assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   343   assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   344 
   345   assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   346   then obtain s' where
   347       c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   348       w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
   349     by auto
   350 
   351   from c "IH\<^sub>c" have "s' = s2" by blast
   352   with w "IH\<^sub>w" show "u = s1" by blast
   353 qed blast+ -- "prove the rest automatically"
   354 
   355 end