added wrapper for bspec
authoroheimb
Mon Sep 21 23:12:31 1998 +0200 (1998-09-21)
changeset 55217970832271cc
parent 5520 e2484f1786b7
child 5522 982c710450c6
added wrapper for bspec
src/HOL/Lex/RegSet_of_nat_DA.ML
src/HOL/MiniML/Instance.ML
src/HOL/Real/PReal.ML
src/HOL/Real/RComplete.ML
src/HOL/Real/Real.ML
src/HOL/Set.ML
src/HOL/UNITY/Reach.ML
src/HOL/UNITY/WFair.ML
src/HOL/WF.ML
src/HOL/equalities.ML
src/HOL/ex/PiSets.ML
     1.1 --- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Mon Sep 21 23:06:37 1998 +0200
     1.2 +++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Mon Sep 21 23:12:31 1998 +0200
     1.3 @@ -135,7 +135,6 @@
     1.4  by (ALLGOALS trans_tac);
     1.5  val lemma = result();
     1.6  
     1.7 -
     1.8  Goal
     1.9   "!i j xs. xs : regset d i j k = \
    1.10  \          ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)";
    1.11 @@ -181,9 +180,7 @@
    1.12   by (asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1);
    1.13  by (rtac ballI 1);
    1.14  by (rtac lemma 1);
    1.15 - by (Asm_simp_tac 2);
    1.16 -by (EVERY[dtac bspec 1, atac 2]);
    1.17 -by (Asm_simp_tac 1);
    1.18 + by (Auto_tac);
    1.19  qed_spec_mp "regset_spec";
    1.20  
    1.21  Goalw [bounded_def]
     2.1 --- a/src/HOL/MiniML/Instance.ML	Mon Sep 21 23:06:37 1998 +0200
     2.2 +++ b/src/HOL/MiniML/Instance.ML	Mon Sep 21 23:12:31 1998 +0200
     2.3 @@ -65,15 +65,7 @@
     2.4  by Safe_tac;
     2.5  by (rename_tac "S1 S2" 1);
     2.6  by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
     2.7 -by Safe_tac;
     2.8 -by (Asm_simp_tac 1);
     2.9 -by (Asm_simp_tac 1);
    2.10 -by (strip_tac 1);
    2.11 -by (dres_inst_tac [("x","x")] bspec 1);
    2.12 -by (assume_tac 1);
    2.13 -by (dres_inst_tac [("x","x")] bspec 1);
    2.14 -by (Asm_simp_tac 1);
    2.15 -by (Asm_full_simp_tac 1);
    2.16 +by (Auto_tac);
    2.17  qed_spec_mp "bound_scheme_inst_type";
    2.18  
    2.19  
     3.1 --- a/src/HOL/Real/PReal.ML	Mon Sep 21 23:06:37 1998 +0200
     3.2 +++ b/src/HOL/Real/PReal.ML	Mon Sep 21 23:12:31 1998 +0200
     3.3 @@ -6,6 +6,8 @@
     3.4                    [Gleason- p. 121] provides some of the definitions.
     3.5  *)
     3.6  
     3.7 +claset_ref() := claset() delWrapper "bspec";
     3.8 +
     3.9  open PReal;
    3.10  
    3.11  Goal "inj_on Abs_preal preal";
     4.1 --- a/src/HOL/Real/RComplete.ML	Mon Sep 21 23:06:37 1998 +0200
     4.2 +++ b/src/HOL/Real/RComplete.ML	Mon Sep 21 23:12:31 1998 +0200
     4.3 @@ -8,6 +8,8 @@
     4.4  
     4.5  open RComplete;
     4.6  
     4.7 +claset_ref() := claset() delWrapper "bspec";
     4.8 +
     4.9  Goal "!!(x::real). [| isLub R S x; isLub R S y |] ==> x = y";
    4.10  by (forward_tac [isLub_isUb] 1);
    4.11  by (forw_inst_tac [("x","y")] isLub_isUb 1);
     5.1 --- a/src/HOL/Real/Real.ML	Mon Sep 21 23:06:37 1998 +0200
     5.2 +++ b/src/HOL/Real/Real.ML	Mon Sep 21 23:12:31 1998 +0200
     5.3 @@ -686,7 +686,7 @@
     5.4  
     5.5  Goal "~ 0r < %~ %#m";
     5.6  by (cut_facts_tac [real_preal_minus_less_zero] 1);
     5.7 -by (blast_tac (claset() addDs [real_less_trans] 
     5.8 +by (fast_tac (claset() addDs [real_less_trans] 
     5.9                          addEs [real_less_irrefl]) 1);
    5.10  qed "real_preal_not_minus_gt_zero";
    5.11  
    5.12 @@ -815,7 +815,7 @@
    5.13  
    5.14  Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)";
    5.15  by (cut_facts_tac [real_linear] 1);
    5.16 -by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
    5.17 +by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
    5.18  qed "real_less_or_eq_imp_le";
    5.19  
    5.20  Goal "(x <= (y::real)) = (x < y | x=y)";
    5.21 @@ -843,7 +843,7 @@
    5.22  
    5.23  Goal "[| z <= w; w <= z |] ==> z = (w::real)";
    5.24  by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
    5.25 -            blast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
    5.26 +            fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
    5.27  qed "real_le_anti_sym";
    5.28  
    5.29  Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)";
     6.1 --- a/src/HOL/Set.ML	Mon Sep 21 23:06:37 1998 +0200
     6.2 +++ b/src/HOL/Set.ML	Mon Sep 21 23:12:31 1998 +0200
     6.3 @@ -59,14 +59,16 @@
     6.4  
     6.5  AddSIs [ballI];
     6.6  AddEs  [ballE];
     6.7 +(* gives better instantiation for bound: *)
     6.8 +claset_ref() := claset() addWrapper ("bspec", fn tac2 =>
     6.9 +			 (dtac bspec THEN' atac) APPEND' tac2);
    6.10  
    6.11  Goalw [Bex_def] "[| P(x);  x:A |] ==> ? x:A. P(x)";
    6.12  by (Blast_tac 1);
    6.13  qed "bexI";
    6.14  
    6.15  qed_goal "bexCI" Set.thy 
    6.16 -   "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)"
    6.17 - (fn prems=>
    6.18 +   "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)" (fn prems =>
    6.19    [ (rtac classical 1),
    6.20      (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ]);
    6.21  
     7.1 --- a/src/HOL/UNITY/Reach.ML	Mon Sep 21 23:06:37 1998 +0200
     7.2 +++ b/src/HOL/UNITY/Reach.ML	Mon Sep 21 23:12:31 1998 +0200
     7.3 @@ -51,7 +51,6 @@
     7.4  Goalw [FP_def, fixedpoint_def, stable_def, constrains_def]
     7.5       "FP (Acts Rprg) <= fixedpoint";
     7.6  by Auto_tac;
     7.7 -by (dtac bspec 1 THEN Blast_tac 1);
     7.8  by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
     7.9  by (dtac fun_cong 1);
    7.10  by Auto_tac;
    7.11 @@ -78,12 +77,7 @@
    7.12  	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym])) 1);
    7.13  by Auto_tac;
    7.14  by (rtac fun_upd_idem 1);
    7.15 -by (Blast_tac 1);
    7.16 -by (Full_simp_tac 1);
    7.17 -by (REPEAT (dtac bspec 1 THEN Simp_tac 1));
    7.18 -by (dtac subsetD 1);
    7.19 -by (Simp_tac 1);
    7.20 -by (asm_full_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
    7.21 + by (auto_tac (claset(),simpset() addsimps [fun_upd_idem_iff]));
    7.22  qed "Compl_fixedpoint";
    7.23  
    7.24  Goal "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
     8.1 --- a/src/HOL/UNITY/WFair.ML	Mon Sep 21 23:06:37 1998 +0200
     8.2 +++ b/src/HOL/UNITY/WFair.ML	Mon Sep 21 23:12:31 1998 +0200
     8.3 @@ -434,8 +434,7 @@
     8.4  \      constrains acts (A1 - B) (A1 Un B); \
     8.5  \      constrains acts (A2 - C) (A2 Un C) |] \
     8.6  \   ==> constrains acts (A1 Un A2 - C) (A1 Un A2 Un C)";
     8.7 -by (Clarify_tac 1);
     8.8 -by (blast_tac (claset() addSDs [bspec]) 1);
     8.9 +by(Blast_tac 1);
    8.10  val lemma1 = result();
    8.11  
    8.12  
     9.1 --- a/src/HOL/WF.ML	Mon Sep 21 23:06:37 1998 +0200
     9.2 +++ b/src/HOL/WF.ML	Mon Sep 21 23:12:31 1998 +0200
     9.3 @@ -177,7 +177,7 @@
     9.4    by (Blast_tac 1);
     9.5   by (blast_tac (claset() addEs [equalityE]) 1);
     9.6  by (Asm_full_simp_tac 1);
     9.7 -by (Fast_tac 1);  (*faster than Blast_tac*)
     9.8 +by (fast_tac (claset() delWrapper "bspec") 1); (*faster than Blast_tac*)
     9.9  qed "wf_UN";
    9.10  
    9.11  Goalw [Union_def]
    10.1 --- a/src/HOL/equalities.ML	Mon Sep 21 23:06:37 1998 +0200
    10.2 +++ b/src/HOL/equalities.ML	Mon Sep 21 23:12:31 1998 +0200
    10.3 @@ -722,8 +722,7 @@
    10.4  qed "ex_bool_eq";
    10.5  
    10.6  Goal "A Un B = (UN b. if b then A else B)";
    10.7 -by Auto_tac;
    10.8 -by (asm_full_simp_tac (simpset() addsimps [split_if_mem2]) 1);
    10.9 +by(auto_tac(claset()delWrapper"bspec",simpset()addsimps [split_if_mem2]));
   10.10  qed "Un_eq_UN";
   10.11  
   10.12  Goal "(UN b::bool. A b) = (A True Un A False)";
    11.1 --- a/src/HOL/ex/PiSets.ML	Mon Sep 21 23:06:37 1998 +0200
    11.2 +++ b/src/HOL/ex/PiSets.ML	Mon Sep 21 23:12:31 1998 +0200
    11.3 @@ -613,9 +613,7 @@
    11.4  \                ==> f x = g x";
    11.5  by (etac equalityE 1);
    11.6  by (rewtac subset_def);
    11.7 -by (dres_inst_tac [("x","(x, f x)")] bspec 1);
    11.8 -by (Fast_tac 1);
    11.9 -by (Fast_tac 1);
   11.10 +by (Auto_tac);
   11.11  val set_eq_lemma = result();
   11.12  
   11.13  goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)";
   11.14 @@ -639,64 +637,59 @@
   11.15  
   11.16  goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B";
   11.17  by (rtac equalityI 1);
   11.18 -by (afs [image_def] 1);
   11.19 -by (rtac subsetI 1);
   11.20 -by (Asm_full_simp_tac 1);
   11.21 -by (etac bexE 1);
   11.22 -by (etac ssubst 1);
   11.23 -by (afs [PiBij_in_Graph] 1);
   11.24 +by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1);
   11.25  by (rtac subsetI 1);
   11.26  by (afs [image_def] 1);
   11.27  by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);
   11.28 -by (rtac restrictI_Pi 2);
   11.29 -by (strip 2);
   11.30 -by (rtac ex1E 2);
   11.31 -by (afs [Graph_def] 2);
   11.32 -by (etac conjE 2);
   11.33 -by (dtac bspec 2);
   11.34 -by (assume_tac 2);
   11.35 -by (assume_tac 2);
   11.36 -by (stac select_equality 2);
   11.37 -by (assume_tac 2);
   11.38 -by (Blast_tac 2);
   11.39 + by (rtac restrictI_Pi 2);
   11.40 + by (strip 2);
   11.41 + by (rtac ex1E 2);
   11.42 +  by (afs [Graph_def] 2);
   11.43 +  by (etac conjE 2);
   11.44 +  by (dtac bspec 2);
   11.45 +   by (assume_tac 2);
   11.46 +  by (assume_tac 2);
   11.47 + by (stac select_equality 2);
   11.48 +   by (assume_tac 2);
   11.49 +  by (Blast_tac 2);
   11.50  (* gets hung up on by (afs [Graph_def] 2); *)
   11.51 -by (SELECT_GOAL (rewtac Graph_def) 2);
   11.52 -by (Blast_tac 2);
   11.53 + by (SELECT_GOAL (rewtac Graph_def) 2);
   11.54 + by (Blast_tac 2);
   11.55  (* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
   11.56  by (afs [PiBij_def,Graph_def] 1);
   11.57  by (stac restrictE1 1);
   11.58 -by (rtac restrictI_Pi 1);
   11.59 + by (rtac restrictI_Pi 1);
   11.60  (* again like the old 2. subgoal *)
   11.61 -by (strip 1);
   11.62 -by (rtac ex1E 1);
   11.63 -by (etac conjE 1);
   11.64 -by (dtac bspec 1);
   11.65 -by (assume_tac 1);
   11.66 -by (assume_tac 1);
   11.67 -by (stac select_equality 1);
   11.68 -by (assume_tac 1);
   11.69 -by (Blast_tac 1);
   11.70 -by (Blast_tac 1);
   11.71 + by (strip 1);
   11.72 + by (rtac ex1E 1);
   11.73 +  by (etac conjE 1);
   11.74 +  by (dtac bspec 1);
   11.75 +   by (assume_tac 1);
   11.76 +  by (assume_tac 1);
   11.77 + by (stac select_equality 1);
   11.78 +   by (assume_tac 1);
   11.79 +  by (Blast_tac 1);
   11.80 + by (Blast_tac 1);
   11.81  (* *)
   11.82  by (rtac equalityI 1);
   11.83  by (rtac subsetI 1);
   11.84 -by (rtac CollectI 1);
   11.85 -by (split_all_tac 1);
   11.86 -by (Simp_tac 1);
   11.87 -by (rtac conjI 1);
   11.88 -by (Blast_tac 1);
   11.89 -by (etac conjE 1);
   11.90 -by (dtac subsetD 1);
   11.91 -by (assume_tac 1);
   11.92 -by (dtac SigmaD1 1);
   11.93 -by (dtac bspec 1);
   11.94 -by (assume_tac 1);
   11.95 -by (stac restrictE1 1);
   11.96 -by (assume_tac 1);
   11.97 -by (rtac sym 1);
   11.98 -by (rtac select_equality 1);
   11.99 -by (assume_tac 1);
  11.100 -by (Blast_tac 1);
  11.101 + by (rtac CollectI 1);
  11.102 + by (split_all_tac 1);
  11.103 + by (Simp_tac 1);
  11.104 + by (rtac conjI 1);
  11.105 +  by (Blast_tac 1);
  11.106 + by (etac conjE 1);
  11.107 + by (dtac subsetD 1);
  11.108 +  by (assume_tac 1);
  11.109 + by (dtac SigmaD1 1);
  11.110 + by (dtac bspec 1);
  11.111 +  by (assume_tac 1);
  11.112 + by (stac restrictE1 1);
  11.113 +  by (assume_tac 1);
  11.114 + by (rtac sym 1);
  11.115 + by (rtac select_equality 1);
  11.116 +  by (assume_tac 1);
  11.117 + by (Blast_tac 1);
  11.118  (* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x   *)
  11.119  by (rtac subsetI 1);
  11.120  by (Asm_full_simp_tac 1);
  11.121 @@ -706,7 +699,7 @@
  11.122  by (etac conjE 1);
  11.123  by (afs [restrictE1] 1);
  11.124  by (dtac bspec 1);
  11.125 -by (assume_tac 1);
  11.126 + by (assume_tac 1);
  11.127  by (dtac Ex1_Ex 1);
  11.128  by (rewtac Ex_def);
  11.129  by (assume_tac 1);