--- a/src/ZF/Induct/Brouwer.thy Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/Induct/Brouwer.thy Wed Dec 19 11:13:27 2001 +0100
@@ -6,15 +6,15 @@
header {* Infinite branching datatype definitions *}
-theory Brouwer = Main:
+theory Brouwer = Main_ZFC:
subsection {* The Brouwer ordinals *}
consts
brouwer :: i
-datatype \<subseteq> "Vfrom(0, csucc(nat))"
- "brouwer" = Zero | Suc ("b \<in> brouwer") | Lim ("h \<in> nat -> brouwer")
+datatype \\<subseteq> "Vfrom(0, csucc(nat))"
+ "brouwer" = Zero | Suc ("b \\<in> brouwer") | Lim ("h \\<in> nat -> brouwer")
monos Pi_mono
type_intros inf_datatype_intrs
@@ -23,16 +23,16 @@
elim: brouwer.cases [unfolded brouwer.con_defs])
lemma brouwer_induct2:
- "[| b \<in> brouwer;
+ "[| b \\<in> brouwer;
P(Zero);
- !!b. [| b \<in> brouwer; P(b) |] ==> P(Suc(b));
- !!h. [| h \<in> nat -> brouwer; \<forall>i \<in> nat. P(h`i)
+ !!b. [| b \\<in> brouwer; P(b) |] ==> P(Suc(b));
+ !!h. [| h \\<in> nat -> brouwer; \\<forall>i \\<in> nat. P(h`i)
|] ==> P(Lim(h))
|] ==> P(b)"
-- {* A nicer induction rule than the standard one. *}
proof -
case rule_context
- assume "b \<in> brouwer"
+ assume "b \\<in> brouwer"
thus ?thesis
apply induct
apply (assumption | rule rule_context)+
@@ -47,26 +47,26 @@
consts
Well :: "[i, i => i] => i"
-datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))"
+datatype \\<subseteq> "Vfrom(A \\<union> (\\<Union>x \\<in> A. B(x)), csucc(nat \\<union> |\\<Union>x \\<in> A. B(x)|))"
-- {* The union with @{text nat} ensures that the cardinal is infinite. *}
- "Well(A, B)" = Sup ("a \<in> A", "f \<in> B(a) -> Well(A, B)")
+ "Well(A, B)" = Sup ("a \\<in> A", "f \\<in> B(a) -> Well(A, B)")
monos Pi_mono
type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intrs
-lemma Well_unfold: "Well(A, B) = (\<Sigma>x \<in> A. B(x) -> Well(A, B))"
+lemma Well_unfold: "Well(A, B) = (\\<Sigma>x \\<in> A. B(x) -> Well(A, B))"
by (fast intro!: Well.intros [unfolded Well.con_defs]
elim: Well.cases [unfolded Well.con_defs])
lemma Well_induct2:
- "[| w \<in> Well(A, B);
- !!a f. [| a \<in> A; f \<in> B(a) -> Well(A,B); \<forall>y \<in> B(a). P(f`y)
+ "[| w \\<in> Well(A, B);
+ !!a f. [| a \\<in> A; f \\<in> B(a) -> Well(A,B); \\<forall>y \\<in> B(a). P(f`y)
|] ==> P(Sup(a,f))
|] ==> P(w)"
-- {* A nicer induction rule than the standard one. *}
proof -
case rule_context
- assume "w \<in> Well(A, B)"
+ assume "w \\<in> Well(A, B)"
thus ?thesis
apply induct
apply (assumption | rule rule_context)+
--- a/src/ZF/IsaMakefile Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/IsaMakefile Wed Dec 19 11:13:27 2001 +0100
@@ -37,6 +37,7 @@
Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy \
Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML \
Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy \
+ Main_ZFC.ML Main_ZFC.thy \
Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML OrderArith.thy \
OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy Perm.ML Perm.thy \
QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML \
--- a/src/ZF/Main.thy Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/Main.thy Wed Dec 19 11:13:27 2001 +0100
@@ -1,8 +1,7 @@
+(*$Id$
+ theory Main includes everything except AC*)
-(*$Id$
- theory Main includes everything*)
-
-theory Main = Update + InfDatatype + List + EquivClass + IntDiv:
+theory Main = Update + List + EquivClass + IntDiv + CardinalArith:
(* belongs to theory Trancl *)
lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Main_ZFC.ML Wed Dec 19 11:13:27 2001 +0100
@@ -0,0 +1,4 @@
+structure Main_ZFC =
+struct
+ val thy = the_context ();
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Main_ZFC.thy Wed Dec 19 11:13:27 2001 +0100
@@ -0,0 +1,3 @@
+theory Main_ZFC = Main + InfDatatype:
+
+end
--- a/src/ZF/Nat.ML Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/Nat.ML Wed Dec 19 11:13:27 2001 +0100
@@ -234,3 +234,8 @@
by (rtac (Int_greatest_lt RS ltD) 1);
by (REPEAT (ares_tac [ltI, Ord_nat] 1));
qed "Int_nat_type";
+
+Goal "nat ~= 0";
+by (Blast_tac 1);
+qed "nat_nonempty";
+Addsimps [nat_nonempty]; (*needed to simplify unions over nat*)
--- a/src/ZF/OrdQuant.thy Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/OrdQuant.thy Wed Dec 19 11:13:27 2001 +0100
@@ -26,9 +26,9 @@
"UN x<a. B" == "OUnion(a, %x. B)"
syntax (xsymbols)
- "@oall" :: [idt, i, o] => o ("(3\\<forall> _<_./ _)" 10)
- "@oex" :: [idt, i, o] => o ("(3\\<exists> _<_./ _)" 10)
- "@OUNION" :: [idt, i, i] => i ("(3\\<Union> _<_./ _)" 10)
+ "@oall" :: [idt, i, o] => o ("(3\\<forall>_<_./ _)" 10)
+ "@oex" :: [idt, i, o] => o ("(3\\<exists>_<_./ _)" 10)
+ "@OUNION" :: [idt, i, i] => i ("(3\\<Union>_<_./ _)" 10)
defs
--- a/src/ZF/ROOT.ML Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/ROOT.ML Wed Dec 19 11:13:27 2001 +0100
@@ -21,7 +21,7 @@
use "~~/src/Provers/Arith/cancel_numerals.ML";
use "~~/src/Provers/Arith/combine_numerals.ML";
-with_path "Integ" use_thy "Main";
+with_path "Integ" use_thy "Main_ZFC";
simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
print_depth 8;
--- a/src/ZF/UNITY/WFair.thy Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/UNITY/WFair.thy Wed Dec 19 11:13:27 2001 +0100
@@ -10,7 +10,7 @@
Theory ported from HOL.
*)
-WFair = UNITY +
+WFair = UNITY + Main_ZFC +
constdefs
(* This definition specifies weak fairness. The rest of the theory
--- a/src/ZF/ZF.thy Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/ZF.thy Wed Dec 19 11:13:27 2001 +0100
@@ -153,8 +153,10 @@
"@Collect" :: [pttrn, i, o] => i ("(1{_ \\<in> _ ./ _})")
"@Replace" :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _ \\<in> _, _})")
"@RepFun" :: [i, pttrn, i] => i ("(1{_ ./ _ \\<in> _})" [51,0,51])
+ "@UNION" :: [pttrn, i, i] => i ("(3\\<Union>_\\<in>_./ _)" 10)
"@INTER" :: [pttrn, i, i] => i ("(3\\<Inter>_\\<in>_./ _)" 10)
- "@UNION" :: [pttrn, i, i] => i ("(3\\<Union>_\\<in>_./ _)" 10)
+ Union :: i =>i ("\\<Union>_" [90] 90)
+ Inter :: i =>i ("\\<Inter>_" [90] 90)
"@PROD" :: [pttrn, i, i] => i ("(3\\<Pi>_\\<in>_./ _)" 10)
"@SUM" :: [pttrn, i, i] => i ("(3\\<Sigma>_\\<in>_./ _)" 10)
"@lam" :: [pttrn, i, i] => i ("(3\\<lambda>_\\<in>_./ _)" 10)
@@ -274,4 +276,3 @@
[(*("split", split_tr'),*)
("Pi", dependent_tr' ("@PROD", "op ->")),
("Sigma", dependent_tr' ("@SUM", "op *"))];
-
--- a/src/ZF/simpdata.ML Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/simpdata.ML Wed Dec 19 11:13:27 2001 +0100
@@ -104,8 +104,7 @@
val Rep_simps = map prover
["{x. y:0, R(x,y)} = 0", (*Replace*)
"{x:0. P(x)} = 0", (*Collect*)
- "{x:A. False} = 0",
- "{x:A. True} = A",
+ "{x:A. P} = (if P then A else 0)",
"RepFun(0,f) = 0", (*RepFun*)
"RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
"RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
--- a/src/ZF/subset.ML Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/subset.ML Wed Dec 19 11:13:27 2001 +0100
@@ -53,6 +53,10 @@
by (REPEAT (ares_tac prems 1)) ;
qed "succ_subsetE";
+Goalw [succ_def] "succ(a) <= B <-> (a <= B & a : B)";
+by (Blast_tac 1) ;
+qed "succ_subset_iff";
+
(*** singletons ***)
Goal "a:C ==> {a} <= C";