# HG changeset patch
# User kleing
# Date 1371273408 25200
# Node ID 90fd1922f45f7be169e0ea04559bd2a0a208a8f2
# Parent  bae65fd74633c83763d3409264a9f9fb6fc169ee
another example lemma

diff -r bae65fd74633 -r 90fd1922f45f src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Thu Jun 13 17:26:39 2013 -0400
+++ b/src/HOL/IMP/Big_Step.thy	Fri Jun 14 22:16:48 2013 -0700
@@ -25,8 +25,8 @@
           (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
 
 WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
-WhileTrue:  "\<lbrakk> bval b s\<^isub>1;  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
-                (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
+WhileTrue:  "\<lbrakk> bval b s\<^isub>1;  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> 
+              \<Longrightarrow> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
 text_raw{*}%endsnip*}
 
 text_raw{*\snip{BigStepEx}{1}{2}{% *}
@@ -137,6 +137,26 @@
   "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
   by auto
 
+text {* An example combining rule inversion and derivations *}
+lemma Semi_assoc:
+  "(c1;; c2;; c3, s) \<Rightarrow> s' \<longleftrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> s'"
+proof
+  assume "(c1;; c2;; c3, s) \<Rightarrow> s'"
+  then obtain s1 s2 where
+    c1: "(c1, s) \<Rightarrow> s1" and
+    c2: "(c2, s1) \<Rightarrow> s2" and
+    c3: "(c3, s2) \<Rightarrow> s'" by auto
+  from c2 c3
+  have "(c2;; c3, s1) \<Rightarrow> s'" by (rule Seq)
+  with c1
+  show "(c1;; (c2;; c3), s) \<Rightarrow> s'" by (rule Seq)
+next
+  -- "The other direction is analogous"
+  assume "(c1;; (c2;; c3), s) \<Rightarrow> s'"
+  thus "(c1;; c2;; c3, s) \<Rightarrow> s'" by auto
+qed
+
+
 subsection "Command Equivalence"
 
 text {*