src/HOL/HoareParallel/RG_Examples.thy

--- a/src/HOL/HoareParallel/RG_Examples.thy	Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Tue Aug 03 13:48:00 2004 +0200
@@ -26,16 +26,7 @@
     COEND
  SAT [\<lbrace> n < length \<acute>A \<rbrace>, \<lbrace> \<ordmasculine>A = \<ordfeminine>A \<rbrace>, \<lbrace> True \<rbrace>, \<lbrace> \<forall>i < n. \<acute>A ! i = 0 \<rbrace>]"
 apply(rule Parallel)
-    apply simp
-    apply clarify
-    apply simp
-    apply(erule disjE)
-     apply simp
-    apply clarify
-    apply simp
-   apply auto
-apply(rule Basic)
-apply auto
+apply (auto intro!: Basic) 
 done
 
 lemma Example1_parameterized: 
@@ -53,33 +44,14 @@
       (\<forall>i<length \<ordmasculine>A . (i<k*n \<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i) \<and> ((Suc k)*n \<le> i\<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i))\<rbrace>, 
       \<lbrace>\<forall>i<n. \<acute>A!(k*n+i) = 0\<rbrace>]"
 apply(rule Parallel)
-    apply simp
-    apply clarify
-    apply simp
-    apply(erule disjE)
-     apply clarify
-     apply simp
-    apply clarify
-    apply simp
-    apply clarify
-    apply simp
-    apply(erule_tac x="k*n +i" in allE)
-    apply(subgoal_tac "k*n+i <length (A b)")
-     apply force
-    apply(erule le_less_trans2) 
-    apply(case_tac t,simp+)
-    apply (simp add:add_commute)
-    apply(rule add_le_mono)
-     apply simp
-    apply simp
-   apply simp
-   apply clarify
-   apply(rotate_tac -1)
+    apply auto
+  apply(erule_tac x="k*n +i" in allE)
+  apply(subgoal_tac "k*n+i <length (A b)")
    apply force
-  apply force
- apply force
-apply simp
-apply clarify
+  apply(erule le_less_trans2) 
+  apply(case_tac t,simp+)
+  apply (simp add:add_commute)
+  apply(simp add: add_le_mono)
 apply(rule Basic)
    apply simp
    apply clarify
@@ -88,12 +60,10 @@
    apply(erule le_less_trans2)
    apply(case_tac t,simp+)
    apply (simp add:add_commute)
-   apply(rule add_le_mono)
-    apply simp
-   apply simp
-  apply force+
+   apply(rule add_le_mono, auto)
 done
 
+
 subsection {* Increment a Variable in Parallel *}
 
 subsubsection {* Two components *}
@@ -134,7 +104,7 @@
    apply clarify
    apply(case_tac i)
     apply simp
-    apply(erule disjE)
+    apply(rule conjI)
      apply clarify
      apply simp
     apply clarify
@@ -142,7 +112,7 @@
     apply(case_tac j,simp)
     apply simp
    apply simp
-   apply(erule disjE)
+   apply(rule conjI)
     apply clarify
     apply simp
    apply clarify
@@ -179,10 +149,7 @@
  apply(rule Basic)
   apply simp_all
  apply(rule subset_refl)
-apply(rule Basic)
-apply simp_all
-apply clarify
-apply simp
+apply(auto intro!: Basic)
 done
 
 subsubsection {* Parameterized *}