# HG changeset patch
# User oheimb
# Date 906412351 -7200
# Node ID 7970832271cc5b1a4bd31f7c871dfa58ffb6b4bf
# Parent  e2484f1786b7cb6e278a20b587e181ae889161ab
added wrapper for bspec

diff -r e2484f1786b7 -r 7970832271cc src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -135,7 +135,6 @@
 by (ALLGOALS trans_tac);
 val lemma = result();
 
-
 Goal
  "!i j xs. xs : regset d i j k = \
 \          ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)";
@@ -181,9 +180,7 @@
  by (asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1);
 by (rtac ballI 1);
 by (rtac lemma 1);
- by (Asm_simp_tac 2);
-by (EVERY[dtac bspec 1, atac 2]);
-by (Asm_simp_tac 1);
+ by (Auto_tac);
 qed_spec_mp "regset_spec";
 
 Goalw [bounded_def]
diff -r e2484f1786b7 -r 7970832271cc src/HOL/MiniML/Instance.ML
--- a/src/HOL/MiniML/Instance.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/MiniML/Instance.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -65,15 +65,7 @@
 by Safe_tac;
 by (rename_tac "S1 S2" 1);
 by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
-by Safe_tac;
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
-by (strip_tac 1);
-by (dres_inst_tac [("x","x")] bspec 1);
-by (assume_tac 1);
-by (dres_inst_tac [("x","x")] bspec 1);
-by (Asm_simp_tac 1);
-by (Asm_full_simp_tac 1);
+by (Auto_tac);
 qed_spec_mp "bound_scheme_inst_type";
 
 
diff -r e2484f1786b7 -r 7970832271cc src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/Real/PReal.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -6,6 +6,8 @@
                   [Gleason- p. 121] provides some of the definitions.
 *)
 
+claset_ref() := claset() delWrapper "bspec";
+
 open PReal;
 
 Goal "inj_on Abs_preal preal";
diff -r e2484f1786b7 -r 7970832271cc src/HOL/Real/RComplete.ML
--- a/src/HOL/Real/RComplete.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/Real/RComplete.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -8,6 +8,8 @@
 
 open RComplete;
 
+claset_ref() := claset() delWrapper "bspec";
+
 Goal "!!(x::real). [| isLub R S x; isLub R S y |] ==> x = y";
 by (forward_tac [isLub_isUb] 1);
 by (forw_inst_tac [("x","y")] isLub_isUb 1);
diff -r e2484f1786b7 -r 7970832271cc src/HOL/Real/Real.ML
--- a/src/HOL/Real/Real.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/Real/Real.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -686,7 +686,7 @@
 
 Goal "~ 0r < %~ %#m";
 by (cut_facts_tac [real_preal_minus_less_zero] 1);
-by (blast_tac (claset() addDs [real_less_trans] 
+by (fast_tac (claset() addDs [real_less_trans] 
                         addEs [real_less_irrefl]) 1);
 qed "real_preal_not_minus_gt_zero";
 
@@ -815,7 +815,7 @@
 
 Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)";
 by (cut_facts_tac [real_linear] 1);
-by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
+by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
 qed "real_less_or_eq_imp_le";
 
 Goal "(x <= (y::real)) = (x < y | x=y)";
@@ -843,7 +843,7 @@
 
 Goal "[| z <= w; w <= z |] ==> z = (w::real)";
 by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
-            blast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
+            fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
 qed "real_le_anti_sym";
 
 Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)";
diff -r e2484f1786b7 -r 7970832271cc src/HOL/Set.ML
--- a/src/HOL/Set.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/Set.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -59,14 +59,16 @@
 
 AddSIs [ballI];
 AddEs  [ballE];
+(* gives better instantiation for bound: *)
+claset_ref() := claset() addWrapper ("bspec", fn tac2 =>
+			 (dtac bspec THEN' atac) APPEND' tac2);
 
 Goalw [Bex_def] "[| P(x);  x:A |] ==> ? x:A. P(x)";
 by (Blast_tac 1);
 qed "bexI";
 
 qed_goal "bexCI" Set.thy 
-   "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)"
- (fn prems=>
+   "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)" (fn prems =>
   [ (rtac classical 1),
     (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ]);
 
diff -r e2484f1786b7 -r 7970832271cc src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -51,7 +51,6 @@
 Goalw [FP_def, fixedpoint_def, stable_def, constrains_def]
      "FP (Acts Rprg) <= fixedpoint";
 by Auto_tac;
-by (dtac bspec 1 THEN Blast_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
 by (dtac fun_cong 1);
 by Auto_tac;
@@ -78,12 +77,7 @@
 	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym])) 1);
 by Auto_tac;
 by (rtac fun_upd_idem 1);
-by (Blast_tac 1);
-by (Full_simp_tac 1);
-by (REPEAT (dtac bspec 1 THEN Simp_tac 1));
-by (dtac subsetD 1);
-by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
+ by (auto_tac (claset(),simpset() addsimps [fun_upd_idem_iff]));
 qed "Compl_fixedpoint";
 
 Goal "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
diff -r e2484f1786b7 -r 7970832271cc src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -434,8 +434,7 @@
 \      constrains acts (A1 - B) (A1 Un B); \
 \      constrains acts (A2 - C) (A2 Un C) |] \
 \   ==> constrains acts (A1 Un A2 - C) (A1 Un A2 Un C)";
