Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
authorpaulson
Mon Aug 17 13:09:08 1998 +0200 (1998-08-17 ago)
changeset 5325f7a5e06adea1
parent 5324 ec84178243ff
child 5326 8f9056ce5dfb
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
contains fewer theorems than before
src/ZF/AC/AC7_AC9.ML
src/ZF/AC/AC_Equiv.ML
src/ZF/AC/WO6_WO1.ML
src/ZF/Arith.ML
src/ZF/Cardinal.ML
src/ZF/CardinalArith.ML
src/ZF/Nat.ML
src/ZF/Sum.thy
src/ZF/domrange.ML
src/ZF/domrange.thy
src/ZF/equalities.ML
src/ZF/ex/PropLog.ML
src/ZF/ex/misc.ML
src/ZF/func.ML
src/ZF/mono.ML
src/ZF/mono.thy
src/ZF/pair.ML
src/ZF/simpdata.ML
src/ZF/subset.ML
src/ZF/upair.ML
     1.1 --- a/src/ZF/AC/AC7_AC9.ML	Mon Aug 17 13:06:29 1998 +0200
     1.2 +++ b/src/ZF/AC/AC7_AC9.ML	Mon Aug 17 13:09:08 1998 +0200
     1.3 @@ -13,13 +13,10 @@
     1.4  (*  - Sigma_fun_space_eqpoll                                              *)
     1.5  (* ********************************************************************** *)
     1.6  
     1.7 -goal ZF.thy "!!A. [| C~:A; B:A |] ==> B~=C";
     1.8 -by (Fast_tac 1);
     1.9 -qed "mem_not_eq_not_mem";
    1.10 -
    1.11  Goal "[| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
    1.12 -by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1]
    1.13 -                addDs [fun_space_emptyD, mem_not_eq_not_mem]) 1);
    1.14 +by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1, 
    1.15 +				Union_empty_iff RS iffD1]
    1.16 +                        addDs [fun_space_emptyD]) 1);
    1.17  qed "Sigma_fun_space_not0";
    1.18  
    1.19  Goal "(ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
     2.1 --- a/src/ZF/AC/AC_Equiv.ML	Mon Aug 17 13:06:29 1998 +0200
     2.2 +++ b/src/ZF/AC/AC_Equiv.ML	Mon Aug 17 13:09:08 1998 +0200
     2.3 @@ -44,8 +44,7 @@
     2.4  
     2.5  (* used only in WO1_DC.ML *)
     2.6  (*Note simpler proof*)
     2.7 -goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg;  \
     2.8 -\         A<=Df; A<=Dg |] ==> f``A=g``A";
     2.9 +Goal "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A";
    2.10  by (asm_simp_tac (simpset() addsimps [image_fun]) 1);
    2.11  qed "images_eq";
    2.12  
     3.1 --- a/src/ZF/AC/WO6_WO1.ML	Mon Aug 17 13:06:29 1998 +0200
     3.2 +++ b/src/ZF/AC/WO6_WO1.ML	Mon Aug 17 13:09:08 1998 +0200
     3.3 @@ -172,9 +172,8 @@
     3.4  by (fast_tac (claset() addSEs [LeastI, lt_Ord]) 1);
     3.5  qed "uu_not_empty";
     3.6  
     3.7 -goal ZF.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
     3.8 -by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE, 
     3.9 -                sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1));
    3.10 +Goal "[| r<=A*B; r~=0 |] ==> domain(r)~=0";
    3.11 +by (Blast_tac 1);
    3.12  qed "not_empty_rel_imp_domain";
    3.13  
    3.14  Goal "[| b<a; g<a; f`b~=0; f`g~=0;  \
    3.15 @@ -186,7 +185,7 @@
    3.16          THEN (REPEAT (ares_tac [lt_Ord] 1)));
    3.17  qed "Least_uu_not_empty_lt_a";
    3.18  
    3.19 -goal ZF.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
    3.20 +Goal "[| B<=A; a~:B |] ==> B <= A-{a}";
    3.21  by (Blast_tac 1);
    3.22  qed "subset_Diff_sing";
    3.23  
    3.24 @@ -194,14 +193,11 @@
    3.25  Goal "[| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
    3.26  by (etac natE 1);
    3.27  by (fast_tac (claset() addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
    3.28 -by (hyp_subst_tac 1);
    3.29 -by (rtac equalityI 1);
    3.30 -by (assume_tac 2);
    3.31 -by (rtac subsetI 1);
    3.32 -by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
    3.33 -by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2, 
    3.34 -                Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS 
    3.35 -                succ_lepoll_natE] 1
    3.36 +by (safe_tac (claset() addSIs [equalityI])); 
    3.37 +by (rtac ccontr 1);
    3.38 +by (etac (subset_Diff_sing RS subset_imp_lepoll 
    3.39 +	  RSN (2, Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS 
    3.40 +	  succ_lepoll_natE) 1
    3.41          THEN REPEAT (assume_tac 1));
    3.42  qed "supset_lepoll_imp_eq";
    3.43  
     4.1 --- a/src/ZF/Arith.ML	Mon Aug 17 13:06:29 1998 +0200
     4.2 +++ b/src/ZF/Arith.ML	Mon Aug 17 13:09:08 1998 +0200
     4.3 @@ -34,7 +34,7 @@
     4.4  
     4.5  Addsimps [rec_0, rec_succ];
     4.6  
     4.7 -val major::prems = goal Arith.thy
     4.8 +val major::prems = Goal
     4.9      "[| n: nat;  \
    4.10  \       a: C(0);  \
    4.11  \       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
    4.12 @@ -467,7 +467,7 @@
    4.13  qed "add_lt_mono";
    4.14  
    4.15  (*A [clumsy] way of lifting < monotonicity to le monotonicity *)
    4.16 -val lt_mono::ford::prems = goal Ordinal.thy
    4.17 +val lt_mono::ford::prems = Goal
    4.18       "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
    4.19  \        !!i. i:k ==> Ord(f(i));                \
    4.20  \        i le j;  j:k                           \
     5.1 --- a/src/ZF/Cardinal.ML	Mon Aug 17 13:06:29 1998 +0200
     5.2 +++ b/src/ZF/Cardinal.ML	Mon Aug 17 13:09:08 1998 +0200
     5.3 @@ -29,16 +29,15 @@
     5.4                               gfun RS fun_is_rel RS image_subset]) 1);
     5.5  qed "Banach_last_equation";
     5.6  
     5.7 -val prems = goal Cardinal.thy
     5.8 -    "[| f: X->Y;  g: Y->X |] ==>   \
     5.9 -\    EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) &    \
    5.10 -\                    (YA Int YB = 0) & (YA Un YB = Y) &    \
    5.11 -\                    f``XA=YA & g``YB=XB";
    5.12 +Goal "[| f: X->Y;  g: Y->X |] ==>   \
    5.13 +\     EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) &    \
    5.14 +\                     (YA Int YB = 0) & (YA Un YB = Y) &    \
    5.15 +\                     f``XA=YA & g``YB=XB";
    5.16  by (REPEAT 
    5.17      (FIRSTGOAL
    5.18       (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition])));
    5.19  by (rtac Banach_last_equation 3);
    5.20 -by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1));
    5.21 +by (REPEAT (ares_tac [fun_is_rel, image_subset, lfp_subset] 1));
    5.22  qed "decomposition";
    5.23  
    5.24  val prems = goal Cardinal.thy
    5.25 @@ -740,7 +739,7 @@
    5.26  (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
    5.27    set is well-ordered.  Proofs simplified by lcp. *)
    5.28  
    5.29 -goal Nat.thy "!!n. n:nat ==> wf[n](converse(Memrel(n)))";
    5.30 +Goal "n:nat ==> wf[n](converse(Memrel(n)))";
    5.31  by (etac nat_induct 1);
    5.32  by (blast_tac (claset() addIs [wf_onI]) 1);
    5.33  by (rtac wf_onI 1);
     6.1 --- a/src/ZF/CardinalArith.ML	Mon Aug 17 13:06:29 1998 +0200
     6.2 +++ b/src/ZF/CardinalArith.ML	Mon Aug 17 13:09:08 1998 +0200
     6.3 @@ -380,8 +380,8 @@
     6.4  (*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***)
     6.5  
     6.6  (*A general fact about ordermap*)
     6.7 -goalw Cardinal.thy [eqpoll_def]
     6.8 -    "!!A. [| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";
     6.9 +Goalw [eqpoll_def]
    6.10 +    "[| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";
    6.11  by (rtac exI 1);
    6.12  by (asm_simp_tac (simpset() addsimps [ordermap_eq_image, well_ord_is_wf]) 1);
    6.13  by (etac (ordermap_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1);
    6.14 @@ -808,7 +808,3 @@
    6.15  		  addsimps [nat_cadd_eq_add RS sym, cadd_def, eqpoll_refl]) 1);
    6.16  qed "nat_sum_eqpoll_sum";
    6.17  
    6.18 -goal Nat.thy "!!m. [| m le n; n:nat |] ==> m:nat";
    6.19 -by (blast_tac (claset() addSDs [lt_nat_in_nat]) 1);
    6.20 -qed "le_in_nat";
    6.21 -
     7.1 --- a/src/ZF/Nat.ML	Mon Aug 17 13:06:29 1998 +0200
     7.2 +++ b/src/ZF/Nat.ML	Mon Aug 17 13:09:08 1998 +0200
     7.3 @@ -125,6 +125,10 @@
     7.4  by (assume_tac 1);
     7.5  qed "lt_nat_in_nat";
     7.6  
     7.7 +Goal "[| m le n; n:nat |] ==> m:nat";
     7.8 +by (blast_tac (claset() addSDs [lt_nat_in_nat]) 1);
     7.9 +qed "le_in_nat";
    7.10 +
    7.11  
    7.12  (** Variations on mathematical induction **)
    7.13  
     8.1 --- a/src/ZF/Sum.thy	Mon Aug 17 13:06:29 1998 +0200
     8.2 +++ b/src/ZF/Sum.thy	Mon Aug 17 13:09:08 1998 +0200
     8.3 @@ -7,7 +7,7 @@
     8.4  "Part" primitive for simultaneous recursive type definitions
     8.5  *)
     8.6  
     8.7 -Sum = Bool + pair + 
     8.8 +Sum = Bool + equalities + 
     8.9  
    8.10  global
    8.11  
     9.1 --- a/src/ZF/domrange.ML	Mon Aug 17 13:06:29 1998 +0200
     9.2 +++ b/src/ZF/domrange.ML	Mon Aug 17 13:09:08 1998 +0200
     9.3 @@ -8,19 +8,19 @@
     9.4  
     9.5  (*** converse ***)
     9.6  
     9.7 -qed_goalw "converse_iff" ZF.thy [converse_def]
     9.8 +qed_goalw "converse_iff" thy [converse_def]
     9.9      "<a,b>: converse(r) <-> <b,a>:r"
    9.10   (fn _ => [ (Blast_tac 1) ]);
    9.11  
    9.12 -qed_goalw "converseI" ZF.thy [converse_def]
    9.13 +qed_goalw "converseI" thy [converse_def]
    9.14      "!!a b r. <a,b>:r ==> <b,a>:converse(r)"
    9.15   (fn _ => [ (Blast_tac 1) ]);
    9.16  
    9.17 -qed_goalw "converseD" ZF.thy [converse_def]
    9.18 +qed_goalw "converseD" thy [converse_def]
    9.19      "!!a b r. <a,b> : converse(r) ==> <b,a> : r"
    9.20   (fn _ => [ (Blast_tac 1) ]);
    9.21  
    9.22 -qed_goalw "converseE" ZF.thy [converse_def]
    9.23 +qed_goalw "converseE" thy [converse_def]
    9.24      "[| yx : converse(r);  \
    9.25  \       !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P \
    9.26  \    |] ==> P"
    9.27 @@ -34,36 +34,36 @@
    9.28  AddSIs [converseI];
    9.29  AddSEs [converseD,converseE];
    9.30  
    9.31 -qed_goal "converse_converse" ZF.thy
    9.32 +qed_goal "converse_converse" thy
    9.33      "!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
    9.34   (fn _ => [ (Blast_tac 1) ]);
    9.35  
    9.36 -qed_goal "converse_type" ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
    9.37 +qed_goal "converse_type" thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
    9.38   (fn _ => [ (Blast_tac 1) ]);
    9.39  
    9.40 -qed_goal "converse_prod" ZF.thy "converse(A*B) = B*A"
    9.41 +qed_goal "converse_prod" thy "converse(A*B) = B*A"
    9.42   (fn _ => [ (Blast_tac 1) ]);
    9.43  
    9.44 -qed_goal "converse_empty" ZF.thy "converse(0) = 0"
    9.45 +qed_goal "converse_empty" thy "converse(0) = 0"
    9.46   (fn _ => [ (Blast_tac 1) ]);
    9.47  
    9.48  Addsimps [converse_prod, converse_empty];
    9.49  
    9.50 -val converse_subset_iff = prove_goal ZF.thy
    9.51 +val converse_subset_iff = prove_goal thy
    9.52    "!!z. A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
    9.53   (fn _=> [ (Blast_tac 1) ]);
    9.54  
    9.55  
    9.56  (*** domain ***)
    9.57  
    9.58 -qed_goalw "domain_iff" ZF.thy [domain_def]
    9.59 +qed_goalw "domain_iff" thy [domain_def]
    9.60      "a: domain(r) <-> (EX y. <a,y>: r)"
    9.61   (fn _=> [ (Blast_tac 1) ]);
    9.62  
    9.63 -qed_goal "domainI" ZF.thy "!!a b r. <a,b>: r ==> a: domain(r)"
    9.64 +qed_goal "domainI" thy "!!a b r. <a,b>: r ==> a: domain(r)"
    9.65   (fn _=> [ (etac (exI RS (domain_iff RS iffD2)) 1) ]);
    9.66  
    9.67 -qed_goal "domainE" ZF.thy
    9.68 +qed_goal "domainE" thy
    9.69      "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
    9.70   (fn prems=>
    9.71    [ (rtac (domain_iff RS iffD1 RS exE) 1),
    9.72 @@ -72,15 +72,15 @@
    9.73  AddIs  [domainI];
    9.74  AddSEs [domainE];
    9.75  
    9.76 -qed_goal "domain_subset" ZF.thy "domain(Sigma(A,B)) <= A"
    9.77 +qed_goal "domain_subset" thy "domain(Sigma(A,B)) <= A"
    9.78   (fn _=> [ (Blast_tac 1) ]);
    9.79  
    9.80  (*** range ***)
    9.81  
    9.82 -qed_goalw "rangeI" ZF.thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
    9.83 +qed_goalw "rangeI" thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
    9.84   (fn _ => [ (etac (converseI RS domainI) 1) ]);
    9.85  
    9.86 -qed_goalw "rangeE" ZF.thy [range_def]
    9.87 +qed_goalw "rangeE" thy [range_def]
    9.88      "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P"
    9.89   (fn major::prems=>
    9.90    [ (rtac (major RS domainE) 1),
    9.91 @@ -90,7 +90,7 @@
    9.92  AddIs  [rangeI];
    9.93  AddSEs [rangeE];
    9.94  
    9.95 -qed_goalw "range_subset" ZF.thy [range_def] "range(A*B) <= B"
    9.96 +qed_goalw "range_subset" thy [range_def] "range(A*B) <= B"
    9.97   (fn _ =>
    9.98    [ (stac converse_prod 1),
    9.99      (rtac domain_subset 1) ]);
   9.100 @@ -98,17 +98,17 @@
   9.101  
   9.102  (*** field ***)
   9.103  
   9.104 -qed_goalw "fieldI1" ZF.thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
   9.105 +qed_goalw "fieldI1" thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
   9.106   (fn _ => [ (Blast_tac 1) ]);
   9.107  
   9.108 -qed_goalw "fieldI2" ZF.thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
   9.109 +qed_goalw "fieldI2" thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
   9.110   (fn _ => [ (Blast_tac 1) ]);
   9.111  
   9.112 -qed_goalw "fieldCI" ZF.thy [field_def]
   9.113 +qed_goalw "fieldCI" thy [field_def]
   9.114      "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
   9.115   (fn [prem]=> [ (blast_tac (claset() addIs [prem]) 1) ]);
   9.116  
   9.117 -qed_goalw "fieldE" ZF.thy [field_def]
   9.118 +qed_goalw "fieldE" thy [field_def]
   9.119       "[| a : field(r);  \
   9.120  \        !!x. <a,x>: r ==> P;  \
   9.121  \        !!x. <x,a>: r ==> P        |] ==> P"
   9.122 @@ -119,40 +119,40 @@
   9.123  AddIs  [fieldCI];
   9.124  AddSEs [fieldE];
   9.125  
   9.126 -qed_goal "field_subset" ZF.thy "field(A*B) <= A Un B"
   9.127 +qed_goal "field_subset" thy "field(A*B) <= A Un B"
   9.128   (fn _ => [ (Blast_tac 1) ]);
   9.129  
   9.130 -qed_goalw "domain_subset_field" ZF.thy [field_def]
   9.131 +qed_goalw "domain_subset_field" thy [field_def]
   9.132      "domain(r) <= field(r)"
   9.133   (fn _ => [ (rtac Un_upper1 1) ]);
   9.134  
   9.135 -qed_goalw "range_subset_field" ZF.thy [field_def]
   9.136 +qed_goalw "range_subset_field" thy [field_def]
   9.137      "range(r) <= field(r)"
   9.138   (fn _ => [ (rtac Un_upper2 1) ]);
   9.139  
   9.140 -qed_goal "domain_times_range" ZF.thy
   9.141 +qed_goal "domain_times_range" thy
   9.142      "!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
   9.143   (fn _ => [ (Blast_tac 1) ]);
   9.144  
   9.145 -qed_goal "field_times_field" ZF.thy
   9.146 +qed_goal "field_times_field" thy
   9.147      "!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)"
   9.148   (fn _ => [ (Blast_tac 1) ]);
   9.149  
   9.150  
   9.151  (*** Image of a set under a function/relation ***)
   9.152  
   9.153 -qed_goalw "image_iff" ZF.thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
   9.154 +qed_goalw "image_iff" thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
   9.155   (fn _ => [ (Blast_tac 1) ]);
   9.156  
   9.157 -qed_goal "image_singleton_iff" ZF.thy    "b : r``{a} <-> <a,b>:r"
   9.158 +qed_goal "image_singleton_iff" thy    "b : r``{a} <-> <a,b>:r"
   9.159   (fn _ => [ rtac (image_iff RS iff_trans) 1,
   9.160              Blast_tac 1 ]);
   9.161  
   9.162 -qed_goalw "imageI" ZF.thy [image_def]
   9.163 +qed_goalw "imageI" thy [image_def]
   9.164      "!!a b r. [| <a,b>: r;  a:A |] ==> b : r``A"
   9.165   (fn _ => [ (Blast_tac 1) ]);
   9.166  
   9.167 -qed_goalw "imageE" ZF.thy [image_def]
   9.168 +qed_goalw "imageE" thy [image_def]
   9.169      "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
   9.170   (fn major::prems=>
   9.171    [ (rtac (major RS CollectE) 1),
   9.172 @@ -161,32 +161,32 @@
   9.173  AddIs  [imageI];
   9.174  AddSEs [imageE];
   9.175  
   9.176 -qed_goal "image_subset" ZF.thy "!!A B r. r <= A*B ==> r``C <= B"
   9.177 +qed_goal "image_subset" thy "!!A B r. r <= A*B ==> r``C <= B"
   9.178   (fn _ => [ (Blast_tac 1) ]);
   9.179  
   9.180  
   9.181  (*** Inverse image of a set under a function/relation ***)
   9.182  
   9.183 -qed_goalw "vimage_iff" ZF.thy [vimage_def,image_def,converse_def]
   9.184 +qed_goalw "vimage_iff" thy [vimage_def,image_def,converse_def]
   9.185      "a : r-``B <-> (EX y:B. <a,y>:r)"
   9.186   (fn _ => [ (Blast_tac 1) ]);
   9.187  
   9.188 -qed_goal "vimage_singleton_iff" ZF.thy
   9.189 +qed_goal "vimage_singleton_iff" thy
   9.190      "a : r-``{b} <-> <a,b>:r"
   9.191   (fn _ => [ rtac (vimage_iff RS iff_trans) 1,
   9.192              Blast_tac 1 ]);
   9.193  
   9.194 -qed_goalw "vimageI" ZF.thy [vimage_def]
   9.195 +qed_goalw "vimageI" thy [vimage_def]
   9.196      "!!A B r. [| <a,b>: r;  b:B |] ==> a : r-``B"
   9.197   (fn _ => [ (Blast_tac 1) ]);
   9.198  
   9.199 -qed_goalw "vimageE" ZF.thy [vimage_def]
   9.200 +qed_goalw "vimageE" thy [vimage_def]
   9.201      "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P"
   9.202   (fn major::prems=>
   9.203    [ (rtac (major RS imageE) 1),
   9.204      (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);
   9.205  
   9.206 -qed_goalw "vimage_subset" ZF.thy [vimage_def]
   9.207 +qed_goalw "vimage_subset" thy [vimage_def]
   9.208      "!!A B r. r <= A*B ==> r-``C <= A"
   9.209   (fn _ => [ (etac (converse_type RS image_subset) 1) ]);
   9.210  
   9.211 @@ -199,22 +199,22 @@
   9.212  val ZF_cs = claset() delrules [equalityI];
   9.213  
   9.214  (** The Union of a set of relations is a relation -- Lemma for fun_Union **)
   9.215 -goal ZF.thy "!!S. (ALL x:S. EX A B. x <= A*B) ==>  \
   9.216 +Goal "(ALL x:S. EX A B. x <= A*B) ==>  \
   9.217  \                 Union(S) <= domain(Union(S)) * range(Union(S))";
   9.218  by (Blast_tac 1);
   9.219  qed "rel_Union";
   9.220  
   9.221  (** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
   9.222 -qed_goal "rel_Un" ZF.thy
   9.223 +qed_goal "rel_Un" thy
   9.224      "!!r s. [| r <= A*B;  s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
   9.225   (fn _ => [ (Blast_tac 1) ]);
   9.226  
   9.227  
   9.228 -goal ZF.thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
   9.229 +Goal "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
   9.230  by (Blast_tac 1);
   9.231  qed "domain_Diff_eq";
   9.232  
   9.233 -goal ZF.thy "!!r. [| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
   9.234 +Goal "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
   9.235  by (Blast_tac 1);
   9.236  qed "range_Diff_eq";
   9.237  
    10.1 --- a/src/ZF/domrange.thy	Mon Aug 17 13:06:29 1998 +0200
    10.2 +++ b/src/ZF/domrange.thy	Mon Aug 17 13:09:08 1998 +0200
    10.3 @@ -1,4 +1,4 @@
    10.4  (*Dummy theory to document dependencies *)
    10.5  
    10.6 -domrange = pair + "subset" 
    10.7 +domrange = pair + subset
    10.8  
    11.1 --- a/src/ZF/equalities.ML	Mon Aug 17 13:06:29 1998 +0200
    11.2 +++ b/src/ZF/equalities.ML	Mon Aug 17 13:09:08 1998 +0200
    11.3 @@ -182,7 +182,11 @@
    11.4  by (blast_tac (claset() addSEs [equalityE]) 1);
    11.5  qed "Union_disjoint";
    11.6  
    11.7 -goalw ZF.thy [Inter_def] "Inter(0) = 0";
    11.8 +Goal "Union(A) = 0 <-> (ALL B:A. B=0)";
    11.9 +by (Blast_tac 1);
   11.10 +qed "Union_empty_iff";
   11.11 +
   11.12 +Goalw [Inter_def] "Inter(0) = 0";
   11.13  by (Blast_tac 1);
   11.14  qed "Inter_0";
   11.15  
   11.16 @@ -209,7 +213,7 @@
   11.17  by (Blast_tac 1);
   11.18  qed "Union_eq_UN";
   11.19  
   11.20 -goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)";
   11.21 +Goalw [Inter_def] "Inter(A) = (INT x:A. x)";
   11.22  by (Blast_tac 1);
   11.23  qed "Inter_eq_INT";
   11.24  
   11.25 @@ -344,10 +348,10 @@
   11.26  by (Blast_tac 1);
   11.27  qed "domain_of_prod";
   11.28  
   11.29 -qed_goal "domain_0" ZF.thy "domain(0) = 0"
   11.30 +qed_goal "domain_0" thy "domain(0) = 0"
   11.31   (fn _ => [ Blast_tac 1 ]);
   11.32  
   11.33 -qed_goal "domain_cons" ZF.thy
   11.34 +qed_goal "domain_cons" thy
   11.35      "domain(cons(<a,b>,r)) = cons(a, domain(r))"
   11.36   (fn _ => [ Blast_tac 1 ]);
   11.37  
   11.38 @@ -376,10 +380,10 @@
   11.39  by (Blast_tac 1);
   11.40  qed "range_of_prod";
   11.41  
   11.42 -qed_goal "range_0" ZF.thy "range(0) = 0"
   11.43 +qed_goal "range_0" thy "range(0) = 0"
   11.44   (fn _ => [ Blast_tac 1 ]); 
   11.45  
   11.46 -qed_goal "range_cons" ZF.thy
   11.47 +qed_goal "range_cons" thy
   11.48      "range(cons(<a,b>,r)) = cons(b, range(r))"
   11.49   (fn _ => [ Blast_tac 1 ]);
   11.50  
   11.51 @@ -404,13 +408,13 @@
   11.52  
   11.53  (** Field **)
   11.54  
   11.55 -qed_goal "field_of_prod" ZF.thy "field(A*A) = A"
   11.56 +qed_goal "field_of_prod" thy "field(A*A) = A"
   11.57   (fn _ => [ Blast_tac 1 ]); 
   11.58  
   11.59 -qed_goal "field_0" ZF.thy "field(0) = 0"
   11.60 +qed_goal "field_0" thy "field(0) = 0"
   11.61   (fn _ => [ Blast_tac 1 ]); 
   11.62  
   11.63 -qed_goal "field_cons" ZF.thy
   11.64 +qed_goal "field_cons" thy
   11.65      "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
   11.66   (fn _ => [ rtac equalityI 1, ALLGOALS (Blast_tac) ]);
   11.67  
   11.68 @@ -543,7 +547,7 @@
   11.69  qed "converse_UN";
   11.70  
   11.71  (*Unfolding Inter avoids using excluded middle on A=0*)
   11.72 -goalw ZF.thy [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
   11.73 +Goalw [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
   11.74  by (Blast_tac 1);
   11.75  qed "converse_INT";
   11.76  
    12.1 --- a/src/ZF/ex/PropLog.ML	Mon Aug 17 13:06:29 1998 +0200
    12.2 +++ b/src/ZF/ex/PropLog.ML	Mon Aug 17 13:09:08 1998 +0200
    12.3 @@ -3,7 +3,7 @@
    12.4      Author:     Tobias Nipkow & Lawrence C Paulson
    12.5      Copyright   1992  University of Cambridge
    12.6  
    12.7 -For ex/prop-log.thy.  Inductive definition of propositional logic.
    12.8 +Inductive definition of propositional logic.
    12.9  Soundness and completeness w.r.t. truth-tables.
   12.10  
   12.11  Prove: If H|=p then G|=p where G:Fin(H)
   12.12 @@ -169,23 +169,20 @@
   12.13  qed "Imp_Fls";
   12.14  
   12.15  (*Typical example of strengthening the induction formula*)
   12.16 -val [major] = goal PropLog.thy 
   12.17 -    "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
   12.18 +Goal "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
   12.19  by (rtac (split_if RS iffD2) 1);
   12.20 -by (rtac (major RS prop.induct) 1);
   12.21 +by (etac prop.induct 1);
   12.22  by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H])));
   12.23  by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1, 
   12.24 -                            Fls_Imp RS weaken_left_Un2]));
   12.25 +			       Fls_Imp RS weaken_left_Un2]));
   12.26  by (ALLGOALS (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
   12.27                                       weaken_right, Imp_Fls])));
   12.28  qed "hyps_thms_if";
   12.29  
   12.30  (*Key lemma for completeness; yields a set of assumptions satisfying p*)
   12.31 -val [premp,sat] = goalw PropLog.thy [logcon_def]
   12.32 -    "[| p: prop;  0 |= p |] ==> hyps(p,t) |- p";
   12.33 -by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
   12.34 -    rtac (premp RS hyps_thms_if) 2);
   12.35 -by (Fast_tac 1);
   12.36 +Goalw [logcon_def] "[| p: prop;  0 |= p |] ==> hyps(p,t) |- p";
   12.37 +by (dtac hyps_thms_if 1);
   12.38 +by (Asm_full_simp_tac 1);
   12.39  qed "logcon_thms_p";
   12.40  
   12.41  (*For proving certain theorems in our new propositional logic*)
   12.42 @@ -194,27 +191,24 @@
   12.43            addIs [thms_in_pl, thms.H, thms.H RS thms_MP];
   12.44  
   12.45  (*The excluded middle in the form of an elimination rule*)
   12.46 -val prems = goal PropLog.thy
   12.47 -    "[| p: prop;  q: prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
   12.48 +Goal "[| p: prop;  q: prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
   12.49  by (rtac (deduction RS deduction) 1);
   12.50  by (rtac (thms.DN RS thms_MP) 1);
   12.51 -by (ALLGOALS (best_tac (thms_cs addSIs prems)));
   12.52 +by (ALLGOALS (blast_tac thms_cs));
   12.53  qed "thms_excluded_middle";
   12.54  
   12.55  (*Hard to prove directly because it requires cuts*)
   12.56 -val prems = goal PropLog.thy
   12.57 -    "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p: prop |] ==> H |- q";
   12.58 +Goal "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p: prop |] ==> H |- q";
   12.59  by (rtac (thms_excluded_middle RS thms_MP RS thms_MP) 1);
   12.60 -by (REPEAT (resolve_tac (prems@prop.intrs@[deduction,thms_in_pl]) 1));
   12.61 +by (REPEAT (ares_tac (prop.intrs@[deduction,thms_in_pl]) 1));
   12.62  qed "thms_excluded_middle_rule";
   12.63  
   12.64  (*** Completeness -- lemmas for reducing the set of assumptions ***)
   12.65  
   12.66  (*For the case hyps(p,t)-cons(#v,Y) |- p;
   12.67    we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
   12.68 -val [major] = goal PropLog.thy
   12.69 -    "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
   12.70 -by (rtac (major RS prop.induct) 1);
   12.71 +Goal "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
   12.72 +by (etac prop.induct 1);
   12.73  by (Simp_tac 1);
   12.74  by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
   12.75  by (fast_tac (claset() addSEs prop.free_SEs) 1);
   12.76 @@ -224,9 +218,8 @@
   12.77  
   12.78  (*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
   12.79    we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *)
   12.80 -val [major] = goal PropLog.thy
   12.81 -    "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
   12.82 -by (rtac (major RS prop.induct) 1);
   12.83 +Goal "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
   12.84 +by (etac prop.induct 1);
   12.85  by (Simp_tac 1);
   12.86  by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
   12.87  by (fast_tac (claset() addSEs prop.free_SEs) 1);
   12.88 @@ -236,19 +229,18 @@
   12.89  
   12.90  (** Two lemmas for use with weaken_left **)
   12.91  
   12.92 -goal ZF.thy "B-C <= cons(a, B-cons(a,C))";
   12.93 +Goal "B-C <= cons(a, B-cons(a,C))";
   12.94  by (Fast_tac 1);
   12.95  qed "cons_Diff_same";
   12.96  
   12.97 -goal ZF.thy "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))";
   12.98 +Goal "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))";
   12.99  by (Fast_tac 1);
  12.100  qed "cons_Diff_subset2";
  12.101  
  12.102  (*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls;
  12.103   could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*)
  12.104 -val [major] = goal PropLog.thy
  12.105 -    "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
  12.106 -by (rtac (major RS prop.induct) 1);
  12.107 +Goal "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
  12.108 +by (etac prop.induct 1);
  12.109  by (asm_simp_tac (simpset() addsimps [UN_I]
  12.110                    setloop (split_tac [split_if])) 2);
  12.111  by (ALLGOALS Asm_simp_tac);
    13.1 --- a/src/ZF/ex/misc.ML	Mon Aug 17 13:06:29 1998 +0200
    13.2 +++ b/src/ZF/ex/misc.ML	Mon Aug 17 13:09:08 1998 +0200
    13.3 @@ -10,12 +10,12 @@
    13.4  writeln"ZF/ex/misc";
    13.5  
    13.6  (*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
    13.7 -goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
    13.8 +Goal "ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
    13.9  by (Blast_tac 1);
   13.10  result();
   13.11  
   13.12  (*variant of the benchmark above*)
   13.13 -goal ZF.thy "!!S. ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
   13.14 +Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
   13.15  by (Blast_tac 1);
   13.16  result();
   13.17  
    14.1 --- a/src/ZF/func.ML	Mon Aug 17 13:06:29 1998 +0200
    14.2 +++ b/src/ZF/func.ML	Mon Aug 17 13:09:08 1998 +0200
    14.3 @@ -8,32 +8,32 @@
    14.4  
    14.5  (*** The Pi operator -- dependent function space ***)
    14.6  
    14.7 -goalw ZF.thy [Pi_def]
    14.8 +Goalw [Pi_def]
    14.9      "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)";
   14.10  by (Blast_tac 1);
   14.11  qed "Pi_iff";
   14.12  
   14.13  (*For upward compatibility with the former definition*)
   14.14 -goalw ZF.thy [Pi_def, function_def]
   14.15 +Goalw [Pi_def, function_def]
   14.16      "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)";
   14.17  by (Blast_tac 1);
   14.18  qed "Pi_iff_old";
   14.19  
   14.20 -goal ZF.thy "!!f. f: Pi(A,B) ==> function(f)";
   14.21 +Goal "f: Pi(A,B) ==> function(f)";
   14.22  by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
   14.23  qed "fun_is_function";
   14.24  
   14.25  (**Two "destruct" rules for Pi **)
   14.26  
   14.27 -val [major] = goalw ZF.thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";  
   14.28 -by (rtac (major RS CollectD1 RS PowD) 1);
   14.29 +Goalw [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";  
   14.30 +by (Blast_tac 1);
   14.31  qed "fun_is_rel";
   14.32  
   14.33 -goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> EX! y. <a,y>: f";  
   14.34 +Goal "[| f: Pi(A,B);  a:A |] ==> EX! y. <a,y>: f";  
   14.35  by (blast_tac (claset() addSDs [Pi_iff_old RS iffD1]) 1);
   14.36  qed "fun_unique_Pair";
   14.37  
   14.38 -val prems = goalw ZF.thy [Pi_def]
   14.39 +val prems = Goalw [Pi_def]
   14.40      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
   14.41  by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
   14.42  qed "Pi_cong";
   14.43 @@ -43,26 +43,26 @@
   14.44    Sigmas and Pis are abbreviated as * or -> *)
   14.45  
   14.46  (*Weakening one function type to another; see also Pi_type*)
   14.47 -goalw ZF.thy [Pi_def] "!!f. [| f: A->B;  B<=D |] ==> f: A->D";
   14.48 +Goalw [Pi_def] "[| f: A->B;  B<=D |] ==> f: A->D";
   14.49  by (Best_tac 1);
   14.50  qed "fun_weaken_type";
   14.51  
   14.52  (*Empty function spaces*)
   14.53 -goalw ZF.thy [Pi_def, function_def] "Pi(0,A) = {0}";
   14.54 +Goalw [Pi_def, function_def] "Pi(0,A) = {0}";
   14.55  by (Blast_tac 1);
   14.56  qed "Pi_empty1";
   14.57  
   14.58 -goalw ZF.thy [Pi_def] "!!A a. a:A ==> A->0 = 0";
   14.59 +Goalw [Pi_def] "a:A ==> A->0 = 0";
   14.60  by (Blast_tac 1);
   14.61  qed "Pi_empty2";
   14.62  
   14.63  (*The empty function*)
   14.64 -goalw ZF.thy [Pi_def, function_def] "0: Pi(0,B)";
   14.65 +Goalw [Pi_def, function_def] "0: Pi(0,B)";
   14.66  by (Blast_tac 1);
   14.67  qed "empty_fun";
   14.68  
   14.69  (*The singleton function*)
   14.70 -goalw ZF.thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
   14.71 +Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
   14.72  by (Blast_tac 1);
   14.73  qed "singleton_fun";
   14.74  
   14.75 @@ -70,58 +70,56 @@
   14.76  
   14.77  (*** Function Application ***)
   14.78  
   14.79 -goalw ZF.thy [Pi_def, function_def]
   14.80 -     "!!a b f. [| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c";
   14.81 +Goalw [Pi_def, function_def]
   14.82 +     "[| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c";
   14.83  by (Blast_tac 1);
   14.84  qed "apply_equality2";
   14.85  
   14.86 -goalw ZF.thy [apply_def, function_def]
   14.87 -     "!!a b f. [| <a,b>: f;  function(f) |] ==> f`a = b";
   14.88 +Goalw [apply_def, function_def]
   14.89 +     "[| <a,b>: f;  function(f) |] ==> f`a = b";
   14.90  by (blast_tac (claset() addIs [the_equality]) 1);
   14.91  qed "function_apply_equality";
   14.92  
   14.93 -goalw ZF.thy [Pi_def] "!!a b f. [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
   14.94 +Goalw [Pi_def] "[| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
   14.95  by (blast_tac (claset() addIs [function_apply_equality]) 1);
   14.96  qed "apply_equality";
   14.97  
   14.98  (*Applying a function outside its domain yields 0*)
   14.99 -goalw ZF.thy [apply_def]
  14.100 -    "!!a. a ~: domain(f) ==> f`a = 0";
  14.101 +Goalw [apply_def]
  14.102 +    "a ~: domain(f) ==> f`a = 0";
  14.103  by (rtac the_0 1);
  14.104  by (Blast_tac 1);
  14.105  qed "apply_0";
  14.106  
  14.107 -goal ZF.thy "!!f. [| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>";
  14.108 +Goal "[| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>";
  14.109  by (forward_tac [fun_is_rel] 1);
  14.110  by (blast_tac (claset() addDs [apply_equality]) 1);
  14.111  qed "Pi_memberD";
  14.112  
  14.113 -goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
  14.114 +Goal "[| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
  14.115  by (rtac (fun_unique_Pair RS ex1E) 1);
  14.116  by (resolve_tac [apply_equality RS ssubst] 3);
  14.117  by (REPEAT (assume_tac 1));
  14.118  qed "apply_Pair";
  14.119  
  14.120  (*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
  14.121 -goal ZF.thy "!!f. [| f: Pi(A,B);  a:A |] ==> f`a : B(a)"; 
  14.122 +Goal "[| f: Pi(A,B);  a:A |] ==> f`a : B(a)"; 
  14.123  by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
  14.124  by (REPEAT (ares_tac [apply_Pair] 1));
  14.125  qed "apply_type";
  14.126  
  14.127  (*This version is acceptable to the simplifier*)
  14.128 -goal ZF.thy "!!f. [| f: A->B;  a:A |] ==> f`a : B"; 
  14.129 +Goal "[| f: A->B;  a:A |] ==> f`a : B"; 
  14.130  by (REPEAT (ares_tac [apply_type] 1));
  14.131  qed "apply_funtype";
  14.132  
  14.133 -val [major] = goal ZF.thy
  14.134 -    "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
  14.135 -by (cut_facts_tac [major RS fun_is_rel] 1);
  14.136 -by (blast_tac (claset() addSIs [major RS apply_Pair, 
  14.137 -			      major RSN (2,apply_equality)]) 1);
  14.138 +Goal "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
  14.139 +by (forward_tac [fun_is_rel] 1);
  14.140 +by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1);
  14.141  qed "apply_iff";
  14.142  
  14.143  (*Refining one Pi type to another*)
  14.144 -val pi_prem::prems = goal ZF.thy
  14.145 +val pi_prem::prems = Goal
  14.146      "[| f: Pi(A,C);  !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)";
  14.147  by (cut_facts_tac [pi_prem] 1);
  14.148  by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
  14.149 @@ -131,16 +129,16 @@
  14.150  
  14.151  (** Elimination of membership in a function **)
  14.152  
  14.153 -goal ZF.thy "!!a A. [| <a,b> : f;  f: Pi(A,B) |] ==> a : A";
  14.154 +Goal "[| <a,b> : f;  f: Pi(A,B) |] ==> a : A";
  14.155  by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));
  14.156  qed "domain_type";
  14.157  
  14.158 -goal ZF.thy "!!b B a. [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)";
  14.159 +Goal "[| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)";
  14.160  by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);
  14.161  by (assume_tac 1);
  14.162  qed "range_type";
  14.163  
  14.164 -val prems = goal ZF.thy
  14.165 +val prems = Goal
  14.166      "[| <a,b>: f;  f: Pi(A,B);       \
  14.167  \       [| a:A;  b:B(a);  f`a = b |] ==> P  \
  14.168  \    |] ==> P";
  14.169 @@ -151,35 +149,35 @@
  14.170  
  14.171  (*** Lambda Abstraction ***)
  14.172  
  14.173 -goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";  
  14.174 +Goalw [lam_def] "a:A ==> <a,b(a)> : (lam x:A. b(x))";  
  14.175  by (etac RepFunI 1);
  14.176  qed "lamI";
  14.177  
  14.178 -val major::prems = goalw ZF.thy [lam_def]
  14.179 +val major::prems = Goalw [lam_def]
  14.180      "[| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P  \
  14.181  \    |] ==>  P";  
  14.182  by (rtac (major RS RepFunE) 1);
  14.183  by (REPEAT (ares_tac prems 1));
  14.184  qed "lamE";
  14.185  
  14.186 -goal ZF.thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";  
  14.187 +Goal "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";  
  14.188  by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));
  14.189  qed "lamD";
  14.190  
  14.191 -val prems = goalw ZF.thy [lam_def, Pi_def, function_def]
  14.192 +val prems = Goalw [lam_def, Pi_def, function_def]
  14.193      "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)";  
  14.194  by (blast_tac (claset() addIs prems) 1);
  14.195  qed "lam_type";
  14.196  
  14.197 -goal ZF.thy "(lam x:A. b(x)) : A -> {b(x). x:A}";
  14.198 +Goal "(lam x:A. b(x)) : A -> {b(x). x:A}";
  14.199  by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
  14.200  qed "lam_funtype";
  14.201  
  14.202 -goal ZF.thy "!!a A. a : A ==> (lam x:A. b(x)) ` a = b(a)";
  14.203 +Goal "a : A ==> (lam x:A. b(x)) ` a = b(a)";
  14.204  by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
  14.205  qed "beta";
  14.206  
  14.207 -goalw ZF.thy [lam_def] "(lam x:0. b(x)) = 0";
  14.208 +Goalw [lam_def] "(lam x:0. b(x)) = 0";
  14.209  by (Simp_tac 1);
  14.210  qed "lam_empty";
  14.211  
  14.212 @@ -190,14 +188,14 @@
  14.213  Addsimps [beta, lam_empty, domain_lam];
  14.214  
  14.215  (*congruence rule for lambda abstraction*)
  14.216 -val prems = goalw ZF.thy [lam_def] 
  14.217 +val prems = Goalw [lam_def] 
  14.218      "[| A=A';  !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')";
  14.219  by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
  14.220  qed "lam_cong";
  14.221  
  14.222  Addcongs [lam_cong];
  14.223  
  14.224 -val [major] = goal ZF.thy
  14.225 +val [major] = Goal
  14.226      "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
  14.227  by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
  14.228  by (rtac ballI 1);
  14.229 @@ -210,7 +208,7 @@
  14.230  (** Extensionality **)
  14.231  
  14.232  (*Semi-extensionality!*)
  14.233 -val prems = goal ZF.thy
  14.234 +val prems = Goal
  14.235      "[| f : Pi(A,B);  g: Pi(C,D);  A<=C; \
  14.236  \       !!x. x:A ==> f`x = g`x       |] ==> f<=g";
  14.237  by (rtac subsetI 1);
  14.238 @@ -220,27 +218,27 @@
  14.239  by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
  14.240  qed "fun_subset";
  14.241  
  14.242 -val prems = goal ZF.thy
  14.243 +val prems = Goal
  14.244      "[| f : Pi(A,B);  g: Pi(A,D);  \
  14.245  \       !!x. x:A ==> f`x = g`x       |] ==> f=g";
  14.246  by (REPEAT (ares_tac (prems @ (prems RL [sym]) @
  14.247                        [subset_refl,equalityI,fun_subset]) 1));
  14.248  qed "fun_extension";
  14.249  
  14.250 -goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f";
  14.251 +Goal "f : Pi(A,B) ==> (lam x:A. f`x) = f";
  14.252  by (rtac fun_extension 1);
  14.253  by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));
  14.254  qed "eta";
  14.255  
  14.256  Addsimps [eta];
  14.257  
  14.258 -val fun_extension_iff = prove_goal ZF.thy
  14.259 -  "!!z. [| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g"
  14.260 - (fn _=> [ (blast_tac (claset() addIs [fun_extension]) 1) ]);
  14.261 +Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g";
  14.262 +by (blast_tac (claset() addIs [fun_extension]) 1);
  14.263 +qed "fun_extension_iff";
  14.264  
  14.265  (*thanks to Mark Staples*)
  14.266 -val fun_subset_eq = prove_goal ZF.thy
  14.267 -    "!!z. [| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
  14.268 +val fun_subset_eq = prove_goal thy
  14.269 +    "!!f. [| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
  14.270   (fn _=> 
  14.271    [ (rtac iffI 1), (asm_full_simp_tac ZF_ss 2),
  14.272      (rtac fun_extension 1), (REPEAT (atac 1)),
  14.273 @@ -249,7 +247,7 @@
  14.274  
  14.275  
  14.276  (*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
  14.277 -val prems = goal ZF.thy
  14.278 +val prems = Goal
  14.279      "[| f: Pi(A,B);        \
  14.280  \       !!b. [| ALL x:A. b(x):B(x);  f = (lam x:A. b(x)) |] ==> P   \
  14.281  \    |] ==> P";
  14.282 @@ -261,14 +259,13 @@
  14.283  
  14.284  (** Images of functions **)
  14.285  
  14.286 -goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
  14.287 +Goalw [lam_def] "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
  14.288  by (Blast_tac 1);
  14.289  qed "image_lam";
  14.290  
  14.291 -goal ZF.thy "!!C A. [| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}";
  14.292 +Goal "[| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}";
  14.293  by (etac (eta RS subst) 1);
  14.294 -by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff]
  14.295 -                              addcongs [RepFun_cong]) 1);
  14.296 +by (asm_full_simp_tac (simpset() addsimps [image_lam, subset_iff]) 1);
  14.297  qed "image_fun";
  14.298  
  14.299  Goal "[| f: Pi(A,B);  x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)";
  14.300 @@ -278,47 +275,46 @@
  14.301  
  14.302  (*** properties of "restrict" ***)
  14.303  
  14.304 -goalw ZF.thy [restrict_def,lam_def]
  14.305 -    "!!f A. [| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f";
  14.306 +Goalw [restrict_def,lam_def]
  14.307 +    "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f";
  14.308  by (blast_tac (claset() addIs [apply_Pair]) 1);
  14.309  qed "restrict_subset";
  14.310  
  14.311 -val prems = goalw ZF.thy [restrict_def]
  14.312 +val prems = Goalw [restrict_def]
  14.313      "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";  
  14.314  by (rtac lam_type 1);
  14.315  by (eresolve_tac prems 1);
  14.316  qed "restrict_type";
  14.317  
  14.318 -val [pi,subs] = goal ZF.thy 
  14.319 -    "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)";  
  14.320 -by (rtac (pi RS apply_type RS restrict_type) 1);
  14.321 -by (etac (subs RS subsetD) 1);
  14.322 +Goal "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)";  
  14.323 +by (blast_tac (claset() addIs [apply_type, restrict_type]) 1);
  14.324  qed "restrict_type2";
  14.325  
  14.326 -goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";
  14.327 +Goalw [restrict_def] "a : A ==> restrict(f,A) ` a = f`a";
  14.328  by (etac beta 1);
  14.329  qed "restrict";
  14.330  
  14.331 -goalw ZF.thy [restrict_def] "restrict(f,0) = 0";
  14.332 +Goalw [restrict_def] "restrict(f,0) = 0";
  14.333  by (Simp_tac 1);
  14.334  qed "restrict_empty";
  14.335  
  14.336  Addsimps [restrict, restrict_empty];
  14.337  
  14.338  (*NOT SAFE as a congruence rule for the simplifier!  Can cause it to fail!*)
  14.339 -val prems = goalw ZF.thy [restrict_def]
  14.340 +val prems = Goalw [restrict_def]
  14.341      "[| A=B;  !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
  14.342  by (REPEAT (ares_tac (prems@[lam_cong]) 1));
  14.343  qed "restrict_eqI";
  14.344  
  14.345 -goalw ZF.thy [restrict_def, lam_def] "domain(restrict(f,C)) = C";
  14.346 +Goalw [restrict_def, lam_def] "domain(restrict(f,C)) = C";
  14.347  by (Blast_tac 1);
  14.348  qed "domain_restrict";
  14.349  
  14.350 -val [prem] = goalw ZF.thy [restrict_def]
  14.351 +Goalw [restrict_def]
  14.352      "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
  14.353  by (rtac (refl RS lam_cong) 1);
  14.354 -by (etac (prem RS subsetD RS beta) 1);  (*easier than calling simp_tac*)
  14.355 +by (set_mp_tac 1);
  14.356 +by (Asm_simp_tac 1);
  14.357  qed "restrict_lam_eq";
  14.358  
  14.359  
  14.360 @@ -327,16 +323,16 @@
  14.361  
  14.362  (** The Union of a set of COMPATIBLE functions is a function **)
  14.363  
  14.364 -goalw ZF.thy [function_def]
  14.365 -    "!!S. [| ALL x:S. function(x); \
  14.366 +Goalw [function_def]
  14.367 +    "[| ALL x:S. function(x); \
  14.368  \            ALL x:S. ALL y:S. x<=y | y<=x  |] ==>  \
  14.369  \         function(Union(S))";
  14.370  by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1);
  14.371  	(*by (Blast_tac 1);  takes too long...*)
  14.372  qed "function_Union";
  14.373  
  14.374 -goalw ZF.thy [Pi_def]
  14.375 -    "!!S. [| ALL f:S. EX C D. f:C->D; \
  14.376 +Goalw [Pi_def]
  14.377 +    "[| ALL f:S. EX C D. f:C->D; \
  14.378  \            ALL f:S. ALL y:S. f<=y | y<=f  |] ==>  \
  14.379  \         Union(S) : domain(Union(S)) -> range(Union(S))";
  14.380  by (blast_tac (subset_cs addSIs [rel_Union, function_Union]) 1);
  14.381 @@ -349,7 +345,7 @@
  14.382                Un_upper1 RSN (2, subset_trans), 
  14.383                Un_upper2 RSN (2, subset_trans)];
  14.384  
  14.385 -goal ZF.thy "!!f. [| f: A->B;  g: C->D;  A Int C = 0  |]  \
  14.386 +Goal "[| f: A->B;  g: C->D;  A Int C = 0  |]  \
  14.387  \                 ==> (f Un g) : (A Un C) -> (B Un D)";
  14.388  (*Prove the product and domain subgoals using distributive laws*)
  14.389  by (asm_full_simp_tac (simpset() addsimps [Pi_iff,extension]@Un_rls) 1);
  14.390 @@ -357,15 +353,13 @@
  14.391  by (Blast_tac 1);
  14.392  qed "fun_disjoint_Un";
  14.393  
  14.394 -goal ZF.thy
  14.395 -    "!!f g a. [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
  14.396 +Goal "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
  14.397  \             (f Un g)`a = f`a";
  14.398  by (rtac (apply_Pair RS UnI1 RS apply_equality) 1);
  14.399  by (REPEAT (ares_tac [fun_disjoint_Un] 1));
  14.400  qed "fun_disjoint_apply1";
  14.401  
  14.402 -goal ZF.thy
  14.403 -    "!!f g c. [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
  14.404 +Goal "[| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
  14.405  \             (f Un g)`c = g`c";
  14.406  by (rtac (apply_Pair RS UnI2 RS apply_equality) 1);
  14.407  by (REPEAT (ares_tac [fun_disjoint_Un] 1));
  14.408 @@ -373,18 +367,17 @@
  14.409  
  14.410  (** Domain and range of a function/relation **)
  14.411  
  14.412 -goalw ZF.thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A";
  14.413 +Goalw [Pi_def] "f : Pi(A,B) ==> domain(f)=A";
  14.414  by (Blast_tac 1);
  14.415  qed "domain_of_fun";
  14.416  
  14.417 -goal ZF.thy "!!f. [| f : Pi(A,B);  a: A |] ==> f`a : range(f)";
  14.418 +Goal "[| f : Pi(A,B);  a: A |] ==> f`a : range(f)";
  14.419  by (etac (apply_Pair RS rangeI) 1);
  14.420  by (assume_tac 1);
  14.421  qed "apply_rangeI";
  14.422  
  14.423 -val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
  14.424 -by (rtac (major RS Pi_type) 1);
  14.425 -by (etac (major RS apply_rangeI) 1);
  14.426 +Goal "f : Pi(A,B) ==> f : A->range(f)";
  14.427 +by (REPEAT (ares_tac [Pi_type, apply_rangeI] 1));
  14.428  qed "range_of_fun";
  14.429  
  14.430  (*** Extensions of functions ***)
    15.1 --- a/src/ZF/mono.ML	Mon Aug 17 13:06:29 1998 +0200
    15.2 +++ b/src/ZF/mono.ML	Mon Aug 17 13:09:08 1998 +0200
    15.3 @@ -28,7 +28,7 @@
    15.4  by (Blast_tac 1);
    15.5  qed "Union_mono";
    15.6  
    15.7 -val prems = goal thy
    15.8 +val prems = Goal
    15.9      "[| A<=C;  !!x. x:A ==> B(x)<=D(x) \
   15.10  \    |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))";
   15.11  by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
   15.12 @@ -57,8 +57,7 @@
   15.13  
   15.14  (** Standard products, sums and function spaces **)
   15.15  
   15.16 -Goal "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==> \
   15.17 -\                       Sigma(A,B) <= Sigma(C,D)";
   15.18 +Goal "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)";
   15.19  by (Blast_tac 1);
   15.20  qed "Sigma_mono_lemma";
   15.21  val Sigma_mono = ballI RSN (2,Sigma_mono_lemma);
   15.22 @@ -131,12 +130,12 @@
   15.23  
   15.24  (** Images **)
   15.25  
   15.26 -val [prem1,prem2] = goal thy
   15.27 +val [prem1,prem2] = Goal
   15.28      "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r``A <= s``B";
   15.29  by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1);
   15.30  qed "image_pair_mono";
   15.31  
   15.32 -val [prem1,prem2] = goal thy
   15.33 +val [prem1,prem2] = Goal
   15.34      "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r-``A <= s-``B";
   15.35  by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1);
   15.36  qed "vimage_pair_mono";
   15.37 @@ -149,7 +148,7 @@
   15.38  by (Blast_tac 1);
   15.39  qed "vimage_mono";
   15.40  
   15.41 -val [sub,PQimp] = goal thy
   15.42 +val [sub,PQimp] = Goal
   15.43      "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)";
   15.44  by (blast_tac (claset() addIs [sub RS subsetD, PQimp RS mp]) 1);
   15.45  qed "Collect_mono";
    16.1 --- a/src/ZF/mono.thy	Mon Aug 17 13:06:29 1998 +0200
    16.2 +++ b/src/ZF/mono.thy	Mon Aug 17 13:09:08 1998 +0200
    16.3 @@ -1,4 +1,2 @@
    16.4 -(*Dummy theory to document dependencies *)
    16.5 +mono = QPair + Sum + func
    16.6  
    16.7 -mono = QPair + Sum + domrange
    16.8 -
    17.1 --- a/src/ZF/pair.ML	Mon Aug 17 13:06:29 1998 +0200
    17.2 +++ b/src/ZF/pair.ML	Mon Aug 17 13:09:08 1998 +0200
    17.3 @@ -8,17 +8,17 @@
    17.4  
    17.5  (** Lemmas for showing that <a,b> uniquely determines a and b **)
    17.6  
    17.7 -qed_goal "singleton_eq_iff" ZF.thy
    17.8 +qed_goal "singleton_eq_iff" thy
    17.9      "{a} = {b} <-> a=b"
   17.10   (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
   17.11             (Blast_tac 1) ]);
   17.12  
   17.13 -qed_goal "doubleton_eq_iff" ZF.thy
   17.14 +qed_goal "doubleton_eq_iff" thy
   17.15      "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
   17.16   (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
   17.17             (Blast_tac 1) ]);
   17.18  
   17.19 -qed_goalw "Pair_iff" ZF.thy [Pair_def]
   17.20 +qed_goalw "Pair_iff" thy [Pair_def]
   17.21      "<a,b> = <c,d> <-> a=c & b=d"
   17.22   (fn _=> [ (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1),
   17.23             (Blast_tac 1) ]);
   17.24 @@ -32,20 +32,20 @@
   17.25  bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1);
   17.26  bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2);
   17.27  
   17.28 -qed_goalw "Pair_not_0" ZF.thy [Pair_def] "<a,b> ~= 0"
   17.29 +qed_goalw "Pair_not_0" thy [Pair_def] "<a,b> ~= 0"
   17.30   (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
   17.31  
   17.32  bind_thm ("Pair_neq_0", Pair_not_0 RS notE);
   17.33  
   17.34  AddSEs [Pair_neq_0, sym RS Pair_neq_0];
   17.35  
   17.36 -qed_goalw "Pair_neq_fst" ZF.thy [Pair_def] "<a,b>=a ==> P"
   17.37 +qed_goalw "Pair_neq_fst" thy [Pair_def] "<a,b>=a ==> P"
   17.38   (fn [major]=>
   17.39    [ (rtac (consI1 RS mem_asym RS FalseE) 1),
   17.40      (rtac (major RS subst) 1),
   17.41      (rtac consI1 1) ]);
   17.42  
   17.43 -qed_goalw "Pair_neq_snd" ZF.thy [Pair_def] "<a,b>=b ==> P"
   17.44 +qed_goalw "Pair_neq_snd" thy [Pair_def] "<a,b>=b ==> P"
   17.45   (fn [major]=>
   17.46    [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1),
   17.47      (rtac (major RS subst) 1),
   17.48 @@ -55,12 +55,12 @@
   17.49  (*** Sigma: Disjoint union of a family of sets
   17.50       Generalizes Cartesian product ***)
   17.51  
   17.52 -qed_goalw "Sigma_iff" ZF.thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
   17.53 +qed_goalw "Sigma_iff" thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
   17.54   (fn _ => [ Blast_tac 1 ]);
   17.55  
   17.56  Addsimps [Sigma_iff];
   17.57  
   17.58 -qed_goal "SigmaI" ZF.thy
   17.59 +qed_goal "SigmaI" thy
   17.60      "!!a b. [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
   17.61   (fn _ => [ Asm_simp_tac 1 ]);
   17.62  
   17.63 @@ -68,7 +68,7 @@
   17.64  bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);
   17.65  
   17.66  (*The general elimination rule*)
   17.67 -qed_goalw "SigmaE" ZF.thy [Sigma_def]
   17.68 +qed_goalw "SigmaE" thy [Sigma_def]
   17.69      "[| c: Sigma(A,B);  \
   17.70  \       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \
   17.71  \    |] ==> P"
   17.72 @@ -76,7 +76,7 @@
   17.73    [ (cut_facts_tac [major] 1),
   17.74      (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
   17.75  
   17.76 -qed_goal "SigmaE2" ZF.thy
   17.77 +qed_goal "SigmaE2" thy
   17.78      "[| <a,b> : Sigma(A,B);    \
   17.79  \       [| a:A;  b:B(a) |] ==> P   \
   17.80  \    |] ==> P"
   17.81 @@ -85,7 +85,7 @@
   17.82      (rtac (major RS SigmaD1) 1),
   17.83      (rtac (major RS SigmaD2) 1) ]);
   17.84  
   17.85 -qed_goalw "Sigma_cong" ZF.thy [Sigma_def]
   17.86 +qed_goalw "Sigma_cong" thy [Sigma_def]
   17.87      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
   17.88  \    Sigma(A,B) = Sigma(A',B')"
   17.89   (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
   17.90 @@ -98,10 +98,10 @@
   17.91  AddSIs [SigmaI];
   17.92  AddSEs [SigmaE2, SigmaE];
   17.93  
   17.94 -qed_goal "Sigma_empty1" ZF.thy "Sigma(0,B) = 0"
   17.95 +qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0"
   17.96   (fn _ => [ (Blast_tac 1) ]);
   17.97  
   17.98 -qed_goal "Sigma_empty2" ZF.thy "A*0 = 0"
   17.99 +qed_goal "Sigma_empty2" thy "A*0 = 0"
  17.100   (fn _ => [ (Blast_tac 1) ]);
  17.101  
  17.102  Addsimps [Sigma_empty1, Sigma_empty2];
  17.103 @@ -113,21 +113,21 @@
  17.104  
  17.105  (*** Projections: fst, snd ***)
  17.106  
  17.107 -qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a"
  17.108 +qed_goalw "fst_conv" thy [fst_def] "fst(<a,b>) = a"
  17.109   (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
  17.110  
  17.111 -qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b"
  17.112 +qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b"
  17.113   (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
  17.114  
  17.115  Addsimps [fst_conv,snd_conv];
  17.116  
  17.117 -qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
  17.118 +qed_goal "fst_type" thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
  17.119   (fn _=> [ Auto_tac ]);
  17.120  
  17.121 -qed_goal "snd_type" ZF.thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
  17.122 +qed_goal "snd_type" thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
  17.123   (fn _=> [ Auto_tac ]);
  17.124  
  17.125 -qed_goal "Pair_fst_snd_eq" ZF.thy
  17.126 +qed_goal "Pair_fst_snd_eq" thy
  17.127      "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
  17.128   (fn _=> [ Auto_tac ]);
  17.129  
  17.130 @@ -135,13 +135,13 @@
  17.131  (*** Eliminator - split ***)
  17.132  
  17.133  (*A META-equality, so that it applies to higher types as well...*)
  17.134 -qed_goalw "split" ZF.thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
  17.135 +qed_goalw "split" thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
  17.136   (fn _ => [ (Simp_tac 1),
  17.137              (rtac reflexive_thm 1) ]);
  17.138  
  17.139  Addsimps [split];
  17.140  
  17.141 -qed_goal "split_type" ZF.thy
  17.142 +qed_goal "split_type" thy
  17.143      "[|  p:Sigma(A,B);   \
  17.144  \        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \
  17.145  \    |] ==> split(%x y. c(x,y), p) : C(p)"
  17.146 @@ -149,8 +149,8 @@
  17.147    [ (rtac (major RS SigmaE) 1),
  17.148      (asm_simp_tac (simpset() addsimps prems) 1) ]);
  17.149  
  17.150 -goalw ZF.thy [split_def]
  17.151 -  "!!u. u: A*B ==>   \
  17.152 +Goalw [split_def]
  17.153 +  "u: A*B ==>   \
  17.154  \       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
  17.155  by Auto_tac;
  17.156  qed "expand_split";
  17.157 @@ -158,11 +158,11 @@
  17.158  
  17.159  (*** split for predicates: result type o ***)
  17.160  
  17.161 -goalw ZF.thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)";
  17.162 +Goalw [split_def] "R(a,b) ==> split(R, <a,b>)";
  17.163  by (Asm_simp_tac 1);
  17.164  qed "splitI";
  17.165  
  17.166 -val major::sigma::prems = goalw ZF.thy [split_def]
  17.167 +val major::sigma::prems = Goalw [split_def]
  17.168      "[| split(R,z);  z:Sigma(A,B);                      \
  17.169  \       !!x y. [| z = <x,y>;  R(x,y) |] ==> P           \
  17.170  \    |] ==> P";
  17.171 @@ -172,7 +172,7 @@
  17.172  by (Asm_full_simp_tac 1);
  17.173  qed "splitE";
  17.174  
  17.175 -goalw ZF.thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)";
  17.176 +Goalw [split_def] "split(R,<a,b>) ==> R(a,b)";
  17.177  by (Full_simp_tac 1);
  17.178  qed "splitD";
  17.179  
    18.1 --- a/src/ZF/simpdata.ML	Mon Aug 17 13:06:29 1998 +0200
    18.2 +++ b/src/ZF/simpdata.ML	Mon Aug 17 13:09:08 1998 +0200
    18.3 @@ -10,7 +10,7 @@
    18.4  
    18.5  local
    18.6    (*For proving rewrite rules*)
    18.7 -  fun prover s = (prove_goal ZF.thy s (fn _ => [Blast_tac 1]));
    18.8 +  fun prover s = (prove_goal thy s (fn _ => [Blast_tac 1]));
    18.9  
   18.10  in
   18.11  
    19.1 --- a/src/ZF/subset.ML	Mon Aug 17 13:06:29 1998 +0200
    19.2 +++ b/src/ZF/subset.ML	Mon Aug 17 13:09:08 1998 +0200
    19.3 @@ -9,38 +9,38 @@
    19.4  
    19.5  (*** cons ***)
    19.6  
    19.7 -qed_goal "cons_subsetI" ZF.thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C"
    19.8 +qed_goal "cons_subsetI" thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C"
    19.9   (fn _ => [ Blast_tac 1 ]);
   19.10  
   19.11 -qed_goal "subset_consI" ZF.thy "B <= cons(a,B)"
   19.12 +qed_goal "subset_consI" thy "B <= cons(a,B)"
   19.13   (fn _ => [ Blast_tac 1 ]);
   19.14  
   19.15 -qed_goal "cons_subset_iff" ZF.thy "cons(a,B)<=C <-> a:C & B<=C"
   19.16 +qed_goal "cons_subset_iff" thy "cons(a,B)<=C <-> a:C & B<=C"
   19.17   (fn _ => [ Blast_tac 1 ]);
   19.18  
   19.19  (*A safe special case of subset elimination, adding no new variables 
   19.20    [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
   19.21  bind_thm ("cons_subsetE", cons_subset_iff RS iffD1 RS conjE);
   19.22  
   19.23 -qed_goal "subset_empty_iff" ZF.thy "A<=0 <-> A=0"
   19.24 +qed_goal "subset_empty_iff" thy "A<=0 <-> A=0"
   19.25   (fn _=> [ (Blast_tac 1) ]);
   19.26  
   19.27 -qed_goal "subset_cons_iff" ZF.thy
   19.28 +qed_goal "subset_cons_iff" thy
   19.29      "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
   19.30   (fn _=> [ (Blast_tac 1) ]);
   19.31  
   19.32  (*** succ ***)
   19.33  
   19.34 -qed_goal "subset_succI" ZF.thy "i <= succ(i)"
   19.35 +qed_goal "subset_succI" thy "i <= succ(i)"
   19.36   (fn _=> [ (Blast_tac 1) ]);
   19.37  
   19.38  (*But if j is an ordinal or is transitive, then i:j implies i<=j! 
   19.39    See ordinal/Ord_succ_subsetI*)
   19.40 -qed_goalw "succ_subsetI" ZF.thy [succ_def]
   19.41 +qed_goalw "succ_subsetI" thy [succ_def]
   19.42      "!!i j. [| i:j;  i<=j |] ==> succ(i)<=j"
   19.43   (fn _=> [ (Blast_tac 1) ]);
   19.44  
   19.45 -qed_goalw "succ_subsetE" ZF.thy [succ_def] 
   19.46 +qed_goalw "succ_subsetE" thy [succ_def] 
   19.47      "[| succ(i) <= j;  [| i:j;  i<=j |] ==> P \
   19.48  \    |] ==> P"
   19.49   (fn major::prems=>
   19.50 @@ -49,22 +49,22 @@
   19.51  
   19.52  (*** singletons ***)
   19.53  
   19.54 -qed_goal "singleton_subsetI" ZF.thy "!!a c. a:C ==> {a} <= C"
   19.55 +qed_goal "singleton_subsetI" thy "!!a c. a:C ==> {a} <= C"
   19.56   (fn _=> [ (Blast_tac 1) ]);
   19.57  
   19.58 -qed_goal "singleton_subsetD" ZF.thy "!!a C. {a} <= C  ==>  a:C"
   19.59 +qed_goal "singleton_subsetD" thy "!!a C. {a} <= C  ==>  a:C"
   19.60   (fn _=> [ (Blast_tac 1) ]);
   19.61  
   19.62  (*** Big Union -- least upper bound of a set  ***)
   19.63  
   19.64 -qed_goal "Union_subset_iff" ZF.thy "Union(A) <= C <-> (ALL x:A. x <= C)"
   19.65 +qed_goal "Union_subset_iff" thy "Union(A) <= C <-> (ALL x:A. x <= C)"
   19.66   (fn _ => [ Blast_tac 1 ]);
   19.67  
   19.68 -qed_goal "Union_upper" ZF.thy
   19.69 +qed_goal "Union_upper" thy
   19.70      "!!B A. B:A ==> B <= Union(A)"
   19.71   (fn _ => [ Blast_tac 1 ]);
   19.72  
   19.73 -qed_goal "Union_least" ZF.thy
   19.74 +qed_goal "Union_least" thy
   19.75      "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"
   19.76   (fn [prem]=>
   19.77    [ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1),
   19.78 @@ -72,19 +72,19 @@
   19.79  
   19.80  (*** Union of a family of sets  ***)
   19.81  
   19.82 -goal ZF.thy "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
   19.83 +Goal "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
   19.84  by (blast_tac (claset() addSEs [equalityE]) 1);
   19.85  qed "subset_UN_iff_eq";
   19.86  
   19.87 -qed_goal "UN_subset_iff" ZF.thy
   19.88 +qed_goal "UN_subset_iff" thy
   19.89       "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"
   19.90   (fn _ => [ Blast_tac 1 ]);
   19.91  
   19.92 -qed_goal "UN_upper" ZF.thy
   19.93 +qed_goal "UN_upper" thy
   19.94      "!!x A. x:A ==> B(x) <= (UN x:A. B(x))"
   19.95   (fn _ => [ etac (RepFunI RS Union_upper) 1 ]);
   19.96  
   19.97 -qed_goal "UN_least" ZF.thy
   19.98 +qed_goal "UN_least" thy
   19.99      "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"
  19.100   (fn [prem]=>
  19.101    [ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1),
  19.102 @@ -93,14 +93,14 @@
  19.103  
  19.104  (*** Big Intersection -- greatest lower bound of a nonempty set ***)
  19.105  
  19.106 -qed_goal "Inter_subset_iff" ZF.thy
  19.107 +qed_goal "Inter_subset_iff" thy
  19.108       "!!a A. a: A  ==>  C <= Inter(A) <-> (ALL x:A. C <= x)"
  19.109   (fn _ => [ Blast_tac 1 ]);
  19.110  
  19.111 -qed_goal "Inter_lower" ZF.thy "!!B A. B:A ==> Inter(A) <= B"
  19.112 +qed_goal "Inter_lower" thy "!!B A. B:A ==> Inter(A) <= B"
  19.113   (fn _ => [ Blast_tac 1 ]);
  19.114  
  19.115 -qed_goal "Inter_greatest" ZF.thy
  19.116 +qed_goal "Inter_greatest" thy
  19.117      "[| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)"
  19.118   (fn [prem1,prem2]=>
  19.119    [ (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1),
  19.120 @@ -108,11 +108,11 @@
  19.121  
  19.122  (*** Intersection of a family of sets  ***)
  19.123  
  19.124 -qed_goal "INT_lower" ZF.thy
  19.125 +qed_goal "INT_lower" thy
  19.126      "!!x. x:A ==> (INT x:A. B(x)) <= B(x)"
  19.127   (fn _ => [ Blast_tac 1 ]);
  19.128  
  19.129 -qed_goal "INT_greatest" ZF.thy
  19.130 +qed_goal "INT_greatest" thy
  19.131      "[| a:A;  !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"
  19.132   (fn [nonempty,prem] =>
  19.133    [ rtac (nonempty RS RepFunI RS Inter_greatest) 1,
  19.134 @@ -121,53 +121,58 @@
  19.135  
  19.136  (*** Finite Union -- the least upper bound of 2 sets ***)
  19.137  
  19.138 -qed_goal "Un_subset_iff" ZF.thy "A Un B <= C <-> A <= C & B <= C"
  19.139 +qed_goal "Un_subset_iff" thy "A Un B <= C <-> A <= C & B <= C"
  19.140   (fn _ => [ Blast_tac 1 ]);
  19.141  
  19.142 -qed_goal "Un_upper1" ZF.thy "A <= A Un B"
  19.143 +qed_goal "Un_upper1" thy "A <= A Un B"
  19.144   (fn _ => [ Blast_tac 1 ]);
  19.145  
  19.146 -qed_goal "Un_upper2" ZF.thy "B <= A Un B"
  19.147 +qed_goal "Un_upper2" thy "B <= A Un B"
  19.148   (fn _ => [ Blast_tac 1 ]);
  19.149  
  19.150 -qed_goal "Un_least" ZF.thy "!!A B C. [| A<=C;  B<=C |] ==> A Un B <= C"
  19.151 +qed_goal "Un_least" thy "!!A B C. [| A<=C;  B<=C |] ==> A Un B <= C"
  19.152   (fn _ => [ Blast_tac 1 ]);
  19.153  
  19.154  
  19.155  (*** Finite Intersection -- the greatest lower bound of 2 sets *)
  19.156  
  19.157 -qed_goal "Int_subset_iff" ZF.thy "C <= A Int B <-> C <= A & C <= B"
  19.158 +qed_goal "Int_subset_iff" thy "C <= A Int B <-> C <= A & C <= B"
  19.159   (fn _ => [ Blast_tac 1 ]);
  19.160  
  19.161 -qed_goal "Int_lower1" ZF.thy "A Int B <= A"
  19.162 +qed_goal "Int_lower1" thy "A Int B <= A"
  19.163   (fn _ => [ Blast_tac 1 ]);
  19.164  
  19.165 -qed_goal "Int_lower2" ZF.thy "A Int B <= B"
  19.166 +qed_goal "Int_lower2" thy "A Int B <= B"
  19.167   (fn _ => [ Blast_tac 1 ]);
  19.168  
  19.169 -qed_goal "Int_greatest" ZF.thy "!!A B C. [| C<=A;  C<=B |] ==> C <= A Int B"
  19.170 +qed_goal "Int_greatest" thy "!!A B C. [| C<=A;  C<=B |] ==> C <= A Int B"
  19.171   (fn _ => [ Blast_tac 1 ]);
  19.172  
  19.173  
  19.174  (*** Set difference *)
  19.175  
  19.176 -qed_goal "Diff_subset" ZF.thy "A-B <= A"
  19.177 +qed_goal "Diff_subset" thy "A-B <= A"
  19.178   (fn _ => [ Blast_tac 1 ]);
  19.179  
  19.180 -qed_goal "Diff_contains" ZF.thy
  19.181 +qed_goal "Diff_contains" thy
  19.182      "!!C. [| C<=A;  C Int B = 0 |] ==> C <= A-B"
  19.183 - (fn _ => [ (blast_tac (claset() addSEs [equalityE]) 1) ]);
  19.184 + (fn _ => [ Blast_tac 1 ]);
  19.185 +
  19.186 +Goal "B <= A - cons(c,C)  <->  B<=A-C & c ~: B";
  19.187 +by (Blast_tac 1);
  19.188 +qed "subset_Diff_cons_iff";
  19.189 +
  19.190  
  19.191  
  19.192  (** Collect **)
  19.193  
  19.194 -qed_goal "Collect_subset" ZF.thy "Collect(A,P) <= A"
  19.195 +qed_goal "Collect_subset" thy "Collect(A,P) <= A"
  19.196   (fn _ => [ Blast_tac 1 ]);
  19.197  
  19.198  
  19.199  (** RepFun **)
  19.200  
  19.201 -val prems = goal ZF.thy "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
  19.202 +val prems = Goal "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
  19.203  by (blast_tac (claset() addIs prems) 1);
  19.204  qed "RepFun_subset";
  19.205  
    20.1 --- a/src/ZF/upair.ML	Mon Aug 17 13:06:29 1998 +0200
    20.2 +++ b/src/ZF/upair.ML	Mon Aug 17 13:09:08 1998 +0200
    20.3 @@ -21,19 +21,19 @@
    20.4  
    20.5  (*** Unordered pairs - Upair ***)
    20.6  
    20.7 -qed_goalw "Upair_iff" ZF.thy [Upair_def]
    20.8 +qed_goalw "Upair_iff" thy [Upair_def]
    20.9      "c : Upair(a,b) <-> (c=a | c=b)"
   20.10   (fn _ => [ (blast_tac (claset() addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);
   20.11  
   20.12  Addsimps [Upair_iff];
   20.13  
   20.14 -qed_goal "UpairI1" ZF.thy "a : Upair(a,b)"
   20.15 +qed_goal "UpairI1" thy "a : Upair(a,b)"
   20.16   (fn _ => [ Simp_tac 1 ]);
   20.17  
   20.18 -qed_goal "UpairI2" ZF.thy "b : Upair(a,b)"
   20.19 +qed_goal "UpairI2" thy "b : Upair(a,b)"
   20.20   (fn _ => [ Simp_tac 1 ]);
   20.21  
   20.22 -qed_goal "UpairE" ZF.thy
   20.23 +qed_goal "UpairE" thy
   20.24      "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
   20.25   (fn major::prems=>
   20.26    [ (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1),
   20.27 @@ -44,25 +44,25 @@
   20.28  
   20.29  (*** Rules for binary union -- Un -- defined via Upair ***)
   20.30  
   20.31 -qed_goalw "Un_iff" ZF.thy [Un_def] "c : A Un B <-> (c:A | c:B)"
   20.32 +qed_goalw "Un_iff" thy [Un_def] "c : A Un B <-> (c:A | c:B)"
   20.33   (fn _ => [ Blast_tac 1 ]);
   20.34  
   20.35  Addsimps [Un_iff];
   20.36  
   20.37 -qed_goal "UnI1" ZF.thy "!!c. c : A ==> c : A Un B"
   20.38 +qed_goal "UnI1" thy "!!c. c : A ==> c : A Un B"
   20.39   (fn _ => [ Asm_simp_tac 1 ]);
   20.40  
   20.41 -qed_goal "UnI2" ZF.thy "!!c. c : B ==> c : A Un B"
   20.42 +qed_goal "UnI2" thy "!!c. c : B ==> c : A Un B"
   20.43   (fn _ => [ Asm_simp_tac 1 ]);
   20.44  
   20.45 -qed_goal "UnE" ZF.thy 
   20.46 +qed_goal "UnE" thy 
   20.47      "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
   20.48   (fn major::prems=>
   20.49    [ (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1),
   20.50      (REPEAT (eresolve_tac prems 1)) ]);
   20.51  
   20.52  (*Stronger version of the rule above*)
   20.53 -qed_goal "UnE'" ZF.thy
   20.54 +qed_goal "UnE'" thy
   20.55      "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P"
   20.56   (fn major::prems =>
   20.57    [(rtac (major RS UnE) 1),
   20.58 @@ -73,7 +73,7 @@
   20.59     (etac notnotD 1)]);
   20.60  
   20.61  (*Classical introduction rule: no commitment to A vs B*)
   20.62 -qed_goal "UnCI" ZF.thy "(c ~: B ==> c : A) ==> c : A Un B"
   20.63 +qed_goal "UnCI" thy "(c ~: B ==> c : A) ==> c : A Un B"
   20.64   (fn prems=>
   20.65    [ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
   20.66  
   20.67 @@ -83,21 +83,21 @@
   20.68  
   20.69  (*** Rules for small intersection -- Int -- defined via Upair ***)
   20.70  
   20.71 -qed_goalw "Int_iff" ZF.thy [Int_def] "c : A Int B <-> (c:A & c:B)"
   20.72 +qed_goalw "Int_iff" thy [Int_def] "c : A Int B <-> (c:A & c:B)"
   20.73   (fn _ => [ Blast_tac 1 ]);
   20.74  
   20.75  Addsimps [Int_iff];
   20.76  
   20.77 -qed_goal "IntI" ZF.thy "!!c. [| c : A;  c : B |] ==> c : A Int B"
   20.78 +qed_goal "IntI" thy "!!c. [| c : A;  c : B |] ==> c : A Int B"
   20.79   (fn _ => [ Asm_simp_tac 1 ]);
   20.80  
   20.81 -qed_goal "IntD1" ZF.thy "!!c. c : A Int B ==> c : A"
   20.82 +qed_goal "IntD1" thy "!!c. c : A Int B ==> c : A"
   20.83   (fn _ => [ Asm_full_simp_tac 1 ]);
   20.84  
   20.85 -qed_goal "IntD2" ZF.thy "!!c. c : A Int B ==> c : B"
   20.86 +qed_goal "IntD2" thy "!!c. c : A Int B ==> c : B"
   20.87   (fn _ => [ Asm_full_simp_tac 1 ]);
   20.88  
   20.89 -qed_goal "IntE" ZF.thy
   20.90 +qed_goal "IntE" thy
   20.91      "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
   20.92   (fn prems=>
   20.93    [ (resolve_tac prems 1),
   20.94 @@ -108,21 +108,21 @@
   20.95  
   20.96  (*** Rules for set difference -- defined via Upair ***)
   20.97  
   20.98 -qed_goalw "Diff_iff" ZF.thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
   20.99 +qed_goalw "Diff_iff" thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
  20.100   (fn _ => [ Blast_tac 1 ]);
  20.101  
  20.102  Addsimps [Diff_iff];
  20.103  
  20.104 -qed_goal "DiffI" ZF.thy "!!c. [| c : A;  c ~: B |] ==> c : A - B"
  20.105 +qed_goal "DiffI" thy "!!c. [| c : A;  c ~: B |] ==> c : A - B"
  20.106   (fn _ => [ Asm_simp_tac 1 ]);
  20.107  
  20.108 -qed_goal "DiffD1" ZF.thy "!!c. c : A - B ==> c : A"
  20.109 +qed_goal "DiffD1" thy "!!c. c : A - B ==> c : A"
  20.110   (fn _ => [ Asm_full_simp_tac 1 ]);
  20.111  
  20.112 -qed_goal "DiffD2" ZF.thy "!!c. c : A - B ==> c ~: B"
  20.113 +qed_goal "DiffD2" thy "!!c. c : A - B ==> c ~: B"
  20.114   (fn _ => [ Asm_full_simp_tac 1 ]);
  20.115  
  20.116 -qed_goal "DiffE" ZF.thy
  20.117 +qed_goal "DiffE" thy
  20.118      "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
  20.119   (fn prems=>
  20.120    [ (resolve_tac prems 1),
  20.121 @@ -133,27 +133,27 @@
  20.122  
  20.123  (*** Rules for cons -- defined via Un and Upair ***)
  20.124  
  20.125 -qed_goalw "cons_iff" ZF.thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
  20.126 +qed_goalw "cons_iff" thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
  20.127   (fn _ => [ Blast_tac 1 ]);
  20.128  
  20.129  Addsimps [cons_iff];
  20.130  
  20.131 -qed_goal "consI1" ZF.thy "a : cons(a,B)"
  20.132 +qed_goal "consI1" thy "a : cons(a,B)"
  20.133   (fn _ => [ Simp_tac 1 ]);
  20.134  
  20.135  Addsimps [consI1];
  20.136  
  20.137 -qed_goal "consI2" ZF.thy "!!B. a : B ==> a : cons(b,B)"
  20.138 +qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)"
  20.139   (fn _ => [ Asm_simp_tac 1 ]);
  20.140  
  20.141 -qed_goal "consE" ZF.thy
  20.142 +qed_goal "consE" thy
  20.143      "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P"
  20.144   (fn major::prems=>
  20.145    [ (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1),
  20.146      (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);
  20.147  
  20.148  (*Stronger version of the rule above*)
  20.149 -qed_goal "consE'" ZF.thy
  20.150 +qed_goal "consE'" thy
  20.151      "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
  20.152   (fn major::prems =>
  20.153    [(rtac (major RS consE) 1),
  20.154 @@ -164,14 +164,14 @@
  20.155     (etac notnotD 1)]);
  20.156  
  20.157  (*Classical introduction rule*)
  20.158 -qed_goal "consCI" ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)"
  20.159 +qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)"
  20.160   (fn prems=>
  20.161    [ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
  20.162  
  20.163  AddSIs [consCI];
  20.164  AddSEs [consE];
  20.165  
  20.166 -qed_goal "cons_not_0" ZF.thy "cons(a,B) ~= 0"
  20.167 +qed_goal "cons_not_0" thy "cons(a,B) ~= 0"
  20.168   (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
  20.169  
  20.170  bind_thm ("cons_neq_0", cons_not_0 RS notE);
  20.171 @@ -181,10 +181,10 @@
  20.172  
  20.173  (*** Singletons - using cons ***)
  20.174  
  20.175 -qed_goal "singleton_iff" ZF.thy "a : {b} <-> a=b"
  20.176 +qed_goal "singleton_iff" thy "a : {b} <-> a=b"
  20.177   (fn _ => [ Simp_tac 1 ]);
  20.178  
  20.179 -qed_goal "singletonI" ZF.thy "a : {a}"
  20.180 +qed_goal "singletonI" thy "a : {a}"
  20.181   (fn _=> [ (rtac consI1 1) ]);
  20.182  
  20.183  bind_thm ("singletonE", make_elim (singleton_iff RS iffD1));
  20.184 @@ -194,25 +194,25 @@
  20.185  
  20.186  (*** Rules for Descriptions ***)
  20.187  
  20.188 -qed_goalw "the_equality" ZF.thy [the_def]
  20.189 +qed_goalw "the_equality" thy [the_def]
  20.190      "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
  20.191   (fn [pa,eq] =>
  20.192    [ (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ]);
  20.193  
  20.194  (* Only use this if you already know EX!x. P(x) *)
  20.195 -qed_goal "the_equality2" ZF.thy
  20.196 +qed_goal "the_equality2" thy
  20.197      "!!P. [| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
  20.198   (fn _ =>
  20.199    [ (deepen_tac (claset() addSIs [the_equality]) 1 1) ]);
  20.200  
  20.201 -qed_goal "theI" ZF.thy "EX! x. P(x) ==> P(THE x. P(x))"
  20.202 +qed_goal "theI" thy "EX! x. P(x) ==> P(THE x. P(x))"
  20.203   (fn [major]=>
  20.204    [ (rtac (major RS ex1E) 1),
  20.205      (resolve_tac [major RS the_equality2 RS ssubst] 1),
  20.206      (REPEAT (assume_tac 1)) ]);
  20.207  
  20.208  (*Easier to apply than theI: conclusion has only one occurrence of P*)
  20.209 -qed_goal "theI2" ZF.thy
  20.210 +qed_goal "theI2" thy
  20.211      "[| EX! x. P(x);  !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))"
  20.212   (fn prems => [ resolve_tac prems 1, 
  20.213                  rtac theI 1, 
  20.214 @@ -222,42 +222,42 @@
  20.215    (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
  20.216  
  20.217  (*If it's "undefined", it's zero!*)
  20.218 -qed_goalw "the_0" ZF.thy [the_def]
  20.219 +qed_goalw "the_0" thy [the_def]
  20.220      "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
  20.221   (fn _ => [ (deepen_tac (claset() addSEs [ReplaceE]) 0 1) ]);
  20.222  
  20.223  
  20.224  (*** if -- a conditional expression for formulae ***)
  20.225  
  20.226 -goalw ZF.thy [if_def] "if(True,a,b) = a";
  20.227 +Goalw [if_def] "if(True,a,b) = a";
  20.228  by (blast_tac (claset() addSIs [the_equality]) 1);
  20.229  qed "if_true";
  20.230  
  20.231 -goalw ZF.thy [if_def] "if(False,a,b) = b";
  20.232 +Goalw [if_def] "if(False,a,b) = b";
  20.233  by (blast_tac (claset() addSIs [the_equality]) 1);
  20.234  qed "if_false";
  20.235  
  20.236  (*Never use with case splitting, or if P is known to be true or false*)
  20.237 -val prems = goalw ZF.thy [if_def]
  20.238 +val prems = Goalw [if_def]
  20.239      "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
  20.240  by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1);
  20.241  qed "if_cong";
  20.242  
  20.243  (*Not needed for rewriting, since P would rewrite to True anyway*)
  20.244 -goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
  20.245 +Goalw [if_def] "P ==> if(P,a,b) = a";
  20.246  by (blast_tac (claset() addSIs [the_equality]) 1);
  20.247  qed "if_P";
  20.248  
  20.249  (*Not needed for rewriting, since P would rewrite to False anyway*)
  20.250 -goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
  20.251 +Goalw [if_def] "~P ==> if(P,a,b) = b";
  20.252  by (blast_tac (claset() addSIs [the_equality]) 1);
  20.253  qed "if_not_P";
  20.254  
  20.255  Addsimps [if_true, if_false];
  20.256  
  20.257 -qed_goal "split_if" ZF.thy
  20.258 +qed_goal "split_if" thy
  20.259      "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
  20.260 - (fn _=> [ (excluded_middle_tac "Q" 1),
  20.261 + (fn _=> [ (case_tac "Q" 1),
  20.262             (Asm_simp_tac 1),
  20.263             (Asm_simp_tac 1) ]);
  20.264  
  20.265 @@ -275,10 +275,10 @@
  20.266  		 split_if_mem1, split_if_mem2];
  20.267  
  20.268  (*Logically equivalent to split_if_mem2*)
  20.269 -qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
  20.270 +qed_goal "if_iff" thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
  20.271   (fn _=> [ (simp_tac (simpset() addsplits [split_if]) 1) ]);
  20.272  
  20.273 -qed_goal "if_type" ZF.thy
  20.274 +qed_goal "if_type" thy
  20.275      "[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A"
  20.276   (fn prems=> [ (simp_tac 
  20.277                  (simpset() addsimps prems addsplits [split_if]) 1) ]);
  20.278 @@ -287,48 +287,48 @@
  20.279  (*** Foundation lemmas ***)
  20.280  
  20.281  (*was called mem_anti_sym*)
  20.282 -qed_goal "mem_asym" ZF.thy "[| a:b;  ~P ==> b:a |] ==> P"
  20.283 +qed_goal "mem_asym" thy "[| a:b;  ~P ==> b:a |] ==> P"
  20.284   (fn prems=>
  20.285    [ (rtac classical 1),
  20.286      (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
  20.287      REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1) ]);
  20.288  
  20.289  (*was called mem_anti_refl*)
  20.290 -qed_goal "mem_irrefl" ZF.thy "a:a ==> P"
  20.291 +qed_goal "mem_irrefl" thy "a:a ==> P"
  20.292   (fn [major]=> [ (rtac ([major,major] MRS mem_asym) 1) ]);
  20.293  
  20.294  (*mem_irrefl should NOT be added to default databases:
  20.295        it would be tried on most goals, making proofs slower!*)
  20.296  
  20.297 -qed_goal "mem_not_refl" ZF.thy "a ~: a"
  20.298 +qed_goal "mem_not_refl" thy "a ~: a"
  20.299   (K [ (rtac notI 1), (etac mem_irrefl 1) ]);
  20.300  
  20.301  (*Good for proving inequalities by rewriting*)
  20.302 -qed_goal "mem_imp_not_eq" ZF.thy "!!a A. a:A ==> a ~= A"
  20.303 +qed_goal "mem_imp_not_eq" thy "!!a A. a:A ==> a ~= A"
  20.304   (fn _=> [ blast_tac (claset() addSEs [mem_irrefl]) 1 ]);
  20.305  
  20.306  (*** Rules for succ ***)
  20.307  
  20.308 -qed_goalw "succ_iff" ZF.thy [succ_def] "i : succ(j) <-> i=j | i:j"
  20.309 +qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j"
  20.310   (fn _ => [ Blast_tac 1 ]);
  20.311  
  20.312 -qed_goalw "succI1" ZF.thy [succ_def] "i : succ(i)"
  20.313 +qed_goalw "succI1" thy [succ_def] "i : succ(i)"
  20.314   (fn _=> [ (rtac consI1 1) ]);
  20.315  
  20.316  Addsimps [succI1];
  20.317  
  20.318 -qed_goalw "succI2" ZF.thy [succ_def]
  20.319 +qed_goalw "succI2" thy [succ_def]
  20.320      "i : j ==> i : succ(j)"
  20.321   (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
  20.322  
  20.323 -qed_goalw "succE" ZF.thy [succ_def]
  20.324 +qed_goalw "succE" thy [succ_def]
  20.325      "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
  20.326   (fn major::prems=>
  20.327    [ (rtac (major RS consE) 1),
  20.328      (REPEAT (eresolve_tac prems 1)) ]);
  20.329  
  20.330  (*Classical introduction rule*)
  20.331 -qed_goal "succCI" ZF.thy "(i~:j ==> i=j) ==> i: succ(j)"
  20.332 +qed_goal "succCI" thy "(i~:j ==> i=j) ==> i: succ(j)"
  20.333   (fn [prem]=>
  20.334    [ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
  20.335      (etac prem 1) ]);
  20.336 @@ -336,7 +336,7 @@
  20.337  AddSIs [succCI];
  20.338  AddSEs [succE];
  20.339  
  20.340 -qed_goal "succ_not_0" ZF.thy "succ(n) ~= 0"
  20.341 +qed_goal "succ_not_0" thy "succ(n) ~= 0"
  20.342   (fn _=> [ (blast_tac (claset() addSEs [equalityE]) 1) ]);
  20.343  
  20.344  bind_thm ("succ_neq_0", succ_not_0 RS notE);
  20.345 @@ -352,7 +352,7 @@
  20.346  bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
  20.347  
  20.348  
  20.349 -qed_goal "succ_inject_iff" ZF.thy "succ(m) = succ(n) <-> m=n"
  20.350 +qed_goal "succ_inject_iff" thy "succ(m) = succ(n) <-> m=n"
  20.351   (fn _=> [ (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ]);
  20.352  
  20.353  bind_thm ("succ_inject", succ_inject_iff RS iffD1);