author nipkow Mon, 28 Nov 2016 15:09:23 +0100 changeset 64530 a720c3911308 parent 64529 1c0b93961cb1 child 64531 166a2563e0ca child 64533 172f3a047f4a
tuned proof
 src/HOL/IMP/Big_Step.thy file | annotate | diff | comparison | revisions
```--- 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```