# HG changeset patch # User paulson # Date 962188448 -7200 # Node ID 3bda56c0d70daf3634ed8e9b5eee0cf00b619e0e # Parent 44eabc57ed468e214a33f102e96fe8273c049b8f tidying and unbatchifying diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/CardinalArith.ML --- 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"; diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/Nat.ML --- 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 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); diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/OrdQuant.ML --- 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 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 Q; P(x) ==> Q |] ==> Q"; +by (rtac (major RS oallE) 1); +by (REPEAT (eresolve_tac prems 1)) ; +qed "rev_oallE"; (*Trival rewrite rule; (ALL xP holds only if a is not 0!*) -qed_goal "oall_simp" thy "(ALL x True" - (fn _=> [ (REPEAT (ares_tac [TrueI,oallI,iffI] 1)) ]); +Goal "(ALL x 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 P(a); a EX x - [ (rtac classical 1), - (REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ]); +val prems = Goal + "[| ALL x P(a); a EX x Q \ @@ -82,11 +83,11 @@ "b : (UN x (EX x [ (fast_tac (claset() addIs [OUN_I] addSEs [OUN_E]) 1) ]); -qed_goal "OUN_cong" thy - "[| i=j; !!x. x C(x)=D(x) |] ==> (UN x - [ rtac equality_iffI 1, - simp_tac (simpset() addcongs [oex_cong] addsimps OUN_iff::prems) 1 ]); +val prems = Goal + "[| i=j; !!x. x C(x)=D(x) |] ==> (UN x P(x) \ \ |] ==> P(i)"; by (rtac (major RS conjE) 1); diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/Ordinal.ML --- 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 *) bind_thm ("lt_asym", lt_not_sym RS swap); -qed_goal "lt_irrefl" Ordinal.thy "i P" - (fn [major]=> [ (rtac (major RS (major RS lt_asym)) 1) ]); +val [major]= goal Ordinal.thy "i P"; +by (rtac (major RS (major RS lt_asym)) 1) ; +qed "lt_irrefl"; -qed_goal "lt_not_refl" Ordinal.thy "~ i [ (rtac notI 1), (etac lt_irrefl 1) ]); +Goal "~ i 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] diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/QPair.ML --- 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=c" - (fn [major]=> - [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]); +val [major]= goal thy " = ==> a=c"; +by (rtac (major RS QPair_inject) 1); +by (assume_tac 1) ; +qed "QPair_inject1"; -qed_goal "QPair_inject2" thy " = ==> b=d" - (fn [major]=> - [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]); +val [major]= goal thy " = ==> 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" "" QSigmaE); -qed_goal "QSigmaD1" thy " : QSigma(A,B) ==> a : A" - (fn [major]=> - [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); +val [major]= goal thy " : QSigma(A,B) ==> a : A"; +by (rtac (major RS QSigmaE2) 1); +by (assume_tac 1) ; +qed "QSigmaD1"; -qed_goal "QSigmaD2" thy " : QSigma(A,B) ==> b : B(a)" - (fn [major]=> - [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); +val [major]= goal thy " : 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) ==> = 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() \ -\ |] ==> 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 = --> 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 ****) diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/WF.ML --- 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"; diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/ZF.ML --- 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 diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/domrange.ML --- 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. : r)" (fn _=> [ (Blast_tac 1) ]); -qed_goal "domainI" thy "!!a b r. : r ==> a: domain(r)" - (fn _=> [ (etac (exI RS (domain_iff RS iffD2)) 1) ]); +Goal ": r ==> a: domain(r)"; +by (etac (exI RS (domain_iff RS iffD2)) 1) ; +qed "domainI"; -qed_goal "domainE" thy - "[| a : domain(r); !!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. : 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. :r)" - (fn _ => [ (Blast_tac 1) ]); +Goalw [image_def] "b : r``A <-> (EX x:A. :r)"; +by (Blast_tac 1); +qed "image_iff"; -qed_goal "image_singleton_iff" thy "b : r``{a} <-> :r" - (fn _ => [ rtac (image_iff RS iff_trans) 1, - Blast_tac 1 ]); +Goal "b : r``{a} <-> :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. [| : 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. :r)" (fn _ => [ (Blast_tac 1) ]); -qed_goal "vimage_singleton_iff" thy - "a : r-``{b} <-> :r" - (fn _ => [ rtac (vimage_iff RS iff_trans) 1, - Blast_tac 1 ]); +Goal "a : r-``{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. [| : 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 "[| : r; c~=b |] ==> domain(r-{}) = domain(r)"; by (Blast_tac 1); diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/equalities.ML --- 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(,r)) = cons(a, domain(r))" - (fn _ => [ Blast_tac 1 ]); +Goal "domain(cons(,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(,r)) = cons(b, range(r))" - (fn _ => [ Blast_tac 1 ]); +Goal "range(cons(,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(,r)) = cons(a, cons(b, field(r)))" - (fn _ => [ rtac equalityI 1, ALLGOALS (Blast_tac) ]); +Goal "field(cons(,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); diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/pair.ML --- 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 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=c & b=d" @@ -60,9 +60,10 @@ Addsimps [Sigma_iff]; -qed_goal "SigmaI" thy - "!!a b. [| a:A; b:B(a) |] ==> : Sigma(A,B)" - (fn _ => [ Asm_simp_tac 1 ]); +Goal "[| a:A; b:B(a) |] ==> : 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 "[| : 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) ==> = a" - (fn _=> [ Auto_tac ]); +Goal "a: Sigma(A,B) ==> = 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() \ -\ |] ==> 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] diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/subset.ML --- 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 **) diff -r 44eabc57ed46 -r 3bda56c0d70d src/ZF/upair.ML --- 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);