# HG changeset patch
# User lcp
# Date 796642787 -7200
# Node ID 547931cbbf085c97c8d99326a1394522479551cd
# Parent  9ec3c7bd774e1f8ba09c14b6502333fae5b75469
New example of AC Equivalences by Krzysztof Grabczewski

diff -r 9ec3c7bd774e -r 547931cbbf08 src/ZF/AC/AC_Equiv.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC_Equiv.ML	Fri Mar 31 11:39:47 1995 +0200
@@ -0,0 +1,114 @@
+(*  Title: 	ZF/AC/AC_Equiv.ML
+    ID:         $Id$
+    Author: 	Krzysztof Gr`abczewski
+
+*)
+
+
+open AC_Equiv;
+
+val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def];
+
+(* ******************************************** *)
+
+(* Theorems analogous to ones presented in "ZF/Ordinal.ML" *)
+
+(* lemma for nat_le_imp_lepoll *)
+val [prem] = goalw Cardinal.thy [lepoll_def]
+             "m:nat ==> ALL n: nat. m le n --> m lepoll n";
+by (nat_ind_tac "m" [prem] 1);
+by (fast_tac (ZF_cs addSIs [le_imp_subset RS id_subset_inj]) 1);
+by (rtac ballI 1);
+by (eres_inst_tac [("n","n")] natE 1);
+by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1);
+by (fast_tac (ZF_cs addSDs [le0D]) 1);
+by (fast_tac (ZF_cs addSIs [le_imp_subset RS id_subset_inj]) 1);
+val nat_le_imp_lepoll_lemma = result();
+
+(* used in : AC10-AC15.ML WO1-WO6.ML WO6WO1.ML*)
+val nat_le_imp_lepoll = nat_le_imp_lepoll_lemma RS bspec RS mp |> standard;
+
+(* ********************************************************************** *)
+(*             lemmas concerning FOL and pure ZF theory                   *)
+(* ********************************************************************** *)
+
+(* The following two theorms are useful when rewriting only one instance  *) 
+(* of a definition							  *)
+(* first one for definitions of formulae and the second for terms	  *)
+
+val prems = goal ZF.thy "(A == B) ==> A <-> B";
+by (asm_simp_tac (ZF_ss addsimps prems) 1);
+val def_imp_iff = result();
+
+val prems = goal ZF.thy "(A == B) ==> P(A) <-> P(B)";
+by (asm_simp_tac (ZF_ss addsimps prems) 1);
+val def_imp_iff_P = result();
+
+(* used only in lemmas4-7.ML *)
+(*Note modified statement and proof*)
+goal ZF.thy "!!X. X~=0 ==> (A->X)~=0";
+by (fast_tac (ZF_cs addSIs [equals0I,lam_type] addSEs [equals0D]) 1);
+val fun_space_not0I = result();
+
+(* used only in WO1_DC.ML *)
+(*Note simpler proof*)
+goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg;  \
+\         A<=Df; A<=Dg |] ==> f``A=g``A";
+by (asm_simp_tac (ZF_ss addsimps [image_fun]) 1);
+val images_eq = result();
+
+(* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *)
+(*I don't know where to put this one.*)
+goal Cardinal.thy
+     "!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m";
+by (resolve_tac [not_emptyE] 1 THEN (atac 1));
+by (forward_tac [singleton_subsetI] 1);
+by (forward_tac [subsetD] 1 THEN (atac 1));
+by (res_inst_tac [("A2","A")] 
+     (diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 
+    THEN (REPEAT (atac 2)));
+by (fast_tac ZF_cs 1);
+val Diff_lepoll = result();
+
+(* ********************************************************************** *)
+(*              lemmas concerning lepoll and eqpoll relations             *)
+(* ********************************************************************** *)
+
+(* ********************************************************************** *)
+(*                    Theorems concerning ordinals                        *)
+(* ********************************************************************** *)
+
+(* lemma for ordertype_Int *)
+goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A";
+by (resolve_tac [equalityI] 1);
+by (step_tac ZF_cs 1);
+by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1
+    THEN (atac 1));
+by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1
+    THEN (REPEAT (atac 1)));
+by (fast_tac (ZF_cs addIs [id_conv RS ssubst]) 1);
+val rvimage_id = result();
+
+(* used only in Hartog.ML *)
+goal Cardinal.thy
+	"!!A r. well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)";
+by (res_inst_tac [("P","%a. ordertype(A,a)=ordertype(A,r)")] 
+    (rvimage_id RS subst) 1);
+by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1);
+val ordertype_Int = result();
+
+(* used only in WO6WO1.ML *)
+(* corrected according to LCP'a advise *)
+goal Cardinal.thy 
+      "!!i j k. [| k < i++j; Ord(i); Ord(j) |] ==>  \
+\                  k<i | (EX! l. l<j & k = i++l)";
+by (dresolve_tac [lt_oadd_disj] 1 THEN (REPEAT (atac 1)));
+by (fast_tac (ZF_cs addIs [ex1I, ltI] addSEs [oadd_inject RS sym, lt_Ord]
+		addEs [Ord_in_Ord]) 1);
+val lt_oadd_disj1 = result();
+
+(* used only in AC16_lemmas.ML *)
+goalw CardinalArith.thy [InfCard_def]
+	"!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)";
+by (asm_simp_tac (ZF_ss addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1);
+val Inf_Card_is_InfCard = result();
diff -r 9ec3c7bd774e -r 547931cbbf08 src/ZF/AC/AC_Equiv.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC_Equiv.thy	Fri Mar 31 11:39:47 1995 +0200
@@ -0,0 +1,195 @@
+(*  Title: 	ZF/AC/AC_Equiv.thy
+    ID:         $Id$
+    Author: 	Krzysztof Gr`abczewski
+
+Axioms AC1 -- AC19 come from "Equivalents of the Axiom of Choice, II"
+by H. Rubin and J.E. Rubin, 1985.
+
+Axiom AC0 comes from "Axiomatic Set Theory" by P. Suppes, 1972.
+
+Some Isabelle proofs of equivalences of these axioms are formalizations of
+proofs presented by Rubin.  The others are based on Rubin's proofs, but
+slightly changed.
+*)
+
+AC_Equiv = CardinalArith + Univ + Transrec2 + 
+
+consts
+  
+(* Well Ordering Theorems *)
+  WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: "o"
+  WO4                               :: "i => o"
+
+(* Axioms of Choice *)  
+  AC0, AC1, AC2, AC3, AC4, AC5, AC6, AC7, AC8, AC9,
+  AC11, AC12, AC14, AC15, AC17, AC18, AC19 :: "o"
+  AC10, AC13              :: "i => o"
+  AC16                    :: "[i, i] => o"
+  
+(* Auxiliary definitions used in theorems *)
+  first                   :: "[i, i, i] => o"
+  exists_first            :: "[i, i] => o"
+  pairwise_disjoint       :: "i => o"
+  sets_of_size_between    :: "[i, i, i] => o"
+
+(* Auxiliary definitions used in proofs *)
+  NN                      :: "i => i"
+  uu                      :: "[i, i, i, i] => i"
+  
+(* Other useful definitions *)
+  vv1                     :: "[i, i, i] => i"
+  ww1                     :: "[i, i, i] => i"
+  vv2                     :: "[i, i, i, i] => i"
+  ww2                     :: "[i, i, i, i] => i"
+
+  GG                      :: "[i, i, i] => i"
+  GG2                     :: "[i, i, i] => i"
+  HH                      :: "[i, i, i] => i"
+
+  recfunAC16              :: "[i, i, i, i] => i"
+
+defs
+
+(* Well Ordering Theorems *)
+
+  WO1_def "WO1 == ALL A. EX R. well_ord(A,R)"
+
+  WO2_def "WO2 == ALL A. EX a. Ord(a) & A eqpoll a"
+
+  WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
+
+  WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &   \
+\	             (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
+
+  WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
+
+  WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a   \
+\	            & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
+
+  WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->   \
+\	            well_ord(A,converse(R)))"
+
+  WO8_def "WO8 == ALL A. (0~:A --> (EX f. f : (PROD X:A. X))) -->  \
+\	            (EX R. well_ord(A,R))"
+
+(* Axioms of Choice *)  
+
+  AC0_def "AC0 == ALL A. EX f. f:(PROD X:Pow(A)-{0}. X)"
+
+  AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
+
+  AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)   \
+\	            --> (EX C. ALL B:A. EX y. B Int C = {y})"
+
+  AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
+
+  AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
+
+  AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.   \
+\	            ALL x:domain(g). f`(g`x) = x"
+
+  AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
+
+  AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)   \
+\	            --> (PROD B:A. B)~=0"
+
+  AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)   \
+\	            --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
+
+  AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->   \
+\	            (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
+
+  AC10_def "AC10(n) ==  ALL A. (ALL B:A. ~Finite(B)) -->   \
+\	            (EX f. ALL B:A. (pairwise_disjoint(f`B) &   \
+\	            sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
+
+  AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
+
+  AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->   \
+\	    (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &   \
+\	    sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
+
+  AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &   \
+\	                                  f`B <= B & f`B lepoll m)"
+
+  AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
+
+  AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.   \
+\	                              f`B~=0 & f`B <= B & f`B lepoll m))"
+
+  AC16_def "AC16(n, k)  == ALL A. ~Finite(A) -->   \
+\	    (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &   \
+\	    (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
+
+  AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.   \
+\	            EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
+
+(***problems!  X is free, and is higher-order!
+  AC18_def "AC18 == ALL A. A~=0 --> (ALL F. (domain(F) = A &   \
+\	            (ALL a:A. F`a ~= 0)) -->   \
+\	            ((INT a:A. UN b:F`a. X(a,b)) =   \
+\	            (UN f: PROD a:A. F`a. INT a:A. X(a, f`a))))"
+***)
+
+  AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =   \
+\	            (UN f:{f: A->Union(A). ALL B:A. f`B:B}. INT a:A. f`a))"
+
+(* Auxiliary definitions used in theorems *)
+
+  first_def                "first(u, X, R)   \
+\			    == u:X & (ALL v:X. v~=u --> <u,v> : R)"
+
+  exists_first_def         "exists_first(X,R)   \
+\			    == EX u:X. first(u, X, R)"
+
+  pairwise_disjoint_def    "pairwise_disjoint(A)   \
+\			    == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
+
+  sets_of_size_between_def "sets_of_size_between(A,m,n)   \
+\			    == ALL B:A. m lepoll B & B lepoll n"
+  
+(* Auxiliary definitions used in proofs *)
+
+  NN_def                  "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a \
+\			   & (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
+
+  uu_def                  "uu(f, beta, gamma, delta)   \
+\			   == (f`beta * f`gamma) Int f`delta"
+  
+(* Other useful definitions *)
+
+  vv1_def "vv1(f,b,m) == if(f`b ~= 0,   \
+\          domain(uu(f,b,   \
+\          LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &   \
+\	   domain(uu(f,b,g,d)) lesspoll m)),   \
+\          LEAST d. domain(uu(f,b,   \
+\          LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &   \
+\	   domain(uu(f,b,g,d)) lesspoll m)), d)) ~= 0 &   \
+\          domain(uu(f,b,   \
+\          LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &   \
+\	   domain(uu(f,b,g,d)) lesspoll m)), d)) lesspoll m)), 0)"
+
+  ww1_def "ww1(f,b,m) == f`b - vv1(f,b,m)"
+
+  vv2_def "vv2(f,b,g,s) ==   \
+\	   if(f`g ~= 0, {uu(f,b,g,LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
+
+  ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
+
+  GG_def  "GG(f,x,a)  == transrec(a, %b r. (lam z:Pow(x).   \
+\	                 if(z=0, x, f`z))`(x - {r`c. c:b}))"
+
+  GG2_def "GG2(f,x,a) == transrec(a, %b r. (lam z:Pow(x).   \
+\	                 if(z=0, {x}, f`z))`(x - Union({r`c. c:b})))"
+
+  HH_def  "HH(f,x,a)  == transrec(a, %b r. (lam z:Pow(x).   \
+\	                 if(z=0|f`z~:z, x, f`z))`(x - {r`c. c:b}))"
+
+  recfunAC16_def
+    "recfunAC16(f,fa,i,a) ==   \
+\	 transrec2(i, 0,   \
+\	      %g r. if(EX y:r. fa`g <= y, r,   \
+\		       r Un {f`(LEAST i. fa`g <= f`i &   \
+\		       (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
+
+end
diff -r 9ec3c7bd774e -r 547931cbbf08 src/ZF/AC/OrdQuant.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/OrdQuant.ML	Fri Mar 31 11:39:47 1995 +0200
@@ -0,0 +1,124 @@
+(*
+  file OrdQuant.ML
+
+  Proofs concerning special instances of quantifiers and union operator.
+  Very useful when proving theorems about ordinals. 
+*)
+
+open OrdQuant;
+
+(*** universal quantifier for ordinals ***)
+
+qed_goalw "oallI" OrdQuant.thy [Oall_def]
+    "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"
+ (fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]);
+
+qed_goalw "ospec" OrdQuant.thy [Oall_def]
+    "[| ALL x<A. P(x);  x<A |] ==> P(x)"
+ (fn major::prems=>
+  [ (rtac (major RS spec RS mp) 1),
+    (resolve_tac prems 1) ]);
+
+qed_goalw "oallE" OrdQuant.thy [Oall_def]
+    "[| ALL x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q"
+ (fn major::prems=>
+  [ (rtac (major RS allE) 1),
+    (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
+
+qed_goal "rev_oallE" OrdQuant.thy
+    "[| ALL x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q"
+ (fn major::prems=>
+  [ (rtac (major RS oallE) 1),
+    (REPEAT (eresolve_tac prems 1)) ]);
+
+(*Trival rewrite rule;   (ALL x<a.P)<->P holds only if a is not 0!*)
+qed_goal "oall_simp" OrdQuant.thy "(ALL x<a. True) <-> True"
+ (fn _=> [ (REPEAT (ares_tac [TrueI,oallI,iffI] 1)) ]);
+
+(*Congruence rule for rewriting*)
+qed_goalw "oall_cong" OrdQuant.thy [Oall_def]
+    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> Oall(a,P) <-> Oall(a',P')"
+ (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
+
+
+(*** existential quantifier for ordinals ***)
+
+qed_goalw "oexI" OrdQuant.thy [Oex_def]
+    "[| P(x);  x<A |] ==> EX x<A. P(x)"
+ (fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]);
+
+(*Not of the general form for such rules; ~EX has become ALL~ *)
+qed_goal "oexCI" OrdQuant.thy 
+   "[| ALL x<A. ~P(x) ==> P(a);  a<A |] ==> EX x<A.P(x)"
+ (fn prems=>
+  [ (rtac classical 1),
+    (REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ]);
+
+qed_goalw "oexE" OrdQuant.thy [Oex_def]
+    "[| EX x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q \
+\    |] ==> Q"
+ (fn major::prems=>
+  [ (rtac (major RS exE) 1),
+    (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);
+
+qed_goalw "oex_cong" OrdQuant.thy [Oex_def]
+    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) \
+\    |] ==> Oex(a,P) <-> Oex(a',P')"
+ (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
+
+
+(*** Rules for Unions ***)
+
+(*The order of the premises presupposes that a is rigid; A may be flexible*)
+qed_goal "OUnionI" OrdQuant.thy "[| b<a;  A: B(b) |] ==> A: OUnion(a, %z. B(z))"
+ (fn prems=>
+  [ (resolve_tac [OUnion_iff RS iffD2] 1),
+    (REPEAT (resolve_tac (prems @ [oexI]) 1)) ]);
+
+qed_goal "OUnionE" OrdQuant.thy
+    "[| A : OUnion(a, %z. B(z));  !!b.[| A: B(b);  b<a |] ==> R |] ==> R"
+ (fn prems=>
+  [ (resolve_tac [OUnion_iff RS iffD1 RS oexE] 1),
+    (REPEAT (ares_tac prems 1)) ]);
+
+
+
+
+(*** Rules for Unions of families ***)
+(* UN x<a. B(x) abbreviates OUnion(a, %x. B(x)) *)
+
+qed_goalw "OUN_iff" OrdQuant.thy [Oex_def]
+    "b : (UN x<a. B(x)) <-> (EX x<a. b : B(x))"
+ (fn _=> [ (fast_tac (FOL_cs addIs [OUnionI] 
+                             addSEs [OUnionE]) 1) ]);
+
+(*The order of the premises presupposes that a is rigid; b may be flexible*)
+qed_goal "OUN_I" OrdQuant.thy "[| c<a;  b: B(c) |] ==> b: (UN x<a. B(x))"
+ (fn prems=>
+  [ (REPEAT (resolve_tac (prems@[OUnionI]) 1)) ]);
+
+qed_goal "OUN_E" OrdQuant.thy
+    "[| b : (UN x<a. B(x));  !!x.[| x<a;  b: B(x) |] ==> R |] ==> R"
+ (fn major::prems=>
+  [ (rtac (major RS OUnionE) 1),
+    (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]);
+
+val prems = goal thy "[| a=b;  !!x. x<b ==> f(x)=g(x) |] ==> OUnion(a,f) = OUnion(b,g)";
+by (resolve_tac [OUnion_iff RS iff_sym RSN (2, OUnion_iff RS iff_trans RS iff_trans) RS equality_iffI] 1);
+by (resolve_tac [oex_cong] 1);
+by (resolve_tac prems 1);
+by (dresolve_tac prems 1);
+by (fast_tac (ZF_cs addSEs [equalityE]) 1);
+qed "OUnion_cong";
+
+val OrdQuant_cs = ZF_cs
+  addSIs [oallI]
+  addIs [oexI, OUnionI]
+  addSEs [oexE, OUnionE]
+  addEs [rev_oallE];
+
+val OrdQuant_ss = ZF_ss addsimps [oall_simp, ltD RS beta]
+                        addcongs [oall_cong, OUnion_cong];
+
+
+