author nipkow Sun, 03 Jan 2010 10:01:23 +0100 changeset 34233 156c42518cfc parent 34232 36a2a3029fd3 child 34235 43bf58fdbace
removed more asm_rl's - unfortunately slowdown of 1 min.
```--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Sun Jan 03 10:01:23 2010 +0100
@@ -1,4 +1,3 @@
-
header {* \section{The Single Mutator Case} *}

theory Gar_Coll imports Graph OG_Syntax begin
@@ -203,12 +202,11 @@
apply clarify
apply simp
apply(subgoal_tac "ind x = length (E x)")
- apply (rotate_tac -1)
- apply (simp (asm_lr))
+ apply (simp)
apply(drule Graph1)
apply simp
-  apply clarify
- apply(erule allE, erule impE, assumption)
+  apply clarify
+  apply(erule allE, erule impE, assumption)
apply force
apply force
apply arith
@@ -318,12 +316,11 @@
apply clarify
apply simp
apply(subgoal_tac "ind x = length (E x)")
- apply (rotate_tac -1)
- apply (simp (asm_lr))
+ apply (simp)
apply(drule Graph1)
apply simp
apply clarify
- apply(erule allE, erule impE, assumption)
+  apply(erule allE, erule impE, assumption)
apply force
apply force
apply arith```
```--- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Sun Jan 03 10:01:23 2010 +0100
@@ -1,4 +1,3 @@
-

theory OG_Examples imports OG_Syntax begin
@@ -434,16 +433,14 @@
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
--{* 112 subgoals left *}
apply(simp_all (no_asm))
+--{* 97 subgoals left *}
apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
--{* 930 subgoals left *}
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
-apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
---{* 44 subgoals left *}
-apply (simp_all (asm_lr) del:length_0_conv add: neq0_conv nth_list_update mod_less_divisor mod_lemma)
---{* 32 subgoals left *}
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
-
-apply(tactic {* TRYALL (Lin_Arith.tac @{context}) *})
+--{* 99 subgoals left *}
+apply(simp_all (*asm_lr*) only:length_0_conv [THEN sym])
+--{* 20 subgoals left *}
+apply (simp_all (*asm_lr*) del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
--{* 9 subgoals left *}
apply(drule sym)```
```--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Sun Jan 03 10:01:23 2010 +0100
@@ -120,12 +120,11 @@
apply clarify
apply simp
apply(subgoal_tac "j=0")
-    apply (rotate_tac -1)
-    apply (simp (asm_lr))
+    apply (simp)
apply arith
apply clarify
apply(case_tac i,simp,simp)
- apply clarify
+ apply clarify
apply simp
apply(erule_tac x=0 in all_dupE)
apply(erule_tac x=1 in allE,simp)```