src/ZF/upair.ML
 changeset 760 f0200e91b272 parent 738 3054a10ed5b5 child 834 ad1d0eb0ee82
```--- a/src/ZF/upair.ML	Wed Dec 07 12:34:47 1994 +0100
+++ b/src/ZF/upair.ML	Wed Dec 07 13:12:04 1994 +0100
@@ -21,17 +21,17 @@

(*** Unordered pairs - Upair ***)

-val pairing = prove_goalw ZF.thy [Upair_def]
+qed_goalw "pairing" ZF.thy [Upair_def]
"c : Upair(a,b) <-> (c=a | c=b)"
(fn _ => [ (fast_tac (lemmas_cs addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);

-val UpairI1 = prove_goal ZF.thy "a : Upair(a,b)"
+qed_goal "UpairI1" ZF.thy "a : Upair(a,b)"
(fn _ => [ (rtac (refl RS disjI1 RS (pairing RS iffD2)) 1) ]);

-val UpairI2 = prove_goal ZF.thy "b : Upair(a,b)"
+qed_goal "UpairI2" ZF.thy "b : Upair(a,b)"
(fn _ => [ (rtac (refl RS disjI2 RS (pairing RS iffD2)) 1) ]);

-val UpairE = prove_goal ZF.thy
+qed_goal "UpairE" ZF.thy
"[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS (pairing RS iffD1 RS disjE)) 1),
@@ -39,13 +39,13 @@

(*** Rules for binary union -- Un -- defined via Upair ***)

-val UnI1 = prove_goalw ZF.thy [Un_def] "c : A ==> c : A Un B"
+qed_goalw "UnI1" ZF.thy [Un_def] "c : A ==> c : A Un B"
(fn [prem]=> [ (rtac (prem RS (UpairI1 RS UnionI)) 1) ]);

-val UnI2 = prove_goalw ZF.thy [Un_def] "c : B ==> c : A Un B"
+qed_goalw "UnI2" ZF.thy [Un_def] "c : B ==> c : A Un B"
(fn [prem]=> [ (rtac (prem RS (UpairI2 RS UnionI)) 1) ]);

-val UnE = prove_goalw ZF.thy [Un_def]
+qed_goalw "UnE" ZF.thy [Un_def]
"[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS UnionE) 1),
@@ -53,7 +53,7 @@
(REPEAT (EVERY1 [resolve_tac prems, etac subst, assume_tac])) ]);

(*Stronger version of the rule above*)
-val UnE' = prove_goal ZF.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),
@@ -63,11 +63,11 @@
(swap_res_tac prems 1),
(etac notnotD 1)]);

-val Un_iff = prove_goal ZF.thy "c : A Un B <-> (c:A | c:B)"
+qed_goal "Un_iff" ZF.thy "c : A Un B <-> (c:A | c:B)"
(fn _ => [ (fast_tac (lemmas_cs addIs [UnI1,UnI2] addSEs [UnE]) 1) ]);

(*Classical introduction rule: no commitment to A vs B*)
-val UnCI = prove_goal ZF.thy "(c ~: B ==> c : A) ==> c : A Un B"
+qed_goal "UnCI" ZF.thy "(c ~: B ==> c : A) ==> c : A Un B"
(fn [prem]=>
[ (rtac (disjCI RS (Un_iff RS iffD2)) 1),
(etac prem 1) ]);
@@ -75,69 +75,69 @@

(*** Rules for small intersection -- Int -- defined via Upair ***)

-val IntI = prove_goalw ZF.thy [Int_def]
+qed_goalw "IntI" ZF.thy [Int_def]
"[| c : A;  c : B |] ==> c : A Int B"
(fn prems=>
[ (REPEAT (resolve_tac (prems @ [UpairI1,InterI]) 1
ORELSE eresolve_tac [UpairE, ssubst] 1)) ]);

-val IntD1 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : A"
+qed_goalw "IntD1" ZF.thy [Int_def] "c : A Int B ==> c : A"
(fn [major]=>
[ (rtac (UpairI1 RS (major RS InterD)) 1) ]);

-val IntD2 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : B"
+qed_goalw "IntD2" ZF.thy [Int_def] "c : A Int B ==> c : B"
(fn [major]=>
[ (rtac (UpairI2 RS (major RS InterD)) 1) ]);

-val IntE = prove_goal ZF.thy
+qed_goal "IntE" ZF.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 Int_iff = prove_goal ZF.thy "c : A Int B <-> (c:A & c:B)"
+qed_goal "Int_iff" ZF.thy "c : A Int B <-> (c:A & c:B)"
(fn _ => [ (fast_tac (lemmas_cs addSIs [IntI] addSEs [IntE]) 1) ]);

(*** Rules for set difference -- defined via Upair ***)

-val DiffI = prove_goalw ZF.thy [Diff_def]
+qed_goalw "DiffI" ZF.thy [Diff_def]
"[| c : A;  c ~: B |] ==> c : A - B"
(fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI]) 1)) ]);

-val DiffD1 = prove_goalw ZF.thy [Diff_def]
+qed_goalw "DiffD1" ZF.thy [Diff_def]
"c : A - B ==> c : A"
(fn [major]=> [ (rtac (major RS CollectD1) 1) ]);

-val DiffD2 = prove_goalw ZF.thy [Diff_def]
+qed_goalw "DiffD2" ZF.thy [Diff_def]
"c : A - B ==> c ~: B"
(fn [major]=> [ (rtac (major RS CollectD2) 1) ]);

-val DiffE = prove_goal ZF.thy
+qed_goal "DiffE" ZF.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 Diff_iff = prove_goal ZF.thy "c : A-B <-> (c:A & c~:B)"
+qed_goal "Diff_iff" ZF.thy "c : A-B <-> (c:A & c~:B)"
(fn _ => [ (fast_tac (lemmas_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);

(*** Rules for cons -- defined via Un and Upair ***)

-val consI1 = prove_goalw ZF.thy [cons_def] "a : cons(a,B)"
+qed_goalw "consI1" ZF.thy [cons_def] "a : cons(a,B)"
(fn _ => [ (rtac (UpairI1 RS UnI1) 1) ]);

-val consI2 = prove_goalw ZF.thy [cons_def] "a : B ==> a : cons(b,B)"
+qed_goalw "consI2" ZF.thy [cons_def] "a : B ==> a : cons(b,B)"
(fn [prem]=> [ (rtac (prem RS UnI2) 1) ]);

-val consE = prove_goalw ZF.thy [cons_def]
+qed_goalw "consE" ZF.thy [cons_def]
"[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS UnE) 1),
(REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);

(*Stronger version of the rule above*)
-val consE' = prove_goal ZF.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),
@@ -147,21 +147,21 @@
(swap_res_tac prems 1),
(etac notnotD 1)]);

-val cons_iff = prove_goal ZF.thy "a : cons(b,A) <-> (a=b | a:A)"
+qed_goal "cons_iff" ZF.thy "a : cons(b,A) <-> (a=b | a:A)"
(fn _ => [ (fast_tac (lemmas_cs addIs [consI1,consI2] addSEs [consE]) 1) ]);

(*Classical introduction rule*)
-val consCI = prove_goal ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)"
+qed_goal "consCI" ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)"
(fn [prem]=>
[ (rtac (disjCI RS (cons_iff RS iffD2)) 1),
(etac prem 1) ]);

(*** Singletons - using cons ***)

-val singletonI = prove_goal ZF.thy "a : {a}"
+qed_goal "singletonI" ZF.thy "a : {a}"
(fn _=> [ (rtac consI1 1) ]);

-val singletonE = prove_goal ZF.thy "[| a: {b};  a=b ==> P |] ==> P"
+qed_goal "singletonE" ZF.thy "[| a: {b};  a=b ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS consE) 1),
(REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
@@ -169,26 +169,26 @@

(*** Rules for Descriptions ***)

-val the_equality = prove_goalw ZF.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] =>
addEs [eq RS subst]) 1) ]);

(* Only use this if you already know EX!x. P(x) *)
-val the_equality2 = prove_goal ZF.thy
+qed_goal "the_equality2" ZF.thy
"!!P. [| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
(fn _ =>
[ (deepen_tac (lemmas_cs addSIs [the_equality]) 1 1) ]);

-val theI = prove_goal ZF.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*)
-val theI2 = prove_goal ZF.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,
@@ -198,7 +198,7 @@
(THE x.P(x))  rewrites to  (THE x. Q(x))  *)

(*If it's "undefined", it's zero!*)
-val the_0 = prove_goalw ZF.thy [the_def]
+qed_goalw "the_0" ZF.thy [the_def]
"!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
(fn _ =>
@@ -208,31 +208,31 @@

goalw ZF.thy [if_def] "if(True,a,b) = a";
by (fast_tac (lemmas_cs addIs [the_equality]) 1);
-val if_true = result();
+qed "if_true";

goalw ZF.thy [if_def] "if(False,a,b) = b";
by (fast_tac (lemmas_cs addIs [the_equality]) 1);
-val if_false = result();
+qed "if_false";

(*Never use with case splitting, or if P is known to be true or false*)
val prems = goalw ZF.thy [if_def]
"[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
-val if_cong = result();
+qed "if_cong";

(*Not needed for rewriting, since P would rewrite to True anyway*)
goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
-val if_P = result();
+qed "if_P";

(*Not needed for rewriting, since P would rewrite to False anyway*)
goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
-val if_not_P = result();
+qed "if_not_P";

val if_ss = FOL_ss addsimps  [if_true,if_false];

-val expand_if = prove_goal ZF.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 if_ss 1),
@@ -242,13 +242,13 @@
"[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A";
by (excluded_middle_tac "P" 1);
by (ALLGOALS (asm_simp_tac (if_ss addsimps prems)));
-val if_type = result();
+qed "if_type";

(*** Foundation lemmas ***)

(*was called mem_anti_sym*)
-val mem_asym = prove_goal ZF.thy "!!P. [| a:b;  b:a |] ==> P"
+qed_goal "mem_asym" ZF.thy "!!P. [| a:b;  b:a |] ==> P"
(fn _=>
[ (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
(etac equals0D 1),
@@ -257,58 +257,58 @@

(*was called mem_anti_refl*)
-val mem_irrefl = prove_goal ZF.thy "a:a ==> P"
+qed_goal "mem_irrefl" ZF.thy "a:a ==> P"
(fn [major]=> [ (rtac (major RS (major RS mem_asym)) 1) ]);

-val mem_not_refl = prove_goal ZF.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*)
-val mem_imp_not_eq = prove_goal ZF.thy "!!a A. a:A ==> a ~= A"
+qed_goal "mem_imp_not_eq" ZF.thy "!!a A. a:A ==> a ~= A"
(fn _=> [ fast_tac (lemmas_cs addSEs [mem_irrefl]) 1 ]);

(*** Rules for succ ***)

-val succI1 = prove_goalw ZF.thy [succ_def] "i : succ(i)"
+qed_goalw "succI1" ZF.thy [succ_def] "i : succ(i)"
(fn _=> [ (rtac consI1 1) ]);

-val succI2 = prove_goalw ZF.thy [succ_def]
+qed_goalw "succI2" ZF.thy [succ_def]
"i : j ==> i : succ(j)"
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]);

-val succE = prove_goalw ZF.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)) ]);

-val succ_iff = prove_goal ZF.thy "i : succ(j) <-> i=j | i:j"
+qed_goal "succ_iff" ZF.thy "i : succ(j) <-> i=j | i:j"
(fn _ => [ (fast_tac (lemmas_cs addIs [succI1,succI2] addSEs [succE]) 1) ]);

(*Classical introduction rule*)
-val succCI = prove_goal ZF.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) ]);

-val succ_neq_0 = prove_goal ZF.thy "succ(n)=0 ==> P"
+qed_goal "succ_neq_0" ZF.thy "succ(n)=0 ==> P"
(fn [major]=>
[ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),
(rtac succI1 1) ]);

(*Useful for rewriting*)
-val succ_not_0 = prove_goal ZF.thy "succ(n) ~= 0"
+qed_goal "succ_not_0" ZF.thy "succ(n) ~= 0"
(fn _=> [ (rtac notI 1), (etac succ_neq_0 1) ]);

(* succ(c) <= B ==> c : B *)
val succ_subsetD = succI1 RSN (2,subsetD);

-val succ_inject = prove_goal ZF.thy "!!m n. succ(m) = succ(n) ==> m=n"
+qed_goal "succ_inject" ZF.thy "!!m n. succ(m) = succ(n) ==> m=n"
(fn _ =>
[ (fast_tac (lemmas_cs addSEs [succE, equalityE, make_elim succ_subsetD]