summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 28 Nov 2016 15:09:23 +0100 | |

changeset 64530 | a720c3911308 |

parent 64529 | 1c0b93961cb1 |

child 64531 | 166a2563e0ca |

child 64533 | 172f3a047f4a |

tuned proof

--- a/src/HOL/IMP/Big_Step.thy Sun Nov 27 20:25:38 2016 +0100 +++ b/src/HOL/IMP/Big_Step.thy Mon Nov 28 15:09:23 2016 +0100 @@ -179,52 +179,39 @@ -- "to show the equivalence, we look at the derivation tree for" -- "each side and from that construct a derivation tree for the other side" { fix s t assume "(?w, s) \<Rightarrow> t" - -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s}," - -- "then both statements do nothing:" - { assume "\<not>bval b s" - hence "t = s" using `(?w,s) \<Rightarrow> t` by blast - hence "(?iw, s) \<Rightarrow> t" using `\<not>bval b s` by blast - } - moreover - -- "on the other hand, if @{text b} is @{text True} in state @{text s}," - -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"} *} - { assume "bval b s" - with `(?w, s) \<Rightarrow> t` obtain s' where + hence "(?iw, s) \<Rightarrow> t" + proof cases --"rule inversion on \<open>(?w, s) \<Rightarrow> t\<close>" + case WhileFalse + thus ?thesis by blast + next + case WhileTrue + from `bval b s` `(?w, s) \<Rightarrow> t` obtain s' where "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto -- "now we can build a derivation tree for the @{text IF}" -- "first, the body of the True-branch:" hence "(c;; ?w, s) \<Rightarrow> t" by (rule Seq) -- "then the whole @{text IF}" - with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue) - } - ultimately - -- "both cases together give us what we want:" - have "(?iw, s) \<Rightarrow> t" by blast + with `bval b s` show ?thesis by (rule IfTrue) + qed } moreover -- "now the other direction:" { fix s t assume "(?iw, s) \<Rightarrow> t" - -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch" - -- "of the @{text IF} is executed, and both statements do nothing:" - { assume "\<not>bval b s" + hence "(?w, s) \<Rightarrow> t" + proof cases --"rule inversion on \<open>(?iw, s) \<Rightarrow> t\<close>" + case IfFalse hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast - hence "(?w, s) \<Rightarrow> t" using `\<not>bval b s` by blast - } - moreover - -- "on the other hand, if @{text b} is @{text True} in state @{text s}," - -- {* then this time only the @{text IfTrue} rule can have be used *} - { assume "bval b s" + thus ?thesis using `\<not>bval b s` by blast + next + case IfTrue with `(?iw, s) \<Rightarrow> t` have "(c;; ?w, s) \<Rightarrow> t" by auto -- "and for this, only the Seq-rule is applicable:" then obtain s' where "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto -- "with this information, we can build a derivation tree for the @{text WHILE}" with `bval b s` - have "(?w, s) \<Rightarrow> t" by (rule WhileTrue) - } - ultimately - -- "both cases together again give us what we want:" - have "(?w, s) \<Rightarrow> t" by blast + show ?thesis by (rule WhileTrue) + qed } ultimately show ?thesis by blast