--- a/src/ZF/upair.ML Wed Apr 02 15:37:35 1997 +0200
+++ b/src/ZF/upair.ML Wed Apr 02 15:39:44 1997 +0200
@@ -21,49 +21,48 @@
(*** Unordered pairs - Upair ***)
-qed_goalw "Upair_iff" thy [Upair_def]
+qed_goalw "Upair_iff" ZF.thy [Upair_def]
"c : Upair(a,b) <-> (c=a | c=b)"
- (fn _ => [ (fast_tac (!claset addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);
+ (fn _ => [ (blast_tac (!claset addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);
Addsimps [Upair_iff];
-qed_goal "UpairI1" thy "a : Upair(a,b)"
+qed_goal "UpairI1" ZF.thy "a : Upair(a,b)"
(fn _ => [ Simp_tac 1 ]);
-qed_goal "UpairI2" thy "b : Upair(a,b)"
+qed_goal "UpairI2" ZF.thy "b : Upair(a,b)"
(fn _ => [ Simp_tac 1 ]);
-qed_goal "UpairE" thy
+qed_goal "UpairE" ZF.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)) ]);
-(*UpairI1/2 should become UpairCI?*)
AddSIs [UpairI1,UpairI2];
AddSEs [UpairE];
(*** Rules for binary union -- Un -- defined via Upair ***)
-qed_goalw "Un_iff" thy [Un_def] "c : A Un B <-> (c:A | c:B)"
- (fn _ => [ Fast_tac 1 ]);
+qed_goalw "Un_iff" ZF.thy [Un_def] "c : A Un B <-> (c:A | c:B)"
+ (fn _ => [ Blast_tac 1 ]);
Addsimps [Un_iff];
-qed_goal "UnI1" thy "!!c. c : A ==> c : A Un B"
+qed_goal "UnI1" ZF.thy "!!c. c : A ==> c : A Un B"
(fn _ => [ Asm_simp_tac 1 ]);
-qed_goal "UnI2" thy "!!c. c : B ==> c : A Un B"
+qed_goal "UnI2" ZF.thy "!!c. c : B ==> c : A Un B"
(fn _ => [ Asm_simp_tac 1 ]);
-qed_goal "UnE" thy
+qed_goal "UnE" ZF.thy
"[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1),
(REPEAT (eresolve_tac prems 1)) ]);
(*Stronger version of the rule above*)
-qed_goal "UnE'" thy
+qed_goal "UnE'" ZF.thy
"[| c : A Un B; c:A ==> P; [| c:B; c~:A |] ==> P |] ==> P"
(fn major::prems =>
[(rtac (major RS UnE) 1),
@@ -74,9 +73,9 @@
(etac notnotD 1)]);
(*Classical introduction rule: no commitment to A vs B*)
-qed_goal "UnCI" thy "(c ~: B ==> c : A) ==> c : A Un B"
+qed_goal "UnCI" ZF.thy "(c ~: B ==> c : A) ==> c : A Un B"
(fn prems=>
- [ Simp_tac 1, fast_tac (!claset addSIs prems) 1 ]);
+ [ Simp_tac 1, blast_tac (!claset addSIs prems) 1 ]);
AddSIs [UnCI];
AddSEs [UnE];
@@ -84,21 +83,21 @@
(*** Rules for small intersection -- Int -- defined via Upair ***)
-qed_goalw "Int_iff" thy [Int_def] "c : A Int B <-> (c:A & c:B)"
- (fn _ => [ Fast_tac 1 ]);
+qed_goalw "Int_iff" ZF.thy [Int_def] "c : A Int B <-> (c:A & c:B)"
+ (fn _ => [ Blast_tac 1 ]);
Addsimps [Int_iff];
-qed_goal "IntI" thy "!!c. [| c : A; c : B |] ==> c : A Int B"
+qed_goal "IntI" ZF.thy "!!c. [| c : A; c : B |] ==> c : A Int B"
(fn _ => [ Asm_simp_tac 1 ]);
-qed_goal "IntD1" thy "!!c. c : A Int B ==> c : A"
+qed_goal "IntD1" ZF.thy "!!c. c : A Int B ==> c : A"
(fn _ => [ Asm_full_simp_tac 1 ]);
-qed_goal "IntD2" thy "!!c. c : A Int B ==> c : B"
+qed_goal "IntD2" ZF.thy "!!c. c : A Int B ==> c : B"
(fn _ => [ Asm_full_simp_tac 1 ]);
-qed_goal "IntE" thy
+qed_goal "IntE" ZF.thy
"[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"
(fn prems=>
[ (resolve_tac prems 1),
@@ -109,21 +108,21 @@
(*** Rules for set difference -- defined via Upair ***)
-qed_goalw "Diff_iff" thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
- (fn _ => [ Fast_tac 1 ]);
+qed_goalw "Diff_iff" ZF.thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
+ (fn _ => [ Blast_tac 1 ]);
Addsimps [Diff_iff];
-qed_goal "DiffI" thy "!!c. [| c : A; c ~: B |] ==> c : A - B"
+qed_goal "DiffI" ZF.thy "!!c. [| c : A; c ~: B |] ==> c : A - B"
(fn _ => [ Asm_simp_tac 1 ]);
-qed_goal "DiffD1" thy "!!c. c : A - B ==> c : A"
+qed_goal "DiffD1" ZF.thy "!!c. c : A - B ==> c : A"
(fn _ => [ Asm_full_simp_tac 1 ]);
-qed_goal "DiffD2" thy "!!c. c : A - B ==> c ~: B"
+qed_goal "DiffD2" ZF.thy "!!c. c : A - B ==> c ~: B"
(fn _ => [ Asm_full_simp_tac 1 ]);
-qed_goal "DiffE" thy
+qed_goal "DiffE" ZF.thy
"[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P"
(fn prems=>
[ (resolve_tac prems 1),
@@ -134,27 +133,27 @@
(*** Rules for cons -- defined via Un and Upair ***)
-qed_goalw "cons_iff" thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
- (fn _ => [ Fast_tac 1 ]);
+qed_goalw "cons_iff" ZF.thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
+ (fn _ => [ Blast_tac 1 ]);
Addsimps [cons_iff];
-qed_goal "consI1" thy "a : cons(a,B)"
+qed_goal "consI1" ZF.thy "a : cons(a,B)"
(fn _ => [ Simp_tac 1 ]);
Addsimps [consI1];
-qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)"
+qed_goal "consI2" ZF.thy "!!B. a : B ==> a : cons(b,B)"
(fn _ => [ Asm_simp_tac 1 ]);
-qed_goal "consE" thy
+qed_goal "consE" ZF.thy
"[| a : cons(b,A); a=b ==> P; a:A ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1),
(REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);
(*Stronger version of the rule above*)
-qed_goal "consE'" thy
+qed_goal "consE'" ZF.thy
"[| a : cons(b,A); a=b ==> P; [| a:A; a~=b |] ==> P |] ==> P"
(fn major::prems =>
[(rtac (major RS consE) 1),
@@ -165,15 +164,15 @@
(etac notnotD 1)]);
(*Classical introduction rule*)
-qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)"
+qed_goal "consCI" ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)"
(fn prems=>
- [ Simp_tac 1, fast_tac (!claset addSIs prems) 1 ]);
+ [ Simp_tac 1, blast_tac (!claset addSIs prems) 1 ]);
AddSIs [consCI];
AddSEs [consE];
-qed_goal "cons_not_0" thy "cons(a,B) ~= 0"
- (fn _ => [ (fast_tac (!claset addEs [equalityE]) 1) ]);
+qed_goal "cons_not_0" ZF.thy "cons(a,B) ~= 0"
+ (fn _ => [ (blast_tac (!claset addEs [equalityE]) 1) ]);
bind_thm ("cons_neq_0", cons_not_0 RS notE);
@@ -182,10 +181,10 @@
(*** Singletons - using cons ***)
-qed_goal "singleton_iff" thy "a : {b} <-> a=b"
+qed_goal "singleton_iff" ZF.thy "a : {b} <-> a=b"
(fn _ => [ Simp_tac 1 ]);
-qed_goal "singletonI" thy "a : {a}"
+qed_goal "singletonI" ZF.thy "a : {a}"
(fn _=> [ (rtac consI1 1) ]);
bind_thm ("singletonE", make_elim (singleton_iff RS iffD1));
@@ -195,25 +194,25 @@
(*** Rules for Descriptions ***)
-qed_goalw "the_equality" thy [the_def]
+qed_goalw "the_equality" ZF.thy [the_def]
"[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
(fn [pa,eq] =>
[ (fast_tac (!claset addSIs [pa] addEs [eq RS subst]) 1) ]);
(* Only use this if you already know EX!x. P(x) *)
-qed_goal "the_equality2" thy
+qed_goal "the_equality2" ZF.thy
"!!P. [| EX! x. P(x); P(a) |] ==> (THE x. P(x)) = a"
(fn _ =>
[ (deepen_tac (!claset addSIs [the_equality]) 1 1) ]);
-qed_goal "theI" thy "EX! x. P(x) ==> P(THE x. P(x))"
+qed_goal "theI" ZF.thy "EX! x. P(x) ==> P(THE x. P(x))"
(fn [major]=>
[ (rtac (major RS ex1E) 1),
(resolve_tac [major RS the_equality2 RS ssubst] 1),
(REPEAT (assume_tac 1)) ]);
(*Easier to apply than theI: conclusion has only one occurrence of P*)
-qed_goal "theI2" thy
+qed_goal "theI2" ZF.thy
"[| EX! x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x.P(x))"
(fn prems => [ resolve_tac prems 1,
rtac theI 1,
@@ -223,49 +222,49 @@
(THE x.P(x)) rewrites to (THE x. Q(x)) *)
(*If it's "undefined", it's zero!*)
-qed_goalw "the_0" thy [the_def]
+qed_goalw "the_0" ZF.thy [the_def]
"!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
- (fn _ => [ (fast_tac (!claset addSEs [ReplaceE]) 1) ]);
+ (fn _ => [ (deepen_tac (!claset addSEs [ReplaceE]) 0 1) ]);
(*** if -- a conditional expression for formulae ***)
-goalw thy [if_def] "if(True,a,b) = a";
-by (fast_tac (!claset addIs [the_equality]) 1);
+goalw ZF.thy [if_def] "if(True,a,b) = a";
+by (blast_tac (!claset addSIs [the_equality]) 1);
qed "if_true";
-goalw thy [if_def] "if(False,a,b) = b";
-by (fast_tac (!claset addIs [the_equality]) 1);
+goalw ZF.thy [if_def] "if(False,a,b) = b";
+by (blast_tac (!claset addSIs [the_equality]) 1);
qed "if_false";
(*Never use with case splitting, or if P is known to be true or false*)
-val prems = goalw thy [if_def]
+val prems = goalw ZF.thy [if_def]
"[| P<->Q; Q ==> a=c; ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
by (simp_tac (!simpset addsimps prems addcongs [conj_cong]) 1);
qed "if_cong";
(*Not needed for rewriting, since P would rewrite to True anyway*)
-goalw thy [if_def] "!!P. P ==> if(P,a,b) = a";
-by (fast_tac (!claset addSIs [the_equality]) 1);
+goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
+by (blast_tac (!claset addSIs [the_equality]) 1);
qed "if_P";
(*Not needed for rewriting, since P would rewrite to False anyway*)
-goalw thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
-by (fast_tac (!claset addSIs [the_equality]) 1);
+goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
+by (blast_tac (!claset addSIs [the_equality]) 1);
qed "if_not_P";
Addsimps [if_true, if_false];
-qed_goal "expand_if" thy
+qed_goal "expand_if" ZF.thy
"P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
(fn _=> [ (excluded_middle_tac "Q" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1) ]);
-qed_goal "if_iff" thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
+qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
(fn _=> [ (simp_tac (!simpset setloop split_tac [expand_if]) 1) ]);
-qed_goal "if_type" thy
+qed_goal "if_type" ZF.thy
"[| P ==> a: A; ~P ==> b: A |] ==> if(P,a,b): A"
(fn prems=> [ (simp_tac
(!simpset addsimps prems setloop split_tac [expand_if]) 1) ]);
@@ -274,47 +273,48 @@
(*** Foundation lemmas ***)
(*was called mem_anti_sym*)
-qed_goal "mem_asym" thy "!!P. [| a:b; b:a |] ==> P"
- (fn _=>
- [ (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
- REPEAT (fast_tac (!claset addSEs [equalityE]) 1) ]);
+qed_goal "mem_asym" ZF.thy "[| a:b; ~P ==> b:a |] ==> P"
+ (fn prems=>
+ [ (rtac classical 1),
+ (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
+ REPEAT (blast_tac (!claset addIs prems addSEs [equalityE]) 1) ]);
(*was called mem_anti_refl*)
-qed_goal "mem_irrefl" thy "a:a ==> P"
+qed_goal "mem_irrefl" ZF.thy "a:a ==> P"
(fn [major]=> [ (rtac ([major,major] MRS mem_asym) 1) ]);
(*mem_irrefl should NOT be added to default databases:
it would be tried on most goals, making proofs slower!*)
-qed_goal "mem_not_refl" thy "a ~: a"
+qed_goal "mem_not_refl" ZF.thy "a ~: a"
(K [ (rtac notI 1), (etac mem_irrefl 1) ]);
(*Good for proving inequalities by rewriting*)
-qed_goal "mem_imp_not_eq" thy "!!a A. a:A ==> a ~= A"
- (fn _=> [ fast_tac (!claset addSEs [mem_irrefl]) 1 ]);
+qed_goal "mem_imp_not_eq" ZF.thy "!!a A. a:A ==> a ~= A"
+ (fn _=> [ blast_tac (!claset addSEs [mem_irrefl]) 1 ]);
(*** Rules for succ ***)
-qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j"
- (fn _ => [ Fast_tac 1 ]);
+qed_goalw "succ_iff" ZF.thy [succ_def] "i : succ(j) <-> i=j | i:j"
+ (fn _ => [ Blast_tac 1 ]);
-qed_goalw "succI1" thy [succ_def] "i : succ(i)"
+qed_goalw "succI1" ZF.thy [succ_def] "i : succ(i)"
(fn _=> [ (rtac consI1 1) ]);
Addsimps [succI1];
-qed_goalw "succI2" thy [succ_def]
+qed_goalw "succI2" ZF.thy [succ_def]
"i : j ==> i : succ(j)"
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
-qed_goalw "succE" thy [succ_def]
+qed_goalw "succE" ZF.thy [succ_def]
"[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS consE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
(*Classical introduction rule*)
-qed_goal "succCI" thy "(i~:j ==> i=j) ==> i: succ(j)"
+qed_goal "succCI" ZF.thy "(i~:j ==> i=j) ==> i: succ(j)"
(fn [prem]=>
[ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
(etac prem 1) ]);
@@ -322,8 +322,8 @@
AddSIs [succCI];
AddSEs [succE];
-qed_goal "succ_not_0" thy "succ(n) ~= 0"
- (fn _=> [ (fast_tac (!claset addSEs [equalityE]) 1) ]);
+qed_goal "succ_not_0" ZF.thy "succ(n) ~= 0"
+ (fn _=> [ (blast_tac (!claset addSEs [equalityE]) 1) ]);
bind_thm ("succ_neq_0", succ_not_0 RS notE);
@@ -338,13 +338,15 @@
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 _=> [ (fast_tac (!claset addEs [mem_asym, equalityE]) 1) ]);
+qed_goal "succ_inject_iff" ZF.thy "succ(m) = succ(n) <-> m=n"
+ (fn _=> [ (blast_tac (!claset addEs [mem_asym] addSEs [equalityE]) 1) ]);
bind_thm ("succ_inject", succ_inject_iff RS iffD1);
Addsimps [succ_inject_iff];
AddSDs [succ_inject];
+(*Not needed now that cons is available. Deletion reduces the search space.*)
+Delrules [UpairI1,UpairI2,UpairE];
use"simpdata.ML";