-by (Clarify_tac 1);
-by (blast_tac (claset() addSDs [bspec]) 1);
+by(Blast_tac 1);
 val lemma1 = result();
 
 
diff -r e2484f1786b7 -r 7970832271cc src/HOL/WF.ML
--- a/src/HOL/WF.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/WF.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -177,7 +177,7 @@
   by (Blast_tac 1);
  by (blast_tac (claset() addEs [equalityE]) 1);
 by (Asm_full_simp_tac 1);
-by (Fast_tac 1);  (*faster than Blast_tac*)
+by (fast_tac (claset() delWrapper "bspec") 1); (*faster than Blast_tac*)
 qed "wf_UN";
 
 Goalw [Union_def]
diff -r e2484f1786b7 -r 7970832271cc src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/equalities.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -722,8 +722,7 @@
 qed "ex_bool_eq";
 
 Goal "A Un B = (UN b. if b then A else B)";
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [split_if_mem2]) 1);
+by(auto_tac(claset()delWrapper"bspec",simpset()addsimps [split_if_mem2]));
 qed "Un_eq_UN";
 
 Goal "(UN b::bool. A b) = (A True Un A False)";
diff -r e2484f1786b7 -r 7970832271cc src/HOL/ex/PiSets.ML
--- a/src/HOL/ex/PiSets.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/ex/PiSets.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -613,9 +613,7 @@
 \                ==> f x = g x";
 by (etac equalityE 1);
 by (rewtac subset_def);
-by (dres_inst_tac [("x","(x, f x)")] bspec 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Auto_tac);
 val set_eq_lemma = result();
 
 goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)";
@@ -639,64 +637,59 @@
 
 goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B";
 by (rtac equalityI 1);
-by (afs [image_def] 1);
-by (rtac subsetI 1);
-by (Asm_full_simp_tac 1);
-by (etac bexE 1);
-by (etac ssubst 1);
-by (afs [PiBij_in_Graph] 1);
+by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1);
 by (rtac subsetI 1);
 by (afs [image_def] 1);
 by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);
-by (rtac restrictI_Pi 2);
-by (strip 2);
-by (rtac ex1E 2);
-by (afs [Graph_def] 2);
-by (etac conjE 2);
-by (dtac bspec 2);
-by (assume_tac 2);
-by (assume_tac 2);
-by (stac select_equality 2);
-by (assume_tac 2);
-by (Blast_tac 2);
+ by (rtac restrictI_Pi 2);
+ by (strip 2);
+ by (rtac ex1E 2);
+  by (afs [Graph_def] 2);
+  by (etac conjE 2);
+  by (dtac bspec 2);
+   by (assume_tac 2);
+  by (assume_tac 2);
+ by (stac select_equality 2);
+   by (assume_tac 2);
+  by (Blast_tac 2);
 (* gets hung up on by (afs [Graph_def] 2); *)
-by (SELECT_GOAL (rewtac Graph_def) 2);
-by (Blast_tac 2);
+ by (SELECT_GOAL (rewtac Graph_def) 2);
+ by (Blast_tac 2);
 (* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
 by (afs [PiBij_def,Graph_def] 1);
 by (stac restrictE1 1);
-by (rtac restrictI_Pi 1);
+ by (rtac restrictI_Pi 1);
 (* again like the old 2. subgoal *)
-by (strip 1);
-by (rtac ex1E 1);
-by (etac conjE 1);
-by (dtac bspec 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (stac select_equality 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
+ by (strip 1);
+ by (rtac ex1E 1);
+  by (etac conjE 1);
+  by (dtac bspec 1);
+   by (assume_tac 1);
+  by (assume_tac 1);
+ by (stac select_equality 1);
+   by (assume_tac 1);
+  by (Blast_tac 1);
+ by (Blast_tac 1);
 (* *)
 by (rtac equalityI 1);
 by (rtac subsetI 1);
-by (rtac CollectI 1);
-by (split_all_tac 1);
-by (Simp_tac 1);
-by (rtac conjI 1);
-by (Blast_tac 1);
-by (etac conjE 1);
-by (dtac subsetD 1);
-by (assume_tac 1);
-by (dtac SigmaD1 1);
-by (dtac bspec 1);
-by (assume_tac 1);
-by (stac restrictE1 1);
-by (assume_tac 1);
-by (rtac sym 1);
-by (rtac select_equality 1);
-by (assume_tac 1);
-by (Blast_tac 1);
+ by (rtac CollectI 1);
+ by (split_all_tac 1);
+ by (Simp_tac 1);
+ by (rtac conjI 1);
+  by (Blast_tac 1);
+ by (etac conjE 1);
+ by (dtac subsetD 1);
+  by (assume_tac 1);
+ by (dtac SigmaD1 1);
+ by (dtac bspec 1);
+  by (assume_tac 1);
+ by (stac restrictE1 1);
+  by (assume_tac 1);
+ by (rtac sym 1);
+ by (rtac select_equality 1);
+  by (assume_tac 1);
+ by (Blast_tac 1);
 (* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x   *)
 by (rtac subsetI 1);
 by (Asm_full_simp_tac 1);
@@ -706,7 +699,7 @@
 by (etac conjE 1);
 by (afs [restrictE1] 1);
 by (dtac bspec 1);
-by (assume_tac 1);
+ by (assume_tac 1);
 by (dtac Ex1_Ex 1);
 by (rewtac Ex_def);
 by (assume_tac 1);