src/HOL/Set.ML
changeset 5316 7a8975451a89
parent 5305 513925de8962
child 5318 72bf8039b53f
     1.1 --- a/src/HOL/Set.ML	Thu Aug 13 18:07:56 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Aug 13 18:14:26 1998 +0200
     1.3 @@ -17,17 +17,17 @@
     1.4  by (Asm_simp_tac 1);
     1.5  qed "CollectI";
     1.6  
     1.7 -val prems = goal Set.thy "!!a. a : {x. P(x)} ==> P(a)";
     1.8 +Goal "a : {x. P(x)} ==> P(a)";
     1.9  by (Asm_full_simp_tac 1);
    1.10  qed "CollectD";
    1.11  
    1.12 -val [prem] = goal Set.thy "[| !!x. (x:A) = (x:B) |] ==> A = B";
    1.13 +val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B";
    1.14  by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
    1.15  by (rtac Collect_mem_eq 1);
    1.16  by (rtac Collect_mem_eq 1);
    1.17  qed "set_ext";
    1.18  
    1.19 -val [prem] = goal Set.thy "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
    1.20 +val [prem] = Goal "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
    1.21  by (rtac (prem RS ext RS arg_cong) 1);
    1.22  qed "Collect_cong";
    1.23  
    1.24 @@ -39,17 +39,16 @@
    1.25  
    1.26  section "Bounded quantifiers";
    1.27  
    1.28 -val prems = goalw Set.thy [Ball_def]
    1.29 +val prems = Goalw [Ball_def]
    1.30      "[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)";
    1.31  by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
    1.32  qed "ballI";
    1.33  
    1.34 -val [major,minor] = goalw Set.thy [Ball_def]
    1.35 -    "[| ! x:A. P(x);  x:A |] ==> P(x)";
    1.36 -by (rtac (minor RS (major RS spec RS mp)) 1);
    1.37 +Goalw [Ball_def] "[| ! x:A. P(x);  x:A |] ==> P(x)";
    1.38 +by (Blast_tac 1);
    1.39  qed "bspec";
    1.40  
    1.41 -val major::prems = goalw Set.thy [Ball_def]
    1.42 +val major::prems = Goalw [Ball_def]
    1.43      "[| ! x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q";
    1.44  by (rtac (major RS spec RS impCE) 1);
    1.45  by (REPEAT (eresolve_tac prems 1));
    1.46 @@ -61,9 +60,8 @@
    1.47  AddSIs [ballI];
    1.48  AddEs  [ballE];
    1.49  
    1.50 -val prems = goalw Set.thy [Bex_def]
    1.51 -    "[| P(x);  x:A |] ==> ? x:A. P(x)";
    1.52 -by (REPEAT (ares_tac (prems @ [exI,conjI]) 1));
    1.53 +Goalw [Bex_def] "[| P(x);  x:A |] ==> ? x:A. P(x)";
    1.54 +by (Blast_tac 1);
    1.55  qed "bexI";
    1.56  
    1.57  qed_goal "bexCI" Set.thy 
    1.58 @@ -72,7 +70,7 @@
    1.59    [ (rtac classical 1),
    1.60      (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ]);
    1.61  
    1.62 -val major::prems = goalw Set.thy [Bex_def]
    1.63 +val major::prems = Goalw [Bex_def]
    1.64      "[| ? x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q";
    1.65  by (rtac (major RS exE) 1);
    1.66  by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
    1.67 @@ -95,7 +93,7 @@
    1.68  
    1.69  (** Congruence rules **)
    1.70  
    1.71 -val prems = goal Set.thy
    1.72 +val prems = Goal
    1.73      "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
    1.74  \    (! x:A. P(x)) = (! x:B. Q(x))";
    1.75  by (resolve_tac (prems RL [ssubst]) 1);
    1.76 @@ -103,7 +101,7 @@
    1.77       ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1));
    1.78  qed "ball_cong";
    1.79  
    1.80 -val prems = goal Set.thy
    1.81 +val prems = Goal
    1.82      "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
    1.83  \    (? x:A. P(x)) = (? x:B. Q(x))";
    1.84  by (resolve_tac (prems RL [ssubst]) 1);
    1.85 @@ -113,7 +111,7 @@
    1.86  
    1.87  section "Subsets";
    1.88  
    1.89 -val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
    1.90 +val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
    1.91  by (REPEAT (ares_tac (prems @ [ballI]) 1));
    1.92  qed "subsetI";
    1.93  
    1.94 @@ -130,9 +128,8 @@
    1.95  Blast.overloaded ("op ``", domain_type o domain_type);
    1.96  
    1.97  (*Rule in Modus Ponens style*)
    1.98 -val major::prems = goalw Set.thy [subset_def] "[| A <= B;  c:A |] ==> c:B";
    1.99 -by (rtac (major RS bspec) 1);
   1.100 -by (resolve_tac prems 1);
   1.101 +Goalw [subset_def] "[| A <= B;  c:A |] ==> c:B";
   1.102 +by (Blast_tac 1);
   1.103  qed "subsetD";
   1.104  
   1.105  (*The same, with reversed premises for use with etac -- cf rev_mp*)
   1.106 @@ -149,7 +146,7 @@
   1.107   (fn prems=>  [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]);
   1.108  
   1.109  (*Classical elimination rule*)
   1.110 -val major::prems = goalw Set.thy [subset_def] 
   1.111 +val major::prems = Goalw [subset_def] 
   1.112      "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";
   1.113  by (rtac (major RS ballE) 1);
   1.114  by (REPEAT (eresolve_tac prems 1));
   1.115 @@ -164,7 +161,7 @@
   1.116  qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
   1.117   (fn _=> [Fast_tac 1]);		(*Blast_tac would try order_refl and fail*)
   1.118  
   1.119 -val prems = goal Set.thy "!!B. [| A<=B;  B<=C |] ==> A<=(C::'a set)";
   1.120 +Goal "[| A<=B;  B<=C |] ==> A<=(C::'a set)";
   1.121  by (Blast_tac 1);
   1.122  qed "subset_trans";
   1.123  
   1.124 @@ -172,32 +169,32 @@
   1.125  section "Equality";
   1.126  
   1.127  (*Anti-symmetry of the subset relation*)
   1.128 -val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = (B::'a set)";
   1.129 -by (rtac (iffI RS set_ext) 1);
   1.130 -by (REPEAT (ares_tac (prems RL [subsetD]) 1));
   1.131 +Goal "[| A <= B;  B <= A |] ==> A = (B::'a set)";
   1.132 +br set_ext 1;
   1.133 +by (blast_tac (claset() addIs [subsetD]) 1);
   1.134  qed "subset_antisym";
   1.135  val equalityI = subset_antisym;
   1.136  
   1.137  AddSIs [equalityI];
   1.138  
   1.139  (* Equality rules from ZF set theory -- are they appropriate here? *)
   1.140 -val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
   1.141 -by (resolve_tac (prems RL [subst]) 1);
   1.142 +Goal "A = B ==> A<=(B::'a set)";
   1.143 +by (etac ssubst 1);
   1.144  by (rtac subset_refl 1);
   1.145  qed "equalityD1";
   1.146  
   1.147 -val prems = goal Set.thy "A = B ==> B<=(A::'a set)";
   1.148 -by (resolve_tac (prems RL [subst]) 1);
   1.149 +Goal "A = B ==> B<=(A::'a set)";
   1.150 +by (etac ssubst 1);
   1.151  by (rtac subset_refl 1);
   1.152  qed "equalityD2";
   1.153  
   1.154 -val prems = goal Set.thy
   1.155 +val prems = Goal
   1.156      "[| A = B;  [| A<=B; B<=(A::'a set) |] ==> P |]  ==>  P";
   1.157  by (resolve_tac prems 1);
   1.158  by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
   1.159  qed "equalityE";
   1.160  
   1.161 -val major::prems = goal Set.thy
   1.162 +val major::prems = Goal
   1.163      "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
   1.164  by (rtac (major RS equalityE) 1);
   1.165  by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
   1.166 @@ -206,7 +203,7 @@
   1.167  (*Lemma for creating induction formulae -- for "pattern matching" on p
   1.168    To make the induction hypotheses usable, apply "spec" or "bspec" to
   1.169    put universal quantifiers over the free variables in p. *)
   1.170 -val prems = goal Set.thy 
   1.171 +val prems = Goal 
   1.172      "[| p:A;  !!z. z:A ==> p=z --> R |] ==> R";
   1.173  by (rtac mp 1);
   1.174  by (REPEAT (resolve_tac (refl::prems) 1));
   1.175 @@ -305,17 +302,15 @@
   1.176  
   1.177  Addsimps [Compl_iff];
   1.178  
   1.179 -val prems = goalw Set.thy [Compl_def]
   1.180 -    "[| c:A ==> False |] ==> c : Compl(A)";
   1.181 +val prems = Goalw [Compl_def] "[| c:A ==> False |] ==> c : Compl(A)";
   1.182  by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
   1.183  qed "ComplI";
   1.184  
   1.185  (*This form, with negated conclusion, works well with the Classical prover.
   1.186    Negated assumptions behave like formulae on the right side of the notional
   1.187    turnstile...*)
   1.188 -val major::prems = goalw Set.thy [Compl_def]
   1.189 -    "c : Compl(A) ==> c~:A";
   1.190 -by (rtac (major RS CollectD) 1);
   1.191 +Goalw [Compl_def] "c : Compl(A) ==> c~:A";
   1.192 +by (etac CollectD 1);
   1.193  qed "ComplD";
   1.194  
   1.195  val ComplE = make_elim ComplD;
   1.196 @@ -345,7 +340,7 @@
   1.197    [ (Simp_tac 1),
   1.198      (REPEAT (ares_tac (prems@[disjCI]) 1)) ]);
   1.199  
   1.200 -val major::prems = goalw Set.thy [Un_def]
   1.201 +val major::prems = Goalw [Un_def]
   1.202      "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P";
   1.203  by (rtac (major RS CollectD RS disjE) 1);
   1.204  by (REPEAT (eresolve_tac prems 1));
   1.205 @@ -374,7 +369,7 @@
   1.206  by (Asm_full_simp_tac 1);
   1.207  qed "IntD2";
   1.208  
   1.209 -val [major,minor] = goal Set.thy
   1.210 +val [major,minor] = Goal
   1.211      "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P";
   1.212  by (rtac minor 1);
   1.213  by (rtac (major RS IntD1) 1);
   1.214 @@ -479,7 +474,7 @@
   1.215  by Auto_tac;
   1.216  qed "UN_I";
   1.217  
   1.218 -val major::prems = goalw Set.thy [UNION_def]
   1.219 +val major::prems = Goalw [UNION_def]
   1.220      "[| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R";
   1.221  by (rtac (major RS CollectD RS bexE) 1);
   1.222  by (REPEAT (ares_tac prems 1));
   1.223 @@ -488,7 +483,7 @@
   1.224  AddIs  [UN_I];
   1.225  AddSEs [UN_E];
   1.226  
   1.227 -val prems = goal Set.thy
   1.228 +val prems = Goal
   1.229      "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
   1.230  \    (UN x:A. C(x)) = (UN x:B. D(x))";
   1.231  by (REPEAT (etac UN_E 1
   1.232 @@ -505,7 +500,7 @@
   1.233  
   1.234  Addsimps [INT_iff];
   1.235  
   1.236 -val prems = goalw Set.thy [INTER_def]
   1.237 +val prems = Goalw [INTER_def]
   1.238      "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
   1.239  by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
   1.240  qed "INT_I";
   1.241 @@ -515,7 +510,7 @@
   1.242  qed "INT_D";
   1.243  
   1.244  (*"Classical" elimination -- by the Excluded Middle on a:A *)
   1.245 -val major::prems = goalw Set.thy [INTER_def]
   1.246 +val major::prems = Goalw [INTER_def]
   1.247      "[| b : (INT x:A. B(x));  b: B(a) ==> R;  a~:A ==> R |] ==> R";
   1.248  by (rtac (major RS CollectD RS ballE) 1);
   1.249  by (REPEAT (eresolve_tac prems 1));
   1.250 @@ -524,7 +519,7 @@
   1.251  AddSIs [INT_I];
   1.252  AddEs  [INT_D, INT_E];
   1.253  
   1.254 -val prems = goal Set.thy
   1.255 +val prems = Goal
   1.256      "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
   1.257  \    (INT x:A. C(x)) = (INT x:B. D(x))";
   1.258  by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI]));
   1.259 @@ -546,7 +541,7 @@
   1.260  by Auto_tac;
   1.261  qed "UnionI";
   1.262  
   1.263 -val major::prems = goalw Set.thy [Union_def]
   1.264 +val major::prems = Goalw [Union_def]
   1.265      "[| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R";
   1.266  by (rtac (major RS UN_E) 1);
   1.267  by (REPEAT (ares_tac prems 1));
   1.268 @@ -564,7 +559,7 @@
   1.269  
   1.270  Addsimps [Inter_iff];
   1.271  
   1.272 -val prems = goalw Set.thy [Inter_def]
   1.273 +val prems = Goalw [Inter_def]
   1.274      "[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
   1.275  by (REPEAT (ares_tac ([INT_I] @ prems) 1));
   1.276  qed "InterI";
   1.277 @@ -576,7 +571,7 @@
   1.278  qed "InterD";
   1.279  
   1.280  (*"Classical" elimination rule -- does not require proving X:C *)
   1.281 -val major::prems = goalw Set.thy [Inter_def]
   1.282 +val major::prems = Goalw [Inter_def]
   1.283      "[| A : Inter(C);  X~:C ==> R;  A:X ==> R |] ==> R";
   1.284  by (rtac (major RS INT_E) 1);
   1.285  by (REPEAT (eresolve_tac prems 1));
   1.286 @@ -589,15 +584,15 @@
   1.287  (*** Image of a set under a function ***)
   1.288  
   1.289  (*Frequently b does not have the syntactic form of f(x).*)
   1.290 -val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
   1.291 -by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
   1.292 +Goalw [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
   1.293 +by (Blast_tac 1);
   1.294  qed "image_eqI";
   1.295  Addsimps [image_eqI];
   1.296  
   1.297  bind_thm ("imageI", refl RS image_eqI);
   1.298  
   1.299  (*The eta-expansion gives variable-name preservation.*)
   1.300 -val major::prems = goalw thy [image_def]
   1.301 +val major::prems = Goalw [image_def]
   1.302      "[| b : (%x. f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
   1.303  by (rtac (major RS CollectD RS bexE) 1);
   1.304  by (REPEAT (ares_tac prems 1));
   1.305 @@ -621,7 +616,7 @@
   1.306  
   1.307  (*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
   1.308    many existing proofs.*)
   1.309 -val prems = goal thy "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
   1.310 +val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
   1.311  by (blast_tac (claset() addIs prems) 1);
   1.312  qed "image_subsetI";
   1.313  
   1.314 @@ -634,7 +629,7 @@
   1.315  
   1.316  bind_thm ("rangeI", UNIV_I RS imageI);
   1.317  
   1.318 -val [major,minor] = goal thy 
   1.319 +val [major,minor] = Goal 
   1.320      "[| b : range(%x. f(x));  !!x. b=f(x) ==> P |] ==> P"; 
   1.321  by (rtac (major RS imageE) 1);
   1.322  by (etac minor 1);