--- a/src/ZF/Cardinal.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/Cardinal.ML Fri Jun 30 12:51:30 2000 +0200
@@ -219,12 +219,13 @@
qed "less_LeastE";
(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
-qed_goal "LeastI2" Cardinal.thy
- "[| P(i); Ord(i); !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))"
- (fn prems => [ resolve_tac prems 1,
- rtac LeastI 1,
- resolve_tac prems 1,
- resolve_tac prems 1 ]);
+val prems = goal Cardinal.thy
+ "[| P(i); Ord(i); !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))";
+by (resolve_tac prems 1);
+by (rtac LeastI 1);
+by (resolve_tac prems 1);
+by (resolve_tac prems 1) ;
+qed "LeastI2";
(*If there is no such P then LEAST is vacuously 0*)
Goalw [Least_def]
--- a/src/ZF/Epsilon.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/Epsilon.ML Fri Jun 30 12:51:30 2000 +0200
@@ -42,7 +42,7 @@
bind_thm ("eclose_induct", Transset_eclose RSN (2, Transset_induct));
(*Epsilon induction*)
-val prems = goal Epsilon.thy
+val prems = Goal
"[| !!x. ALL y:x. P(y) ==> P(x) |] ==> P(a)";
by (rtac (arg_in_eclose_sing RS eclose_induct) 1);
by (eresolve_tac prems 1);
@@ -74,7 +74,7 @@
qed "eclose_least";
(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
-val [major,base,step] = goal Epsilon.thy
+val [major,base,step] = Goal
"[| a: eclose(b); \
\ !!y. [| y: b |] ==> P(y); \
\ !!y z. [| y: eclose(b); P(y); z: y |] ==> P(z) \
@@ -126,10 +126,10 @@
jmemi RSN (2,mem_eclose_sing_trans)]) 1);
qed "wfrec_eclose_eq";
-val [prem] = goal Epsilon.thy
+Goal
"k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)";
by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1);
-by (rtac (prem RS arg_into_eclose_sing) 1);
+by (etac arg_into_eclose_sing 1);
qed "wfrec_eclose_eq2";
Goalw [transrec_def]
@@ -140,13 +140,13 @@
qed "transrec";
(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
-val rew::prems = goal Epsilon.thy
+val rew::prems = Goal
"[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))";
by (rewtac rew);
by (REPEAT (resolve_tac (prems@[transrec]) 1));
qed "def_transrec";
-val prems = goal Epsilon.thy
+val prems = Goal
"[| !!x u. [| x:eclose({a}); u: Pi(x,B) |] ==> H(x,u) : B(x) \
\ |] ==> transrec(a,H) : B(a)";
by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
@@ -159,7 +159,7 @@
by (rtac (succI1 RS singleton_subsetI) 1);
qed "eclose_sing_Ord";
-val prems = goal Epsilon.thy
+val prems = Goal
"[| j: i; Ord(i); \
\ !!x u. [| x: i; u: Pi(x,B) |] ==> H(x,u) : B(x) \
\ |] ==> transrec(j,H) : B(j)";
@@ -186,8 +186,8 @@
qed "Ord_rank";
Addsimps [Ord_rank];
-val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
-by (rtac (major RS trans_induct) 1);
+Goal "Ord(i) ==> rank(i) = i";
+by (etac trans_induct 1);
by (stac rank 1);
by (asm_simp_tac (simpset() addsimps [Ord_equality]) 1);
qed "rank_of_Ord";
@@ -199,8 +199,8 @@
by Auto_tac;
qed "rank_lt";
-val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)";
-by (rtac (major RS eclose_induct_down) 1);
+Goal "a: eclose(b) ==> rank(a) < rank(b)";
+by (etac eclose_induct_down 1);
by (etac rank_lt 1);
by (etac (rank_lt RS lt_trans) 1);
by (assume_tac 1);
--- a/src/ZF/Finite.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/Finite.ML Fri Jun 30 12:51:30 2000 +0200
@@ -48,8 +48,8 @@
(*The union of a set of finite sets is finite.*)
-val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
-by (rtac (major RS Fin_induct) 1);
+Goal "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
+by (etac Fin_induct 1);
by (ALLGOALS Asm_simp_tac);
qed "Fin_UnionI";
--- a/src/ZF/InfDatatype.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/InfDatatype.ML Fri Jun 30 12:51:30 2000 +0200
@@ -71,9 +71,9 @@
qed "Card_fun_in_Vcsucc";
(*Proved explicitly, in theory InfDatatype, to allow the bind_thm calls below*)
-qed_goal "Limit_csucc" InfDatatype.thy
- "!!K. InfCard(K) ==> Limit(csucc(K))"
- (fn _ => [etac (InfCard_csucc RS InfCard_is_Limit) 1]);
+Goal "InfCard(K) ==> Limit(csucc(K))";
+by (etac (InfCard_csucc RS InfCard_is_Limit) 1);
+qed "Limit_csucc";
bind_thm ("Pair_in_Vcsucc", Limit_csucc RSN (3, Pair_in_VLimit));
bind_thm ("Inl_in_Vcsucc", Limit_csucc RSN (2, Inl_in_VLimit));
--- a/src/ZF/OrdQuant.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/OrdQuant.ML Fri Jun 30 12:51:30 2000 +0200
@@ -7,23 +7,23 @@
(*** universal quantifier for ordinals ***)
-qed_goalw "oallI" thy [oall_def]
- "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"
- (fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]);
+val prems = Goalw [oall_def]
+ "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)";
+by (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ;
+qed "oallI";
-qed_goalw "ospec" thy [oall_def]
- "[| ALL x<A. P(x); x<A |] ==> P(x)"
- (fn major::prems=>
- [ (rtac (major RS spec RS mp) 1),
- (resolve_tac prems 1) ]);
+Goalw [oall_def] "[| ALL x<A. P(x); x<A |] ==> P(x)";
+by (etac (spec RS mp) 1);
+by (assume_tac 1) ;
+qed "ospec";
-qed_goalw "oallE" thy [oall_def]
- "[| ALL x<A. P(x); P(x) ==> Q; ~x<A ==> Q |] ==> Q"
- (fn major::prems=>
- [ (rtac (major RS allE) 1),
- (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
+val major::prems = Goalw [oall_def]
+ "[| ALL x<A. P(x); P(x) ==> Q; ~x<A ==> Q |] ==> Q";
+by (rtac (major RS allE) 1);
+by (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ;
+qed "oallE";
-val major::prems= goal thy
+val major::prems = Goal
"[| ALL x<A. P(x); ~x<A ==> Q; P(x) ==> Q |] ==> Q";
by (rtac (major RS oallE) 1);
by (REPEAT (eresolve_tac prems 1)) ;
@@ -35,16 +35,18 @@
qed "oall_simp";
(*Congruence rule for rewriting*)
-qed_goalw "oall_cong" thy [oall_def]
- "[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')"
- (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
+val prems = Goalw [oall_def]
+ "[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')";
+by (simp_tac (simpset() addsimps prems) 1) ;
+qed "oall_cong";
(*** existential quantifier for ordinals ***)
-qed_goalw "oexI" thy [oex_def]
- "[| P(x); x<A |] ==> EX x<A. P(x)"
- (fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]);
+val prems = Goalw [oex_def]
+ "[| P(x); x<A |] ==> EX x<A. P(x)";
+by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ;
+qed "oexI";
(*Not of the general form for such rules; ~EX has become ALL~ *)
val prems = Goal
@@ -53,35 +55,36 @@
by (REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ;
qed "oexCI";
-qed_goalw "oexE" thy [oex_def]
+val major::prems = Goalw [oex_def]
"[| EX x<A. P(x); !!x. [| x<A; P(x) |] ==> Q \
-\ |] ==> Q"
- (fn major::prems=>
- [ (rtac (major RS exE) 1),
- (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);
+\ |] ==> Q";
+by (rtac (major RS exE) 1);
+by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ;
+qed "oexE";
-qed_goalw "oex_cong" thy [oex_def]
+val prems = Goalw [oex_def]
"[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) \
-\ |] ==> oex(a,P) <-> oex(a',P')"
- (fn prems=> [ (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1) ]);
+\ |] ==> oex(a,P) <-> oex(a',P')";
+by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1) ;
+qed "oex_cong";
(*** Rules for Ordinal-Indexed Unions ***)
-qed_goalw "OUN_I" thy [OUnion_def]
- "!!i. [| a<i; b: B(a) |] ==> b: (UN z<i. B(z))"
- (fn _=> [ fast_tac (claset() addSEs [ltE]) 1 ]);
+Goalw [OUnion_def] "[| a<i; b: B(a) |] ==> b: (UN z<i. B(z))";
+by (blast_tac (claset() addSEs [ltE]) 1);
+qed "OUN_I";
-qed_goalw "OUN_E" thy [OUnion_def]
- "[| b : (UN z<i. B(z)); !!a.[| b: B(a); a<i |] ==> R |] ==> R"
- (fn major::prems=>
- [ (rtac (major RS CollectE) 1),
- (rtac UN_E 1),
- (REPEAT (ares_tac (ltI::prems) 1)) ]);
+val major::prems = Goalw [OUnion_def]
+ "[| b : (UN z<i. B(z)); !!a.[| b: B(a); a<i |] ==> R |] ==> R";
+by (rtac (major RS CollectE) 1);
+by (rtac UN_E 1);
+by (REPEAT (ares_tac (ltI::prems) 1)) ;
+qed "OUN_E";
-qed_goalw "OUN_iff" thy [oex_def]
- "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
- (fn _=> [ (fast_tac (claset() addIs [OUN_I] addSEs [OUN_E]) 1) ]);
+Goalw [oex_def] "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))";
+by (fast_tac (claset() addIs [OUN_I] addSEs [OUN_E]) 1) ;
+qed "OUN_iff";
val prems = Goal
"[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))";
--- a/src/ZF/Perm.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/Perm.ML Fri Jun 30 12:51:30 2000 +0200
@@ -25,7 +25,7 @@
(** A function with a right inverse is a surjection **)
-val prems = goalw Perm.thy [surj_def]
+val prems = Goalw [surj_def]
"[| f: A->B; !!y. y:B ==> d(y): A; !!y. y:B ==> f`d(y) = y \
\ |] ==> f: surj(A,B)";
by (blast_tac (claset() addIs prems) 1);
@@ -92,7 +92,7 @@
(* f: bij(A,B) ==> f: A->B *)
bind_thm ("bij_is_fun", bij_is_inj RS inj_is_fun);
-val prems = goalw Perm.thy [bij_def]
+val prems = Goalw [bij_def]
"[| !!x. x:A ==> c(x): B; \
\ !!y. y:B ==> d(y): A; \
\ !!x. x:A ==> d(c(x)) = x; \
@@ -111,11 +111,11 @@
(** Identity function **)
-val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";
-by (rtac (prem RS lamI) 1);
+Goalw [id_def] "a:A ==> <a,a> : id(A)";
+by (etac lamI 1);
qed "idI";
-val major::prems = goalw Perm.thy [id_def]
+val major::prems = Goalw [id_def]
"[| p: id(A); !!x.[| x:A; p=<x,x> |] ==> P \
\ |] ==> P";
by (rtac (major RS lamE) 1);
@@ -133,8 +133,8 @@
Addsimps [id_conv];
-val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)";
-by (rtac (prem RS lam_mono) 1);
+Goalw [id_def] "A<=B ==> id(A) <= id(B)";
+by (etac lam_mono 1);
qed "id_mono";
Goalw [inj_def,id_def] "A<=B ==> id(A): inj(A,B)";
@@ -233,7 +233,7 @@
by (Blast_tac 1);
qed "compI";
-val prems = goalw Perm.thy [comp_def]
+val prems = Goalw [comp_def]
"[| xz : r O s; \
\ !!x y z. [| xz=<x,z>; <x,y>:s; <y,z>:r |] ==> P \
\ |] ==> P";
--- a/src/ZF/QPair.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/QPair.ML Fri Jun 30 12:51:30 2000 +0200
@@ -16,53 +16,49 @@
is not a limit ordinal?
*)
-open QPair;
-
(**** Quine ordered pairing ****)
(** Lemmas for showing that <a;b> uniquely determines a and b **)
-qed_goalw "QPair_empty" thy [QPair_def]
- "<0;0> = 0"
- (fn _=> [Simp_tac 1]);
+Goalw [QPair_def] "<0;0> = 0";
+by (Simp_tac 1);
+qed "QPair_empty";
-qed_goalw "QPair_iff" thy [QPair_def]
- "<a;b> = <c;d> <-> a=c & b=d"
- (fn _=> [rtac sum_equal_iff 1]);
+Goalw [QPair_def] "<a;b> = <c;d> <-> a=c & b=d";
+by (rtac sum_equal_iff 1);
+qed "QPair_iff";
-bind_thm ("QPair_inject", (QPair_iff RS iffD1 RS conjE));
+bind_thm ("QPair_inject", QPair_iff RS iffD1 RS conjE);
Addsimps [QPair_empty, QPair_iff];
AddSEs [QPair_inject];
-val [major]= goal thy "<a;b> = <c;d> ==> a=c";
-by (rtac (major RS QPair_inject) 1);
-by (assume_tac 1) ;
+Goal "<a;b> = <c;d> ==> a=c";
+by (Blast_tac 1) ;
qed "QPair_inject1";
-val [major]= goal thy "<a;b> = <c;d> ==> b=d";
-by (rtac (major RS QPair_inject) 1);
-by (assume_tac 1) ;
+Goal "<a;b> = <c;d> ==> b=d";
+by (Blast_tac 1) ;
qed "QPair_inject2";
(*** QSigma: Disjoint union of a family of sets
Generalizes Cartesian product ***)
-qed_goalw "QSigmaI" thy [QSigma_def]
- "!!A B. [| a:A; b:B(a) |] ==> <a;b> : QSigma(A,B)"
- (fn _ => [ Blast_tac 1 ]);
+Goalw [QSigma_def] "[| a:A; b:B(a) |] ==> <a;b> : QSigma(A,B)";
+by (Blast_tac 1) ;
+qed "QSigmaI";
AddSIs [QSigmaI];
(*The general elimination rule*)
-qed_goalw "QSigmaE" thy [QSigma_def]
+val major::prems= Goalw [QSigma_def]
"[| c: QSigma(A,B); \
\ !!x y.[| x:A; y:B(x); c=<x;y> |] ==> P \
-\ |] ==> P"
- (fn major::prems=>
- [ (cut_facts_tac [major] 1),
- (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
+\ |] ==> P";
+by (cut_facts_tac [major] 1);
+by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
+qed "QSigmaE";
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
@@ -71,23 +67,22 @@
THEN prune_params_tac)
(inst "c" "<a;b>" QSigmaE);
-val [major]= goal thy "<a;b> : QSigma(A,B) ==> a : A";
-by (rtac (major RS QSigmaE2) 1);
-by (assume_tac 1) ;
+AddSEs [QSigmaE2, QSigmaE];
+
+Goal "<a;b> : QSigma(A,B) ==> a : A";
+by (Blast_tac 1) ;
qed "QSigmaD1";
-val [major]= goal thy "<a;b> : QSigma(A,B) ==> b : B(a)";
-by (rtac (major RS QSigmaE2) 1);
-by (assume_tac 1) ;
+Goal "<a;b> : QSigma(A,B) ==> b : B(a)";
+by (Blast_tac 1) ;
qed "QSigmaD2";
-AddSEs [QSigmaE2, QSigmaE];
-
-qed_goalw "QSigma_cong" thy [QSigma_def]
+val prems= Goalw [QSigma_def]
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
-\ QSigma(A,B) = QSigma(A',B')"
- (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
+\ QSigma(A,B) = QSigma(A',B')";
+by (simp_tac (simpset() addsimps prems) 1) ;
+qed "QSigma_cong";
Goal "QSigma(0,B) = 0";
by (Blast_tac 1) ;
@@ -102,13 +97,13 @@
(*** Projections: qfst, qsnd ***)
-qed_goalw "qfst_conv" thy [qfst_def] "qfst(<a;b>) = a"
- (fn _=>
- [ (Blast_tac 1) ]);
+Goalw [qfst_def] "qfst(<a;b>) = a";
+by (Blast_tac 1) ;
+qed "qfst_conv";
-qed_goalw "qsnd_conv" thy [qsnd_def] "qsnd(<a;b>) = b"
- (fn _=>
- [ (Blast_tac 1) ]);
+Goalw [qsnd_def] "qsnd(<a;b>) = b";
+by (Blast_tac 1) ;
+qed "qsnd_conv";
Addsimps [qfst_conv, qsnd_conv];
@@ -133,7 +128,7 @@
qed "qsplit";
Addsimps [qsplit];
-val major::prems= goal thy
+val major::prems= Goal
"[| p:QSigma(A,B); \
\ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
\ |] ==> qsplit(%x y. c(x,y), p) : C(p)";
@@ -153,7 +148,7 @@
by (Asm_simp_tac 1);
qed "qsplitI";
-val major::sigma::prems = goalw thy [qsplit_def]
+val major::sigma::prems = Goalw [qsplit_def]
"[| qsplit(R,z); z:QSigma(A,B); \
\ !!x y. [| z = <x;y>; R(x,y) |] ==> P \
\ |] ==> P";
@@ -170,23 +165,23 @@
(*** qconverse ***)
-qed_goalw "qconverseI" thy [qconverse_def]
- "!!a b r. <a;b>:r ==> <b;a>:qconverse(r)"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [qconverse_def] "<a;b>:r ==> <b;a>:qconverse(r)";
+by (Blast_tac 1) ;
+qed "qconverseI";
-qed_goalw "qconverseD" thy [qconverse_def]
- "!!a b r. <a;b> : qconverse(r) ==> <b;a> : r"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [qconverse_def] "<a;b> : qconverse(r) ==> <b;a> : r";
+by (Blast_tac 1) ;
+qed "qconverseD";
-qed_goalw "qconverseE" thy [qconverse_def]
+val [major,minor]= Goalw [qconverse_def]
"[| yx : qconverse(r); \
\ !!x y. [| yx=<y;x>; <x;y>:r |] ==> P \
-\ |] ==> P"
- (fn [major,minor]=>
- [ (rtac (major RS ReplaceE) 1),
- (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
- (hyp_subst_tac 1),
- (assume_tac 1) ]);
+\ |] ==> P";
+by (rtac (major RS ReplaceE) 1);
+by (REPEAT (eresolve_tac [exE, conjE, minor] 1));
+by (hyp_subst_tac 1);
+by (assume_tac 1) ;
+qed "qconverseE";
AddSIs [qconverseI];
AddSEs [qconverseD, qconverseE];
@@ -224,7 +219,7 @@
(** Elimination rules **)
-val major::prems = goalw thy qsum_defs
+val major::prems = Goalw qsum_defs
"[| u: A <+> B; \
\ !!x. [| x:A; u=QInl(x) |] ==> P; \
\ !!y. [| y:B; u=QInr(y) |] ==> P \
@@ -304,7 +299,7 @@
Addsimps [qcase_QInl, qcase_QInr];
-val major::prems = goal thy
+val major::prems = Goal
"[| u: A <+> B; \
\ !!x. x: A ==> c(x): C(QInl(x)); \
\ !!y. y: B ==> d(y): C(QInr(y)) \
--- a/src/ZF/QUniv.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/QUniv.ML Fri Jun 30 12:51:30 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/quniv
+(* Title: ZF/QUniv
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -8,17 +8,14 @@
(** Properties involving Transset and Sum **)
-val [prem1,prem2] = goalw QUniv.thy [sum_def]
- "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
-by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1);
-by (REPEAT (etac (prem1 RS Transset_includes_range) 1
- ORELSE resolve_tac [conjI, singletonI] 1));
+Goalw [sum_def] "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
+by (dtac (Un_subset_iff RS iffD1) 1);
+by (blast_tac (claset() addDs [Transset_includes_range]) 1);
qed "Transset_includes_summands";
-val [prem] = goalw QUniv.thy [sum_def]
- "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
+Goalw [sum_def] "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
by (stac Int_Un_distrib 1);
-by (blast_tac (claset() addSDs [prem RS Transset_Pair_D]) 1);
+by (blast_tac (claset() addDs [Transset_Pair_D]) 1);
qed "Transset_sum_Int_subset";
(** Introduction and elimination rules avoid tiresome folding/unfolding **)
--- a/src/ZF/ROOT.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/ROOT.ML Fri Jun 30 12:51:30 2000 +0200
@@ -18,7 +18,6 @@
(*Add user sections for inductive/datatype definitions*)
use "thy_syntax";
-use_thy "Let";
use_thy "ZF";
use "Tools/typechk";
use_thy "mono";
@@ -28,7 +27,6 @@
use "Tools/inductive_package";
use "Tools/induct_tacs";
use "Tools/primrec_package";
-use_thy "Inductive";
use_thy "QUniv";
use "Tools/datatype_package";
--- a/src/ZF/Trancl.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/Trancl.ML Fri Jun 30 12:51:30 2000 +0200
@@ -133,8 +133,7 @@
qed "r_subset_trancl";
(*intro rule by definition: from r^* and r *)
-Goalw [trancl_def]
- "!!r. [| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+";
+Goalw [trancl_def] "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+";
by (Blast_tac 1);
qed "rtrancl_into_trancl1";
--- a/src/ZF/ZF.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/ZF.ML Fri Jun 30 12:51:30 2000 +0200
@@ -15,21 +15,21 @@
(*** Bounded universal quantifier ***)
-qed_goalw "ballI" ZF.thy [Ball_def]
- "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
- (fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]);
+val prems= Goalw [Ball_def]
+ "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)";
+by (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ;
+qed "ballI";
-qed_goalw "bspec" ZF.thy [Ball_def]
- "[| ALL x:A. P(x); x: A |] ==> P(x)"
- (fn major::prems=>
- [ (rtac (major RS spec RS mp) 1),
- (resolve_tac prems 1) ]);
+Goalw [Ball_def] "[| ALL x:A. P(x); x: A |] ==> P(x)";
+by (etac (spec RS mp) 1);
+by (assume_tac 1) ;
+qed "bspec";
-qed_goalw "ballE" ZF.thy [Ball_def]
- "[| ALL x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q"
- (fn major::prems=>
- [ (rtac (major RS allE) 1),
- (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
+val major::prems= Goalw [Ball_def]
+ "[| ALL x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q";
+by (rtac (major RS allE) 1);
+by (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ;
+qed "ballE";
(*Used in the datatype package*)
Goal "[| x: A; ALL x:A. P(x) |] ==> P(x)";
@@ -57,9 +57,10 @@
Addsimps [ball_triv];
(*Congruence rule for rewriting*)
-qed_goalw "ball_cong" ZF.thy [Ball_def]
- "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
- (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
+val prems= Goalw [Ball_def]
+ "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')";
+by (simp_tac (FOL_ss addsimps prems) 1) ;
+qed "ball_cong";
(*** Bounded existential quantifier ***)
@@ -78,12 +79,12 @@
by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ;
qed "bexCI";
-qed_goalw "bexE" ZF.thy [Bex_def]
+val major::prems= Goalw [Bex_def]
"[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q \
-\ |] ==> Q"
- (fn major::prems=>
- [ (rtac (major RS exE) 1),
- (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);
+\ |] ==> Q";
+by (rtac (major RS exE) 1);
+by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ;
+qed "bexE";
AddIs [bexI];
AddSEs [bexE];
@@ -94,32 +95,34 @@
qed "bex_triv";
Addsimps [bex_triv];
-qed_goalw "bex_cong" ZF.thy [Bex_def]
+val prems= Goalw [Bex_def]
"[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) \
-\ |] ==> Bex(A,P) <-> Bex(A',P')"
- (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
+\ |] ==> Bex(A,P) <-> Bex(A',P')";
+by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ;
+qed "bex_cong";
Addcongs [ball_cong, bex_cong];
(*** Rules for subsets ***)
-qed_goalw "subsetI" ZF.thy [subset_def]
- "(!!x. x:A ==> x:B) ==> A <= B"
- (fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]);
+val prems= Goalw [subset_def]
+ "(!!x. x:A ==> x:B) ==> A <= B";
+by (REPEAT (ares_tac (prems @ [ballI]) 1)) ;
+qed "subsetI";
(*Rule in Modus Ponens style [was called subsetE] *)
-qed_goalw "subsetD" ZF.thy [subset_def] "[| A <= B; c:A |] ==> c:B"
- (fn major::prems=>
- [ (rtac (major RS bspec) 1),
- (resolve_tac prems 1) ]);
+Goalw [subset_def] "[| A <= B; c:A |] ==> c:B";
+by (etac bspec 1);
+by (assume_tac 1) ;
+qed "subsetD";
(*Classical elimination rule*)
-qed_goalw "subsetCE" ZF.thy [subset_def]
- "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P"
- (fn major::prems=>
- [ (rtac (major RS ballE) 1),
- (REPEAT (eresolve_tac prems 1)) ]);
+val major::prems= Goalw [subset_def]
+ "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P";
+by (rtac (major RS ballE) 1);
+by (REPEAT (eresolve_tac prems 1)) ;
+qed "subsetCE";
AddSIs [subsetI];
AddEs [subsetCE, subsetD];
@@ -155,9 +158,10 @@
qed "subset_trans";
(*Useful for proving A<=B by rewriting in some cases*)
-qed_goalw "subset_iff" ZF.thy [subset_def,Ball_def]
- "A<=B <-> (ALL x. x:A --> x:B)"
- (fn _=> [ (rtac iff_refl 1) ]);
+Goalw [subset_def,Ball_def]
+ "A<=B <-> (ALL x. x:A --> x:B)";
+by (rtac iff_refl 1) ;
+qed "subset_iff";
(*** Rules for equality ***)
@@ -199,12 +203,12 @@
(*** Rules for Replace -- the derived form of replacement ***)
-qed_goalw "Replace_iff" ZF.thy [Replace_def]
- "b : {y. x:A, P(x,y)} <-> (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))"
- (fn _=>
- [ (rtac (replacement RS iff_trans) 1),
- (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1
- ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]);
+Goalw [Replace_def]
+ "b : {y. x:A, P(x,y)} <-> (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))";
+by (rtac (replacement RS iff_trans) 1);
+by (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1
+ ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ;
+qed "Replace_iff";
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
val prems = Goal
@@ -249,9 +253,9 @@
(*** Rules for RepFun ***)
-qed_goalw "RepFunI" ZF.thy [RepFun_def]
- "!!a A. a : A ==> f(a) : {f(x). x:A}"
- (fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
+Goalw [RepFun_def] "a : A ==> f(a) : {f(x). x:A}";
+by (REPEAT (ares_tac [ReplaceI,refl] 1)) ;
+qed "RepFunI";
(*Useful for coinduction proofs*)
Goal "[| b=f(a); a : A |] ==> b : {f(x). x:A}";
@@ -259,26 +263,27 @@
by (etac RepFunI 1) ;
qed "RepFun_eqI";
-qed_goalw "RepFunE" ZF.thy [RepFun_def]
+val major::prems= Goalw [RepFun_def]
"[| b : {f(x). x:A}; \
\ !!x.[| x:A; b=f(x) |] ==> P |] ==> \
-\ P"
- (fn major::prems=>
- [ (rtac (major RS ReplaceE) 1),
- (REPEAT (ares_tac prems 1)) ]);
+\ P";
+by (rtac (major RS ReplaceE) 1);
+by (REPEAT (ares_tac prems 1)) ;
+qed "RepFunE";
AddIs [RepFun_eqI];
AddSEs [RepFunE];
-qed_goalw "RepFun_cong" ZF.thy [RepFun_def]
- "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
- (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
+val prems= Goalw [RepFun_def]
+ "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)";
+by (simp_tac (simpset() addsimps prems) 1) ;
+qed "RepFun_cong";
Addcongs [RepFun_cong];
-qed_goalw "RepFun_iff" ZF.thy [Bex_def]
- "b : {f(x). x:A} <-> (EX x:A. b=f(x))"
- (fn _ => [(Blast_tac 1)]);
+Goalw [Bex_def] "b : {f(x). x:A} <-> (EX x:A. b=f(x))";
+by (Blast_tac 1);
+qed "RepFun_iff";
Goal "{x. x:A} = A";
by (Blast_tac 1);
@@ -289,9 +294,9 @@
(*** Rules for Collect -- forming a subset by separation ***)
(*Separation is derivable from Replacement*)
-qed_goalw "separation" ZF.thy [Collect_def]
- "a : {x:A. P(x)} <-> a:A & P(a)"
- (fn _=> [(Blast_tac 1)]);
+Goalw [Collect_def] "a : {x:A. P(x)} <-> a:A & P(a)";
+by (Blast_tac 1);
+qed "separation";
Addsimps [separation];
@@ -315,9 +320,10 @@
by (assume_tac 1) ;
qed "CollectD2";
-qed_goalw "Collect_cong" ZF.thy [Collect_def]
- "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
- (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
+val prems= Goalw [Collect_def]
+ "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)";
+by (simp_tac (simpset() addsimps prems) 1) ;
+qed "Collect_cong";
AddSIs [CollectI];
AddSEs [CollectE];
@@ -341,9 +347,10 @@
(*** Rules for Unions of families ***)
(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
-qed_goalw "UN_iff" ZF.thy [Bex_def]
- "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))"
- (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
+Goalw [Bex_def] "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))";
+by (Simp_tac 1);
+by (Blast_tac 1) ;
+qed "UN_iff";
Addsimps [UN_iff];
@@ -377,9 +384,11 @@
(*** Rules for Inter ***)
(*Not obviously useful towards proving InterI, InterD, InterE*)
-qed_goalw "Inter_iff" ZF.thy [Inter_def,Ball_def]
- "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)"
- (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
+Goalw [Inter_def,Ball_def]
+ "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)";
+by (Simp_tac 1);
+by (Blast_tac 1) ;
+qed "Inter_iff";
(* Intersection is well-behaved only if the family is non-empty! *)
val prems = Goal
@@ -390,16 +399,16 @@
(*A "destruct" rule -- every B in C contains A as an element, but
A:B can hold when B:C does not! This rule is analogous to "spec". *)
-qed_goalw "InterD" ZF.thy [Inter_def]
- "!!C. [| A : Inter(C); B : C |] ==> A : B"
- (fn _=> [(Blast_tac 1)]);
+Goalw [Inter_def] "[| A : Inter(C); B : C |] ==> A : B";
+by (Blast_tac 1);
+qed "InterD";
(*"Classical" elimination rule -- does not require exhibiting B:C *)
-qed_goalw "InterE" ZF.thy [Inter_def]
- "[| A : Inter(C); B~:C ==> R; A:B ==> R |] ==> R"
- (fn major::prems=>
- [ (rtac (major RS CollectD2 RS ballE) 1),
- (REPEAT (eresolve_tac prems 1)) ]);
+val major::prems= Goalw [Inter_def]
+ "[| A : Inter(C); B~:C ==> R; A:B ==> R |] ==> R";
+by (rtac (major RS CollectD2 RS ballE) 1);
+by (REPEAT (eresolve_tac prems 1)) ;
+qed "InterE";
AddSIs [InterI];
AddEs [InterD, InterE];
@@ -407,9 +416,10 @@
(*** Rules for Intersections of families ***)
(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
-qed_goalw "INT_iff" ZF.thy [Inter_def]
- "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)"
- (fn _=> [ Simp_tac 1, Best_tac 1 ]);
+Goalw [Inter_def] "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)";
+by (Simp_tac 1);
+by (Best_tac 1) ;
+qed "INT_iff";
val prems = Goal
"[| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x))";
--- a/src/ZF/domrange.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/domrange.ML Fri Jun 30 12:51:30 2000 +0200
@@ -8,27 +8,27 @@
(*** converse ***)
-qed_goalw "converse_iff" thy [converse_def]
- "<a,b>: converse(r) <-> <b,a>:r"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [converse_def] "<a,b>: converse(r) <-> <b,a>:r";
+by (Blast_tac 1) ;
+qed "converse_iff";
-qed_goalw "converseI" thy [converse_def]
- "!!a b r. <a,b>:r ==> <b,a>:converse(r)"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [converse_def] "<a,b>:r ==> <b,a>:converse(r)";
+by (Blast_tac 1) ;
+qed "converseI";
-qed_goalw "converseD" thy [converse_def]
- "!!a b r. <a,b> : converse(r) ==> <b,a> : r"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [converse_def] "<a,b> : converse(r) ==> <b,a> : r";
+by (Blast_tac 1) ;
+qed "converseD";
-qed_goalw "converseE" thy [converse_def]
+val [major,minor]= Goalw [converse_def]
"[| yx : converse(r); \
\ !!x y. [| yx=<y,x>; <x,y>:r |] ==> P \
-\ |] ==> P"
- (fn [major,minor]=>
- [ (rtac (major RS ReplaceE) 1),
- (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
- (hyp_subst_tac 1),
- (assume_tac 1) ]);
+\ |] ==> P";
+by (rtac (major RS ReplaceE) 1);
+by (REPEAT (eresolve_tac [exE, conjE, minor] 1));
+by (hyp_subst_tac 1);
+by (assume_tac 1) ;
+qed "converseE";
Addsimps [converse_iff];
AddSIs [converseI];
@@ -52,16 +52,16 @@
Addsimps [converse_prod, converse_empty];
-val converse_subset_iff = prove_goal thy
- "!!z. A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
- (fn _=> [ (Blast_tac 1) ]);
+Goal "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B";
+by (Blast_tac 1) ;
+qed "converse_subset_iff";
(*** domain ***)
-qed_goalw "domain_iff" thy [domain_def]
- "a: domain(r) <-> (EX y. <a,y>: r)"
- (fn _=> [ (Blast_tac 1) ]);
+Goalw [domain_def] "a: domain(r) <-> (EX y. <a,y>: r)";
+by (Blast_tac 1) ;
+qed "domain_iff";
Goal "<a,b>: r ==> a: domain(r)";
by (etac (exI RS (domain_iff RS iffD2)) 1) ;
@@ -82,44 +82,48 @@
(*** range ***)
-qed_goalw "rangeI" thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
- (fn _ => [ (etac (converseI RS domainI) 1) ]);
+Goalw [range_def] "<a,b>: r ==> b : range(r)";
+by (etac (converseI RS domainI) 1) ;
+qed "rangeI";
-qed_goalw "rangeE" thy [range_def]
- "[| b : range(r); !!x. <x,b>: r ==> P |] ==> P"
- (fn major::prems=>
- [ (rtac (major RS domainE) 1),
- (resolve_tac prems 1),
- (etac converseD 1) ]);
+val major::prems= Goalw [range_def]
+ "[| b : range(r); !!x. <x,b>: r ==> P |] ==> P";
+by (rtac (major RS domainE) 1);
+by (resolve_tac prems 1);
+by (etac converseD 1) ;
+qed "rangeE";
AddIs [rangeI];
AddSEs [rangeE];
-qed_goalw "range_subset" thy [range_def] "range(A*B) <= B"
- (fn _ =>
- [ (stac converse_prod 1),
- (rtac domain_subset 1) ]);
+Goalw [range_def] "range(A*B) <= B";
+by (stac converse_prod 1);
+by (rtac domain_subset 1) ;
+qed "range_subset";
(*** field ***)
-qed_goalw "fieldI1" thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
- (fn _ => [ (Blast_tac 1) ]);
-
-qed_goalw "fieldI2" thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [field_def] "<a,b>: r ==> a : field(r)";
+by (Blast_tac 1) ;
+qed "fieldI1";
-qed_goalw "fieldCI" thy [field_def]
- "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
- (fn [prem]=> [ (blast_tac (claset() addIs [prem]) 1) ]);
+Goalw [field_def] "<a,b>: r ==> b : field(r)";
+by (Blast_tac 1) ;
+qed "fieldI2";
-qed_goalw "fieldE" thy [field_def]
+val [prem]= Goalw [field_def]
+ "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)";
+by (blast_tac (claset() addIs [prem]) 1) ;
+qed "fieldCI";
+
+val major::prems= Goalw [field_def]
"[| a : field(r); \
\ !!x. <a,x>: r ==> P; \
-\ !!x. <x,a>: r ==> P |] ==> P"
- (fn major::prems=>
- [ (rtac (major RS UnE) 1),
- (REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ]);
+\ !!x. <x,a>: r ==> P |] ==> P";
+by (rtac (major RS UnE) 1);
+by (REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ;
+qed "fieldE";
AddIs [fieldCI];
AddSEs [fieldE];
@@ -128,13 +132,13 @@
by (Blast_tac 1) ;
qed "field_subset";
-qed_goalw "domain_subset_field" thy [field_def]
- "domain(r) <= field(r)"
- (fn _ => [ (rtac Un_upper1 1) ]);
+Goalw [field_def] "domain(r) <= field(r)";
+by (rtac Un_upper1 1) ;
+qed "domain_subset_field";
-qed_goalw "range_subset_field" thy [field_def]
- "range(r) <= field(r)"
- (fn _ => [ (rtac Un_upper2 1) ]);
+Goalw [field_def] "range(r) <= field(r)";
+by (rtac Un_upper2 1) ;
+qed "range_subset_field";
Goal "r <= Sigma(A,B) ==> r <= domain(r)*range(r)";
by (Blast_tac 1) ;
@@ -156,15 +160,15 @@
by (Blast_tac 1) ;
qed "image_singleton_iff";
-qed_goalw "imageI" thy [image_def]
- "!!a b r. [| <a,b>: r; a:A |] ==> b : r``A"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [image_def] "[| <a,b>: r; a:A |] ==> b : r``A";
+by (Blast_tac 1) ;
+qed "imageI";
-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),
- (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
+val major::prems= Goalw [image_def]
+ "[| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P";
+by (rtac (major RS CollectE) 1);
+by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ;
+qed "imageE";
AddIs [imageI];
AddSEs [imageE];
@@ -176,28 +180,29 @@
(*** Inverse image of a set under a function/relation ***)
-qed_goalw "vimage_iff" thy [vimage_def,image_def,converse_def]
- "a : r-``B <-> (EX y:B. <a,y>:r)"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [vimage_def,image_def,converse_def]
+ "a : r-``B <-> (EX y:B. <a,y>:r)";
+by (Blast_tac 1) ;
+qed "vimage_iff";
Goal "a : r-``{b} <-> <a,b>:r";
by (rtac (vimage_iff RS iff_trans) 1);
by (Blast_tac 1) ;
qed "vimage_singleton_iff";
-qed_goalw "vimageI" thy [vimage_def]
- "!!A B r. [| <a,b>: r; b:B |] ==> a : r-``B"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [vimage_def] "[| <a,b>: r; b:B |] ==> a : r-``B";
+by (Blast_tac 1) ;
+qed "vimageI";
-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)) ]);
+val major::prems= Goalw [vimage_def]
+ "[| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P";
+by (rtac (major RS imageE) 1);
+by (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ;
+qed "vimageE";
-qed_goalw "vimage_subset" thy [vimage_def]
- "!!A B r. r <= A*B ==> r-``C <= A"
- (fn _ => [ (etac (converse_type RS image_subset) 1) ]);
+Goalw [vimage_def] "r <= A*B ==> r-``C <= A";
+by (etac (converse_type RS image_subset) 1) ;
+qed "vimage_subset";
(** Theorem-proving for ZF set theory **)
--- a/src/ZF/func.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/func.ML Fri Jun 30 12:51:30 2000 +0200
@@ -237,13 +237,16 @@
qed "fun_extension_iff";
(*thanks to Mark Staples*)
-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)),
- (dtac (apply_Pair RSN (2,subsetD)) 1), (REPEAT (atac 1)),
- (rtac (apply_equality RS sym) 1), (REPEAT (atac 1)) ]);
+Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)";
+by (rtac iffI 1);
+by (asm_full_simp_tac ZF_ss 2);
+by (rtac fun_extension 1);
+by (REPEAT (atac 1));
+by (dtac (apply_Pair RSN (2,subsetD)) 1);
+by (REPEAT (atac 1));
+by (rtac (apply_equality RS sym) 1);
+by (REPEAT (atac 1)) ;
+qed "fun_subset_eq";
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
--- a/src/ZF/pair.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/pair.ML Fri Jun 30 12:51:30 2000 +0200
@@ -18,10 +18,10 @@
by (Blast_tac 1) ;
qed "doubleton_eq_iff";
-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) ]);
+Goalw [Pair_def] "<a,b> = <c,d> <-> a=c & b=d";
+by (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1);
+by (Blast_tac 1) ;
+qed "Pair_iff";
Addsimps [Pair_iff];
@@ -32,31 +32,33 @@
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" thy [Pair_def] "<a,b> ~= 0"
- (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
+Goalw [Pair_def] "<a,b> ~= 0";
+by (blast_tac (claset() addEs [equalityE]) 1) ;
+qed "Pair_not_0";
bind_thm ("Pair_neq_0", Pair_not_0 RS notE);
AddSEs [Pair_neq_0, sym RS Pair_neq_0];
-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) ]);
+Goalw [Pair_def] "<a,b>=a ==> P";
+by (rtac (consI1 RS mem_asym RS FalseE) 1);
+by (etac subst 1);
+by (rtac consI1 1) ;
+qed "Pair_neq_fst";
-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),
- (rtac (consI1 RS consI2) 1) ]);
+Goalw [Pair_def] "<a,b>=b ==> P";
+by (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1);
+by (etac subst 1);
+by (rtac (consI1 RS consI2) 1) ;
+qed "Pair_neq_snd";
(*** Sigma: Disjoint union of a family of sets
Generalizes Cartesian product ***)
-qed_goalw "Sigma_iff" thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
- (fn _ => [ Blast_tac 1 ]);
+Goalw [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)";
+by (Blast_tac 1) ;
+qed "Sigma_iff";
Addsimps [Sigma_iff];
@@ -70,13 +72,13 @@
bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);
(*The general elimination rule*)
-qed_goalw "SigmaE" thy [Sigma_def]
+val major::prems= Goalw [Sigma_def]
"[| c: Sigma(A,B); \
\ !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P \
-\ |] ==> P"
- (fn major::prems=>
- [ (cut_facts_tac [major] 1),
- (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
+\ |] ==> P";
+by (cut_facts_tac [major] 1);
+by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
+qed "SigmaE";
val [major,minor]= Goal
"[| <a,b> : Sigma(A,B); \
@@ -87,10 +89,11 @@
by (rtac (major RS SigmaD2) 1) ;
qed "SigmaE2";
-qed_goalw "Sigma_cong" thy [Sigma_def]
+val prems= Goalw [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) ]);
+\ Sigma(A,B) = Sigma(A',B')";
+by (simp_tac (simpset() addsimps prems) 1) ;
+qed "Sigma_cong";
(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
@@ -117,11 +120,13 @@
(*** Projections: fst, snd ***)
-qed_goalw "fst_conv" thy [fst_def] "fst(<a,b>) = a"
- (fn _=> [ (Blast_tac 1) ]);
+Goalw [fst_def] "fst(<a,b>) = a";
+by (Blast_tac 1) ;
+qed "fst_conv";
-qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b"
- (fn _=> [ (Blast_tac 1) ]);
+Goalw [snd_def] "snd(<a,b>) = b";
+by (Blast_tac 1) ;
+qed "snd_conv";
Addsimps [fst_conv,snd_conv];
--- a/src/ZF/subset.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/subset.ML Fri Jun 30 12:51:30 2000 +0200
@@ -41,16 +41,16 @@
(*But if j is an ordinal or is transitive, then i:j implies i<=j!
See ordinal/Ord_succ_subsetI*)
-qed_goalw "succ_subsetI" thy [succ_def]
- "!!i j. [| i:j; i<=j |] ==> succ(i)<=j"
- (fn _=> [ (Blast_tac 1) ]);
+Goalw [succ_def] "[| i:j; i<=j |] ==> succ(i)<=j";
+by (Blast_tac 1) ;
+qed "succ_subsetI";
-qed_goalw "succ_subsetE" thy [succ_def]
+val major::prems= Goalw [succ_def]
"[| succ(i) <= j; [| i:j; i<=j |] ==> P \
-\ |] ==> P"
- (fn major::prems=>
- [ (rtac (major RS cons_subsetE) 1),
- (REPEAT (ares_tac prems 1)) ]);
+\ |] ==> P";
+by (rtac (major RS cons_subsetE) 1);
+by (REPEAT (ares_tac prems 1)) ;
+qed "succ_subsetE";
(*** singletons ***)
--- a/src/ZF/upair.ML Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/upair.ML Fri Jun 30 12:51:30 2000 +0200
@@ -20,9 +20,9 @@
(*** Unordered pairs - Upair ***)
-qed_goalw "Upair_iff" thy [Upair_def]
- "c : Upair(a,b) <-> (c=a | c=b)"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [Upair_def] "c : Upair(a,b) <-> (c=a | c=b)";
+by (Blast_tac 1) ;
+qed "Upair_iff";
Addsimps [Upair_iff];
@@ -45,8 +45,9 @@
(*** Rules for binary union -- Un -- defined via Upair ***)
-qed_goalw "Un_iff" thy [Un_def] "c : A Un B <-> (c:A | c:B)"
- (fn _ => [(Blast_tac 1)]);
+Goalw [Un_def] "c : A Un B <-> (c:A | c:B)";
+by (Blast_tac 1);
+qed "Un_iff";
Addsimps [Un_iff];
@@ -87,8 +88,9 @@
(*** Rules for small intersection -- Int -- defined via Upair ***)
-qed_goalw "Int_iff" thy [Int_def] "c : A Int B <-> (c:A & c:B)"
- (fn _ => [(Blast_tac 1)]);
+Goalw [Int_def] "c : A Int B <-> (c:A & c:B)";
+by (Blast_tac 1);
+qed "Int_iff";
Addsimps [Int_iff];
@@ -114,8 +116,9 @@
(*** Rules for set difference -- defined via Upair ***)
-qed_goalw "Diff_iff" thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
- (fn _ => [(Blast_tac 1)]);
+Goalw [Diff_def] "c : A-B <-> (c:A & c~:B)";
+by (Blast_tac 1);
+qed "Diff_iff";
Addsimps [Diff_iff];
@@ -141,8 +144,9 @@
(*** Rules for cons -- defined via Un and Upair ***)
-qed_goalw "cons_iff" thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
- (fn _ => [(Blast_tac 1)]);
+Goalw [cons_def] "a : cons(b,A) <-> (a=b | a:A)";
+by (Blast_tac 1);
+qed "cons_iff";
Addsimps [cons_iff];
@@ -210,10 +214,10 @@
(*** Rules for Descriptions ***)
-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) ]);
+val [pa,eq] = Goalw [the_def]
+ "[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a";
+by (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ;
+qed "the_equality";
AddIs [the_equality];
@@ -337,23 +341,25 @@
(*** Rules for succ ***)
-qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j"
- (fn _ => [(Blast_tac 1)]);
+Goalw [succ_def] "i : succ(j) <-> i=j | i:j";
+by (Blast_tac 1);
+qed "succ_iff";
-qed_goalw "succI1" thy [succ_def] "i : succ(i)"
- (fn _=> [ (rtac consI1 1) ]);
+Goalw [succ_def] "i : succ(i)";
+by (rtac consI1 1) ;
+qed "succI1";
Addsimps [succI1];
-qed_goalw "succI2" thy [succ_def]
- "i : j ==> i : succ(j)"
- (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
+Goalw [succ_def] "i : j ==> i : succ(j)";
+by (etac consI2 1) ;
+qed "succI2";
-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)) ]);
+val major::prems= Goalw [succ_def]
+ "[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P";
+by (rtac (major RS consE) 1);
+by (REPEAT (eresolve_tac prems 1)) ;
+qed "succE";
(*Classical introduction rule*)
val [prem]= Goal "(i~:j ==> i=j) ==> i: succ(j)";