Calls Blast_tac. Tidied some proofs
authorpaulson
Fri Apr 04 11:27:02 1997 +0200 (1997-04-04)
changeset 28932ee005e46d6d
parent 2892 67fb21ddfe15
child 2894 d2ffee4f811b
Calls Blast_tac. Tidied some proofs
src/HOL/subset.ML
     1.1 --- a/src/HOL/subset.ML	Fri Apr 04 11:20:31 1997 +0200
     1.2 +++ b/src/HOL/subset.ML	Fri Apr 04 11:27:02 1997 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4   (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
     1.5  
     1.6  goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
     1.7 -by (Fast_tac 1);
     1.8 +by (Blast_tac 1);
     1.9  qed "subset_insert";
    1.10  
    1.11  (*** Big Union -- least upper bound of a set  ***)
    1.12 @@ -54,9 +54,8 @@
    1.13  
    1.14  (*** Big Intersection -- greatest lower bound of a set ***)
    1.15  
    1.16 -val prems = goal Set.thy "B:A ==> Inter(A) <= B";
    1.17 -by (rtac subsetI 1);
    1.18 -by (REPEAT (resolve_tac prems 1 ORELSE etac InterD 1));
    1.19 +goal Set.thy "!!B. B:A ==> Inter(A) <= B";
    1.20 +by (Blast_tac 1);
    1.21  qed "Inter_lower";
    1.22  
    1.23  val [prem] = goal Set.thy
    1.24 @@ -77,8 +76,7 @@
    1.25  qed "INT_greatest";
    1.26  
    1.27  goal Set.thy "(INT x. B(x)) <= B(a)";
    1.28 -by (rtac subsetI 1);
    1.29 -by (REPEAT (resolve_tac prems 1 ORELSE etac INT1_D 1));
    1.30 +by (Blast_tac 1);
    1.31  qed "INT1_lower";
    1.32  
    1.33  val [prem] = goal Set.thy
    1.34 @@ -90,39 +88,35 @@
    1.35  (*** Finite Union -- the least upper bound of 2 sets ***)
    1.36  
    1.37  goal Set.thy "A <= A Un B";
    1.38 -by (REPEAT (ares_tac [subsetI,UnI1] 1));
    1.39 +by (Blast_tac 1);
    1.40  qed "Un_upper1";
    1.41  
    1.42  goal Set.thy "B <= A Un B";
    1.43 -by (REPEAT (ares_tac [subsetI,UnI2] 1));
    1.44 +by (Blast_tac 1);
    1.45  qed "Un_upper2";
    1.46  
    1.47 -val prems = goal Set.thy "[| A<=C;  B<=C |] ==> A Un B <= C";
    1.48 -by (cut_facts_tac prems 1);
    1.49 -by (DEPTH_SOLVE (ares_tac [subsetI] 1 
    1.50 -          ORELSE eresolve_tac [UnE,subsetD] 1));
    1.51 +goal Set.thy "!!C. [| A<=C;  B<=C |] ==> A Un B <= C";
    1.52 +by (Blast_tac 1);
    1.53  qed "Un_least";
    1.54  
    1.55  (*** Finite Intersection -- the greatest lower bound of 2 sets *)
    1.56  
    1.57  goal Set.thy "A Int B <= A";
    1.58 -by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
    1.59 +by (Blast_tac 1);
    1.60  qed "Int_lower1";
    1.61  
    1.62  goal Set.thy "A Int B <= B";
    1.63 -by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
    1.64 +by (Blast_tac 1);
    1.65  qed "Int_lower2";
    1.66  
    1.67 -val prems = goal Set.thy "[| C<=A;  C<=B |] ==> C <= A Int B";
    1.68 -by (cut_facts_tac prems 1);
    1.69 -by (REPEAT (ares_tac [subsetI,IntI] 1
    1.70 -     ORELSE etac subsetD 1));
    1.71 +goal Set.thy "!!C. [| C<=A;  C<=B |] ==> C <= A Int B";
    1.72 +by (Blast_tac 1);
    1.73  qed "Int_greatest";
    1.74  
    1.75  (*** Set difference ***)
    1.76  
    1.77  qed_goal "Diff_subset" Set.thy "A-B <= (A::'a set)"
    1.78 - (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]);
    1.79 + (fn _ => [ (Blast_tac 1) ]);
    1.80  
    1.81  (*** Monotonicity ***)
    1.82