--- a/src/ZF/CardinalArith.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/CardinalArith.ML Wed Jun 28 12:34:08 2000 +0200
@@ -683,7 +683,7 @@
ORELSE eresolve_tac [ltE, Card_is_Ord] 1));
qed "lt_csucc_iff";
-Goal "!!K' K. [| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K";
+Goal "[| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K";
by (asm_simp_tac
(simpset() addsimps [lt_csucc_iff, Card_cardinal_eq, Card_is_Ord]) 1);
qed "Card_lt_csucc_iff";
--- a/src/ZF/Nat.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/Nat.ML Wed Jun 28 12:34:08 2000 +0200
@@ -50,7 +50,7 @@
(** Injectivity properties and induction **)
(*Mathematical induction*)
-val major::prems = goal Nat.thy
+val major::prems = Goal
"[| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)";
by (rtac ([nat_def, nat_bnd_mono, major] MRS def_induct) 1);
by (blast_tac (claset() addIs prems) 1);
@@ -62,15 +62,15 @@
rename_last_tac a ["1"] (i+2),
ares_tac prems i];
-val major::prems = goal Nat.thy
+val major::prems = Goal
"[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P";
by (rtac (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1);
by (DEPTH_SOLVE (eresolve_tac [singletonE,RepFunE] 1
ORELSE ares_tac prems 1));
qed "natE";
-val prems = goal Nat.thy "n: nat ==> Ord(n)";
-by (nat_ind_tac "n" prems 1);
+Goal "n: nat ==> Ord(n)";
+by (nat_ind_tac "n" [] 1);
by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
qed "nat_into_Ord";
@@ -135,7 +135,7 @@
(*complete induction*)
val complete_induct = Ord_nat RSN (2, Ord_induct);
-val prems = goal Nat.thy
+val prems = Goal
"[| m: nat; n: nat; \
\ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \
\ |] ==> m le n --> P(m) --> P(n)";
@@ -146,7 +146,7 @@
qed "nat_induct_from_lemma";
(*Induction starting from m rather than 0*)
-val prems = goal Nat.thy
+val prems = Goal
"[| m le n; m: nat; n: nat; \
\ P(m); \
\ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \
@@ -156,7 +156,7 @@
qed "nat_induct_from";
(*Induction suitable for subtraction and less-than*)
-val prems = goal Nat.thy
+val prems = Goal
"[| m: nat; n: nat; \
\ !!x. x: nat ==> P(x,0); \
\ !!y. y: nat ==> P(0,succ(y)); \
@@ -180,7 +180,7 @@
blast_tac le_cs, blast_tac le_cs]));
qed "succ_lt_induct_lemma";
-val prems = goal Nat.thy
+val prems = Goal
"[| m<n; n: nat; \
\ P(m,succ(m)); \
\ !!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) \
@@ -202,7 +202,7 @@
Addsimps [nat_case_0, nat_case_succ];
-val major::prems = goal Nat.thy
+val major::prems = Goal
"[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) \
\ |] ==> nat_case(a,b,n) : C(n)";
by (rtac (major RS nat_induct) 1);
--- a/src/ZF/OrdQuant.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/OrdQuant.ML Wed Jun 28 12:34:08 2000 +0200
@@ -23,15 +23,16 @@
[ (rtac (major RS allE) 1),
(REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
-qed_goal "rev_oallE" thy
- "[| ALL x<A. P(x); ~x<A ==> Q; P(x) ==> Q |] ==> Q"
- (fn major::prems=>
- [ (rtac (major RS oallE) 1),
- (REPEAT (eresolve_tac prems 1)) ]);
+val major::prems= goal thy
+ "[| ALL x<A. P(x); ~x<A ==> Q; P(x) ==> Q |] ==> Q";
+by (rtac (major RS oallE) 1);
+by (REPEAT (eresolve_tac prems 1)) ;
+qed "rev_oallE";
(*Trival rewrite rule; (ALL x<a.P)<->P holds only if a is not 0!*)
-qed_goal "oall_simp" thy "(ALL x<a. True) <-> True"
- (fn _=> [ (REPEAT (ares_tac [TrueI,oallI,iffI] 1)) ]);
+Goal "(ALL x<a. True) <-> True";
+by (REPEAT (ares_tac [TrueI,oallI,iffI] 1)) ;
+qed "oall_simp";
(*Congruence rule for rewriting*)
qed_goalw "oall_cong" thy [oall_def]
@@ -46,11 +47,11 @@
(fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]);
(*Not of the general form for such rules; ~EX has become ALL~ *)
-qed_goal "oexCI" thy
- "[| ALL x<A. ~P(x) ==> P(a); a<A |] ==> EX x<A. P(x)"
- (fn prems=>
- [ (rtac classical 1),
- (REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ]);
+val prems = Goal
+ "[| ALL x<A. ~P(x) ==> P(a); a<A |] ==> EX x<A. P(x)";
+by (rtac classical 1);
+by (REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ;
+qed "oexCI";
qed_goalw "oexE" thy [oex_def]
"[| EX x<A. P(x); !!x. [| x<A; P(x) |] ==> Q \
@@ -82,11 +83,11 @@
"b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
(fn _=> [ (fast_tac (claset() addIs [OUN_I] addSEs [OUN_E]) 1) ]);
-qed_goal "OUN_cong" thy
- "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
- (fn prems=>
- [ rtac equality_iffI 1,
- simp_tac (simpset() addcongs [oex_cong] addsimps OUN_iff::prems) 1 ]);
+val prems = Goal
+ "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))";
+by (rtac equality_iffI 1);
+by (simp_tac (simpset() addcongs [oex_cong] addsimps OUN_iff::prems) 1) ;
+qed "OUN_cong";
AddSIs [oallI];
AddIs [oexI, OUN_I];
@@ -100,7 +101,7 @@
addsimps [oall_simp, ltD RS beta]
addcongs [oall_cong, oex_cong, OUN_cong];
-val major::prems = goalw thy [lt_def, oall_def]
+val major::prems = Goalw [lt_def, oall_def]
"[| i<k; !!x.[| x<k; ALL y<x. P(y) |] ==> P(x) \
\ |] ==> P(i)";
by (rtac (major RS conjE) 1);
--- a/src/ZF/Ordinal.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/Ordinal.ML Wed Jun 28 12:34:08 2000 +0200
@@ -235,11 +235,14 @@
(* [| i<j; ~P ==> j<i |] ==> P *)
bind_thm ("lt_asym", lt_not_sym RS swap);
-qed_goal "lt_irrefl" Ordinal.thy "i<i ==> P"
- (fn [major]=> [ (rtac (major RS (major RS lt_asym)) 1) ]);
+val [major]= goal Ordinal.thy "i<i ==> P";
+by (rtac (major RS (major RS lt_asym)) 1) ;
+qed "lt_irrefl";
-qed_goal "lt_not_refl" Ordinal.thy "~ i<i"
- (fn _=> [ (rtac notI 1), (etac lt_irrefl 1) ]);
+Goal "~ i<i";
+by (rtac notI 1);
+by (etac lt_irrefl 1) ;
+qed "lt_not_refl";
AddSEs [lt_irrefl, lt0E];
--- a/src/ZF/Perm.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/Perm.ML Wed Jun 28 12:34:08 2000 +0200
@@ -529,14 +529,13 @@
by (blast_tac (claset() addIs [fun_weaken_type]) 1);
qed "inj_weaken_type";
-val [major] = goal Perm.thy
- "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})";
-by (rtac (major RS restrict_bij RS bij_is_inj RS inj_weaken_type) 1);
+Goal "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})";
+by (rtac (restrict_bij RS bij_is_inj RS inj_weaken_type) 1);
+by (assume_tac 1);
by (Blast_tac 1);
-by (cut_facts_tac [major] 1);
by (rewtac inj_def);
by (fast_tac (claset() addEs [range_type, mem_irrefl]
- addDs [apply_equality]) 1);
+ addDs [apply_equality]) 1);
qed "inj_succ_restrict";
Goalw [inj_def]
--- a/src/ZF/QPair.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/QPair.ML Wed Jun 28 12:34:08 2000 +0200
@@ -35,13 +35,15 @@
Addsimps [QPair_empty, QPair_iff];
AddSEs [QPair_inject];
-qed_goal "QPair_inject1" thy "<a;b> = <c;d> ==> a=c"
- (fn [major]=>
- [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]);
+val [major]= goal thy "<a;b> = <c;d> ==> a=c";
+by (rtac (major RS QPair_inject) 1);
+by (assume_tac 1) ;
+qed "QPair_inject1";
-qed_goal "QPair_inject2" thy "<a;b> = <c;d> ==> b=d"
- (fn [major]=>
- [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]);
+val [major]= goal thy "<a;b> = <c;d> ==> b=d";
+by (rtac (major RS QPair_inject) 1);
+by (assume_tac 1) ;
+qed "QPair_inject2";
(*** QSigma: Disjoint union of a family of sets
@@ -69,13 +71,15 @@
THEN prune_params_tac)
(inst "c" "<a;b>" QSigmaE);
-qed_goal "QSigmaD1" thy "<a;b> : QSigma(A,B) ==> a : A"
- (fn [major]=>
- [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
+val [major]= goal thy "<a;b> : QSigma(A,B) ==> a : A";
+by (rtac (major RS QSigmaE2) 1);
+by (assume_tac 1) ;
+qed "QSigmaD1";
-qed_goal "QSigmaD2" thy "<a;b> : QSigma(A,B) ==> b : B(a)"
- (fn [major]=>
- [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
+val [major]= goal thy "<a;b> : QSigma(A,B) ==> b : B(a)";
+by (rtac (major RS QSigmaE2) 1);
+by (assume_tac 1) ;
+qed "QSigmaD2";
AddSEs [QSigmaE2, QSigmaE];
@@ -85,11 +89,13 @@
\ QSigma(A,B) = QSigma(A',B')"
(fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
-qed_goal "QSigma_empty1" thy "QSigma(0,B) = 0"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "QSigma(0,B) = 0";
+by (Blast_tac 1) ;
+qed "QSigma_empty1";
-qed_goal "QSigma_empty2" thy "A <*> 0 = 0"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "A <*> 0 = 0";
+by (Blast_tac 1) ;
+qed "QSigma_empty2";
Addsimps [QSigma_empty1, QSigma_empty2];
@@ -106,13 +112,13 @@
Addsimps [qfst_conv, qsnd_conv];
-qed_goal "qfst_type" thy
- "!!p. p:QSigma(A,B) ==> qfst(p) : A"
- (fn _=> [ Auto_tac ]);
+Goal "p:QSigma(A,B) ==> qfst(p) : A";
+by (Auto_tac) ;
+qed "qfst_type";
-qed_goal "qsnd_type" thy
- "!!p. p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"
- (fn _=> [ Auto_tac ]);
+Goal "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))";
+by (Auto_tac) ;
+qed "qsnd_type";
Goal "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a";
by Auto_tac;
@@ -127,13 +133,13 @@
qed "qsplit";
Addsimps [qsplit];
-qed_goal "qsplit_type" thy
+val major::prems= goal thy
"[| 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)"
- (fn major::prems=>
- [ (rtac (major RS QSigmaE) 1),
- (asm_simp_tac (simpset() addsimps prems) 1) ]);
+\ |] ==> qsplit(%x y. c(x,y), p) : C(p)";
+by (rtac (major RS QSigmaE) 1);
+by (asm_simp_tac (simpset() addsimps prems) 1) ;
+qed "qsplit_type";
Goalw [qsplit_def]
"u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))";
@@ -185,19 +191,21 @@
AddSIs [qconverseI];
AddSEs [qconverseD, qconverseE];
-qed_goal "qconverse_qconverse" thy
- "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r";
+by (Blast_tac 1) ;
+qed "qconverse_qconverse";
+
+Goal "r <= A <*> B ==> qconverse(r) <= B <*> A";
+by (Blast_tac 1) ;
+qed "qconverse_type";
-qed_goal "qconverse_type" thy
- "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "qconverse(A <*> B) = B <*> A";
+by (Blast_tac 1) ;
+qed "qconverse_prod";
-qed_goal "qconverse_prod" thy "qconverse(A <*> B) = B <*> A"
- (fn _ => [ (Blast_tac 1) ]);
-
-qed_goal "qconverse_empty" thy "qconverse(0) = 0"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "qconverse(0) = 0";
+by (Blast_tac 1) ;
+qed "qconverse_empty";
(**** The Quine-inspired notion of disjoint sum ****)
--- a/src/ZF/WF.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/WF.ML Wed Jun 28 12:34:08 2000 +0200
@@ -101,7 +101,7 @@
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
qed "wf_induct2";
-Goal "!!r A. field(r Int A*A) <= A";
+Goal "field(r Int A*A) <= A";
by (Blast_tac 1);
qed "field_Int_square";
--- a/src/ZF/ZF.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/ZF.ML Wed Jun 28 12:34:08 2000 +0200
@@ -32,17 +32,16 @@
(REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
(*Used in the datatype package*)
-qed_goal "rev_bspec" ZF.thy
- "!!x A P. [| x: A; ALL x:A. P(x) |] ==> P(x)"
- (fn _ =>
- [ REPEAT (ares_tac [bspec] 1) ]);
+Goal "[| x: A; ALL x:A. P(x) |] ==> P(x)";
+by (REPEAT (ares_tac [bspec] 1)) ;
+qed "rev_bspec";
(*Instantiates x first: better for automatic theorem proving?*)
-qed_goal "rev_ballE" ZF.thy
- "[| ALL x:A. P(x); x~:A ==> Q; P(x) ==> Q |] ==> Q"
- (fn major::prems=>
- [ (rtac (major RS ballE) 1),
- (REPEAT (eresolve_tac prems 1)) ]);
+val major::prems= Goal
+ "[| ALL x:A. P(x); x~:A ==> Q; P(x) ==> Q |] ==> Q";
+by (rtac (major RS ballE) 1);
+by (REPEAT (eresolve_tac prems 1)) ;
+qed "rev_ballE";
AddSIs [ballI];
AddEs [rev_ballE];
@@ -52,8 +51,9 @@
val ball_tac = dtac bspec THEN' assume_tac;
(*Trival rewrite rule; (ALL x:A.P)<->P holds only if A is nonempty!*)
-qed_goal "ball_triv" ZF.thy "(ALL x:A. P) <-> ((EX x. x:A) --> P)"
- (fn _=> [ simp_tac (simpset() addsimps [Ball_def]) 1 ]);
+Goal "(ALL x:A. P) <-> ((EX x. x:A) --> P)";
+by (simp_tac (simpset() addsimps [Ball_def]) 1) ;
+qed "ball_triv";
Addsimps [ball_triv];
(*Congruence rule for rewriting*)
@@ -73,11 +73,10 @@
qed "rev_bexI";
(*Not of the general form for such rules; ~EX has become ALL~ *)
-qed_goal "bexCI" ZF.thy
- "[| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A. P(x)"
- (fn prems=>
- [ (rtac classical 1),
- (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
+val prems= Goal "[| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A. P(x)";
+by (rtac classical 1);
+by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ;
+qed "bexCI";
qed_goalw "bexE" ZF.thy [Bex_def]
"[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q \
@@ -90,8 +89,9 @@
AddSEs [bexE];
(*We do not even have (EX x:A. True) <-> True unless A is nonempty!!*)
-qed_goal "bex_triv" ZF.thy "(EX x:A. P) <-> ((EX x. x:A) & P)"
- (fn _=> [ simp_tac (simpset() addsimps [Bex_def]) 1 ]);
+Goal "(EX x:A. P) <-> ((EX x. x:A) & P)";
+by (simp_tac (simpset() addsimps [Bex_def]) 1) ;
+qed "bex_triv";
Addsimps [bex_triv];
qed_goalw "bex_cong" ZF.thy [Bex_def]
@@ -129,25 +129,30 @@
val set_mp_tac = dtac subsetD THEN' assume_tac;
(*Sometimes useful with premises in this order*)
-qed_goal "rev_subsetD" ZF.thy "!!A B c. [| c:A; A<=B |] ==> c:B"
- (fn _=> [ Blast_tac 1 ]);
+Goal "[| c:A; A<=B |] ==> c:B";
+by (Blast_tac 1);
+qed "rev_subsetD";
(*Converts A<=B to x:A ==> x:B*)
fun impOfSubs th = th RSN (2, rev_subsetD);
-qed_goal "contra_subsetD" ZF.thy "!!c. [| A <= B; c ~: B |] ==> c ~: A"
- (fn _=> [ Blast_tac 1 ]);
+Goal "[| A <= B; c ~: B |] ==> c ~: A";
+by (Blast_tac 1);
+qed "contra_subsetD";
-qed_goal "rev_contra_subsetD" ZF.thy "!!c. [| c ~: B; A <= B |] ==> c ~: A"
- (fn _=> [ Blast_tac 1 ]);
+Goal "[| c ~: B; A <= B |] ==> c ~: A";
+by (Blast_tac 1);
+qed "rev_contra_subsetD";
-qed_goal "subset_refl" ZF.thy "A <= A"
- (fn _=> [ Blast_tac 1 ]);
+Goal "A <= A";
+by (Blast_tac 1);
+qed "subset_refl";
Addsimps [subset_refl];
-qed_goal "subset_trans" ZF.thy "!!A B C. [| A<=B; B<=C |] ==> A<=C"
- (fn _=> [ Blast_tac 1 ]);
+Goal "[| A<=B; B<=C |] ==> A<=C";
+by (Blast_tac 1);
+qed "subset_trans";
(*Useful for proving A<=B by rewriting in some cases*)
qed_goalw "subset_iff" ZF.thy [subset_def,Ball_def]
@@ -158,39 +163,38 @@
(*** Rules for equality ***)
(*Anti-symmetry of the subset relation*)
-qed_goal "equalityI" ZF.thy "[| A <= B; B <= A |] ==> A = B"
- (fn prems=> [ (REPEAT (resolve_tac (prems@[conjI, extension RS iffD2]) 1)) ]);
+Goal "[| A <= B; B <= A |] ==> A = B";
+by (REPEAT (ares_tac [conjI, extension RS iffD2] 1)) ;
+qed "equalityI";
AddIs [equalityI];
-qed_goal "equality_iffI" ZF.thy "(!!x. x:A <-> x:B) ==> A = B"
- (fn [prem] =>
- [ (rtac equalityI 1),
- (REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ]);
+val [prem] = Goal "(!!x. x:A <-> x:B) ==> A = B";
+by (rtac equalityI 1);
+by (REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ;
+qed "equality_iffI";
bind_thm ("equalityD1", extension RS iffD1 RS conjunct1);
bind_thm ("equalityD2", extension RS iffD1 RS conjunct2);
-qed_goal "equalityE" ZF.thy
- "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P"
- (fn prems=>
- [ (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ]);
+val prems = Goal "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P";
+by (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ;
+qed "equalityE";
-qed_goal "equalityCE" ZF.thy
- "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"
- (fn major::prems=>
- [ (rtac (major RS equalityE) 1),
- (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ]);
+val major::prems= Goal
+ "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P";
+by (rtac (major RS equalityE) 1);
+by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ;
+qed "equalityCE";
(*Lemma for creating induction formulae -- for "pattern matching" on p
To make the induction hypotheses usable, apply "spec" or "bspec" to
put universal quantifiers over the free variables in p.
Would it be better to do subgoal_tac "ALL z. p = f(z) --> R(z)" ??*)
-qed_goal "setup_induction" ZF.thy
- "[| p: A; !!z. z: A ==> p=z --> R |] ==> R"
- (fn prems=>
- [ (rtac mp 1),
- (REPEAT (resolve_tac (refl::prems) 1)) ]);
+val prems = Goal "[| p: A; !!z. z: A ==> p=z --> R |] ==> R";
+by (rtac mp 1);
+by (REPEAT (resolve_tac (refl::prems) 1)) ;
+qed "setup_induction";
(*** Rules for Replace -- the derived form of replacement ***)
@@ -203,46 +207,43 @@
ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]);
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
-qed_goal "ReplaceI" ZF.thy
+val prems = Goal
"[| P(x,b); x: A; !!y. P(x,y) ==> y=b |] ==> \
-\ b : {y. x:A, P(x,y)}"
- (fn prems=>
- [ (rtac (Replace_iff RS iffD2) 1),
- (REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ]);
+\ b : {y. x:A, P(x,y)}";
+by (rtac (Replace_iff RS iffD2) 1);
+by (REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ;
+qed "ReplaceI";
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
-qed_goal "ReplaceE" ZF.thy
+val prems = Goal
"[| b : {y. x:A, P(x,y)}; \
\ !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R \
-\ |] ==> R"
- (fn prems=>
- [ (rtac (Replace_iff RS iffD1 RS bexE) 1),
- (etac conjE 2),
- (REPEAT (ares_tac prems 1)) ]);
+\ |] ==> R";
+by (rtac (Replace_iff RS iffD1 RS bexE) 1);
+by (etac conjE 2);
+by (REPEAT (ares_tac prems 1)) ;
+qed "ReplaceE";
(*As above but without the (generally useless) 3rd assumption*)
-qed_goal "ReplaceE2" ZF.thy
+val major::prems = Goal
"[| b : {y. x:A, P(x,y)}; \
\ !!x. [| x: A; P(x,b) |] ==> R \
-\ |] ==> R"
- (fn major::prems=>
- [ (rtac (major RS ReplaceE) 1),
- (REPEAT (ares_tac prems 1)) ]);
+\ |] ==> R";
+by (rtac (major RS ReplaceE) 1);
+by (REPEAT (ares_tac prems 1)) ;
+qed "ReplaceE2";
AddIs [ReplaceI];
AddSEs [ReplaceE2];
-qed_goal "Replace_cong" ZF.thy
+val prems = Goal
"[| A=B; !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
-\ Replace(A,P) = Replace(B,Q)"
- (fn prems=>
- let val substprems = prems RL [subst, ssubst]
- and iffprems = prems RL [iffD1,iffD2]
- in [ (rtac equalityI 1),
- (REPEAT (eresolve_tac (substprems@[asm_rl, ReplaceE, spec RS mp]) 1
- ORELSE resolve_tac [subsetI, ReplaceI] 1
- ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]
- end);
+\ Replace(A,P) = Replace(B,Q)";
+by (rtac equalityI 1);
+by (REPEAT
+ (eresolve_tac ((prems RL [subst, ssubst])@[asm_rl, ReplaceE, spec RS mp]) 1 ORELSE resolve_tac [subsetI, ReplaceI] 1
+ ORELSE (resolve_tac (prems RL [iffD1,iffD2]) 1 THEN assume_tac 2)));
+qed "Replace_cong";
Addcongs [Replace_cong];
@@ -253,9 +254,10 @@
(fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
(*Useful for coinduction proofs*)
-qed_goal "RepFun_eqI" ZF.thy
- "!!b a f. [| b=f(a); a : A |] ==> b : {f(x). x:A}"
- (fn _ => [ etac ssubst 1, etac RepFunI 1 ]);
+Goal "[| b=f(a); a : A |] ==> b : {f(x). x:A}";
+by (etac ssubst 1);
+by (etac RepFunI 1) ;
+qed "RepFun_eqI";
qed_goalw "RepFunE" ZF.thy [RepFun_def]
"[| b : {f(x). x:A}; \
@@ -276,7 +278,7 @@
qed_goalw "RepFun_iff" ZF.thy [Bex_def]
"b : {f(x). x:A} <-> (EX x:A. b=f(x))"
- (fn _ => [Blast_tac 1]);
+ (fn _ => [(Blast_tac 1)]);
Goal "{x. x:A} = A";
by (Blast_tac 1);
@@ -289,25 +291,29 @@
(*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]);
+ (fn _=> [(Blast_tac 1)]);
Addsimps [separation];
-qed_goal "CollectI" ZF.thy
- "!!P. [| a:A; P(a) |] ==> a : {x:A. P(x)}"
- (fn _=> [ Asm_simp_tac 1 ]);
+Goal "[| a:A; P(a) |] ==> a : {x:A. P(x)}";
+by (Asm_simp_tac 1);
+qed "CollectI";
+
+val prems = Goal
+ "[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> R |] ==> R";
+by (rtac (separation RS iffD1 RS conjE) 1);
+by (REPEAT (ares_tac prems 1)) ;
+qed "CollectE";
-qed_goal "CollectE" ZF.thy
- "[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> R |] ==> R"
- (fn prems=>
- [ (rtac (separation RS iffD1 RS conjE) 1),
- (REPEAT (ares_tac prems 1)) ]);
+Goal "a : {x:A. P(x)} ==> a:A";
+by (etac CollectE 1);
+by (assume_tac 1) ;
+qed "CollectD1";
-qed_goal "CollectD1" ZF.thy "!!P. a : {x:A. P(x)} ==> a:A"
- (fn _=> [ (etac CollectE 1), (assume_tac 1) ]);
-
-qed_goal "CollectD2" ZF.thy "!!P. a : {x:A. P(x)} ==> P(a)"
- (fn _=> [ (etac CollectE 1), (assume_tac 1) ]);
+Goal "a : {x:A. P(x)} ==> P(a)";
+by (etac CollectE 1);
+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)"
@@ -322,14 +328,15 @@
Addsimps [Union_iff];
(*The order of the premises presupposes that C is rigid; A may be flexible*)
-qed_goal "UnionI" ZF.thy "!!C. [| B: C; A: B |] ==> A: Union(C)"
- (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
+Goal "[| B: C; A: B |] ==> A: Union(C)";
+by (Simp_tac 1);
+by (Blast_tac 1) ;
+qed "UnionI";
-qed_goal "UnionE" ZF.thy
- "[| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R"
- (fn prems=>
- [ (resolve_tac [Union_iff RS iffD1 RS bexE] 1),
- (REPEAT (ares_tac prems 1)) ]);
+val prems = Goal "[| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R";
+by (resolve_tac [Union_iff RS iffD1 RS bexE] 1);
+by (REPEAT (ares_tac prems 1)) ;
+qed "UnionE";
(*** Rules for Unions of families ***)
(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
@@ -341,18 +348,21 @@
Addsimps [UN_iff];
(*The order of the premises presupposes that A is rigid; b may be flexible*)
-qed_goal "UN_I" ZF.thy "!!A B. [| a: A; b: B(a) |] ==> b: (UN x:A. B(x))"
- (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
+Goal "[| a: A; b: B(a) |] ==> b: (UN x:A. B(x))";
+by (Simp_tac 1);
+by (Blast_tac 1) ;
+qed "UN_I";
-qed_goal "UN_E" ZF.thy
- "[| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R"
- (fn major::prems=>
- [ (rtac (major RS UnionE) 1),
- (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]);
+val major::prems= Goal
+ "[| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R";
+by (rtac (major RS UnionE) 1);
+by (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ;
+qed "UN_E";
-qed_goal "UN_cong" ZF.thy
- "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A. C(x)) = (UN x:B. D(x))"
- (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
+val prems = Goal
+ "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A. C(x)) = (UN x:B. D(x))";
+by (simp_tac (simpset() addsimps prems) 1) ;
+qed "UN_cong";
(*No "Addcongs [UN_cong]" because UN is a combination of constants*)
@@ -372,16 +382,17 @@
(fn _=> [ Simp_tac 1, Blast_tac 1 ]);
(* Intersection is well-behaved only if the family is non-empty! *)
-qed_goal "InterI" ZF.thy
- "[| !!x. x: C ==> A: x; EX c. c:C |] ==> A : Inter(C)"
- (fn prems=> [ (simp_tac (simpset() addsimps [Inter_iff]) 1),
- blast_tac (claset() addIs prems) 1 ]);
+val prems = Goal
+ "[| !!x. x: C ==> A: x; EX c. c:C |] ==> A : Inter(C)";
+by (simp_tac (simpset() addsimps [Inter_iff]) 1);
+by (blast_tac (claset() addIs prems) 1) ;
+qed "InterI";
(*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 ]);
+ (fn _=> [(Blast_tac 1)]);
(*"Classical" elimination rule -- does not require exhibiting B:C *)
qed_goalw "InterE" ZF.thy [Inter_def]
@@ -400,30 +411,32 @@
"b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)"
(fn _=> [ Simp_tac 1, Best_tac 1 ]);
-qed_goal "INT_I" ZF.thy
- "[| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x))"
- (fn prems=> [ blast_tac (claset() addIs prems) 1 ]);
+val prems = Goal
+ "[| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x))";
+by (blast_tac (claset() addIs prems) 1);
+qed "INT_I";
-qed_goal "INT_E" ZF.thy
- "[| b : (INT x:A. B(x)); a: A |] ==> b : B(a)"
- (fn [major,minor]=>
- [ (rtac (major RS InterD) 1),
- (rtac (minor RS RepFunI) 1) ]);
+Goal "[| b : (INT x:A. B(x)); a: A |] ==> b : B(a)";
+by (Blast_tac 1);
+qed "INT_E";
-qed_goal "INT_cong" ZF.thy
- "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A. C(x)) = (INT x:B. D(x))"
- (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
+val prems = Goal
+ "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A. C(x)) = (INT x:B. D(x))";
+by (simp_tac (simpset() addsimps prems) 1) ;
+qed "INT_cong";
(*No "Addcongs [INT_cong]" because INT is a combination of constants*)
(*** Rules for Powersets ***)
-qed_goal "PowI" ZF.thy "A <= B ==> A : Pow(B)"
- (fn [prem]=> [ (rtac (prem RS (Pow_iff RS iffD2)) 1) ]);
+Goal "A <= B ==> A : Pow(B)";
+by (etac (Pow_iff RS iffD2) 1) ;
+qed "PowI";
-qed_goal "PowD" ZF.thy "A : Pow(B) ==> A<=B"
- (fn [major]=> [ (rtac (major RS (Pow_iff RS iffD1)) 1) ]);
+Goal "A : Pow(B) ==> A<=B";
+by (etac (Pow_iff RS iffD1) 1) ;
+qed "PowD";
AddSIs [PowI];
AddSDs [PowD];
@@ -433,37 +446,41 @@
(*The set {x:0.False} is empty; by foundation it equals 0
See Suppes, page 21.*)
-qed_goal "not_mem_empty" ZF.thy "a ~: 0"
- (fn _=>
- [ (cut_facts_tac [foundation] 1),
- (best_tac (claset() addDs [equalityD2]) 1) ]);
+Goal "a ~: 0";
+by (cut_facts_tac [foundation] 1);
+by (best_tac (claset() addDs [equalityD2]) 1) ;
+qed "not_mem_empty";
bind_thm ("emptyE", not_mem_empty RS notE);
Addsimps [not_mem_empty];
AddSEs [emptyE];
-qed_goal "empty_subsetI" ZF.thy "0 <= A"
- (fn _=> [ Blast_tac 1 ]);
+Goal "0 <= A";
+by (Blast_tac 1);
+qed "empty_subsetI";
Addsimps [empty_subsetI];
-qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
- (fn prems=> [ blast_tac (claset() addDs prems) 1 ]);
+val prems = Goal "[| !!y. y:A ==> False |] ==> A=0";
+by (blast_tac (claset() addDs prems) 1) ;
+qed "equals0I";
-qed_goal "equals0D" ZF.thy "!!P. A=0 ==> a ~: A"
- (fn _=> [ Blast_tac 1 ]);
+Goal "A=0 ==> a ~: A";
+by (Blast_tac 1);
+qed "equals0D";
AddDs [equals0D, sym RS equals0D];
-qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0"
- (fn _=> [ Blast_tac 1 ]);
+Goal "a:A ==> A ~= 0";
+by (Blast_tac 1);
+qed "not_emptyI";
-qed_goal "not_emptyE" ZF.thy "[| A ~= 0; !!x. x:A ==> R |] ==> R"
- (fn [major,minor]=>
- [ rtac ([major, equals0I] MRS swap) 1,
- swap_res_tac [minor] 1,
- assume_tac 1 ]);
+val [major,minor]= Goal "[| A ~= 0; !!x. x:A ==> R |] ==> R";
+by (rtac ([major, equals0I] MRS swap) 1);
+by (swap_res_tac [minor] 1);
+by (assume_tac 1) ;
+qed "not_emptyE";
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
@@ -474,13 +491,14 @@
(*The search is undirected; similar proof attempts may fail.
b represents ANY map, such as (lam x:A.b(x)): A->Pow(A). *)
-qed_goal "cantor" ZF.thy "EX S: Pow(A). ALL x:A. b(x) ~= S"
- (fn _ => [best_tac cantor_cs 1]);
+Goal "EX S: Pow(A). ALL x:A. b(x) ~= S";
+by (best_tac cantor_cs 1);
+qed "cantor";
(*Lemma for the inductive definition in Zorn.thy*)
-qed_goal "Union_in_Pow" ZF.thy
- "!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"
- (fn _ => [Blast_tac 1]);
+Goal "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)";
+by (Blast_tac 1);
+qed "Union_in_Pow";
local
--- a/src/ZF/domrange.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/domrange.ML Wed Jun 28 12:34:08 2000 +0200
@@ -34,18 +34,21 @@
AddSIs [converseI];
AddSEs [converseD,converseE];
-qed_goal "converse_converse" thy
- "!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "r<=Sigma(A,B) ==> converse(converse(r)) = r";
+by (Blast_tac 1) ;
+qed "converse_converse";
+
+Goal "r<=A*B ==> converse(r)<=B*A";
+by (Blast_tac 1) ;
+qed "converse_type";
-qed_goal "converse_type" thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "converse(A*B) = B*A";
+by (Blast_tac 1) ;
+qed "converse_prod";
-qed_goal "converse_prod" thy "converse(A*B) = B*A"
- (fn _ => [ (Blast_tac 1) ]);
-
-qed_goal "converse_empty" thy "converse(0) = 0"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "converse(0) = 0";
+by (Blast_tac 1) ;
+qed "converse_empty";
Addsimps [converse_prod, converse_empty];
@@ -60,20 +63,22 @@
"a: domain(r) <-> (EX y. <a,y>: r)"
(fn _=> [ (Blast_tac 1) ]);
-qed_goal "domainI" thy "!!a b r. <a,b>: r ==> a: domain(r)"
- (fn _=> [ (etac (exI RS (domain_iff RS iffD2)) 1) ]);
+Goal "<a,b>: r ==> a: domain(r)";
+by (etac (exI RS (domain_iff RS iffD2)) 1) ;
+qed "domainI";
-qed_goal "domainE" thy
- "[| a : domain(r); !!y. <a,y>: r ==> P |] ==> P"
- (fn prems=>
- [ (rtac (domain_iff RS iffD1 RS exE) 1),
- (REPEAT (ares_tac prems 1)) ]);
+val prems= Goal
+ "[| a : domain(r); !!y. <a,y>: r ==> P |] ==> P";
+by (rtac (domain_iff RS iffD1 RS exE) 1);
+by (REPEAT (ares_tac prems 1)) ;
+qed "domainE";
AddIs [domainI];
AddSEs [domainE];
-qed_goal "domain_subset" thy "domain(Sigma(A,B)) <= A"
- (fn _=> [ (Blast_tac 1) ]);
+Goal "domain(Sigma(A,B)) <= A";
+by (Blast_tac 1) ;
+qed "domain_subset";
(*** range ***)
@@ -119,8 +124,9 @@
AddIs [fieldCI];
AddSEs [fieldE];
-qed_goal "field_subset" thy "field(A*B) <= A Un B"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "field(A*B) <= A Un B";
+by (Blast_tac 1) ;
+qed "field_subset";
qed_goalw "domain_subset_field" thy [field_def]
"domain(r) <= field(r)"
@@ -130,23 +136,25 @@
"range(r) <= field(r)"
(fn _ => [ (rtac Un_upper2 1) ]);
-qed_goal "domain_times_range" thy
- "!!A B r. r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "r <= Sigma(A,B) ==> r <= domain(r)*range(r)";
+by (Blast_tac 1) ;
+qed "domain_times_range";
-qed_goal "field_times_field" thy
- "!!A B r. r <= Sigma(A,B) ==> r <= field(r)*field(r)"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "r <= Sigma(A,B) ==> r <= field(r)*field(r)";
+by (Blast_tac 1) ;
+qed "field_times_field";
(*** Image of a set under a function/relation ***)
-qed_goalw "image_iff" thy [image_def] "b : r``A <-> (EX x:A. <x,b>:r)"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [image_def] "b : r``A <-> (EX x:A. <x,b>:r)";
+by (Blast_tac 1);
+qed "image_iff";
-qed_goal "image_singleton_iff" thy "b : r``{a} <-> <a,b>:r"
- (fn _ => [ rtac (image_iff RS iff_trans) 1,
- Blast_tac 1 ]);
+Goal "b : r``{a} <-> <a,b>:r";
+by (rtac (image_iff RS iff_trans) 1);
+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"
@@ -161,8 +169,9 @@
AddIs [imageI];
AddSEs [imageE];
-qed_goal "image_subset" thy "!!A B r. r <= A*B ==> r``C <= B"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "r <= A*B ==> r``C <= B";
+by (Blast_tac 1) ;
+qed "image_subset";
(*** Inverse image of a set under a function/relation ***)
@@ -171,10 +180,10 @@
"a : r-``B <-> (EX y:B. <a,y>:r)"
(fn _ => [ (Blast_tac 1) ]);
-qed_goal "vimage_singleton_iff" thy
- "a : r-``{b} <-> <a,b>:r"
- (fn _ => [ rtac (vimage_iff RS iff_trans) 1,
- Blast_tac 1 ]);
+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"
@@ -205,10 +214,9 @@
qed "rel_Union";
(** The Union of 2 relations is a relation (Lemma for fun_Un) **)
-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 "[| r <= A*B; s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)";
+by (Blast_tac 1) ;
+qed "rel_Un";
Goal "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
by (Blast_tac 1);
--- a/src/ZF/equalities.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/equalities.ML Wed Jun 28 12:34:08 2000 +0200
@@ -348,12 +348,13 @@
by (Blast_tac 1);
qed "domain_of_prod";
-qed_goal "domain_0" thy "domain(0) = 0"
- (fn _ => [ Blast_tac 1 ]);
+Goal "domain(0) = 0";
+by (Blast_tac 1);
+qed "domain_0";
-qed_goal "domain_cons" thy
- "domain(cons(<a,b>,r)) = cons(a, domain(r))"
- (fn _ => [ Blast_tac 1 ]);
+Goal "domain(cons(<a,b>,r)) = cons(a, domain(r))";
+by (Blast_tac 1);
+qed "domain_cons";
Goal "domain(A Un B) = domain(A) Un domain(B)";
by (Blast_tac 1);
@@ -380,12 +381,13 @@
by (Blast_tac 1);
qed "range_of_prod";
-qed_goal "range_0" thy "range(0) = 0"
- (fn _ => [ Blast_tac 1 ]);
+Goal "range(0) = 0";
+by (Blast_tac 1);
+qed "range_0";
-qed_goal "range_cons" thy
- "range(cons(<a,b>,r)) = cons(b, range(r))"
- (fn _ => [ Blast_tac 1 ]);
+Goal "range(cons(<a,b>,r)) = cons(b, range(r))";
+by (Blast_tac 1);
+qed "range_cons";
Goal "range(A Un B) = range(A) Un range(B)";
by (Blast_tac 1);
@@ -408,15 +410,18 @@
(** Field **)
-qed_goal "field_of_prod" thy "field(A*A) = A"
- (fn _ => [ Blast_tac 1 ]);
+Goal "field(A*A) = A";
+by (Blast_tac 1);
+qed "field_of_prod";
-qed_goal "field_0" thy "field(0) = 0"
- (fn _ => [ Blast_tac 1 ]);
+Goal "field(0) = 0";
+by (Blast_tac 1);
+qed "field_0";
-qed_goal "field_cons" thy
- "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
- (fn _ => [ rtac equalityI 1, ALLGOALS (Blast_tac) ]);
+Goal "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))";
+by (rtac equalityI 1);
+by (ALLGOALS Blast_tac) ;
+qed "field_cons";
Goal "field(A Un B) = field(A) Un field(B)";
by (Blast_tac 1);
--- a/src/ZF/pair.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/pair.ML Wed Jun 28 12:34:08 2000 +0200
@@ -8,15 +8,15 @@
(** Lemmas for showing that <a,b> uniquely determines a and b **)
-qed_goal "singleton_eq_iff" thy
- "{a} = {b} <-> a=b"
- (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
- (Blast_tac 1) ]);
+Goal "{a} = {b} <-> a=b";
+by (resolve_tac [extension RS iff_trans] 1);
+by (Blast_tac 1) ;
+qed "singleton_eq_iff";
-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) ]);
+Goal "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)";
+by (resolve_tac [extension RS iff_trans] 1);
+by (Blast_tac 1) ;
+qed "doubleton_eq_iff";
qed_goalw "Pair_iff" thy [Pair_def]
"<a,b> = <c,d> <-> a=c & b=d"
@@ -60,9 +60,10 @@
Addsimps [Sigma_iff];
-qed_goal "SigmaI" thy
- "!!a b. [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)"
- (fn _ => [ Asm_simp_tac 1 ]);
+Goal "[| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)";
+by (Asm_simp_tac 1);
+qed "SigmaI";
+
AddTCs [SigmaI];
bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1);
@@ -77,14 +78,14 @@
[ (cut_facts_tac [major] 1),
(REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
-qed_goal "SigmaE2" thy
+val [major,minor]= Goal
"[| <a,b> : Sigma(A,B); \
\ [| a:A; b:B(a) |] ==> P \
-\ |] ==> P"
- (fn [major,minor]=>
- [ (rtac minor 1),
- (rtac (major RS SigmaD1) 1),
- (rtac (major RS SigmaD2) 1) ]);
+\ |] ==> P";
+by (rtac minor 1);
+by (rtac (major RS SigmaD1) 1);
+by (rtac (major RS SigmaD2) 1) ;
+qed "SigmaE2";
qed_goalw "Sigma_cong" thy [Sigma_def]
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
@@ -99,11 +100,13 @@
AddSIs [SigmaI];
AddSEs [SigmaE2, SigmaE];
-qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "Sigma(0,B) = 0";
+by (Blast_tac 1) ;
+qed "Sigma_empty1";
-qed_goal "Sigma_empty2" thy "A*0 = 0"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "A*0 = 0";
+by (Blast_tac 1) ;
+qed "Sigma_empty2";
Addsimps [Sigma_empty1, Sigma_empty2];
@@ -122,15 +125,17 @@
Addsimps [fst_conv,snd_conv];
-qed_goal "fst_type" thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
- (fn _=> [ Auto_tac ]);
+Goal "p:Sigma(A,B) ==> fst(p) : A";
+by (Auto_tac) ;
+qed "fst_type";
-qed_goal "snd_type" thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
- (fn _=> [ Auto_tac ]);
+Goal "p:Sigma(A,B) ==> snd(p) : B(fst(p))";
+by (Auto_tac) ;
+qed "snd_type";
-qed_goal "Pair_fst_snd_eq" thy
- "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
- (fn _=> [ Auto_tac ]);
+Goal "a: Sigma(A,B) ==> <fst(a),snd(a)> = a";
+by (Auto_tac) ;
+qed "Pair_fst_snd_eq";
(*** Eliminator - split ***)
@@ -141,13 +146,13 @@
qed "split";
Addsimps [split];
-qed_goal "split_type" thy
+val major::prems= Goal
"[| 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)"
- (fn major::prems=>
- [ (rtac (major RS SigmaE) 1),
- (asm_simp_tac (simpset() addsimps prems) 1) ]);
+\ |] ==> split(%x y. c(x,y), p) : C(p)";
+by (rtac (major RS SigmaE) 1);
+by (asm_simp_tac (simpset() addsimps prems) 1);
+qed "split_type";
AddTCs [split_type];
Goalw [split_def]
--- a/src/ZF/subset.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/subset.ML Wed Jun 28 12:34:08 2000 +0200
@@ -9,30 +9,35 @@
(*** cons ***)
-qed_goal "cons_subsetI" thy "!!a. [| a:C; B<=C |] ==> cons(a,B) <= C"
- (fn _ => [ Blast_tac 1 ]);
+Goal "[| a:C; B<=C |] ==> cons(a,B) <= C";
+by (Blast_tac 1);
+qed "cons_subsetI";
-qed_goal "subset_consI" thy "B <= cons(a,B)"
- (fn _ => [ Blast_tac 1 ]);
+Goal "B <= cons(a,B)";
+by (Blast_tac 1);
+qed "subset_consI";
-qed_goal "cons_subset_iff" thy "cons(a,B)<=C <-> a:C & B<=C"
- (fn _ => [ Blast_tac 1 ]);
+Goal "cons(a,B)<=C <-> a:C & B<=C";
+by (Blast_tac 1);
+qed "cons_subset_iff";
(*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" thy "A<=0 <-> A=0"
- (fn _=> [ (Blast_tac 1) ]);
+Goal "A<=0 <-> A=0";
+by (Blast_tac 1) ;
+qed "subset_empty_iff";
-qed_goal "subset_cons_iff" thy
- "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
- (fn _=> [ (Blast_tac 1) ]);
+Goal "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)";
+by (Blast_tac 1) ;
+qed "subset_cons_iff";
(*** succ ***)
-qed_goal "subset_succI" thy "i <= succ(i)"
- (fn _=> [ (Blast_tac 1) ]);
+Goal "i <= succ(i)";
+by (Blast_tac 1) ;
+qed "subset_succI";
(*But if j is an ordinal or is transitive, then i:j implies i<=j!
See ordinal/Ord_succ_subsetI*)
@@ -49,26 +54,29 @@
(*** singletons ***)
-qed_goal "singleton_subsetI" thy "!!a c. a:C ==> {a} <= C"
- (fn _=> [ (Blast_tac 1) ]);
+Goal "a:C ==> {a} <= C";
+by (Blast_tac 1) ;
+qed "singleton_subsetI";
-qed_goal "singleton_subsetD" thy "!!a C. {a} <= C ==> a:C"
- (fn _=> [ (Blast_tac 1) ]);
+Goal "{a} <= C ==> a:C";
+by (Blast_tac 1) ;
+qed "singleton_subsetD";
(*** Big Union -- least upper bound of a set ***)
-qed_goal "Union_subset_iff" thy "Union(A) <= C <-> (ALL x:A. x <= C)"
- (fn _ => [ Blast_tac 1 ]);
+Goal "Union(A) <= C <-> (ALL x:A. x <= C)";
+by (Blast_tac 1);
+qed "Union_subset_iff";
-qed_goal "Union_upper" thy
- "!!B A. B:A ==> B <= Union(A)"
- (fn _ => [ Blast_tac 1 ]);
+Goal "B:A ==> B <= Union(A)";
+by (Blast_tac 1);
+qed "Union_upper";
-qed_goal "Union_least" thy
- "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"
- (fn [prem]=>
- [ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1),
- (etac prem 1) ]);
+val [prem]= Goal
+ "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C";
+by (rtac (ballI RS (Union_subset_iff RS iffD2)) 1);
+by (etac prem 1) ;
+qed "Union_least";
(*** Union of a family of sets ***)
@@ -76,87 +84,97 @@
by (blast_tac (claset() addSEs [equalityE]) 1);
qed "subset_UN_iff_eq";
-qed_goal "UN_subset_iff" thy
- "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"
- (fn _ => [ Blast_tac 1 ]);
+Goal "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)";
+by (Blast_tac 1);
+qed "UN_subset_iff";
-qed_goal "UN_upper" thy
- "!!x A. x:A ==> B(x) <= (UN x:A. B(x))"
- (fn _ => [ etac (RepFunI RS Union_upper) 1 ]);
+Goal "x:A ==> B(x) <= (UN x:A. B(x))";
+by (etac (RepFunI RS Union_upper) 1);
+qed "UN_upper";
-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),
- (etac prem 1) ]);
+val [prem]= Goal
+ "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
+by (rtac (ballI RS (UN_subset_iff RS iffD2)) 1);
+by (etac prem 1) ;
+qed "UN_least";
(*** Big Intersection -- greatest lower bound of a nonempty set ***)
-qed_goal "Inter_subset_iff" thy
- "!!a A. a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)"
- (fn _ => [ Blast_tac 1 ]);
+Goal "a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)";
+by (Blast_tac 1);
+qed "Inter_subset_iff";
-qed_goal "Inter_lower" thy "!!B A. B:A ==> Inter(A) <= B"
- (fn _ => [ Blast_tac 1 ]);
+Goal "B:A ==> Inter(A) <= B";
+by (Blast_tac 1);
+qed "Inter_lower";
-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),
- (etac prem2 1) ]);
+val [prem1,prem2]= Goal
+ "[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)";
+by (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1);
+by (etac prem2 1) ;
+qed "Inter_greatest";
(*** Intersection of a family of sets ***)
-qed_goal "INT_lower" thy
- "!!x. x:A ==> (INT x:A. B(x)) <= B(x)"
- (fn _ => [ Blast_tac 1 ]);
+Goal "x:A ==> (INT x:A. B(x)) <= B(x)";
+by (Blast_tac 1);
+qed "INT_lower";
-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,
- REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1) ]);
+val [nonempty,prem] = Goal
+ "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
+by (rtac (nonempty RS RepFunI RS Inter_greatest) 1);
+by (REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1));
+qed "INT_greatest";
(*** Finite Union -- the least upper bound of 2 sets ***)
-qed_goal "Un_subset_iff" thy "A Un B <= C <-> A <= C & B <= C"
- (fn _ => [ Blast_tac 1 ]);
+Goal "A Un B <= C <-> A <= C & B <= C";
+by (Blast_tac 1);
+qed "Un_subset_iff";
-qed_goal "Un_upper1" thy "A <= A Un B"
- (fn _ => [ Blast_tac 1 ]);
+Goal "A <= A Un B";
+by (Blast_tac 1);
+qed "Un_upper1";
-qed_goal "Un_upper2" thy "B <= A Un B"
- (fn _ => [ Blast_tac 1 ]);
+Goal "B <= A Un B";
+by (Blast_tac 1);
+qed "Un_upper2";
-qed_goal "Un_least" thy "!!A B C. [| A<=C; B<=C |] ==> A Un B <= C"
- (fn _ => [ Blast_tac 1 ]);
+Goal "[| A<=C; B<=C |] ==> A Un B <= C";
+by (Blast_tac 1);
+qed "Un_least";
(*** Finite Intersection -- the greatest lower bound of 2 sets *)
-qed_goal "Int_subset_iff" thy "C <= A Int B <-> C <= A & C <= B"
- (fn _ => [ Blast_tac 1 ]);
+Goal "C <= A Int B <-> C <= A & C <= B";
+by (Blast_tac 1);
+qed "Int_subset_iff";
-qed_goal "Int_lower1" thy "A Int B <= A"
- (fn _ => [ Blast_tac 1 ]);
+Goal "A Int B <= A";
+by (Blast_tac 1);
+qed "Int_lower1";
-qed_goal "Int_lower2" thy "A Int B <= B"
- (fn _ => [ Blast_tac 1 ]);
+Goal "A Int B <= B";
+by (Blast_tac 1);
+qed "Int_lower2";
-qed_goal "Int_greatest" thy "!!A B C. [| C<=A; C<=B |] ==> C <= A Int B"
- (fn _ => [ Blast_tac 1 ]);
+Goal "[| C<=A; C<=B |] ==> C <= A Int B";
+by (Blast_tac 1);
+qed "Int_greatest";
(*** Set difference *)
-qed_goal "Diff_subset" thy "A-B <= A"
- (fn _ => [ Blast_tac 1 ]);
+Goal "A-B <= A";
+by (Blast_tac 1);
+qed "Diff_subset";
-qed_goal "Diff_contains" thy
- "!!C. [| C<=A; C Int B = 0 |] ==> C <= A-B"
- (fn _ => [ Blast_tac 1 ]);
+Goal "[| C<=A; C Int B = 0 |] ==> C <= A-B";
+by (Blast_tac 1);
+qed "Diff_contains";
Goal "B <= A - cons(c,C) <-> B<=A-C & c ~: B";
by (Blast_tac 1);
@@ -166,8 +184,9 @@
(** Collect **)
-qed_goal "Collect_subset" thy "Collect(A,P) <= A"
- (fn _ => [ Blast_tac 1 ]);
+Goal "Collect(A,P) <= A";
+by (Blast_tac 1);
+qed "Collect_subset";
(** RepFun **)
--- a/src/ZF/upair.ML Wed Jun 28 12:16:36 2000 +0200
+++ b/src/ZF/upair.ML Wed Jun 28 12:34:08 2000 +0200
@@ -26,17 +26,19 @@
Addsimps [Upair_iff];
-qed_goal "UpairI1" thy "a : Upair(a,b)"
- (fn _ => [ Simp_tac 1 ]);
-
-qed_goal "UpairI2" thy "b : Upair(a,b)"
- (fn _ => [ Simp_tac 1 ]);
+Goal "a : Upair(a,b)";
+by (Simp_tac 1);
+qed "UpairI1";
-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),
- (REPEAT (eresolve_tac prems 1)) ]);
+Goal "b : Upair(a,b)";
+by (Simp_tac 1);
+qed "UpairI2";
+
+val major::prems= Goal
+ "[| a : Upair(b,c); a=b ==> P; a=c ==> P |] ==> P";
+by (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1);
+by (REPEAT (eresolve_tac prems 1)) ;
+qed "UpairE";
AddSIs [UpairI1,UpairI2];
AddSEs [UpairE];
@@ -44,37 +46,40 @@
(*** 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 ]);
+ (fn _ => [(Blast_tac 1)]);
Addsimps [Un_iff];
-qed_goal "UnI1" thy "!!c. c : A ==> c : A Un B"
- (fn _ => [ Asm_simp_tac 1 ]);
-
-qed_goal "UnI2" thy "!!c. c : B ==> c : A Un B"
- (fn _ => [ Asm_simp_tac 1 ]);
+Goal "c : A ==> c : A Un B";
+by (Asm_simp_tac 1);
+qed "UnI1";
-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)) ]);
+Goal "c : B ==> c : A Un B";
+by (Asm_simp_tac 1);
+qed "UnI2";
+
+val major::prems= Goal
+ "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P";
+by (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1);
+by (REPEAT (eresolve_tac prems 1)) ;
+qed "UnE";
(*Stronger version of the rule above*)
-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),
- (eresolve_tac prems 1),
- (rtac classical 1),
- (eresolve_tac prems 1),
- (swap_res_tac prems 1),
- (etac notnotD 1)]);
+val major::prems = Goal
+ "[| c : A Un B; c:A ==> P; [| c:B; c~:A |] ==> P |] ==> P";
+by (rtac (major RS UnE) 1);
+by (eresolve_tac prems 1);
+by (rtac classical 1);
+by (eresolve_tac prems 1);
+by (swap_res_tac prems 1);
+by (etac notnotD 1);
+qed "UnE'";
(*Classical introduction rule: no commitment to A vs B*)
-qed_goal "UnCI" thy "(c ~: B ==> c : A) ==> c : A Un B"
- (fn prems=>
- [ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
+val prems = Goal "(c ~: B ==> c : A) ==> c : A Un B";
+by (Simp_tac 1);
+by (blast_tac (claset() addSIs prems) 1);
+qed "UnCI";
AddSIs [UnCI];
AddSEs [UnE];
@@ -83,24 +88,26 @@
(*** 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 ]);
+ (fn _ => [(Blast_tac 1)]);
Addsimps [Int_iff];
-qed_goal "IntI" thy "!!c. [| c : A; c : B |] ==> c : A Int B"
- (fn _ => [ Asm_simp_tac 1 ]);
+Goal "[| c : A; c : B |] ==> c : A Int B";
+by (Asm_simp_tac 1);
+qed "IntI";
-qed_goal "IntD1" thy "!!c. c : A Int B ==> c : A"
- (fn _ => [ Asm_full_simp_tac 1 ]);
+Goal "c : A Int B ==> c : A";
+by (Asm_full_simp_tac 1);
+qed "IntD1";
-qed_goal "IntD2" thy "!!c. c : A Int B ==> c : B"
- (fn _ => [ Asm_full_simp_tac 1 ]);
+Goal "c : A Int B ==> c : B";
+by (Asm_full_simp_tac 1);
+qed "IntD2";
-qed_goal "IntE" thy
- "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"
- (fn prems=>
- [ (resolve_tac prems 1),
- (REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ]);
+val prems = Goal "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P";
+by (resolve_tac prems 1);
+by (REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ;
+qed "IntE";
AddSIs [IntI];
AddSEs [IntE];
@@ -108,24 +115,26 @@
(*** 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 ]);
+ (fn _ => [(Blast_tac 1)]);
Addsimps [Diff_iff];
-qed_goal "DiffI" thy "!!c. [| c : A; c ~: B |] ==> c : A - B"
- (fn _ => [ Asm_simp_tac 1 ]);
+Goal "[| c : A; c ~: B |] ==> c : A - B";
+by (Asm_simp_tac 1);
+qed "DiffI";
-qed_goal "DiffD1" thy "!!c. c : A - B ==> c : A"
- (fn _ => [ Asm_full_simp_tac 1 ]);
+Goal "c : A - B ==> c : A";
+by (Asm_full_simp_tac 1);
+qed "DiffD1";
-qed_goal "DiffD2" thy "!!c. c : A - B ==> c ~: B"
- (fn _ => [ Asm_full_simp_tac 1 ]);
+Goal "c : A - B ==> c ~: B";
+by (Asm_full_simp_tac 1);
+qed "DiffD2";
-qed_goal "DiffE" thy
- "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P"
- (fn prems=>
- [ (resolve_tac prems 1),
- (REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ]);
+val prems = Goal "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P";
+by (resolve_tac prems 1);
+by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ;
+qed "DiffE";
AddSIs [DiffI];
AddSEs [DiffE];
@@ -133,47 +142,51 @@
(*** 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 ]);
+ (fn _ => [(Blast_tac 1)]);
Addsimps [cons_iff];
-qed_goal "consI1" thy "a : cons(a,B)"
- (fn _ => [ Simp_tac 1 ]);
+Goal "a : cons(a,B)";
+by (Simp_tac 1);
+qed "consI1";
Addsimps [consI1];
AddTCs [consI1]; (*risky as a typechecking rule, but solves otherwise
unconstrained goals of the form x : ?A*)
-qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)"
- (fn _ => [ Asm_simp_tac 1 ]);
+Goal "a : B ==> a : cons(b,B)";
+by (Asm_simp_tac 1);
+qed "consI2";
-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)) ]);
+val major::prems= Goal
+ "[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P";
+by (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1);
+by (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ;
+qed "consE";
(*Stronger version of the rule above*)
-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),
- (eresolve_tac prems 1),
- (rtac classical 1),
- (eresolve_tac prems 1),
- (swap_res_tac prems 1),
- (etac notnotD 1)]);
+val major::prems = Goal
+ "[| a : cons(b,A); a=b ==> P; [| a:A; a~=b |] ==> P |] ==> P";
+by (rtac (major RS consE) 1);
+by (eresolve_tac prems 1);
+by (rtac classical 1);
+by (eresolve_tac prems 1);
+by (swap_res_tac prems 1);
+by (etac notnotD 1);
+qed "consE'";
(*Classical introduction rule*)
-qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)"
- (fn prems=>
- [ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
+val prems = Goal "(a~:B ==> a=b) ==> a: cons(b,B)";
+by (Simp_tac 1);
+by (blast_tac (claset() addSIs prems) 1);
+qed "consCI";
AddSIs [consCI];
AddSEs [consE];
-qed_goal "cons_not_0" thy "cons(a,B) ~= 0"
- (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
+Goal "cons(a,B) ~= 0";
+by (blast_tac (claset() addEs [equalityE]) 1) ;
+qed "cons_not_0";
bind_thm ("cons_neq_0", cons_not_0 RS notE);
@@ -182,11 +195,13 @@
(*** Singletons - using cons ***)
-qed_goal "singleton_iff" thy "a : {b} <-> a=b"
- (fn _ => [ Simp_tac 1 ]);
+Goal "a : {b} <-> a=b";
+by (Simp_tac 1);
+qed "singleton_iff";
-qed_goal "singletonI" thy "a : {a}"
- (fn _=> [ (rtac consI1 1) ]);
+Goal "a : {a}";
+by (rtac consI1 1) ;
+qed "singletonI";
bind_thm ("singletonE", make_elim (singleton_iff RS iffD1));
@@ -217,7 +232,7 @@
(THE x.P(x)) rewrites to (THE x. Q(x)) *)
(*If it's "undefined", it's zero!*)
-Goalw [the_def] "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0";
+Goalw [the_def] "~ (EX! x. P(x)) ==> (THE x. P(x))=0";
by (blast_tac (claset() addSEs [ReplaceE]) 1);
qed "the_0";
@@ -262,11 +277,11 @@
Addsimps [if_true, if_false];
-qed_goal "split_if" thy
- "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
- (fn _=> [ (case_tac "Q" 1),
- (Asm_simp_tac 1),
- (Asm_simp_tac 1) ]);
+Goal "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))";
+by (case_tac "Q" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1) ;
+qed "split_if";
(** Rewrite rules for boolean case-splitting: faster than
addsplits[split_if]
@@ -282,42 +297,48 @@
split_if_mem1, split_if_mem2];
(*Logically equivalent to split_if_mem2*)
-qed_goal "if_iff" thy "a: (if P then x else y) <-> P & a:x | ~P & a:y"
- (fn _=> [ (simp_tac (simpset() addsplits [split_if]) 1) ]);
+Goal "a: (if P then x else y) <-> P & a:x | ~P & a:y";
+by (simp_tac (simpset() addsplits [split_if]) 1) ;
+qed "if_iff";
-qed_goal "if_type" thy
- "[| P ==> a: A; ~P ==> b: A |] ==> (if P then a else b): A"
- (fn prems=> [ (simp_tac
- (simpset() addsimps prems addsplits [split_if]) 1) ]);
+val prems = Goal
+ "[| P ==> a: A; ~P ==> b: A |] ==> (if P then a else b): A";
+by (simp_tac (simpset() addsimps prems addsplits [split_if]) 1) ;
+qed "if_type";
+
AddTCs [if_type];
(*** Foundation lemmas ***)
(*was called mem_anti_sym*)
-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) ]);
+val prems = Goal "[| a:b; ~P ==> b:a |] ==> P";
+by (rtac classical 1);
+by (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1);
+by (REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1));
+qed "mem_asym";
(*was called mem_anti_refl*)
-qed_goal "mem_irrefl" thy "a:a ==> P"
- (fn [major]=> [ (rtac ([major,major] MRS mem_asym) 1) ]);
+Goal "a:a ==> P";
+by (blast_tac (claset() addIs [mem_asym]) 1);
+qed "mem_irrefl";
(*mem_irrefl should NOT be added to default databases:
it would be tried on most goals, making proofs slower!*)
-qed_goal "mem_not_refl" thy "a ~: a"
- (K [ (rtac notI 1), (etac mem_irrefl 1) ]);
+Goal "a ~: a";
+by (rtac notI 1);
+by (etac mem_irrefl 1);
+qed "mem_not_refl";
(*Good for proving inequalities by rewriting*)
-qed_goal "mem_imp_not_eq" thy "!!a A. a:A ==> a ~= A"
- (fn _=> [ blast_tac (claset() addSEs [mem_irrefl]) 1 ]);
+Goal "a:A ==> a ~= A";
+by (blast_tac (claset() addSEs [mem_irrefl]) 1);
+qed "mem_imp_not_eq";
(*** Rules for succ ***)
qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j"
- (fn _ => [ Blast_tac 1 ]);
+ (fn _ => [(Blast_tac 1)]);
qed_goalw "succI1" thy [succ_def] "i : succ(i)"
(fn _=> [ (rtac consI1 1) ]);
@@ -335,16 +356,17 @@
(REPEAT (eresolve_tac prems 1)) ]);
(*Classical introduction rule*)
-qed_goal "succCI" thy "(i~:j ==> i=j) ==> i: succ(j)"
- (fn [prem]=>
- [ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
- (etac prem 1) ]);
+val [prem]= Goal "(i~:j ==> i=j) ==> i: succ(j)";
+by (rtac (disjCI RS (succ_iff RS iffD2)) 1);
+by (etac prem 1) ;
+qed "succCI";
AddSIs [succCI];
AddSEs [succE];
-qed_goal "succ_not_0" thy "succ(n) ~= 0"
- (fn _=> [ (blast_tac (claset() addSEs [equalityE]) 1) ]);
+Goal "succ(n) ~= 0";
+by (blast_tac (claset() addSEs [equalityE]) 1) ;
+qed "succ_not_0";
bind_thm ("succ_neq_0", succ_not_0 RS notE);
@@ -358,9 +380,9 @@
(* succ(b) ~= b *)
bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
-
-qed_goal "succ_inject_iff" thy "succ(m) = succ(n) <-> m=n"
- (fn _=> [ (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ]);
+Goal "succ(m) = succ(n) <-> m=n";
+by (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ;
+qed "succ_inject_iff";
bind_thm ("succ_inject", succ_inject_iff RS iffD1);