# HG changeset patch
# User paulson
# Date 1008756807 -3600
# Node ID d2d2ab3f1f37cab89b4e35e442f7376c97f90c58
# Parent  f44734e5e7463fa854fbe39b1a93deda3c511e78
separation of the AC part of Main into Main_ZFC, plus a few new lemmas

diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/Induct/Brouwer.thy
--- 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)+
diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/IsaMakefile
--- 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	\
diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/Main.thy
--- 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]
diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/Main_ZFC.ML
--- /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;
diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/Main_ZFC.thy
--- /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
diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/Nat.ML
--- 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*)
diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/OrdQuant.thy
--- 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
   
diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/ROOT.ML
--- 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;
diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/UNITY/WFair.thy
--- 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
diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/ZF.thy
--- 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 *"))];
-
diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/simpdata.ML
--- 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))"]
diff -r f44734e5e746 -r d2d2ab3f1f37 src/ZF/subset.ML
--- 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";