--- a/src/ZF/subset.ML Wed Dec 07 12:34:47 1994 +0100
+++ b/src/ZF/subset.ML Wed Dec 07 13:12:04 1994 +0100
@@ -9,43 +9,43 @@
(*** cons ***)
-val cons_subsetI = prove_goal ZF.thy "[| a:C; B<=C |] ==> cons(a,B) <= C"
+qed_goal "cons_subsetI" ZF.thy "[| a:C; B<=C |] ==> cons(a,B) <= C"
(fn prems=>
[ (cut_facts_tac prems 1),
(REPEAT (ares_tac [subsetI] 1
ORELSE eresolve_tac [consE,ssubst,subsetD] 1)) ]);
-val subset_consI = prove_goal ZF.thy "B <= cons(a,B)"
+qed_goal "subset_consI" ZF.thy "B <= cons(a,B)"
(fn _=> [ (rtac subsetI 1), (etac consI2 1) ]);
(*Useful for rewriting!*)
-val cons_subset_iff = prove_goal ZF.thy "cons(a,B)<=C <-> a:C & B<=C"
+qed_goal "cons_subset_iff" ZF.thy "cons(a,B)<=C <-> a:C & B<=C"
(fn _=> [ (fast_tac upair_cs 1) ]);
(*A safe special case of subset elimination, adding no new variables
[| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
val cons_subsetE = standard (cons_subset_iff RS iffD1 RS conjE);
-val subset_empty_iff = prove_goal ZF.thy "A<=0 <-> A=0"
+qed_goal "subset_empty_iff" ZF.thy "A<=0 <-> A=0"
(fn _=> [ (fast_tac (upair_cs addIs [equalityI]) 1) ]);
-val subset_cons_iff = prove_goal ZF.thy
+qed_goal "subset_cons_iff" ZF.thy
"C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
(fn _=> [ (fast_tac upair_cs 1) ]);
(*** succ ***)
-val subset_succI = prove_goal ZF.thy "i <= succ(i)"
+qed_goal "subset_succI" ZF.thy "i <= succ(i)"
(fn _=> [ (rtac subsetI 1), (etac succI2 1) ]);
(*But if j is an ordinal or is transitive, then i:j implies i<=j!
See ordinal/Ord_succ_subsetI*)
-val succ_subsetI = prove_goalw ZF.thy [succ_def]
+qed_goalw "succ_subsetI" ZF.thy [succ_def]
"[| i:j; i<=j |] ==> succ(i)<=j"
(fn prems=>
[ (REPEAT (ares_tac (prems@[cons_subsetI]) 1)) ]);
-val succ_subsetE = prove_goalw ZF.thy [succ_def]
+qed_goalw "succ_subsetE" ZF.thy [succ_def]
"[| succ(i) <= j; [| i:j; i<=j |] ==> P \
\ |] ==> P"
(fn major::prems=>
@@ -54,25 +54,25 @@
(*** singletons ***)
-val singleton_subsetI = prove_goal ZF.thy
+qed_goal "singleton_subsetI" ZF.thy
"a:C ==> {a} <= C"
(fn prems=>
[ (REPEAT (resolve_tac (prems@[cons_subsetI,empty_subsetI]) 1)) ]);
-val singleton_subsetD = prove_goal ZF.thy
+qed_goal "singleton_subsetD" ZF.thy
"{a} <= C ==> a:C"
(fn prems=> [ (REPEAT (ares_tac (prems@[cons_subsetE]) 1)) ]);
(*** Big Union -- least upper bound of a set ***)
-val Union_subset_iff = prove_goal ZF.thy "Union(A) <= C <-> (ALL x:A. x <= C)"
+qed_goal "Union_subset_iff" ZF.thy "Union(A) <= C <-> (ALL x:A. x <= C)"
(fn _ => [ fast_tac upair_cs 1 ]);
-val Union_upper = prove_goal ZF.thy
+qed_goal "Union_upper" ZF.thy
"B:A ==> B <= Union(A)"
(fn prems=> [ (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)) ]);
-val Union_least = prove_goal ZF.thy
+qed_goal "Union_least" ZF.thy
"[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"
(fn [prem]=>
[ (rtac (ballI RS (Union_subset_iff RS iffD2)) 1),
@@ -82,17 +82,17 @@
goal ZF.thy "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
by (fast_tac (upair_cs addSIs [equalityI] addSEs [equalityE]) 1);
-val subset_UN_iff_eq = result();
+qed "subset_UN_iff_eq";
-val UN_subset_iff = prove_goal ZF.thy
+qed_goal "UN_subset_iff" ZF.thy
"(UN x:A.B(x)) <= C <-> (ALL x:A. B(x) <= C)"
(fn _ => [ fast_tac upair_cs 1 ]);
-val UN_upper = prove_goal ZF.thy
+qed_goal "UN_upper" ZF.thy
"!!x A. x:A ==> B(x) <= (UN x:A.B(x))"
(fn _ => [ etac (RepFunI RS Union_upper) 1 ]);
-val UN_least = prove_goal ZF.thy
+qed_goal "UN_least" ZF.thy
"[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A.B(x)) <= C"
(fn [prem]=>
[ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1),
@@ -101,16 +101,16 @@
(*** Big Intersection -- greatest lower bound of a nonempty set ***)
-val Inter_subset_iff = prove_goal ZF.thy
+qed_goal "Inter_subset_iff" ZF.thy
"!!a A. a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)"
(fn _ => [ fast_tac upair_cs 1 ]);
-val Inter_lower = prove_goal ZF.thy "B:A ==> Inter(A) <= B"
+qed_goal "Inter_lower" ZF.thy "B:A ==> Inter(A) <= B"
(fn prems=>
[ (REPEAT (resolve_tac (prems@[subsetI]) 1
ORELSE etac InterD 1)) ]);
-val Inter_greatest = prove_goal ZF.thy
+qed_goal "Inter_greatest" ZF.thy
"[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)"
(fn [prem1,prem2]=>
[ (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1),
@@ -118,12 +118,12 @@
(*** Intersection of a family of sets ***)
-val INT_lower = prove_goal ZF.thy
+qed_goal "INT_lower" ZF.thy
"x:A ==> (INT x:A.B(x)) <= B(x)"
(fn [prem] =>
[ rtac (prem RS RepFunI RS Inter_lower) 1 ]);
-val INT_greatest = prove_goal ZF.thy
+qed_goal "INT_greatest" ZF.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,
@@ -132,32 +132,32 @@
(*** Finite Union -- the least upper bound of 2 sets ***)
-val Un_subset_iff = prove_goal ZF.thy "A Un B <= C <-> A <= C & B <= C"
+qed_goal "Un_subset_iff" ZF.thy "A Un B <= C <-> A <= C & B <= C"
(fn _ => [ fast_tac upair_cs 1 ]);
-val Un_upper1 = prove_goal ZF.thy "A <= A Un B"
+qed_goal "Un_upper1" ZF.thy "A <= A Un B"
(fn _ => [ (REPEAT (ares_tac [subsetI,UnI1] 1)) ]);
-val Un_upper2 = prove_goal ZF.thy "B <= A Un B"
+qed_goal "Un_upper2" ZF.thy "B <= A Un B"
(fn _ => [ (REPEAT (ares_tac [subsetI,UnI2] 1)) ]);
-val Un_least = prove_goal ZF.thy "!!A B C. [| A<=C; B<=C |] ==> A Un B <= C"
+qed_goal "Un_least" ZF.thy "!!A B C. [| A<=C; B<=C |] ==> A Un B <= C"
(fn _ =>
[ (rtac (Un_subset_iff RS iffD2) 1),
(REPEAT (ares_tac [conjI] 1)) ]);
(*** Finite Intersection -- the greatest lower bound of 2 sets *)
-val Int_subset_iff = prove_goal ZF.thy "C <= A Int B <-> C <= A & C <= B"
+qed_goal "Int_subset_iff" ZF.thy "C <= A Int B <-> C <= A & C <= B"
(fn _ => [ fast_tac upair_cs 1 ]);
-val Int_lower1 = prove_goal ZF.thy "A Int B <= A"
+qed_goal "Int_lower1" ZF.thy "A Int B <= A"
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);
-val Int_lower2 = prove_goal ZF.thy "A Int B <= B"
+qed_goal "Int_lower2" ZF.thy "A Int B <= B"
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)) ]);
-val Int_greatest = prove_goal ZF.thy
+qed_goal "Int_greatest" ZF.thy
"!!A B C. [| C<=A; C<=B |] ==> C <= A Int B"
(fn prems=>
[ (rtac (Int_subset_iff RS iffD2) 1),
@@ -165,10 +165,10 @@
(*** Set difference *)
-val Diff_subset = prove_goal ZF.thy "A-B <= A"
+qed_goal "Diff_subset" ZF.thy "A-B <= A"
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]);
-val Diff_contains = prove_goal ZF.thy
+qed_goal "Diff_contains" ZF.thy
"[| C<=A; C Int B = 0 |] ==> C <= A-B"
(fn prems=>
[ (cut_facts_tac prems 1),
@@ -178,7 +178,7 @@
(** Collect **)
-val Collect_subset = prove_goal ZF.thy "Collect(A,P) <= A"
+qed_goal "Collect_subset" ZF.thy "Collect(A,P) <= A"
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac CollectD1 1)) ]);
(** RepFun **)
@@ -188,7 +188,7 @@
by (etac RepFunE 1);
by (etac ssubst 1);
by (eresolve_tac prems 1);
-val RepFun_subset = result();
+qed "RepFun_subset";
(*A more powerful claset for subset reasoning*)
val subset_cs = subset0_cs