src/HOL/Set.ML
changeset 2891 d8f254ad1ab9
parent 2881 62ecde1015ae
child 2912 3fac3e8d5d3e
     1.1 --- a/src/HOL/Set.ML	Fri Apr 04 11:18:19 1997 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Apr 04 11:18:52 1997 +0200
     1.3 @@ -151,10 +151,10 @@
     1.4  AddEs  [subsetD, subsetCE];
     1.5  
     1.6  qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
     1.7 - (fn _=> [Fast_tac 1]);
     1.8 + (fn _=> [Blast_tac 1]);
     1.9  
    1.10  val prems = goal Set.thy "!!B. [| A<=B;  B<=C |] ==> A<=(C::'a set)";
    1.11 -by (Fast_tac 1);
    1.12 +by (Blast_tac 1);
    1.13  qed "subset_trans";
    1.14  
    1.15  
    1.16 @@ -206,7 +206,7 @@
    1.17  section "The empty set -- {}";
    1.18  
    1.19  qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False"
    1.20 - (fn _ => [ (Fast_tac 1) ]);
    1.21 + (fn _ => [ (Blast_tac 1) ]);
    1.22  
    1.23  Addsimps [empty_iff];
    1.24  
    1.25 @@ -216,14 +216,14 @@
    1.26  AddSEs [emptyE];
    1.27  
    1.28  qed_goal "empty_subsetI" Set.thy "{} <= A"
    1.29 - (fn _ => [ (Fast_tac 1) ]);
    1.30 + (fn _ => [ (Blast_tac 1) ]);
    1.31  
    1.32  qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
    1.33   (fn [prem]=>
    1.34    [ (fast_tac (!claset addIs [prem RS FalseE]) 1) ]);
    1.35  
    1.36  qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
    1.37 - (fn _ => [ (Fast_tac 1) ]);
    1.38 + (fn _ => [ (Blast_tac 1) ]);
    1.39  
    1.40  goal Set.thy "Ball {} P = True";
    1.41  by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Ball_def, empty_def]) 1);
    1.42 @@ -235,13 +235,13 @@
    1.43  Addsimps [ball_empty, bex_empty];
    1.44  
    1.45  goalw Set.thy [Ball_def] "(!x:A.False) = (A = {})";
    1.46 -by(Fast_tac 1);
    1.47 +by(Blast_tac 1);
    1.48  qed "ball_False";
    1.49  Addsimps [ball_False];
    1.50  
    1.51  (* The dual is probably not helpful:
    1.52  goal Set.thy "(? x:A.True) = (A ~= {})";
    1.53 -by(Fast_tac 1);
    1.54 +by(Blast_tac 1);
    1.55  qed "bex_True";
    1.56  Addsimps [bex_True];
    1.57  *)
    1.58 @@ -267,7 +267,7 @@
    1.59  section "Set complement -- Compl";
    1.60  
    1.61  qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : Compl(A)) = (c~:A)"
    1.62 - (fn _ => [ (Fast_tac 1) ]);
    1.63 + (fn _ => [ (Blast_tac 1) ]);
    1.64  
    1.65  Addsimps [Compl_iff];
    1.66  
    1.67 @@ -293,7 +293,7 @@
    1.68  section "Binary union -- Un";
    1.69  
    1.70  qed_goalw "Un_iff" Set.thy [Un_def] "(c : A Un B) = (c:A | c:B)"
    1.71 - (fn _ => [ Fast_tac 1 ]);
    1.72 + (fn _ => [ Blast_tac 1 ]);
    1.73  
    1.74  Addsimps [Un_iff];
    1.75  
    1.76 @@ -324,7 +324,7 @@
    1.77  section "Binary intersection -- Int";
    1.78  
    1.79  qed_goalw "Int_iff" Set.thy [Int_def] "(c : A Int B) = (c:A & c:B)"
    1.80 - (fn _ => [ (Fast_tac 1) ]);
    1.81 + (fn _ => [ (Blast_tac 1) ]);
    1.82  
    1.83  Addsimps [Int_iff];
    1.84  
    1.85 @@ -353,7 +353,7 @@
    1.86  section "Set difference";
    1.87  
    1.88  qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : A-B) = (c:A & c~:B)"
    1.89 - (fn _ => [ (Fast_tac 1) ]);
    1.90 + (fn _ => [ (Blast_tac 1) ]);
    1.91  
    1.92  Addsimps [Diff_iff];
    1.93  
    1.94 @@ -378,7 +378,7 @@
    1.95  section "Augmenting a set -- insert";
    1.96  
    1.97  qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b | a:A)"
    1.98 - (fn _ => [Fast_tac 1]);
    1.99 + (fn _ => [Blast_tac 1]);
   1.100  
   1.101  Addsimps [insert_iff];
   1.102  
   1.103 @@ -409,13 +409,13 @@
   1.104   (fn _=> [ (rtac insertI1 1) ]);
   1.105  
   1.106  goal Set.thy "!!a. b : {a} ==> b=a";
   1.107 -by (Fast_tac 1);
   1.108 +by (Blast_tac 1);
   1.109  qed "singletonD";
   1.110  
   1.111  bind_thm ("singletonE", make_elim singletonD);
   1.112  
   1.113  qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" 
   1.114 -(fn _ => [Fast_tac 1]);
   1.115 +(fn _ => [Blast_tac 1]);
   1.116  
   1.117  goal Set.thy "!!a b. {a}={b} ==> a=b";
   1.118  by (fast_tac (!claset addEs [equalityE]) 1);
   1.119 @@ -439,7 +439,7 @@
   1.120  section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
   1.121  
   1.122  goalw Set.thy [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
   1.123 -by (Fast_tac 1);
   1.124 +by (Blast_tac 1);
   1.125  qed "UN_iff";
   1.126  
   1.127  Addsimps [UN_iff];
   1.128 @@ -507,7 +507,7 @@
   1.129  
   1.130  goalw Set.thy [UNION1_def] "(b: (UN x. B(x))) = (EX x. b: B(x))";
   1.131  by (Simp_tac 1);
   1.132 -by (Fast_tac 1);
   1.133 +by (Blast_tac 1);
   1.134  qed "UN1_iff";
   1.135  
   1.136  Addsimps [UN1_iff];
   1.137 @@ -531,7 +531,7 @@
   1.138  
   1.139  goalw Set.thy [INTER1_def] "(b: (INT x. B(x))) = (ALL x. b: B(x))";
   1.140  by (Simp_tac 1);
   1.141 -by (Fast_tac 1);
   1.142 +by (Blast_tac 1);
   1.143  qed "INT1_iff";
   1.144  
   1.145  Addsimps [INT1_iff];
   1.146 @@ -552,7 +552,7 @@
   1.147  section "Union";
   1.148  
   1.149  goalw Set.thy [Union_def] "(A : Union(C)) = (EX X:C. A:X)";
   1.150 -by (Fast_tac 1);
   1.151 +by (Blast_tac 1);
   1.152  qed "Union_iff";
   1.153  
   1.154  Addsimps [Union_iff];
   1.155 @@ -575,7 +575,7 @@
   1.156  section "Inter";
   1.157  
   1.158  goalw Set.thy [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)";
   1.159 -by (Fast_tac 1);
   1.160 +by (Blast_tac 1);
   1.161  qed "Inter_iff";
   1.162  
   1.163  Addsimps [Inter_iff];