# HG changeset patch
# User nipkow
# Date 1480342163 -3600
# Node ID a720c39113080d741265f4dd40afbeddeaa9aae7
# Parent  1c0b93961cb121abe685e45ea705e005266e9303
tuned proof

diff -r 1c0b93961cb1 -r a720c3911308 src/HOL/IMP/Big_Step.thy
--- 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