src/HOL/IMP/Natural.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 20503 503ac4c5ef91
child 23746 a455e69c31cc
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 (*  Title:        HOL/IMP/Natural.thy
     2     ID:           $Id$
     3     Author:       Tobias Nipkow & Robert Sandner, TUM
     4     Isar Version: Gerwin Klein, 2001
     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 consts  evalc   :: "(com \<times> state \<times> state) set"
    15 syntax "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("<_,_>/ -c-> _" [0,0,60] 60)
    16 
    17 syntax (xsymbols)
    18   "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
    19 
    20 syntax (HTML output)
    21   "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
    22 
    23 text {*
    24   We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
    25   in state @{text s}, terminates in state @{text s'}}. Formally,
    26   @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} is just another form of saying \emph{the tuple
    27   @{text "(c,s,s')"} is part of the relation @{text evalc}}:
    28 *}
    29 translations  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" == "(c,s,s') \<in> evalc"
    30 
    31 constdefs
    32   update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
    33   "update == fun_upd"
    34 
    35 syntax (xsymbols)
    36   update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)
    37 
    38 text {*
    39   The big-step execution relation @{text evalc} is defined inductively:
    40 *}
    41 inductive evalc
    42   intros
    43   Skip:    "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
    44   Assign:  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
    45 
    46   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'"
    47 
    48   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'"
    49   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'"
    50 
    51   WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s"
    52   WhileTrue:  "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'
    53                \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'"
    54 
    55 lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
    56 
    57 text {*
    58 The induction principle induced by this definition looks like this:
    59 
    60 @{thm [display] evalc.induct [no_vars]}
    61 
    62 
    63 (@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
    64   meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
    65 *}
    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. The proofs for this
    72   are all the same: one direction is trivial, the other one is shown
    73   by using the @{text evalc} rules backwards:
    74 *}
    75 lemma skip:
    76   "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
    77   by (rule, erule evalc.elims) auto
    78 
    79 lemma assign:
    80   "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])"
    81   by (rule, erule evalc.elims) auto
    82 
    83 lemma semi:
    84   "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s' = (\<exists>s''. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s')"
    85   by (rule, erule evalc.elims) auto
    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 (rule, erule evalc.elims) 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 (rule, erule evalc.elims) 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 (rule, erule evalc.elims) 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 (rule, erule evalc.elims) 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 constdefs
   117   equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
   118   "c \<sim> c' \<equiv> \<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 simp
   149     hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
   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 simp
   172     hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
   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 
   194 subsection "Execution is deterministic"
   195 
   196 text {*
   197 The following proof presents all the details:
   198 *}
   199 theorem com_det:
   200   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   201   shows "u = t"
   202   using prems
   203 proof (induct arbitrary: u set: evalc)
   204   fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   205   thus "u = s" by simp
   206 next
   207   fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
   208   thus "u = s[x \<mapsto> a s]" by simp
   209 next
   210   fix c0 c1 s s1 s2 u
   211   assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   212   assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   213 
   214   assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
   215   then obtain s' where
   216       c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   217       c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u"
   218     by auto
   219 
   220   from c0 IH0 have "s'=s2" by blast
   221   with c1 IH1 show "u=s1" by blast
   222 next
   223   fix b c0 c1 s s1 u
   224   assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   225 
   226   assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
   227   hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
   228   with IH show "u = s1" by blast
   229 next
   230   fix b c0 c1 s s1 u
   231   assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   232 
   233   assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
   234   hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
   235   with IH show "u = s1" by blast
   236 next
   237   fix b c s u
   238   assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   239   thus "u = s" by simp
   240 next
   241   fix b c s s1 s2 u
   242   assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   243   assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   244 
   245   assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   246   then obtain s' where
   247       c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   248       w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
   249     by auto
   250 
   251   from c "IH\<^sub>c" have "s' = s2" by blast
   252   with w "IH\<^sub>w" show "u = s1" by blast
   253 qed
   254 
   255 
   256 text {*
   257   This is the proof as you might present it in a lecture. The remaining
   258   cases are simple enough to be proved automatically:
   259 *}
   260 theorem
   261   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   262   shows "u = t"
   263   using prems
   264 proof (induct arbitrary: u)
   265   -- "the simple @{text \<SKIP>} case for demonstration:"
   266   fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   267   thus "u = s" by simp
   268 next
   269   -- "and the only really interesting case, @{text \<WHILE>}:"
   270   fix b c s s1 s2 u
   271   assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   272   assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   273 
   274   assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   275   then obtain s' where
   276       c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   277       w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
   278     by auto
   279 
   280   from c "IH\<^sub>c" have "s' = s2" by blast
   281   with w "IH\<^sub>w" show "u = s1" by blast
   282 qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
   283 
   284 end