Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
contains fewer theorems than before
--- a/src/ZF/AC/AC7_AC9.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/AC/AC7_AC9.ML Mon Aug 17 13:09:08 1998 +0200
@@ -13,13 +13,10 @@
(* - Sigma_fun_space_eqpoll *)
(* ********************************************************************** *)
-goal ZF.thy "!!A. [| C~:A; B:A |] ==> B~=C";
-by (Fast_tac 1);
-qed "mem_not_eq_not_mem";
-
Goal "[| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
-by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1]
- addDs [fun_space_emptyD, mem_not_eq_not_mem]) 1);
+by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1,
+ Union_empty_iff RS iffD1]
+ addDs [fun_space_emptyD]) 1);
qed "Sigma_fun_space_not0";
Goal "(ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
--- a/src/ZF/AC/AC_Equiv.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/AC/AC_Equiv.ML Mon Aug 17 13:09:08 1998 +0200
@@ -44,8 +44,7 @@
(* used only in WO1_DC.ML *)
(*Note simpler proof*)
-goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; \
-\ A<=Df; A<=Dg |] ==> f``A=g``A";
+Goal "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A";
by (asm_simp_tac (simpset() addsimps [image_fun]) 1);
qed "images_eq";
--- a/src/ZF/AC/WO6_WO1.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/AC/WO6_WO1.ML Mon Aug 17 13:09:08 1998 +0200
@@ -172,9 +172,8 @@
by (fast_tac (claset() addSEs [LeastI, lt_Ord]) 1);
qed "uu_not_empty";
-goal ZF.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
-by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE,
- sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1));
+Goal "[| r<=A*B; r~=0 |] ==> domain(r)~=0";
+by (Blast_tac 1);
qed "not_empty_rel_imp_domain";
Goal "[| b<a; g<a; f`b~=0; f`g~=0; \
@@ -186,7 +185,7 @@
THEN (REPEAT (ares_tac [lt_Ord] 1)));
qed "Least_uu_not_empty_lt_a";
-goal ZF.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
+Goal "[| B<=A; a~:B |] ==> B <= A-{a}";
by (Blast_tac 1);
qed "subset_Diff_sing";
@@ -194,14 +193,11 @@
Goal "[| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
by (etac natE 1);
by (fast_tac (claset() addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
-by (hyp_subst_tac 1);
-by (rtac equalityI 1);
-by (assume_tac 2);
-by (rtac subsetI 1);
-by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
-by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2,
- Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS
- succ_lepoll_natE] 1
+by (safe_tac (claset() addSIs [equalityI]));
+by (rtac ccontr 1);
+by (etac (subset_Diff_sing RS subset_imp_lepoll
+ RSN (2, Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS
+ succ_lepoll_natE) 1
THEN REPEAT (assume_tac 1));
qed "supset_lepoll_imp_eq";
--- a/src/ZF/Arith.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/Arith.ML Mon Aug 17 13:09:08 1998 +0200
@@ -34,7 +34,7 @@
Addsimps [rec_0, rec_succ];
-val major::prems = goal Arith.thy
+val major::prems = Goal
"[| n: nat; \
\ a: C(0); \
\ !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) \
@@ -467,7 +467,7 @@
qed "add_lt_mono";
(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
-val lt_mono::ford::prems = goal Ordinal.thy
+val lt_mono::ford::prems = Goal
"[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
\ !!i. i:k ==> Ord(f(i)); \
\ i le j; j:k \
--- a/src/ZF/Cardinal.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/Cardinal.ML Mon Aug 17 13:09:08 1998 +0200
@@ -29,16 +29,15 @@
gfun RS fun_is_rel RS image_subset]) 1);
qed "Banach_last_equation";
-val prems = goal Cardinal.thy
- "[| f: X->Y; g: Y->X |] ==> \
-\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \
-\ (YA Int YB = 0) & (YA Un YB = Y) & \
-\ f``XA=YA & g``YB=XB";
+Goal "[| f: X->Y; g: Y->X |] ==> \
+\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \
+\ (YA Int YB = 0) & (YA Un YB = Y) & \
+\ f``XA=YA & g``YB=XB";
by (REPEAT
(FIRSTGOAL
(resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition])));
by (rtac Banach_last_equation 3);
-by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1));
+by (REPEAT (ares_tac [fun_is_rel, image_subset, lfp_subset] 1));
qed "decomposition";
val prems = goal Cardinal.thy
@@ -740,7 +739,7 @@
(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
set is well-ordered. Proofs simplified by lcp. *)
-goal Nat.thy "!!n. n:nat ==> wf[n](converse(Memrel(n)))";
+Goal "n:nat ==> wf[n](converse(Memrel(n)))";
by (etac nat_induct 1);
by (blast_tac (claset() addIs [wf_onI]) 1);
by (rtac wf_onI 1);
--- a/src/ZF/CardinalArith.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/CardinalArith.ML Mon Aug 17 13:09:08 1998 +0200
@@ -380,8 +380,8 @@
(*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***)
(*A general fact about ordermap*)
-goalw Cardinal.thy [eqpoll_def]
- "!!A. [| well_ord(A,r); x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";
+Goalw [eqpoll_def]
+ "[| well_ord(A,r); x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";
by (rtac exI 1);
by (asm_simp_tac (simpset() addsimps [ordermap_eq_image, well_ord_is_wf]) 1);
by (etac (ordermap_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1);
@@ -808,7 +808,3 @@
addsimps [nat_cadd_eq_add RS sym, cadd_def, eqpoll_refl]) 1);
qed "nat_sum_eqpoll_sum";
-goal Nat.thy "!!m. [| m le n; n:nat |] ==> m:nat";
-by (blast_tac (claset() addSDs [lt_nat_in_nat]) 1);
-qed "le_in_nat";
-
--- a/src/ZF/Nat.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/Nat.ML Mon Aug 17 13:09:08 1998 +0200
@@ -125,6 +125,10 @@
by (assume_tac 1);
qed "lt_nat_in_nat";
+Goal "[| m le n; n:nat |] ==> m:nat";
+by (blast_tac (claset() addSDs [lt_nat_in_nat]) 1);
+qed "le_in_nat";
+
(** Variations on mathematical induction **)
--- a/src/ZF/Sum.thy Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/Sum.thy Mon Aug 17 13:09:08 1998 +0200
@@ -7,7 +7,7 @@
"Part" primitive for simultaneous recursive type definitions
*)
-Sum = Bool + pair +
+Sum = Bool + equalities +
global
--- a/src/ZF/domrange.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/domrange.ML Mon Aug 17 13:09:08 1998 +0200
@@ -8,19 +8,19 @@
(*** converse ***)
-qed_goalw "converse_iff" ZF.thy [converse_def]
+qed_goalw "converse_iff" thy [converse_def]
"<a,b>: converse(r) <-> <b,a>:r"
(fn _ => [ (Blast_tac 1) ]);
-qed_goalw "converseI" ZF.thy [converse_def]
+qed_goalw "converseI" thy [converse_def]
"!!a b r. <a,b>:r ==> <b,a>:converse(r)"
(fn _ => [ (Blast_tac 1) ]);
-qed_goalw "converseD" ZF.thy [converse_def]
+qed_goalw "converseD" thy [converse_def]
"!!a b r. <a,b> : converse(r) ==> <b,a> : r"
(fn _ => [ (Blast_tac 1) ]);
-qed_goalw "converseE" ZF.thy [converse_def]
+qed_goalw "converseE" thy [converse_def]
"[| yx : converse(r); \
\ !!x y. [| yx=<y,x>; <x,y>:r |] ==> P \
\ |] ==> P"
@@ -34,36 +34,36 @@
AddSIs [converseI];
AddSEs [converseD,converseE];
-qed_goal "converse_converse" ZF.thy
+qed_goal "converse_converse" thy
"!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
(fn _ => [ (Blast_tac 1) ]);
-qed_goal "converse_type" ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
+qed_goal "converse_type" thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
(fn _ => [ (Blast_tac 1) ]);
-qed_goal "converse_prod" ZF.thy "converse(A*B) = B*A"
+qed_goal "converse_prod" thy "converse(A*B) = B*A"
(fn _ => [ (Blast_tac 1) ]);
-qed_goal "converse_empty" ZF.thy "converse(0) = 0"
+qed_goal "converse_empty" thy "converse(0) = 0"
(fn _ => [ (Blast_tac 1) ]);
Addsimps [converse_prod, converse_empty];
-val converse_subset_iff = prove_goal ZF.thy
+val converse_subset_iff = prove_goal thy
"!!z. A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
(fn _=> [ (Blast_tac 1) ]);
(*** domain ***)
-qed_goalw "domain_iff" ZF.thy [domain_def]
+qed_goalw "domain_iff" thy [domain_def]
"a: domain(r) <-> (EX y. <a,y>: r)"
(fn _=> [ (Blast_tac 1) ]);
-qed_goal "domainI" ZF.thy "!!a b r. <a,b>: r ==> a: domain(r)"
+qed_goal "domainI" thy "!!a b r. <a,b>: r ==> a: domain(r)"
(fn _=> [ (etac (exI RS (domain_iff RS iffD2)) 1) ]);
-qed_goal "domainE" ZF.thy
+qed_goal "domainE" thy
"[| a : domain(r); !!y. <a,y>: r ==> P |] ==> P"
(fn prems=>
[ (rtac (domain_iff RS iffD1 RS exE) 1),
@@ -72,15 +72,15 @@
AddIs [domainI];
AddSEs [domainE];
-qed_goal "domain_subset" ZF.thy "domain(Sigma(A,B)) <= A"
+qed_goal "domain_subset" thy "domain(Sigma(A,B)) <= A"
(fn _=> [ (Blast_tac 1) ]);
(*** range ***)
-qed_goalw "rangeI" ZF.thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
+qed_goalw "rangeI" thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
(fn _ => [ (etac (converseI RS domainI) 1) ]);
-qed_goalw "rangeE" ZF.thy [range_def]
+qed_goalw "rangeE" thy [range_def]
"[| b : range(r); !!x. <x,b>: r ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS domainE) 1),
@@ -90,7 +90,7 @@
AddIs [rangeI];
AddSEs [rangeE];
-qed_goalw "range_subset" ZF.thy [range_def] "range(A*B) <= B"
+qed_goalw "range_subset" thy [range_def] "range(A*B) <= B"
(fn _ =>
[ (stac converse_prod 1),
(rtac domain_subset 1) ]);
@@ -98,17 +98,17 @@
(*** field ***)
-qed_goalw "fieldI1" ZF.thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
+qed_goalw "fieldI1" thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
(fn _ => [ (Blast_tac 1) ]);
-qed_goalw "fieldI2" ZF.thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
+qed_goalw "fieldI2" thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
(fn _ => [ (Blast_tac 1) ]);
-qed_goalw "fieldCI" ZF.thy [field_def]
+qed_goalw "fieldCI" thy [field_def]
"(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
(fn [prem]=> [ (blast_tac (claset() addIs [prem]) 1) ]);
-qed_goalw "fieldE" ZF.thy [field_def]
+qed_goalw "fieldE" thy [field_def]
"[| a : field(r); \
\ !!x. <a,x>: r ==> P; \
\ !!x. <x,a>: r ==> P |] ==> P"
@@ -119,40 +119,40 @@
AddIs [fieldCI];
AddSEs [fieldE];
-qed_goal "field_subset" ZF.thy "field(A*B) <= A Un B"
+qed_goal "field_subset" thy "field(A*B) <= A Un B"
(fn _ => [ (Blast_tac 1) ]);
-qed_goalw "domain_subset_field" ZF.thy [field_def]
+qed_goalw "domain_subset_field" thy [field_def]
"domain(r) <= field(r)"
(fn _ => [ (rtac Un_upper1 1) ]);
-qed_goalw "range_subset_field" ZF.thy [field_def]
+qed_goalw "range_subset_field" thy [field_def]
"range(r) <= field(r)"
(fn _ => [ (rtac Un_upper2 1) ]);
-qed_goal "domain_times_range" ZF.thy
+qed_goal "domain_times_range" thy
"!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
(fn _ => [ (Blast_tac 1) ]);
-qed_goal "field_times_field" ZF.thy
+qed_goal "field_times_field" thy
"!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)"
(fn _ => [ (Blast_tac 1) ]);
(*** Image of a set under a function/relation ***)
-qed_goalw "image_iff" ZF.thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
+qed_goalw "image_iff" thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
(fn _ => [ (Blast_tac 1) ]);
-qed_goal "image_singleton_iff" ZF.thy "b : r``{a} <-> <a,b>:r"
+qed_goal "image_singleton_iff" thy "b : r``{a} <-> <a,b>:r"
(fn _ => [ rtac (image_iff RS iff_trans) 1,
Blast_tac 1 ]);
-qed_goalw "imageI" ZF.thy [image_def]
+qed_goalw "imageI" thy [image_def]
"!!a b r. [| <a,b>: r; a:A |] ==> b : r``A"
(fn _ => [ (Blast_tac 1) ]);
-qed_goalw "imageE" ZF.thy [image_def]
+qed_goalw "imageE" thy [image_def]
"[| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS CollectE) 1),
@@ -161,32 +161,32 @@
AddIs [imageI];
AddSEs [imageE];
-qed_goal "image_subset" ZF.thy "!!A B r. r <= A*B ==> r``C <= B"
+qed_goal "image_subset" thy "!!A B r. r <= A*B ==> r``C <= B"
(fn _ => [ (Blast_tac 1) ]);
(*** Inverse image of a set under a function/relation ***)
-qed_goalw "vimage_iff" ZF.thy [vimage_def,image_def,converse_def]
+qed_goalw "vimage_iff" thy [vimage_def,image_def,converse_def]
"a : r-``B <-> (EX y:B. <a,y>:r)"
(fn _ => [ (Blast_tac 1) ]);
-qed_goal "vimage_singleton_iff" ZF.thy
+qed_goal "vimage_singleton_iff" thy
"a : r-``{b} <-> <a,b>:r"
(fn _ => [ rtac (vimage_iff RS iff_trans) 1,
Blast_tac 1 ]);
-qed_goalw "vimageI" ZF.thy [vimage_def]
+qed_goalw "vimageI" thy [vimage_def]
"!!A B r. [| <a,b>: r; b:B |] ==> a : r-``B"
(fn _ => [ (Blast_tac 1) ]);
-qed_goalw "vimageE" ZF.thy [vimage_def]
+qed_goalw "vimageE" thy [vimage_def]
"[| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS imageE) 1),
(REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);
-qed_goalw "vimage_subset" ZF.thy [vimage_def]
+qed_goalw "vimage_subset" thy [vimage_def]
"!!A B r. r <= A*B ==> r-``C <= A"
(fn _ => [ (etac (converse_type RS image_subset) 1) ]);
@@ -199,22 +199,22 @@
val ZF_cs = claset() delrules [equalityI];
(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
-goal ZF.thy "!!S. (ALL x:S. EX A B. x <= A*B) ==> \
+Goal "(ALL x:S. EX A B. x <= A*B) ==> \
\ Union(S) <= domain(Union(S)) * range(Union(S))";
by (Blast_tac 1);
qed "rel_Union";
(** The Union of 2 relations is a relation (Lemma for fun_Un) **)
-qed_goal "rel_Un" ZF.thy
+qed_goal "rel_Un" thy
"!!r s. [| r <= A*B; s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
(fn _ => [ (Blast_tac 1) ]);
-goal ZF.thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
+Goal "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
by (Blast_tac 1);
qed "domain_Diff_eq";
-goal ZF.thy "!!r. [| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
+Goal "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
by (Blast_tac 1);
qed "range_Diff_eq";
--- a/src/ZF/domrange.thy Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/domrange.thy Mon Aug 17 13:09:08 1998 +0200
@@ -1,4 +1,4 @@
(*Dummy theory to document dependencies *)
-domrange = pair + "subset"
+domrange = pair + subset
--- a/src/ZF/equalities.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/equalities.ML Mon Aug 17 13:09:08 1998 +0200
@@ -182,7 +182,11 @@
by (blast_tac (claset() addSEs [equalityE]) 1);
qed "Union_disjoint";
-goalw ZF.thy [Inter_def] "Inter(0) = 0";
+Goal "Union(A) = 0 <-> (ALL B:A. B=0)";
+by (Blast_tac 1);
+qed "Union_empty_iff";
+
+Goalw [Inter_def] "Inter(0) = 0";
by (Blast_tac 1);
qed "Inter_0";
@@ -209,7 +213,7 @@
by (Blast_tac 1);
qed "Union_eq_UN";
-goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)";
+Goalw [Inter_def] "Inter(A) = (INT x:A. x)";
by (Blast_tac 1);
qed "Inter_eq_INT";
@@ -344,10 +348,10 @@
by (Blast_tac 1);
qed "domain_of_prod";
-qed_goal "domain_0" ZF.thy "domain(0) = 0"
+qed_goal "domain_0" thy "domain(0) = 0"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "domain_cons" ZF.thy
+qed_goal "domain_cons" thy
"domain(cons(<a,b>,r)) = cons(a, domain(r))"
(fn _ => [ Blast_tac 1 ]);
@@ -376,10 +380,10 @@
by (Blast_tac 1);
qed "range_of_prod";
-qed_goal "range_0" ZF.thy "range(0) = 0"
+qed_goal "range_0" thy "range(0) = 0"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "range_cons" ZF.thy
+qed_goal "range_cons" thy
"range(cons(<a,b>,r)) = cons(b, range(r))"
(fn _ => [ Blast_tac 1 ]);
@@ -404,13 +408,13 @@
(** Field **)
-qed_goal "field_of_prod" ZF.thy "field(A*A) = A"
+qed_goal "field_of_prod" thy "field(A*A) = A"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "field_0" ZF.thy "field(0) = 0"
+qed_goal "field_0" thy "field(0) = 0"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "field_cons" ZF.thy
+qed_goal "field_cons" thy
"field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
(fn _ => [ rtac equalityI 1, ALLGOALS (Blast_tac) ]);
@@ -543,7 +547,7 @@
qed "converse_UN";
(*Unfolding Inter avoids using excluded middle on A=0*)
-goalw ZF.thy [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
+Goalw [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
by (Blast_tac 1);
qed "converse_INT";
--- a/src/ZF/ex/PropLog.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/ex/PropLog.ML Mon Aug 17 13:09:08 1998 +0200
@@ -3,7 +3,7 @@
Author: Tobias Nipkow & Lawrence C Paulson
Copyright 1992 University of Cambridge
-For ex/prop-log.thy. Inductive definition of propositional logic.
+Inductive definition of propositional logic.
Soundness and completeness w.r.t. truth-tables.
Prove: If H|=p then G|=p where G:Fin(H)
@@ -169,23 +169,20 @@
qed "Imp_Fls";
(*Typical example of strengthening the induction formula*)
-val [major] = goal PropLog.thy
- "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
+Goal "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
by (rtac (split_if RS iffD2) 1);
-by (rtac (major RS prop.induct) 1);
+by (etac prop.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H])));
by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1,
- Fls_Imp RS weaken_left_Un2]));
+ Fls_Imp RS weaken_left_Un2]));
by (ALLGOALS (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2,
weaken_right, Imp_Fls])));
qed "hyps_thms_if";
(*Key lemma for completeness; yields a set of assumptions satisfying p*)
-val [premp,sat] = goalw PropLog.thy [logcon_def]
- "[| p: prop; 0 |= p |] ==> hyps(p,t) |- p";
-by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
- rtac (premp RS hyps_thms_if) 2);
-by (Fast_tac 1);
+Goalw [logcon_def] "[| p: prop; 0 |= p |] ==> hyps(p,t) |- p";
+by (dtac hyps_thms_if 1);
+by (Asm_full_simp_tac 1);
qed "logcon_thms_p";
(*For proving certain theorems in our new propositional logic*)
@@ -194,27 +191,24 @@
addIs [thms_in_pl, thms.H, thms.H RS thms_MP];
(*The excluded middle in the form of an elimination rule*)
-val prems = goal PropLog.thy
- "[| p: prop; q: prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
+Goal "[| p: prop; q: prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
by (rtac (deduction RS deduction) 1);
by (rtac (thms.DN RS thms_MP) 1);
-by (ALLGOALS (best_tac (thms_cs addSIs prems)));
+by (ALLGOALS (blast_tac thms_cs));
qed "thms_excluded_middle";
(*Hard to prove directly because it requires cuts*)
-val prems = goal PropLog.thy
- "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p: prop |] ==> H |- q";
+Goal "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p: prop |] ==> H |- q";
by (rtac (thms_excluded_middle RS thms_MP RS thms_MP) 1);
-by (REPEAT (resolve_tac (prems@prop.intrs@[deduction,thms_in_pl]) 1));
+by (REPEAT (ares_tac (prop.intrs@[deduction,thms_in_pl]) 1));
qed "thms_excluded_middle_rule";
(*** Completeness -- lemmas for reducing the set of assumptions ***)
(*For the case hyps(p,t)-cons(#v,Y) |- p;
we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
-val [major] = goal PropLog.thy
- "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
-by (rtac (major RS prop.induct) 1);
+Goal "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
+by (etac prop.induct 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
by (fast_tac (claset() addSEs prop.free_SEs) 1);
@@ -224,9 +218,8 @@
(*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *)
-val [major] = goal PropLog.thy
- "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
-by (rtac (major RS prop.induct) 1);
+Goal "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
+by (etac prop.induct 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
by (fast_tac (claset() addSEs prop.free_SEs) 1);
@@ -236,19 +229,18 @@
(** Two lemmas for use with weaken_left **)
-goal ZF.thy "B-C <= cons(a, B-cons(a,C))";
+Goal "B-C <= cons(a, B-cons(a,C))";
by (Fast_tac 1);
qed "cons_Diff_same";
-goal ZF.thy "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))";
+Goal "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))";
by (Fast_tac 1);
qed "cons_Diff_subset2";
(*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls;
could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*)
-val [major] = goal PropLog.thy
- "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
-by (rtac (major RS prop.induct) 1);
+Goal "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
+by (etac prop.induct 1);
by (asm_simp_tac (simpset() addsimps [UN_I]
setloop (split_tac [split_if])) 2);
by (ALLGOALS Asm_simp_tac);
--- a/src/ZF/ex/misc.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/ex/misc.ML Mon Aug 17 13:09:08 1998 +0200
@@ -10,12 +10,12 @@
writeln"ZF/ex/misc";
(*Nice Blast_tac benchmark. Proved in 0.3s; old tactics can't manage it!*)
-goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
+Goal "ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
by (Blast_tac 1);
result();
(*variant of the benchmark above*)
-goal ZF.thy "!!S. ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
+Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
by (Blast_tac 1);
result();
--- a/src/ZF/func.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/func.ML Mon Aug 17 13:09:08 1998 +0200
@@ -8,32 +8,32 @@
(*** The Pi operator -- dependent function space ***)
-goalw ZF.thy [Pi_def]
+Goalw [Pi_def]
"f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)";
by (Blast_tac 1);
qed "Pi_iff";
(*For upward compatibility with the former definition*)
-goalw ZF.thy [Pi_def, function_def]
+Goalw [Pi_def, function_def]
"f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)";
by (Blast_tac 1);
qed "Pi_iff_old";
-goal ZF.thy "!!f. f: Pi(A,B) ==> function(f)";
+Goal "f: Pi(A,B) ==> function(f)";
by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
qed "fun_is_function";
(**Two "destruct" rules for Pi **)
-val [major] = goalw ZF.thy [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";
-by (rtac (major RS CollectD1 RS PowD) 1);
+Goalw [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";
+by (Blast_tac 1);
qed "fun_is_rel";
-goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> EX! y. <a,y>: f";
+Goal "[| f: Pi(A,B); a:A |] ==> EX! y. <a,y>: f";
by (blast_tac (claset() addSDs [Pi_iff_old RS iffD1]) 1);
qed "fun_unique_Pair";
-val prems = goalw ZF.thy [Pi_def]
+val prems = Goalw [Pi_def]
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
qed "Pi_cong";
@@ -43,26 +43,26 @@
Sigmas and Pis are abbreviated as * or -> *)
(*Weakening one function type to another; see also Pi_type*)
-goalw ZF.thy [Pi_def] "!!f. [| f: A->B; B<=D |] ==> f: A->D";
+Goalw [Pi_def] "[| f: A->B; B<=D |] ==> f: A->D";
by (Best_tac 1);
qed "fun_weaken_type";
(*Empty function spaces*)
-goalw ZF.thy [Pi_def, function_def] "Pi(0,A) = {0}";
+Goalw [Pi_def, function_def] "Pi(0,A) = {0}";
by (Blast_tac 1);
qed "Pi_empty1";
-goalw ZF.thy [Pi_def] "!!A a. a:A ==> A->0 = 0";
+Goalw [Pi_def] "a:A ==> A->0 = 0";
by (Blast_tac 1);
qed "Pi_empty2";
(*The empty function*)
-goalw ZF.thy [Pi_def, function_def] "0: Pi(0,B)";
+Goalw [Pi_def, function_def] "0: Pi(0,B)";
by (Blast_tac 1);
qed "empty_fun";
(*The singleton function*)
-goalw ZF.thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
+Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
by (Blast_tac 1);
qed "singleton_fun";
@@ -70,58 +70,56 @@
(*** Function Application ***)
-goalw ZF.thy [Pi_def, function_def]
- "!!a b f. [| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c";
+Goalw [Pi_def, function_def]
+ "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c";
by (Blast_tac 1);
qed "apply_equality2";
-goalw ZF.thy [apply_def, function_def]
- "!!a b f. [| <a,b>: f; function(f) |] ==> f`a = b";
+Goalw [apply_def, function_def]
+ "[| <a,b>: f; function(f) |] ==> f`a = b";
by (blast_tac (claset() addIs [the_equality]) 1);
qed "function_apply_equality";
-goalw ZF.thy [Pi_def] "!!a b f. [| <a,b>: f; f: Pi(A,B) |] ==> f`a = b";
+Goalw [Pi_def] "[| <a,b>: f; f: Pi(A,B) |] ==> f`a = b";
by (blast_tac (claset() addIs [function_apply_equality]) 1);
qed "apply_equality";
(*Applying a function outside its domain yields 0*)
-goalw ZF.thy [apply_def]
- "!!a. a ~: domain(f) ==> f`a = 0";
+Goalw [apply_def]
+ "a ~: domain(f) ==> f`a = 0";
by (rtac the_0 1);
by (Blast_tac 1);
qed "apply_0";
-goal ZF.thy "!!f. [| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>";
+Goal "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>";
by (forward_tac [fun_is_rel] 1);
by (blast_tac (claset() addDs [apply_equality]) 1);
qed "Pi_memberD";
-goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> <a,f`a>: f";
+Goal "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f";
by (rtac (fun_unique_Pair RS ex1E) 1);
by (resolve_tac [apply_equality RS ssubst] 3);
by (REPEAT (assume_tac 1));
qed "apply_Pair";
(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
-goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> f`a : B(a)";
+Goal "[| f: Pi(A,B); a:A |] ==> f`a : B(a)";
by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
by (REPEAT (ares_tac [apply_Pair] 1));
qed "apply_type";
(*This version is acceptable to the simplifier*)
-goal ZF.thy "!!f. [| f: A->B; a:A |] ==> f`a : B";
+Goal "[| f: A->B; a:A |] ==> f`a : B";
by (REPEAT (ares_tac [apply_type] 1));
qed "apply_funtype";
-val [major] = goal ZF.thy
- "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
-by (cut_facts_tac [major RS fun_is_rel] 1);
-by (blast_tac (claset() addSIs [major RS apply_Pair,
- major RSN (2,apply_equality)]) 1);
+Goal "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
+by (forward_tac [fun_is_rel] 1);
+by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1);
qed "apply_iff";
(*Refining one Pi type to another*)
-val pi_prem::prems = goal ZF.thy
+val pi_prem::prems = Goal
"[| f: Pi(A,C); !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)";
by (cut_facts_tac [pi_prem] 1);
by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
@@ -131,16 +129,16 @@
(** Elimination of membership in a function **)
-goal ZF.thy "!!a A. [| <a,b> : f; f: Pi(A,B) |] ==> a : A";
+Goal "[| <a,b> : f; f: Pi(A,B) |] ==> a : A";
by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));
qed "domain_type";
-goal ZF.thy "!!b B a. [| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)";
+Goal "[| <a,b> : f; f: Pi(A,B) |] ==> b : B(a)";
by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);
by (assume_tac 1);
qed "range_type";
-val prems = goal ZF.thy
+val prems = Goal
"[| <a,b>: f; f: Pi(A,B); \
\ [| a:A; b:B(a); f`a = b |] ==> P \
\ |] ==> P";
@@ -151,35 +149,35 @@
(*** Lambda Abstraction ***)
-goalw ZF.thy [lam_def] "!!A b. a:A ==> <a,b(a)> : (lam x:A. b(x))";
+Goalw [lam_def] "a:A ==> <a,b(a)> : (lam x:A. b(x))";
by (etac RepFunI 1);
qed "lamI";
-val major::prems = goalw ZF.thy [lam_def]
+val major::prems = Goalw [lam_def]
"[| p: (lam x:A. b(x)); !!x.[| x:A; p=<x,b(x)> |] ==> P \
\ |] ==> P";
by (rtac (major RS RepFunE) 1);
by (REPEAT (ares_tac prems 1));
qed "lamE";
-goal ZF.thy "!!a b c. [| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";
+Goal "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";
by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));
qed "lamD";
-val prems = goalw ZF.thy [lam_def, Pi_def, function_def]
+val prems = Goalw [lam_def, Pi_def, function_def]
"[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)";
by (blast_tac (claset() addIs prems) 1);
qed "lam_type";
-goal ZF.thy "(lam x:A. b(x)) : A -> {b(x). x:A}";
+Goal "(lam x:A. b(x)) : A -> {b(x). x:A}";
by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
qed "lam_funtype";
-goal ZF.thy "!!a A. a : A ==> (lam x:A. b(x)) ` a = b(a)";
+Goal "a : A ==> (lam x:A. b(x)) ` a = b(a)";
by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
qed "beta";
-goalw ZF.thy [lam_def] "(lam x:0. b(x)) = 0";
+Goalw [lam_def] "(lam x:0. b(x)) = 0";
by (Simp_tac 1);
qed "lam_empty";
@@ -190,14 +188,14 @@
Addsimps [beta, lam_empty, domain_lam];
(*congruence rule for lambda abstraction*)
-val prems = goalw ZF.thy [lam_def]
+val prems = Goalw [lam_def]
"[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')";
by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
qed "lam_cong";
Addcongs [lam_cong];
-val [major] = goal ZF.thy
+val [major] = Goal
"(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
by (rtac ballI 1);
@@ -210,7 +208,7 @@
(** Extensionality **)
(*Semi-extensionality!*)
-val prems = goal ZF.thy
+val prems = Goal
"[| f : Pi(A,B); g: Pi(C,D); A<=C; \
\ !!x. x:A ==> f`x = g`x |] ==> f<=g";
by (rtac subsetI 1);
@@ -220,27 +218,27 @@
by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
qed "fun_subset";
-val prems = goal ZF.thy
+val prems = Goal
"[| f : Pi(A,B); g: Pi(A,D); \
\ !!x. x:A ==> f`x = g`x |] ==> f=g";
by (REPEAT (ares_tac (prems @ (prems RL [sym]) @
[subset_refl,equalityI,fun_subset]) 1));
qed "fun_extension";
-goal ZF.thy "!!f A B. f : Pi(A,B) ==> (lam x:A. f`x) = f";
+Goal "f : Pi(A,B) ==> (lam x:A. f`x) = f";
by (rtac fun_extension 1);
by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));
qed "eta";
Addsimps [eta];
-val fun_extension_iff = prove_goal ZF.thy
- "!!z. [| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g"
- (fn _=> [ (blast_tac (claset() addIs [fun_extension]) 1) ]);
+Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g";
+by (blast_tac (claset() addIs [fun_extension]) 1);
+qed "fun_extension_iff";
(*thanks to Mark Staples*)
-val fun_subset_eq = prove_goal ZF.thy
- "!!z. [| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
+val fun_subset_eq = prove_goal thy
+ "!!f. [| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
(fn _=>
[ (rtac iffI 1), (asm_full_simp_tac ZF_ss 2),
(rtac fun_extension 1), (REPEAT (atac 1)),
@@ -249,7 +247,7 @@
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
-val prems = goal ZF.thy
+val prems = Goal
"[| f: Pi(A,B); \
\ !!b. [| ALL x:A. b(x):B(x); f = (lam x:A. b(x)) |] ==> P \
\ |] ==> P";
@@ -261,14 +259,13 @@
(** Images of functions **)
-goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
+Goalw [lam_def] "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
by (Blast_tac 1);
qed "image_lam";
-goal ZF.thy "!!C A. [| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}";
+Goal "[| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}";
by (etac (eta RS subst) 1);
-by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff]
- addcongs [RepFun_cong]) 1);
+by (asm_full_simp_tac (simpset() addsimps [image_lam, subset_iff]) 1);
qed "image_fun";
Goal "[| f: Pi(A,B); x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)";
@@ -278,47 +275,46 @@
(*** properties of "restrict" ***)
-goalw ZF.thy [restrict_def,lam_def]
- "!!f A. [| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f";
+Goalw [restrict_def,lam_def]
+ "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) <= f";
by (blast_tac (claset() addIs [apply_Pair]) 1);
qed "restrict_subset";
-val prems = goalw ZF.thy [restrict_def]
+val prems = Goalw [restrict_def]
"[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";
by (rtac lam_type 1);
by (eresolve_tac prems 1);
qed "restrict_type";
-val [pi,subs] = goal ZF.thy
- "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)";
-by (rtac (pi RS apply_type RS restrict_type) 1);
-by (etac (subs RS subsetD) 1);
+Goal "[| f: Pi(C,B); A<=C |] ==> restrict(f,A) : Pi(A,B)";
+by (blast_tac (claset() addIs [apply_type, restrict_type]) 1);
qed "restrict_type2";
-goalw ZF.thy [restrict_def] "!!a A. a : A ==> restrict(f,A) ` a = f`a";
+Goalw [restrict_def] "a : A ==> restrict(f,A) ` a = f`a";
by (etac beta 1);
qed "restrict";
-goalw ZF.thy [restrict_def] "restrict(f,0) = 0";
+Goalw [restrict_def] "restrict(f,0) = 0";
by (Simp_tac 1);
qed "restrict_empty";
Addsimps [restrict, restrict_empty];
(*NOT SAFE as a congruence rule for the simplifier! Can cause it to fail!*)
-val prems = goalw ZF.thy [restrict_def]
+val prems = Goalw [restrict_def]
"[| A=B; !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
by (REPEAT (ares_tac (prems@[lam_cong]) 1));
qed "restrict_eqI";
-goalw ZF.thy [restrict_def, lam_def] "domain(restrict(f,C)) = C";
+Goalw [restrict_def, lam_def] "domain(restrict(f,C)) = C";
by (Blast_tac 1);
qed "domain_restrict";
-val [prem] = goalw ZF.thy [restrict_def]
+Goalw [restrict_def]
"A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
by (rtac (refl RS lam_cong) 1);
-by (etac (prem RS subsetD RS beta) 1); (*easier than calling simp_tac*)
+by (set_mp_tac 1);
+by (Asm_simp_tac 1);
qed "restrict_lam_eq";
@@ -327,16 +323,16 @@
(** The Union of a set of COMPATIBLE functions is a function **)
-goalw ZF.thy [function_def]
- "!!S. [| ALL x:S. function(x); \
+Goalw [function_def]
+ "[| ALL x:S. function(x); \
\ ALL x:S. ALL y:S. x<=y | y<=x |] ==> \
\ function(Union(S))";
by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1);
(*by (Blast_tac 1); takes too long...*)
qed "function_Union";
-goalw ZF.thy [Pi_def]
- "!!S. [| ALL f:S. EX C D. f:C->D; \
+Goalw [Pi_def]
+ "[| ALL f:S. EX C D. f:C->D; \
\ ALL f:S. ALL y:S. f<=y | y<=f |] ==> \
\ Union(S) : domain(Union(S)) -> range(Union(S))";
by (blast_tac (subset_cs addSIs [rel_Union, function_Union]) 1);
@@ -349,7 +345,7 @@
Un_upper1 RSN (2, subset_trans),
Un_upper2 RSN (2, subset_trans)];
-goal ZF.thy "!!f. [| f: A->B; g: C->D; A Int C = 0 |] \
+Goal "[| f: A->B; g: C->D; A Int C = 0 |] \
\ ==> (f Un g) : (A Un C) -> (B Un D)";
(*Prove the product and domain subgoals using distributive laws*)
by (asm_full_simp_tac (simpset() addsimps [Pi_iff,extension]@Un_rls) 1);
@@ -357,15 +353,13 @@
by (Blast_tac 1);
qed "fun_disjoint_Un";
-goal ZF.thy
- "!!f g a. [| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
+Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
\ (f Un g)`a = f`a";
by (rtac (apply_Pair RS UnI1 RS apply_equality) 1);
by (REPEAT (ares_tac [fun_disjoint_Un] 1));
qed "fun_disjoint_apply1";
-goal ZF.thy
- "!!f g c. [| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> \
+Goal "[| c:C; f: A->B; g: C->D; A Int C = 0 |] ==> \
\ (f Un g)`c = g`c";
by (rtac (apply_Pair RS UnI2 RS apply_equality) 1);
by (REPEAT (ares_tac [fun_disjoint_Un] 1));
@@ -373,18 +367,17 @@
(** Domain and range of a function/relation **)
-goalw ZF.thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A";
+Goalw [Pi_def] "f : Pi(A,B) ==> domain(f)=A";
by (Blast_tac 1);
qed "domain_of_fun";
-goal ZF.thy "!!f. [| f : Pi(A,B); a: A |] ==> f`a : range(f)";
+Goal "[| f : Pi(A,B); a: A |] ==> f`a : range(f)";
by (etac (apply_Pair RS rangeI) 1);
by (assume_tac 1);
qed "apply_rangeI";
-val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
-by (rtac (major RS Pi_type) 1);
-by (etac (major RS apply_rangeI) 1);
+Goal "f : Pi(A,B) ==> f : A->range(f)";
+by (REPEAT (ares_tac [Pi_type, apply_rangeI] 1));
qed "range_of_fun";
(*** Extensions of functions ***)
--- a/src/ZF/mono.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/mono.ML Mon Aug 17 13:09:08 1998 +0200
@@ -28,7 +28,7 @@
by (Blast_tac 1);
qed "Union_mono";
-val prems = goal thy
+val prems = Goal
"[| A<=C; !!x. x:A ==> B(x)<=D(x) \
\ |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))";
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
@@ -57,8 +57,7 @@
(** Standard products, sums and function spaces **)
-Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> \
-\ Sigma(A,B) <= Sigma(C,D)";
+Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)";
by (Blast_tac 1);
qed "Sigma_mono_lemma";
val Sigma_mono = ballI RSN (2,Sigma_mono_lemma);
@@ -131,12 +130,12 @@
(** Images **)
-val [prem1,prem2] = goal thy
+val [prem1,prem2] = Goal
"[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r``A <= s``B";
by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1);
qed "image_pair_mono";
-val [prem1,prem2] = goal thy
+val [prem1,prem2] = Goal
"[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r-``A <= s-``B";
by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1);
qed "vimage_pair_mono";
@@ -149,7 +148,7 @@
by (Blast_tac 1);
qed "vimage_mono";
-val [sub,PQimp] = goal thy
+val [sub,PQimp] = Goal
"[| A<=B; !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)";
by (blast_tac (claset() addIs [sub RS subsetD, PQimp RS mp]) 1);
qed "Collect_mono";
--- a/src/ZF/mono.thy Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/mono.thy Mon Aug 17 13:09:08 1998 +0200
@@ -1,4 +1,2 @@
-(*Dummy theory to document dependencies *)
+mono = QPair + Sum + func
-mono = QPair + Sum + domrange
-
--- a/src/ZF/pair.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/pair.ML Mon Aug 17 13:09:08 1998 +0200
@@ -8,17 +8,17 @@
(** Lemmas for showing that <a,b> uniquely determines a and b **)
-qed_goal "singleton_eq_iff" ZF.thy
+qed_goal "singleton_eq_iff" thy
"{a} = {b} <-> a=b"
(fn _=> [ (resolve_tac [extension RS iff_trans] 1),
(Blast_tac 1) ]);
-qed_goal "doubleton_eq_iff" ZF.thy
+qed_goal "doubleton_eq_iff" thy
"{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
(fn _=> [ (resolve_tac [extension RS iff_trans] 1),
(Blast_tac 1) ]);
-qed_goalw "Pair_iff" ZF.thy [Pair_def]
+qed_goalw "Pair_iff" thy [Pair_def]
"<a,b> = <c,d> <-> a=c & b=d"
(fn _=> [ (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1),
(Blast_tac 1) ]);
@@ -32,20 +32,20 @@
bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1);
bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2);
-qed_goalw "Pair_not_0" ZF.thy [Pair_def] "<a,b> ~= 0"
+qed_goalw "Pair_not_0" thy [Pair_def] "<a,b> ~= 0"
(fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
bind_thm ("Pair_neq_0", Pair_not_0 RS notE);
AddSEs [Pair_neq_0, sym RS Pair_neq_0];
-qed_goalw "Pair_neq_fst" ZF.thy [Pair_def] "<a,b>=a ==> P"
+qed_goalw "Pair_neq_fst" thy [Pair_def] "<a,b>=a ==> P"
(fn [major]=>
[ (rtac (consI1 RS mem_asym RS FalseE) 1),
(rtac (major RS subst) 1),
(rtac consI1 1) ]);
-qed_goalw "Pair_neq_snd" ZF.thy [Pair_def] "<a,b>=b ==> P"
+qed_goalw "Pair_neq_snd" thy [Pair_def] "<a,b>=b ==> P"
(fn [major]=>
[ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1),
(rtac (major RS subst) 1),
@@ -55,12 +55,12 @@
(*** Sigma: Disjoint union of a family of sets
Generalizes Cartesian product ***)
-qed_goalw "Sigma_iff" ZF.thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
+qed_goalw "Sigma_iff" thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
(fn _ => [ Blast_tac 1 ]);
Addsimps [Sigma_iff];
-qed_goal "SigmaI" ZF.thy
+qed_goal "SigmaI" thy
"!!a b. [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)"
(fn _ => [ Asm_simp_tac 1 ]);
@@ -68,7 +68,7 @@
bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);
(*The general elimination rule*)
-qed_goalw "SigmaE" ZF.thy [Sigma_def]
+qed_goalw "SigmaE" thy [Sigma_def]
"[| c: Sigma(A,B); \
\ !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P \
\ |] ==> P"
@@ -76,7 +76,7 @@
[ (cut_facts_tac [major] 1),
(REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
-qed_goal "SigmaE2" ZF.thy
+qed_goal "SigmaE2" thy
"[| <a,b> : Sigma(A,B); \
\ [| a:A; b:B(a) |] ==> P \
\ |] ==> P"
@@ -85,7 +85,7 @@
(rtac (major RS SigmaD1) 1),
(rtac (major RS SigmaD2) 1) ]);
-qed_goalw "Sigma_cong" ZF.thy [Sigma_def]
+qed_goalw "Sigma_cong" thy [Sigma_def]
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
\ Sigma(A,B) = Sigma(A',B')"
(fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
@@ -98,10 +98,10 @@
AddSIs [SigmaI];
AddSEs [SigmaE2, SigmaE];
-qed_goal "Sigma_empty1" ZF.thy "Sigma(0,B) = 0"
+qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0"
(fn _ => [ (Blast_tac 1) ]);
-qed_goal "Sigma_empty2" ZF.thy "A*0 = 0"
+qed_goal "Sigma_empty2" thy "A*0 = 0"
(fn _ => [ (Blast_tac 1) ]);
Addsimps [Sigma_empty1, Sigma_empty2];
@@ -113,21 +113,21 @@
(*** Projections: fst, snd ***)
-qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a"
+qed_goalw "fst_conv" thy [fst_def] "fst(<a,b>) = a"
(fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
-qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b"
+qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b"
(fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
Addsimps [fst_conv,snd_conv];
-qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
+qed_goal "fst_type" thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
(fn _=> [ Auto_tac ]);
-qed_goal "snd_type" ZF.thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
+qed_goal "snd_type" thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
(fn _=> [ Auto_tac ]);
-qed_goal "Pair_fst_snd_eq" ZF.thy
+qed_goal "Pair_fst_snd_eq" thy
"!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
(fn _=> [ Auto_tac ]);
@@ -135,13 +135,13 @@
(*** Eliminator - split ***)
(*A META-equality, so that it applies to higher types as well...*)
-qed_goalw "split" ZF.thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
+qed_goalw "split" thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
(fn _ => [ (Simp_tac 1),
(rtac reflexive_thm 1) ]);
Addsimps [split];
-qed_goal "split_type" ZF.thy
+qed_goal "split_type" thy
"[| p:Sigma(A,B); \
\ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \
\ |] ==> split(%x y. c(x,y), p) : C(p)"
@@ -149,8 +149,8 @@
[ (rtac (major RS SigmaE) 1),
(asm_simp_tac (simpset() addsimps prems) 1) ]);
-goalw ZF.thy [split_def]
- "!!u. u: A*B ==> \
+Goalw [split_def]
+ "u: A*B ==> \
\ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
by Auto_tac;
qed "expand_split";
@@ -158,11 +158,11 @@
(*** split for predicates: result type o ***)
-goalw ZF.thy [split_def] "!!R a b. R(a,b) ==> split(R, <a,b>)";
+Goalw [split_def] "R(a,b) ==> split(R, <a,b>)";
by (Asm_simp_tac 1);
qed "splitI";
-val major::sigma::prems = goalw ZF.thy [split_def]
+val major::sigma::prems = Goalw [split_def]
"[| split(R,z); z:Sigma(A,B); \
\ !!x y. [| z = <x,y>; R(x,y) |] ==> P \
\ |] ==> P";
@@ -172,7 +172,7 @@
by (Asm_full_simp_tac 1);
qed "splitE";
-goalw ZF.thy [split_def] "!!R a b. split(R,<a,b>) ==> R(a,b)";
+Goalw [split_def] "split(R,<a,b>) ==> R(a,b)";
by (Full_simp_tac 1);
qed "splitD";
--- a/src/ZF/simpdata.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/simpdata.ML Mon Aug 17 13:09:08 1998 +0200
@@ -10,7 +10,7 @@
local
(*For proving rewrite rules*)
- fun prover s = (prove_goal ZF.thy s (fn _ => [Blast_tac 1]));
+ fun prover s = (prove_goal thy s (fn _ => [Blast_tac 1]));
in
--- a/src/ZF/subset.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/subset.ML Mon Aug 17 13:09:08 1998 +0200
@@ -9,38 +9,38 @@
(*** cons ***)
-qed_goal "cons_subsetI" ZF.thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C"
+qed_goal "cons_subsetI" thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "subset_consI" ZF.thy "B <= cons(a,B)"
+qed_goal "subset_consI" thy "B <= cons(a,B)"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "cons_subset_iff" ZF.thy "cons(a,B)<=C <-> a:C & B<=C"
+qed_goal "cons_subset_iff" thy "cons(a,B)<=C <-> a:C & B<=C"
(fn _ => [ Blast_tac 1 ]);
(*A safe special case of subset elimination, adding no new variables
[| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
bind_thm ("cons_subsetE", cons_subset_iff RS iffD1 RS conjE);
-qed_goal "subset_empty_iff" ZF.thy "A<=0 <-> A=0"
+qed_goal "subset_empty_iff" thy "A<=0 <-> A=0"
(fn _=> [ (Blast_tac 1) ]);
-qed_goal "subset_cons_iff" ZF.thy
+qed_goal "subset_cons_iff" thy
"C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
(fn _=> [ (Blast_tac 1) ]);
(*** succ ***)
-qed_goal "subset_succI" ZF.thy "i <= succ(i)"
+qed_goal "subset_succI" thy "i <= succ(i)"
(fn _=> [ (Blast_tac 1) ]);
(*But if j is an ordinal or is transitive, then i:j implies i<=j!
See ordinal/Ord_succ_subsetI*)
-qed_goalw "succ_subsetI" ZF.thy [succ_def]
+qed_goalw "succ_subsetI" thy [succ_def]
"!!i j. [| i:j; i<=j |] ==> succ(i)<=j"
(fn _=> [ (Blast_tac 1) ]);
-qed_goalw "succ_subsetE" ZF.thy [succ_def]
+qed_goalw "succ_subsetE" thy [succ_def]
"[| succ(i) <= j; [| i:j; i<=j |] ==> P \
\ |] ==> P"
(fn major::prems=>
@@ -49,22 +49,22 @@
(*** singletons ***)
-qed_goal "singleton_subsetI" ZF.thy "!!a c. a:C ==> {a} <= C"
+qed_goal "singleton_subsetI" thy "!!a c. a:C ==> {a} <= C"
(fn _=> [ (Blast_tac 1) ]);
-qed_goal "singleton_subsetD" ZF.thy "!!a C. {a} <= C ==> a:C"
+qed_goal "singleton_subsetD" thy "!!a C. {a} <= C ==> a:C"
(fn _=> [ (Blast_tac 1) ]);
(*** Big Union -- least upper bound of a set ***)
-qed_goal "Union_subset_iff" ZF.thy "Union(A) <= C <-> (ALL x:A. x <= C)"
+qed_goal "Union_subset_iff" thy "Union(A) <= C <-> (ALL x:A. x <= C)"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "Union_upper" ZF.thy
+qed_goal "Union_upper" thy
"!!B A. B:A ==> B <= Union(A)"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "Union_least" ZF.thy
+qed_goal "Union_least" thy
"[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"
(fn [prem]=>
[ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1),
@@ -72,19 +72,19 @@
(*** Union of a family of sets ***)
-goal ZF.thy "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
+Goal "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
by (blast_tac (claset() addSEs [equalityE]) 1);
qed "subset_UN_iff_eq";
-qed_goal "UN_subset_iff" ZF.thy
+qed_goal "UN_subset_iff" thy
"(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "UN_upper" ZF.thy
+qed_goal "UN_upper" thy
"!!x A. x:A ==> B(x) <= (UN x:A. B(x))"
(fn _ => [ etac (RepFunI RS Union_upper) 1 ]);
-qed_goal "UN_least" ZF.thy
+qed_goal "UN_least" thy
"[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"
(fn [prem]=>
[ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1),
@@ -93,14 +93,14 @@
(*** Big Intersection -- greatest lower bound of a nonempty set ***)
-qed_goal "Inter_subset_iff" ZF.thy
+qed_goal "Inter_subset_iff" thy
"!!a A. a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "Inter_lower" ZF.thy "!!B A. B:A ==> Inter(A) <= B"
+qed_goal "Inter_lower" thy "!!B A. B:A ==> Inter(A) <= B"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "Inter_greatest" ZF.thy
+qed_goal "Inter_greatest" thy
"[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)"
(fn [prem1,prem2]=>
[ (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1),
@@ -108,11 +108,11 @@
(*** Intersection of a family of sets ***)
-qed_goal "INT_lower" ZF.thy
+qed_goal "INT_lower" thy
"!!x. x:A ==> (INT x:A. B(x)) <= B(x)"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "INT_greatest" ZF.thy
+qed_goal "INT_greatest" thy
"[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"
(fn [nonempty,prem] =>
[ rtac (nonempty RS RepFunI RS Inter_greatest) 1,
@@ -121,53 +121,58 @@
(*** Finite Union -- the least upper bound of 2 sets ***)
-qed_goal "Un_subset_iff" ZF.thy "A Un B <= C <-> A <= C & B <= C"
+qed_goal "Un_subset_iff" thy "A Un B <= C <-> A <= C & B <= C"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "Un_upper1" ZF.thy "A <= A Un B"
+qed_goal "Un_upper1" thy "A <= A Un B"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "Un_upper2" ZF.thy "B <= A Un B"
+qed_goal "Un_upper2" thy "B <= A Un B"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "Un_least" ZF.thy "!!A B C. [| A<=C; B<=C |] ==> A Un B <= C"
+qed_goal "Un_least" thy "!!A B C. [| A<=C; B<=C |] ==> A Un B <= C"
(fn _ => [ Blast_tac 1 ]);
(*** Finite Intersection -- the greatest lower bound of 2 sets *)
-qed_goal "Int_subset_iff" ZF.thy "C <= A Int B <-> C <= A & C <= B"
+qed_goal "Int_subset_iff" thy "C <= A Int B <-> C <= A & C <= B"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "Int_lower1" ZF.thy "A Int B <= A"
+qed_goal "Int_lower1" thy "A Int B <= A"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "Int_lower2" ZF.thy "A Int B <= B"
+qed_goal "Int_lower2" thy "A Int B <= B"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "Int_greatest" ZF.thy "!!A B C. [| C<=A; C<=B |] ==> C <= A Int B"
+qed_goal "Int_greatest" thy "!!A B C. [| C<=A; C<=B |] ==> C <= A Int B"
(fn _ => [ Blast_tac 1 ]);
(*** Set difference *)
-qed_goal "Diff_subset" ZF.thy "A-B <= A"
+qed_goal "Diff_subset" thy "A-B <= A"
(fn _ => [ Blast_tac 1 ]);
-qed_goal "Diff_contains" ZF.thy
+qed_goal "Diff_contains" thy
"!!C. [| C<=A; C Int B = 0 |] ==> C <= A-B"
- (fn _ => [ (blast_tac (claset() addSEs [equalityE]) 1) ]);
+ (fn _ => [ Blast_tac 1 ]);
+
+Goal "B <= A - cons(c,C) <-> B<=A-C & c ~: B";
+by (Blast_tac 1);
+qed "subset_Diff_cons_iff";
+
(** Collect **)
-qed_goal "Collect_subset" ZF.thy "Collect(A,P) <= A"
+qed_goal "Collect_subset" thy "Collect(A,P) <= A"
(fn _ => [ Blast_tac 1 ]);
(** RepFun **)
-val prems = goal ZF.thy "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
+val prems = Goal "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
by (blast_tac (claset() addIs prems) 1);
qed "RepFun_subset";
--- a/src/ZF/upair.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/upair.ML Mon Aug 17 13:09:08 1998 +0200
@@ -21,19 +21,19 @@
(*** Unordered pairs - Upair ***)
-qed_goalw "Upair_iff" ZF.thy [Upair_def]
+qed_goalw "Upair_iff" thy [Upair_def]
"c : Upair(a,b) <-> (c=a | c=b)"
(fn _ => [ (blast_tac (claset() addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);
Addsimps [Upair_iff];
-qed_goal "UpairI1" ZF.thy "a : Upair(a,b)"
+qed_goal "UpairI1" thy "a : Upair(a,b)"
(fn _ => [ Simp_tac 1 ]);
-qed_goal "UpairI2" ZF.thy "b : Upair(a,b)"
+qed_goal "UpairI2" thy "b : Upair(a,b)"
(fn _ => [ Simp_tac 1 ]);
-qed_goal "UpairE" ZF.thy
+qed_goal "UpairE" thy
"[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1),
@@ -44,25 +44,25 @@
(*** Rules for binary union -- Un -- defined via Upair ***)
-qed_goalw "Un_iff" ZF.thy [Un_def] "c : A Un B <-> (c:A | c:B)"
+qed_goalw "Un_iff" thy [Un_def] "c : A Un B <-> (c:A | c:B)"
(fn _ => [ Blast_tac 1 ]);
Addsimps [Un_iff];
-qed_goal "UnI1" ZF.thy "!!c. c : A ==> c : A Un B"
+qed_goal "UnI1" thy "!!c. c : A ==> c : A Un B"
(fn _ => [ Asm_simp_tac 1 ]);
-qed_goal "UnI2" ZF.thy "!!c. c : B ==> c : A Un B"
+qed_goal "UnI2" thy "!!c. c : B ==> c : A Un B"
(fn _ => [ Asm_simp_tac 1 ]);
-qed_goal "UnE" ZF.thy
+qed_goal "UnE" thy
"[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1),
(REPEAT (eresolve_tac prems 1)) ]);
(*Stronger version of the rule above*)
-qed_goal "UnE'" ZF.thy
+qed_goal "UnE'" thy
"[| c : A Un B; c:A ==> P; [| c:B; c~:A |] ==> P |] ==> P"
(fn major::prems =>
[(rtac (major RS UnE) 1),
@@ -73,7 +73,7 @@
(etac notnotD 1)]);
(*Classical introduction rule: no commitment to A vs B*)
-qed_goal "UnCI" ZF.thy "(c ~: B ==> c : A) ==> c : A Un B"
+qed_goal "UnCI" thy "(c ~: B ==> c : A) ==> c : A Un B"
(fn prems=>
[ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
@@ -83,21 +83,21 @@
(*** Rules for small intersection -- Int -- defined via Upair ***)
-qed_goalw "Int_iff" ZF.thy [Int_def] "c : A Int B <-> (c:A & c:B)"
+qed_goalw "Int_iff" thy [Int_def] "c : A Int B <-> (c:A & c:B)"
(fn _ => [ Blast_tac 1 ]);
Addsimps [Int_iff];
-qed_goal "IntI" ZF.thy "!!c. [| c : A; c : B |] ==> c : A Int B"
+qed_goal "IntI" thy "!!c. [| c : A; c : B |] ==> c : A Int B"
(fn _ => [ Asm_simp_tac 1 ]);
-qed_goal "IntD1" ZF.thy "!!c. c : A Int B ==> c : A"
+qed_goal "IntD1" thy "!!c. c : A Int B ==> c : A"
(fn _ => [ Asm_full_simp_tac 1 ]);
-qed_goal "IntD2" ZF.thy "!!c. c : A Int B ==> c : B"
+qed_goal "IntD2" thy "!!c. c : A Int B ==> c : B"
(fn _ => [ Asm_full_simp_tac 1 ]);
-qed_goal "IntE" ZF.thy
+qed_goal "IntE" thy
"[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"
(fn prems=>
[ (resolve_tac prems 1),
@@ -108,21 +108,21 @@
(*** Rules for set difference -- defined via Upair ***)
-qed_goalw "Diff_iff" ZF.thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
+qed_goalw "Diff_iff" thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
(fn _ => [ Blast_tac 1 ]);
Addsimps [Diff_iff];
-qed_goal "DiffI" ZF.thy "!!c. [| c : A; c ~: B |] ==> c : A - B"
+qed_goal "DiffI" thy "!!c. [| c : A; c ~: B |] ==> c : A - B"
(fn _ => [ Asm_simp_tac 1 ]);
-qed_goal "DiffD1" ZF.thy "!!c. c : A - B ==> c : A"
+qed_goal "DiffD1" thy "!!c. c : A - B ==> c : A"
(fn _ => [ Asm_full_simp_tac 1 ]);
-qed_goal "DiffD2" ZF.thy "!!c. c : A - B ==> c ~: B"
+qed_goal "DiffD2" thy "!!c. c : A - B ==> c ~: B"
(fn _ => [ Asm_full_simp_tac 1 ]);
-qed_goal "DiffE" ZF.thy
+qed_goal "DiffE" thy
"[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P"
(fn prems=>
[ (resolve_tac prems 1),
@@ -133,27 +133,27 @@
(*** Rules for cons -- defined via Un and Upair ***)
-qed_goalw "cons_iff" ZF.thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
+qed_goalw "cons_iff" thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
(fn _ => [ Blast_tac 1 ]);
Addsimps [cons_iff];
-qed_goal "consI1" ZF.thy "a : cons(a,B)"
+qed_goal "consI1" thy "a : cons(a,B)"
(fn _ => [ Simp_tac 1 ]);
Addsimps [consI1];
-qed_goal "consI2" ZF.thy "!!B. a : B ==> a : cons(b,B)"
+qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)"
(fn _ => [ Asm_simp_tac 1 ]);
-qed_goal "consE" ZF.thy
+qed_goal "consE" thy
"[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1),
(REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);
(*Stronger version of the rule above*)
-qed_goal "consE'" ZF.thy
+qed_goal "consE'" thy
"[| a : cons(b,A); a=b ==> P; [| a:A; a~=b |] ==> P |] ==> P"
(fn major::prems =>
[(rtac (major RS consE) 1),
@@ -164,14 +164,14 @@
(etac notnotD 1)]);
(*Classical introduction rule*)
-qed_goal "consCI" ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)"
+qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)"
(fn prems=>
[ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
AddSIs [consCI];
AddSEs [consE];
-qed_goal "cons_not_0" ZF.thy "cons(a,B) ~= 0"
+qed_goal "cons_not_0" thy "cons(a,B) ~= 0"
(fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
bind_thm ("cons_neq_0", cons_not_0 RS notE);
@@ -181,10 +181,10 @@
(*** Singletons - using cons ***)
-qed_goal "singleton_iff" ZF.thy "a : {b} <-> a=b"
+qed_goal "singleton_iff" thy "a : {b} <-> a=b"
(fn _ => [ Simp_tac 1 ]);
-qed_goal "singletonI" ZF.thy "a : {a}"
+qed_goal "singletonI" thy "a : {a}"
(fn _=> [ (rtac consI1 1) ]);
bind_thm ("singletonE", make_elim (singleton_iff RS iffD1));
@@ -194,25 +194,25 @@
(*** Rules for Descriptions ***)
-qed_goalw "the_equality" ZF.thy [the_def]
+qed_goalw "the_equality" thy [the_def]
"[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
(fn [pa,eq] =>
[ (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ]);
(* Only use this if you already know EX!x. P(x) *)
-qed_goal "the_equality2" ZF.thy
+qed_goal "the_equality2" thy
"!!P. [| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a"
(fn _ =>
[ (deepen_tac (claset() addSIs [the_equality]) 1 1) ]);
-qed_goal "theI" ZF.thy "EX! x. P(x) ==> P(THE x. P(x))"
+qed_goal "theI" thy "EX! x. P(x) ==> P(THE x. P(x))"
(fn [major]=>
[ (rtac (major RS ex1E) 1),
(resolve_tac [major RS the_equality2 RS ssubst] 1),
(REPEAT (assume_tac 1)) ]);
(*Easier to apply than theI: conclusion has only one occurrence of P*)
-qed_goal "theI2" ZF.thy
+qed_goal "theI2" thy
"[| EX! x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))"
(fn prems => [ resolve_tac prems 1,
rtac theI 1,
@@ -222,42 +222,42 @@
(THE x.P(x)) rewrites to (THE x. Q(x)) *)
(*If it's "undefined", it's zero!*)
-qed_goalw "the_0" ZF.thy [the_def]
+qed_goalw "the_0" thy [the_def]
"!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
(fn _ => [ (deepen_tac (claset() addSEs [ReplaceE]) 0 1) ]);
(*** if -- a conditional expression for formulae ***)
-goalw ZF.thy [if_def] "if(True,a,b) = a";
+Goalw [if_def] "if(True,a,b) = a";
by (blast_tac (claset() addSIs [the_equality]) 1);
qed "if_true";
-goalw ZF.thy [if_def] "if(False,a,b) = b";
+Goalw [if_def] "if(False,a,b) = b";
by (blast_tac (claset() addSIs [the_equality]) 1);
qed "if_false";
(*Never use with case splitting, or if P is known to be true or false*)
-val prems = goalw ZF.thy [if_def]
+val prems = Goalw [if_def]
"[| P<->Q; Q ==> a=c; ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1);
qed "if_cong";
(*Not needed for rewriting, since P would rewrite to True anyway*)
-goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
+Goalw [if_def] "P ==> if(P,a,b) = a";
by (blast_tac (claset() addSIs [the_equality]) 1);
qed "if_P";
(*Not needed for rewriting, since P would rewrite to False anyway*)
-goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
+Goalw [if_def] "~P ==> if(P,a,b) = b";
by (blast_tac (claset() addSIs [the_equality]) 1);
qed "if_not_P";
Addsimps [if_true, if_false];
-qed_goal "split_if" ZF.thy
+qed_goal "split_if" thy
"P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
- (fn _=> [ (excluded_middle_tac "Q" 1),
+ (fn _=> [ (case_tac "Q" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1) ]);
@@ -275,10 +275,10 @@
split_if_mem1, split_if_mem2];
(*Logically equivalent to split_if_mem2*)
-qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
+qed_goal "if_iff" thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
(fn _=> [ (simp_tac (simpset() addsplits [split_if]) 1) ]);
-qed_goal "if_type" ZF.thy
+qed_goal "if_type" thy
"[| P ==> a: A; ~P ==> b: A |] ==> if(P,a,b): A"
(fn prems=> [ (simp_tac
(simpset() addsimps prems addsplits [split_if]) 1) ]);
@@ -287,48 +287,48 @@
(*** Foundation lemmas ***)
(*was called mem_anti_sym*)
-qed_goal "mem_asym" ZF.thy "[| a:b; ~P ==> b:a |] ==> P"
+qed_goal "mem_asym" thy "[| a:b; ~P ==> b:a |] ==> P"
(fn prems=>
[ (rtac classical 1),
(res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1) ]);
(*was called mem_anti_refl*)
-qed_goal "mem_irrefl" ZF.thy "a:a ==> P"
+qed_goal "mem_irrefl" thy "a:a ==> P"
(fn [major]=> [ (rtac ([major,major] MRS mem_asym) 1) ]);
(*mem_irrefl should NOT be added to default databases:
it would be tried on most goals, making proofs slower!*)
-qed_goal "mem_not_refl" ZF.thy "a ~: a"
+qed_goal "mem_not_refl" thy "a ~: a"
(K [ (rtac notI 1), (etac mem_irrefl 1) ]);
(*Good for proving inequalities by rewriting*)
-qed_goal "mem_imp_not_eq" ZF.thy "!!a A. a:A ==> a ~= A"
+qed_goal "mem_imp_not_eq" thy "!!a A. a:A ==> a ~= A"
(fn _=> [ blast_tac (claset() addSEs [mem_irrefl]) 1 ]);
(*** Rules for succ ***)
-qed_goalw "succ_iff" ZF.thy [succ_def] "i : succ(j) <-> i=j | i:j"
+qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j"
(fn _ => [ Blast_tac 1 ]);
-qed_goalw "succI1" ZF.thy [succ_def] "i : succ(i)"
+qed_goalw "succI1" thy [succ_def] "i : succ(i)"
(fn _=> [ (rtac consI1 1) ]);
Addsimps [succI1];
-qed_goalw "succI2" ZF.thy [succ_def]
+qed_goalw "succI2" thy [succ_def]
"i : j ==> i : succ(j)"
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
-qed_goalw "succE" ZF.thy [succ_def]
+qed_goalw "succE" thy [succ_def]
"[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS consE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
(*Classical introduction rule*)
-qed_goal "succCI" ZF.thy "(i~:j ==> i=j) ==> i: succ(j)"
+qed_goal "succCI" thy "(i~:j ==> i=j) ==> i: succ(j)"
(fn [prem]=>
[ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
(etac prem 1) ]);
@@ -336,7 +336,7 @@
AddSIs [succCI];
AddSEs [succE];
-qed_goal "succ_not_0" ZF.thy "succ(n) ~= 0"
+qed_goal "succ_not_0" thy "succ(n) ~= 0"
(fn _=> [ (blast_tac (claset() addSEs [equalityE]) 1) ]);
bind_thm ("succ_neq_0", succ_not_0 RS notE);
@@ -352,7 +352,7 @@
bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
-qed_goal "succ_inject_iff" ZF.thy "succ(m) = succ(n) <-> m=n"
+qed_goal "succ_inject_iff" thy "succ(m) = succ(n) <-> m=n"
(fn _=> [ (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ]);
bind_thm ("succ_inject", succ_inject_iff RS iffD1);