separation of the AC part of Main into Main_ZFC, plus a few new lemmas
authorpaulson
Wed Dec 19 11:13:27 2001 +0100 (2001-12-19)
changeset 12552d2d2ab3f1f37
parent 12551 f44734e5e746
child 12553 90ac72455fcc
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
src/ZF/Induct/Brouwer.thy
src/ZF/IsaMakefile
src/ZF/Main.thy
src/ZF/Main_ZFC.ML
src/ZF/Main_ZFC.thy
src/ZF/Nat.ML
src/ZF/OrdQuant.thy
src/ZF/ROOT.ML
src/ZF/UNITY/WFair.thy
src/ZF/ZF.thy
src/ZF/simpdata.ML
src/ZF/subset.ML
     1.1 --- a/src/ZF/Induct/Brouwer.thy	Wed Dec 19 11:07:38 2001 +0100
     1.2 +++ b/src/ZF/Induct/Brouwer.thy	Wed Dec 19 11:13:27 2001 +0100
     1.3 @@ -6,15 +6,15 @@
     1.4  
     1.5  header {* Infinite branching datatype definitions *}
     1.6  
     1.7 -theory Brouwer = Main:
     1.8 +theory Brouwer = Main_ZFC:
     1.9  
    1.10  subsection {* The Brouwer ordinals *}
    1.11  
    1.12  consts
    1.13    brouwer :: i
    1.14  
    1.15 -datatype \<subseteq> "Vfrom(0, csucc(nat))"
    1.16 -    "brouwer" = Zero | Suc ("b \<in> brouwer") | Lim ("h \<in> nat -> brouwer")
    1.17 +datatype \\<subseteq> "Vfrom(0, csucc(nat))"
    1.18 +    "brouwer" = Zero | Suc ("b \\<in> brouwer") | Lim ("h \\<in> nat -> brouwer")
    1.19    monos Pi_mono
    1.20    type_intros inf_datatype_intrs
    1.21  
    1.22 @@ -23,16 +23,16 @@
    1.23      elim: brouwer.cases [unfolded brouwer.con_defs])
    1.24  
    1.25  lemma brouwer_induct2:
    1.26 -  "[| b \<in> brouwer;
    1.27 +  "[| b \\<in> brouwer;
    1.28        P(Zero);
    1.29 -      !!b. [| b \<in> brouwer;  P(b) |] ==> P(Suc(b));
    1.30 -      !!h. [| h \<in> nat -> brouwer;  \<forall>i \<in> nat. P(h`i)
    1.31 +      !!b. [| b \\<in> brouwer;  P(b) |] ==> P(Suc(b));
    1.32 +      !!h. [| h \\<in> nat -> brouwer;  \\<forall>i \\<in> nat. P(h`i)
    1.33             |] ==> P(Lim(h))
    1.34     |] ==> P(b)"
    1.35    -- {* A nicer induction rule than the standard one. *}
    1.36  proof -
    1.37    case rule_context
    1.38 -  assume "b \<in> brouwer"
    1.39 +  assume "b \\<in> brouwer"
    1.40    thus ?thesis
    1.41      apply induct
    1.42      apply (assumption | rule rule_context)+
    1.43 @@ -47,26 +47,26 @@
    1.44  consts
    1.45    Well :: "[i, i => i] => i"
    1.46  
    1.47 -datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))"
    1.48 +datatype \\<subseteq> "Vfrom(A \\<union> (\\<Union>x \\<in> A. B(x)), csucc(nat \\<union> |\\<Union>x \\<in> A. B(x)|))"
    1.49      -- {* The union with @{text nat} ensures that the cardinal is infinite. *}
    1.50 -  "Well(A, B)" = Sup ("a \<in> A", "f \<in> B(a) -> Well(A, B)")
    1.51 +  "Well(A, B)" = Sup ("a \\<in> A", "f \\<in> B(a) -> Well(A, B)")
    1.52    monos Pi_mono
    1.53    type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intrs
    1.54  
    1.55 -lemma Well_unfold: "Well(A, B) = (\<Sigma>x \<in> A. B(x) -> Well(A, B))"
    1.56 +lemma Well_unfold: "Well(A, B) = (\\<Sigma>x \\<in> A. B(x) -> Well(A, B))"
    1.57    by (fast intro!: Well.intros [unfolded Well.con_defs]
    1.58      elim: Well.cases [unfolded Well.con_defs])
    1.59  
    1.60  
    1.61  lemma Well_induct2:
    1.62 -  "[| w \<in> Well(A, B);
    1.63 -      !!a f. [| a \<in> A;  f \<in> B(a) -> Well(A,B);  \<forall>y \<in> B(a). P(f`y)
    1.64 +  "[| w \\<in> Well(A, B);
    1.65 +      !!a f. [| a \\<in> A;  f \\<in> B(a) -> Well(A,B);  \\<forall>y \\<in> B(a). P(f`y)
    1.66             |] ==> P(Sup(a,f))
    1.67     |] ==> P(w)"
    1.68    -- {* A nicer induction rule than the standard one. *}
    1.69  proof -
    1.70    case rule_context
    1.71 -  assume "w \<in> Well(A, B)"
    1.72 +  assume "w \\<in> Well(A, B)"
    1.73    thus ?thesis
    1.74      apply induct
    1.75      apply (assumption | rule rule_context)+
     2.1 --- a/src/ZF/IsaMakefile	Wed Dec 19 11:07:38 2001 +0100
     2.2 +++ b/src/ZF/IsaMakefile	Wed Dec 19 11:13:27 2001 +0100
     2.3 @@ -37,6 +37,7 @@
     2.4    Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy	\
     2.5    Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML			\
     2.6    Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
     2.7 +  Main_ZFC.ML Main_ZFC.thy	\
     2.8    Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML OrderArith.thy	\
     2.9    OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy Perm.ML Perm.thy	\
    2.10    QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML	\
     3.1 --- a/src/ZF/Main.thy	Wed Dec 19 11:07:38 2001 +0100
     3.2 +++ b/src/ZF/Main.thy	Wed Dec 19 11:13:27 2001 +0100
     3.3 @@ -1,8 +1,7 @@
     3.4 +(*$Id$
     3.5 +  theory Main includes everything except AC*)
     3.6  
     3.7 -(*$Id$
     3.8 -  theory Main includes everything*)
     3.9 -
    3.10 -theory Main = Update + InfDatatype + List + EquivClass + IntDiv:
    3.11 +theory Main = Update + List + EquivClass + IntDiv + CardinalArith:
    3.12  
    3.13  (* belongs to theory Trancl *)
    3.14  lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl]
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/ZF/Main_ZFC.ML	Wed Dec 19 11:13:27 2001 +0100
     4.3 @@ -0,0 +1,4 @@
     4.4 +structure Main_ZFC =
     4.5 +struct
     4.6 +  val thy = the_context ();
     4.7 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/ZF/Main_ZFC.thy	Wed Dec 19 11:13:27 2001 +0100
     5.3 @@ -0,0 +1,3 @@
     5.4 +theory Main_ZFC = Main + InfDatatype:
     5.5 +
     5.6 +end
     6.1 --- a/src/ZF/Nat.ML	Wed Dec 19 11:07:38 2001 +0100
     6.2 +++ b/src/ZF/Nat.ML	Wed Dec 19 11:13:27 2001 +0100
     6.3 @@ -234,3 +234,8 @@
     6.4  by (rtac (Int_greatest_lt RS ltD) 1);
     6.5  by (REPEAT (ares_tac [ltI, Ord_nat] 1));
     6.6  qed "Int_nat_type";
     6.7 +
     6.8 +Goal "nat ~= 0";
     6.9 +by (Blast_tac 1);
    6.10 +qed "nat_nonempty";
    6.11 +Addsimps [nat_nonempty];  (*needed to simplify unions over nat*)
     7.1 --- a/src/ZF/OrdQuant.thy	Wed Dec 19 11:07:38 2001 +0100
     7.2 +++ b/src/ZF/OrdQuant.thy	Wed Dec 19 11:13:27 2001 +0100
     7.3 @@ -26,9 +26,9 @@
     7.4    "UN x<a. B"   == "OUnion(a, %x. B)"
     7.5  
     7.6  syntax (xsymbols)
     7.7 -  "@oall"     :: [idt, i, o] => o        ("(3\\<forall> _<_./ _)" 10)
     7.8 -  "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
     7.9 -  "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
    7.10 +  "@oall"     :: [idt, i, o] => o        ("(3\\<forall>_<_./ _)" 10)
    7.11 +  "@oex"      :: [idt, i, o] => o        ("(3\\<exists>_<_./ _)" 10)
    7.12 +  "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union>_<_./ _)" 10)
    7.13  
    7.14  defs
    7.15    
     8.1 --- a/src/ZF/ROOT.ML	Wed Dec 19 11:07:38 2001 +0100
     8.2 +++ b/src/ZF/ROOT.ML	Wed Dec 19 11:13:27 2001 +0100
     8.3 @@ -21,7 +21,7 @@
     8.4  use "~~/src/Provers/Arith/cancel_numerals.ML";
     8.5  use "~~/src/Provers/Arith/combine_numerals.ML";
     8.6  
     8.7 -with_path "Integ" use_thy "Main";
     8.8 +with_path "Integ" use_thy "Main_ZFC";
     8.9  simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
    8.10  
    8.11  print_depth 8;
     9.1 --- a/src/ZF/UNITY/WFair.thy	Wed Dec 19 11:07:38 2001 +0100
     9.2 +++ b/src/ZF/UNITY/WFair.thy	Wed Dec 19 11:13:27 2001 +0100
     9.3 @@ -10,7 +10,7 @@
     9.4  Theory ported from HOL.
     9.5  *)
     9.6  
     9.7 -WFair = UNITY +
     9.8 +WFair = UNITY + Main_ZFC + 
     9.9  constdefs
    9.10    
    9.11    (* This definition specifies weak fairness.  The rest of the theory
    10.1 --- a/src/ZF/ZF.thy	Wed Dec 19 11:07:38 2001 +0100
    10.2 +++ b/src/ZF/ZF.thy	Wed Dec 19 11:13:27 2001 +0100
    10.3 @@ -153,8 +153,10 @@
    10.4    "@Collect"  :: [pttrn, i, o] => i        ("(1{_ \\<in> _ ./ _})")
    10.5    "@Replace"  :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _ \\<in> _, _})")
    10.6    "@RepFun"   :: [i, pttrn, i] => i        ("(1{_ ./ _ \\<in> _})" [51,0,51])
    10.7 +  "@UNION"    :: [pttrn, i, i] => i        ("(3\\<Union>_\\<in>_./ _)" 10)
    10.8    "@INTER"    :: [pttrn, i, i] => i        ("(3\\<Inter>_\\<in>_./ _)" 10)
    10.9 -  "@UNION"    :: [pttrn, i, i] => i        ("(3\\<Union>_\\<in>_./ _)" 10)
   10.10 +  Union       :: i =>i                     ("\\<Union>_" [90] 90)
   10.11 +  Inter       :: i =>i                     ("\\<Inter>_" [90] 90)
   10.12    "@PROD"     :: [pttrn, i, i] => i        ("(3\\<Pi>_\\<in>_./ _)" 10)
   10.13    "@SUM"      :: [pttrn, i, i] => i        ("(3\\<Sigma>_\\<in>_./ _)" 10)
   10.14    "@lam"      :: [pttrn, i, i] => i        ("(3\\<lambda>_\\<in>_./ _)" 10)
   10.15 @@ -274,4 +276,3 @@
   10.16    [(*("split", split_tr'),*)
   10.17     ("Pi",    dependent_tr' ("@PROD", "op ->")),
   10.18     ("Sigma", dependent_tr' ("@SUM", "op *"))];
   10.19 -
    11.1 --- a/src/ZF/simpdata.ML	Wed Dec 19 11:07:38 2001 +0100
    11.2 +++ b/src/ZF/simpdata.ML	Wed Dec 19 11:13:27 2001 +0100
    11.3 @@ -104,8 +104,7 @@
    11.4  val Rep_simps = map prover
    11.5      ["{x. y:0, R(x,y)} = 0",	(*Replace*)
    11.6       "{x:0. P(x)} = 0",		(*Collect*)
    11.7 -     "{x:A. False} = 0",
    11.8 -     "{x:A. True} = A",
    11.9 +     "{x:A. P} = (if P then A else 0)",
   11.10       "RepFun(0,f) = 0",		(*RepFun*)
   11.11       "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
   11.12       "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
    12.1 --- a/src/ZF/subset.ML	Wed Dec 19 11:07:38 2001 +0100
    12.2 +++ b/src/ZF/subset.ML	Wed Dec 19 11:13:27 2001 +0100
    12.3 @@ -53,6 +53,10 @@
    12.4  by (REPEAT (ares_tac prems 1)) ;
    12.5  qed "succ_subsetE";
    12.6  
    12.7 +Goalw [succ_def] "succ(a) <= B <-> (a <= B & a : B)";
    12.8 +by (Blast_tac 1) ;
    12.9 +qed "succ_subset_iff";
   12.10 +
   12.11  (*** singletons ***)
   12.12  
   12.13  Goal "a:C ==> {a} <= C";