# HG changeset patch # User paulson # Date 876842581 -7200 # Node ID 6f389875ab33c30e9b33c507aea184bd1c42ac7a # Parent 834ed1471732d6b4d6847dba5bd55e7f8dafe885 Patch to avoid simplification of ~EX to ALL~ Also some better indentation diff -r 834ed1471732 -r 6f389875ab33 src/ZF/AC/DC.ML --- a/src/ZF/AC/DC.ML Tue Oct 14 13:59:12 1997 +0200 +++ b/src/ZF/AC/DC.ML Tue Oct 14 17:23:01 1997 +0200 @@ -210,35 +210,36 @@ by (fast_tac (!claset addss (!simpset)) 1); qed "DC0_DC_nat"; -(* ********************************************************************** *) -(* DC(omega) ==> DC *) -(* *) -(* The scheme of the proof: *) -(* *) -(* Assume DC(omega). Let R and x satisfy the premise of DC. *) -(* *) -(* Define XX and RR as follows: *) -(* *) -(* XX = (UN n:nat. *) -(* {f:succ(n)->domain(R). ALL k:n. : R}) *) -(* RR = {:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) *) -(* & (ALL f:z1. restrict(z2, domain(f)) = f)) | *) -(* (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f)) *) -(* & (ALL f:z1. restrict(g, domain(f)) = f)) & *) -(* z2={<0,x>})} *) -(* *) -(* Then XX and RR satisfy the hypotheses of DC(omega). *) -(* So applying DC: *) -(* *) -(* EX f:nat->XX. ALL n:nat. f``n RR f`n *) -(* *) -(* Thence *) -(* *) -(* ff = {. n:nat} *) -(* *) -(* is the desired function. *) -(* *) -(* ********************************************************************** *) +(* ************************************************************************ + DC(omega) ==> DC + + The scheme of the proof: + + Assume DC(omega). Let R and x satisfy the premise of DC. + + Define XX and RR as follows: + + XX = (UN n:nat. {f:succ(n)->domain(R). ALL k:n. : R}) + + RR = {:Fin(XX)*XX. + (domain(z2)=succ(UN f:z1. domain(f)) & + (ALL f:z1. restrict(z2, domain(f)) = f)) | + (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f)) & + (ALL f:z1. restrict(g, domain(f)) = f)) & + z2={<0,x>})} + + Then XX and RR satisfy the hypotheses of DC(omega). + So applying DC: + + EX f:nat->XX. ALL n:nat. f``n RR f`n + + Thence + + ff = {. n:nat} + + is the desired function. + +************************************************************************* *) goalw thy [lesspoll_def, Finite_def] "!!A. A lesspoll nat ==> Finite(A)"; @@ -304,7 +305,7 @@ by (swap_res_tac [bexI] 1 THEN etac singleton_in_funs 2); by (asm_full_simp_tac (!simpset addsimps [nat_0I RSN (2, bexI), cons_fun_type2, empty_fun]) 1); -val lemma1 = result(); +val lemma4 = result(); goal thy "!!f. [| f:nat->X; n:nat |] ==> \ \ (UN x:f``succ(n). P(x)) = P(f`n) Un (UN x:f``n. P(x))"; @@ -376,10 +377,11 @@ goal thy "!!X.[| ALL b : \ -\ {:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \ -\ & (ALL f:z1. restrict(z2, domain(f)) = f)) | \ -\ (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f)) \ -\ & (ALL f:z1. restrict(g, domain(f)) = f)) & z2={<0,x>})}; \ +\ {:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) & \ +\ (ALL f:z1. restrict(z2, domain(f)) = f)) | \ +\ (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f)) & \ +\ (ALL f:z1. restrict(g, domain(f)) = f)) & \ +\ z2={<0,x>})}; \ \ XX = (UN n:nat. \ \ {f:succ(n)->domain(R). ALL k:n. : R}); \ \ f: nat -> XX; range(R) <= domain(R); x:domain(R) \ @@ -392,10 +394,11 @@ by (etac nat_induct 1); by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); by (fast_tac (FOL_cs addss - (!simpset addsimps [image_0, singleton_fun RS domain_of_fun, + (!simpset addsimps [singleton_fun RS domain_of_fun, singleton_0, singleton_in_funs])) 1); (*induction step*) (** LEVEL 5 **) -by (Full_simp_tac 1); +by (full_simp_tac (*prevent simplification of ~EX to ALL~*) + (FOL_ss addsimps [separation, split]) 1); by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 THEN (assume_tac 1)); by (REPEAT (eresolve_tac [conjE, disjE] 1)); @@ -411,6 +414,7 @@ by (etac domainE 1); by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1)); + by (rtac bexI 1); by (etac nat_succI 2); by (res_inst_tac [("x","cons(, f`xa)")] bexI 1); @@ -451,13 +455,14 @@ by (fast_tac (FOL_cs addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 1); val lemma2 = result(); -goal thy "!!n. [| XX = (UN n:nat. \ -\ {f:succ(n)->domain(R). ALL k:n. : R}); \ +goal thy +"!!n. [| XX = (UN n:nat. \ +\ {f:succ(n)->domain(R). ALL k:n. : R}); \ \ ALL b : \ -\ {:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \ +\ {:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f)) \ \ & (UN f:z1. domain(f)) = b \ \ & (ALL f:z1. restrict(z2, domain(f)) = f))}; \ -\ f : nat -> XX; n:nat; range(R) <= domain(R); x:domain(R) \ +\ f : nat -> XX; n:nat; range(R) <= domain(R); x:domain(R) \ \ |] ==> f`n`n = f`succ(n)`n"; by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1 THEN REPEAT (assume_tac 1)); @@ -472,10 +477,11 @@ addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); val lemma3 = result(); + goalw thy [DC_def, DC0_def] "!!Z. DC(nat) ==> DC0"; by (REPEAT (resolve_tac [allI, impI] 1)); by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1)); -by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 +by (eresolve_tac [[refl, refl] MRS lemma4 RSN (2, impE)] 1 THEN REPEAT (assume_tac 1)); by (etac bexE 1); by (dresolve_tac [refl RSN (2, simplify_recursion)] 1 @@ -499,7 +505,7 @@ "!!A. [| ~ A lesspoll B; C lesspoll B |] ==> A - C ~= 0"; by (fast_tac (!claset addSDs [Diff_eq_0_iff RS iffD1 RS subset_imp_lepoll] addSIs [eqpollI] addEs [notE] addSEs [eqpollE, lepoll_trans]) 1); -val lemma1 = result(); +val lesspoll_lemma = result(); val [f_type, Ord_a, not_eq] = goalw thy [inj_def] "[| f:a->X; Ord(a); (!!b c. [| b f`b~=f`c) \ @@ -529,7 +535,7 @@ \ lesspoll Hartog(A) & z2 ~: z1}")] allE 1); by (Asm_full_simp_tac 1); by (etac impE 1); -by (fast_tac (!claset addEs [lemma1 RS not_emptyE]) 1); +by (fast_tac (!claset addEs [lesspoll_lemma RS not_emptyE]) 1); by (etac bexE 1); by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2)) RS (HartogI RS notE)] 1);