src/HOL/IMP/Natural.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 23746 a455e69c31cc
child 27362 a6dc1769fdda
permissions -rw-r--r--
avoid rebinding of existing facts;
     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 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 constdefs
    22   update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
    23   "update == fun_upd"
    24 
    25 syntax (xsymbols)
    26   update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)
    27 
    28 text {*
    29   The big-step execution relation @{text evalc} is defined inductively:
    30 *}
    31 inductive
    32   evalc :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
    33 where
    34   Skip:    "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
    35 | Assign:  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
    36 
    37 | 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'"
    38 
    39 | 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'"
    40 | 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'"
    41 
    42 | WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s"
    43 | WhileTrue:  "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'
    44                \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'"
    45 
    46 lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
    47 
    48 text {*
    49 The induction principle induced by this definition looks like this:
    50 
    51 @{thm [display] evalc.induct [no_vars]}
    52 
    53 
    54 (@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
    55   meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
    56 *}
    57 
    58 
    59 text {*
    60   The rules of @{text evalc} are syntax directed, i.e.~for each
    61   syntactic category there is always only one rule applicable. That
    62   means we can use the rules in both directions. The proofs for this
    63   are all the same: one direction is trivial, the other one is shown
    64   by using the @{text evalc} rules backwards:
    65 *}
    66 lemma skip:
    67   "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
    68   by (rule, erule evalc.cases) auto
    69 
    70 lemma assign:
    71   "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])"
    72   by (rule, erule evalc.cases) auto
    73 
    74 lemma semi:
    75   "\<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')"
    76   by (rule, erule evalc.cases) auto
    77 
    78 lemma ifTrue:
    79   "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"
    80   by (rule, erule evalc.cases) auto
    81 
    82 lemma ifFalse:
    83   "\<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'"
    84   by (rule, erule evalc.cases) auto
    85 
    86 lemma whileFalse:
    87   "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
    88   by (rule, erule evalc.cases) auto
    89 
    90 lemma whileTrue:
    91   "b s \<Longrightarrow>
    92   \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' =
    93   (\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')"
    94   by (rule, erule evalc.cases) auto
    95 
    96 text "Again, Isabelle may use these rules in automatic proofs:"
    97 lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue
    98 
    99 subsection "Equivalence of statements"
   100 
   101 text {*
   102   We call two statements @{text c} and @{text c'} equivalent wrt.~the
   103   big-step semantics when \emph{@{text c} started in @{text s} terminates
   104   in @{text s'} iff @{text c'} started in the same @{text s} also terminates
   105   in the same @{text s'}}. Formally:
   106 *}
   107 constdefs
   108   equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
   109   "c \<sim> c' \<equiv> \<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
   110 
   111 text {*
   112   Proof rules telling Isabelle to unfold the definition
   113   if there is something to be proved about equivalent
   114   statements: *}
   115 lemma equivI [intro!]:
   116   "(\<And>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s') \<Longrightarrow> c \<sim> c'"
   117   by (unfold equiv_c_def) blast
   118 
   119 lemma equivD1:
   120   "c \<sim> c' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
   121   by (unfold equiv_c_def) blast
   122 
   123 lemma equivD2:
   124   "c \<sim> c' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s'"
   125   by (unfold equiv_c_def) blast
   126 
   127 text {*
   128   As an example, we show that loop unfolding is an equivalence
   129   transformation on programs:
   130 *}
   131 lemma unfold_while:
   132   "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w \<sim> ?if")
   133 proof -
   134   -- "to show the equivalence, we look at the derivation tree for"
   135   -- "each side and from that construct a derivation tree for the other side"
   136   { fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"
   137     -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
   138     -- "then both statements do nothing:"
   139     hence "\<not>b s \<Longrightarrow> s = s'" by simp
   140     hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
   141     moreover
   142     -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
   143     -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"} *}
   144     { assume b: "b s"
   145       with w obtain s'' where
   146         "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
   147       -- "now we can build a derivation tree for the @{text \<IF>}"
   148       -- "first, the body of the True-branch:"
   149       hence "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule Semi)
   150       -- "then the whole @{text \<IF>}"
   151       with b have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule IfTrue)
   152     }
   153     ultimately
   154     -- "both cases together give us what we want:"
   155     have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   156   }
   157   moreover
   158   -- "now the other direction:"
   159   { fix s s' assume "if": "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
   160     -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
   161     -- "of the @{text \<IF>} is executed, and both statements do nothing:"
   162     hence "\<not>b s \<Longrightarrow> s = s'" by simp
   163     hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
   164     moreover
   165     -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
   166     -- {* then this time only the @{text IfTrue} rule can have be used *}
   167     { assume b: "b s"
   168       with "if" have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
   169       -- "and for this, only the Semi-rule is applicable:"
   170       then obtain s'' where
   171         "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
   172       -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
   173       with b
   174       have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue)
   175     }
   176     ultimately
   177     -- "both cases together again give us what we want:"
   178     have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   179   }
   180   ultimately
   181   show ?thesis by blast
   182 qed
   183 
   184 
   185 subsection "Execution is deterministic"
   186 
   187 text {*
   188 The following proof presents all the details:
   189 *}
   190 theorem com_det:
   191   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   192   shows "u = t"
   193   using prems
   194 proof (induct arbitrary: u set: evalc)
   195   fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   196   thus "u = s" by simp
   197 next
   198   fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
   199   thus "u = s[x \<mapsto> a s]" by simp
   200 next
   201   fix c0 c1 s s1 s2 u
   202   assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   203   assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   204 
   205   assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
   206   then obtain s' where
   207       c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   208       c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u"
   209     by auto
   210 
   211   from c0 IH0 have "s'=s2" by blast
   212   with c1 IH1 show "u=s1" by blast
   213 next
   214   fix b c0 c1 s s1 u
   215   assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   216 
   217   assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
   218   hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
   219   with IH show "u = s1" by blast
   220 next
   221   fix b c0 c1 s s1 u
   222   assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   223 
   224   assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
   225   hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
   226   with IH show "u = s1" by blast
   227 next
   228   fix b c s u
   229   assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   230   thus "u = s" by simp
   231 next
   232   fix b c s s1 s2 u
   233   assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   234   assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   235 
   236   assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   237   then obtain s' where
   238       c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   239       w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
   240     by auto
   241 
   242   from c "IH\<^sub>c" have "s' = s2" by blast
   243   with w "IH\<^sub>w" show "u = s1" by blast
   244 qed
   245 
   246 
   247 text {*
   248   This is the proof as you might present it in a lecture. The remaining
   249   cases are simple enough to be proved automatically:
   250 *}
   251 theorem
   252   assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   253   shows "u = t"
   254   using prems
   255 proof (induct arbitrary: u)
   256   -- "the simple @{text \<SKIP>} case for demonstration:"
   257   fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   258   thus "u = s" by simp
   259 next
   260   -- "and the only really interesting case, @{text \<WHILE>}:"
   261   fix b c s s1 s2 u
   262   assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   263   assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   264 
   265   assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   266   then obtain s' where
   267       c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   268       w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
   269     by auto
   270 
   271   from c "IH\<^sub>c" have "s' = s2" by blast
   272   with w "IH\<^sub>w" show "u = s1" by blast
   273 qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
   274 
   275 end