# HG changeset patch # User lcp # Date 772212034 -7200 # Node ID ca5356bd315a140dc6ff92b9fb2de8210944ad17 # Parent 89d45187f04dbddcb46f4a6650af7e137e0e5dd5 Addition of cardinals and order types, various tidying diff -r 89d45187f04d -r ca5356bd315a src/ZF/Arith.ML --- a/src/ZF/Arith.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Arith.ML Tue Jun 21 17:20:34 1994 +0200 @@ -42,7 +42,7 @@ (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ])))); val rec_type = result(); -val nat_le_refl = naturals_are_ordinals RS le_refl; +val nat_le_refl = nat_into_Ord RS le_refl; val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat]; @@ -113,7 +113,7 @@ by (ALLGOALS (asm_simp_tac (nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, - diff_succ_succ, naturals_are_ordinals])))); + diff_succ_succ, nat_into_Ord])))); val diff_le_self = result(); (*** Simplification over add, mult, diff ***) @@ -150,12 +150,21 @@ (*Commutative law for addition*) val add_commute = prove_goal Arith.thy - "[| m:nat; n:nat |] ==> m #+ n = n #+ m" - (fn prems=> - [ (nat_ind_tac "n" prems 1), + "!!m n. [| m:nat; n:nat |] ==> m #+ n = n #+ m" + (fn _ => + [ (nat_ind_tac "n" [] 1), (ALLGOALS - (asm_simp_tac - (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]); + (asm_simp_tac (arith_ss addsimps [add_0_right, add_succ_right]))) ]); + +val add_left_commute = prove_goal Arith.thy + "!!m n k. [| m:nat; n:nat; k:nat |] ==> m#+(n#+k)=n#+(m#+k)" + (fn _ => [rtac (add_commute RS trans) 1, + rtac (add_assoc RS trans) 3, + rtac (add_commute RS subst_context) 4, + REPEAT (ares_tac [add_type] 1)]); + +(*Addition is an AC-operator*) +val add_ac = [add_assoc, add_commute, add_left_commute]; (*Cancellation law on the left*) val [knat,eqn] = goal Arith.thy @@ -170,20 +179,17 @@ (*right annihilation in product*) val mult_0_right = prove_goal Arith.thy - "m:nat ==> m #* 0 = 0" - (fn prems=> - [ (nat_ind_tac "m" prems 1), - (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); + "!!m. m:nat ==> m #* 0 = 0" + (fn _=> + [ (nat_ind_tac "m" [] 1), + (ALLGOALS (asm_simp_tac arith_ss)) ]); (*right successor law for multiplication*) val mult_succ_right = prove_goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)" - (fn _=> + (fn _ => [ (nat_ind_tac "m" [] 1), - (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))), - (*The final goal requires the commutative law for addition*) - (rtac (add_commute RS subst_context) 1), - (REPEAT (assume_tac 1)) ]); + (ALLGOALS (asm_simp_tac (arith_ss addsimps add_ac))) ]); (*Commutative law for multiplication*) val mult_commute = prove_goal Arith.thy @@ -202,12 +208,11 @@ (*Distributive law on the left; requires an extra typing premise*) val add_mult_distrib_left = prove_goal Arith.thy - "[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)" + "!!m. [| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)" (fn prems=> - let val mult_commute' = read_instantiate [("m","k")] mult_commute - val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems) - in [ (simp_tac ss 1) ] - end); + [ (nat_ind_tac "m" [] 1), + (asm_simp_tac (arith_ss addsimps [mult_0_right]) 1), + (asm_simp_tac (arith_ss addsimps ([mult_succ_right] @ add_ac)) 1) ]); (*Associative law for multiplication*) val mult_assoc = prove_goal Arith.thy @@ -261,9 +266,9 @@ val div_rls = (*for mod and div*) nat_typechecks @ [Ord_transrec_type, apply_type, div_termination RS ltD, if_type, - naturals_are_ordinals, not_lt_iff_le RS iffD1]; + nat_into_Ord, not_lt_iff_le RS iffD1]; -val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD, +val div_ss = ZF_ss addsimps [nat_into_Ord, div_termination RS ltD, not_lt_iff_le RS iffD2]; (*Type checking depends upon termination!*) @@ -311,7 +316,7 @@ by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2); (*case n le x*) by (asm_full_simp_tac - (arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals, + (arith_ss addsimps [not_lt_iff_le, nat_into_Ord, mod_geq, div_geq, add_assoc, div_termination RS ltD, add_diff_inverse]) 1); val mod_div_equality = result(); @@ -350,7 +355,7 @@ val add_lt_mono = result(); (*A [clumsy] way of lifting < monotonicity to le monotonicity *) -val lt_mono::ford::prems = goal Ord.thy +val lt_mono::ford::prems = goal Ordinal.thy "[| !!i j. [| i f(i) < f(j); \ \ !!i. i:k ==> Ord(f(i)); \ \ i le j; j:k \ @@ -363,7 +368,7 @@ goal Arith.thy "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k"; by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1); -by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1)); +by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1)); val add_le_mono1 = result(); (* le monotonicity, BOTH arguments*) diff -r 89d45187f04d -r ca5356bd315a src/ZF/Cardinal.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Cardinal.ML Tue Jun 21 17:20:34 1994 +0200 @@ -0,0 +1,352 @@ +(* Title: ZF/Cardinal.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Cardinals in Zermelo-Fraenkel Set Theory + +This theory does NOT assume the Axiom of Choice +*) + +open Cardinal; + +(*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***) + +(** Lemma: Banach's Decomposition Theorem **) + +goal Cardinal.thy "bnd_mono(X, %W. X - g``(Y - f``W))"; +by (rtac bnd_monoI 1); +by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1)); +val decomp_bnd_mono = result(); + +val [gfun] = goal Cardinal.thy + "g: Y->X ==> \ +\ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \ +\ X - lfp(X, %W. X - g``(Y - f``W)) "; +by (res_inst_tac [("P", "%u. ?v = X-u")] + (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1); +by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, + gfun RS fun_is_rel RS image_subset]) 1); +val Banach_last_equation = result(); + +val prems = goal Cardinal.thy + "[| f: X->Y; g: Y->X |] ==> \ +\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \ +\ (YA Int YB = 0) & (YA Un YB = Y) & \ +\ f``XA=YA & g``YB=XB"; +by (REPEAT + (FIRSTGOAL + (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition]))); +by (rtac Banach_last_equation 3); +by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1)); +val decomposition = result(); + +val prems = goal Cardinal.thy + "[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)"; +by (cut_facts_tac prems 1); +by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1); +by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un] + addIs [bij_converse_bij]) 1); +(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))" + is forced by the context!! *) +val schroeder_bernstein = result(); + + +(** Equipollence is an equivalence relation **) + +goalw Cardinal.thy [eqpoll_def] "X eqpoll X"; +br exI 1; +br id_bij 1; +val eqpoll_refl = result(); + +goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X"; +by (fast_tac (ZF_cs addIs [bij_converse_bij]) 1); +val eqpoll_sym = result(); + +goalw Cardinal.thy [eqpoll_def] + "!!X Y. [| X eqpoll Y; Y eqpoll Z |] ==> X eqpoll Z"; +by (fast_tac (ZF_cs addIs [comp_bij]) 1); +val eqpoll_trans = result(); + +(** Le-pollence is a partial ordering **) + +goalw Cardinal.thy [lepoll_def] "!!X Y. X<=Y ==> X lepoll Y"; +br exI 1; +be id_subset_inj 1; +val subset_imp_lepoll = result(); + +val lepoll_refl = subset_refl RS subset_imp_lepoll; + +goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def] + "!!X Y. X eqpoll Y ==> X lepoll Y"; +by (fast_tac ZF_cs 1); +val eqpoll_imp_lepoll = result(); + +goalw Cardinal.thy [lepoll_def] + "!!X Y. [| X lepoll Y; Y lepoll Z |] ==> X lepoll Z"; +by (fast_tac (ZF_cs addIs [comp_inj]) 1); +val lepoll_trans = result(); + +(*Asymmetry law*) +goalw Cardinal.thy [lepoll_def,eqpoll_def] + "!!X Y. [| X lepoll Y; Y lepoll X |] ==> X eqpoll Y"; +by (REPEAT (etac exE 1)); +by (rtac schroeder_bernstein 1); +by (REPEAT (assume_tac 1)); +val eqpollI = result(); + +val [major,minor] = goal Cardinal.thy + "[| X eqpoll Y; [| X lepoll Y; Y lepoll X |] ==> P |] ==> P"; +br minor 1; +by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1)); +val eqpollE = result(); + +goal Cardinal.thy "X eqpoll Y <-> X lepoll Y & Y lepoll X"; +by (fast_tac (ZF_cs addIs [eqpollI] addSEs [eqpollE]) 1); +val eqpoll_iff = result(); + + +(** LEAST -- the least number operator [from HOL/Univ.ML] **) + +val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def] + "[| P(i); Ord(i); !!x. x ~P(x) |] ==> (LEAST x.P(x)) = i"; +by (rtac the_equality 1); +by (fast_tac (ZF_cs addSIs [premP,premOrd,premNot]) 1); +by (REPEAT (etac conjE 1)); +be (premOrd RS Ord_linear_lt) 1; +by (ALLGOALS (fast_tac (ZF_cs addSIs [premP] addSDs [premNot]))); +val Least_equality = result(); + +goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> P(LEAST x.P(x))"; +by (etac rev_mp 1); +by (trans_ind_tac "i" [] 1); +by (rtac impI 1); +by (rtac classical 1); +by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); +by (assume_tac 2); +by (fast_tac (ZF_cs addSEs [ltE]) 1); +val LeastI = result(); + +(*Proof is almost identical to the one above!*) +goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> (LEAST x.P(x)) le i"; +by (etac rev_mp 1); +by (trans_ind_tac "i" [] 1); +by (rtac impI 1); +by (rtac classical 1); +by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); +by (etac le_refl 2); +by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1); +val Least_le = result(); + +(*LEAST really is the smallest*) +goal Cardinal.thy "!!i. [| P(i); i < (LEAST x.P(x)) |] ==> Q"; +br (Least_le RSN (2,lt_trans2) RS lt_anti_refl) 1; +by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); +val less_LeastE = result(); + +goal Cardinal.thy "Ord(LEAST x.P(x))"; +by (res_inst_tac [("Q","EX i. Ord(i) & P(i)")] (excluded_middle RS disjE) 1); +by (safe_tac ZF_cs); +br (Least_le RS ltE) 2; +by (REPEAT_SOME assume_tac); +bw Least_def; +by (rtac (the_0 RS ssubst) 1 THEN rtac Ord_0 2); +by (fast_tac FOL_cs 1); +val Ord_Least = result(); + + +(** Basic properties of cardinals **) + +(*Not needed for simplification, but helpful below*) +val prems = goal Cardinal.thy + "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x.P(x)) = (LEAST x.Q(x))"; +by (simp_tac (FOL_ss addsimps prems) 1); +val Least_cong = result(); + +(*Need AC to prove X lepoll Y ==> |X| le |Y| ; see well_ord_lepoll_imp_le *) +goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|"; +br Least_cong 1; +by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1); +val cardinal_cong = result(); + +(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*) +goalw Cardinal.thy [eqpoll_def, cardinal_def] + "!!A. well_ord(A,r) ==> |A| eqpoll A"; +br LeastI 1; +be Ord_ordertype 2; +br exI 1; +be (ordertype_bij RS bij_converse_bij) 1; +val well_ord_cardinal_eqpoll = result(); + +val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll + |> standard; + +goal Cardinal.thy + "!!X Y. [| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y"; +br (eqpoll_sym RS eqpoll_trans) 1; +be well_ord_cardinal_eqpoll 1; +by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1); +val well_ord_cardinal_eqE = result(); + + +(** Observations from Kunen, page 28 **) + +goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> |i| le i"; +be (eqpoll_refl RS Least_le) 1; +val Ord_cardinal_le = result(); + +goalw Cardinal.thy [Card_def] "!!i. Card(i) ==> |i| = i"; +be sym 1; +val Card_cardinal_eq = result(); + +val prems = goalw Cardinal.thy [Card_def,cardinal_def] + "[| Ord(i); !!j. j ~(j eqpoll i) |] ==> Card(i)"; +br (Least_equality RS ssubst) 1; +by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1)); +val CardI = result(); + +goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)"; +be ssubst 1; +br Ord_Least 1; +val Card_is_Ord = result(); + +goalw Cardinal.thy [cardinal_def] "Ord( |i| )"; +br Ord_Least 1; +val Ord_cardinal = result(); + +(*Kunen's Lemma 10.5*) +goal Cardinal.thy "!!i j. [| |i| le j; j le i |] ==> |j| = |i|"; +br (eqpollI RS cardinal_cong) 1; +be (le_imp_subset RS subset_imp_lepoll) 1; +br lepoll_trans 1; +be (le_imp_subset RS subset_imp_lepoll) 2; +br (eqpoll_sym RS eqpoll_imp_lepoll) 1; +br Ord_cardinal_eqpoll 1; +by (REPEAT (eresolve_tac [ltE, Ord_succD] 1)); +val cardinal_eq_lemma = result(); + +goal Cardinal.thy "!!i j. i le j ==> |i| le |j|"; +by (res_inst_tac [("i","|i|"),("j","|j|")] Ord_linear_le 1); +by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI])); +br cardinal_eq_lemma 1; +ba 2; +be le_trans 1; +be ltE 1; +be Ord_cardinal_le 1; +val cardinal_mono = result(); + +(*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*) +goal Cardinal.thy "!!i j. [| |i| < |j|; Ord(i); Ord(j) |] ==> i < j"; +br Ord_linear2 1; +by (REPEAT_SOME assume_tac); +be (lt_trans2 RS lt_anti_refl) 1; +be cardinal_mono 1; +val cardinal_lt_imp_lt = result(); + +goal Cardinal.thy "!!i j. [| |i| < k; Ord(i); Card(k) |] ==> i < k"; +by (asm_simp_tac (ZF_ss addsimps + [cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1); +val Card_lt_imp_lt = result(); + + +(** The swap operator [NOT USED] **) + +goalw Cardinal.thy [swap_def] + "!!A. [| x:A; y:A |] ==> swap(A,x,y) : A->A"; +by (REPEAT (ares_tac [lam_type,if_type] 1)); +val swap_type = result(); + +goalw Cardinal.thy [swap_def] + "!!A. [| x:A; y:A; z:A |] ==> swap(A,x,y)`(swap(A,x,y)`z) = z"; +by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); +val swap_swap_identity = result(); + +goal Cardinal.thy "!!A. [| x:A; y:A |] ==> swap(A,x,y) : bij(A,A)"; +br nilpotent_imp_bijective 1; +by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2, + ballI, swap_swap_identity] 1)); +val swap_bij = result(); + +(*** The finite cardinals ***) + +(*Lemma suggested by Mike Fourman*) +val [prem] = goalw Cardinal.thy [inj_def] + "f: inj(succ(m), succ(n)) ==> (lam x:m. if(f`x=n, f`m, f`x)) : inj(m,n)"; +br CollectI 1; +(*Proving it's in the function space m->n*) +by (cut_facts_tac [prem] 1); +br (if_type RS lam_type) 1; +by (fast_tac (ZF_cs addSEs [mem_anti_refl] addEs [apply_funtype RS succE]) 1); +by (fast_tac (ZF_cs addSEs [mem_anti_refl] addEs [apply_funtype RS succE]) 1); +(*Proving it's injective*) +by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); +(*Adding prem earlier would cause the simplifier to loop*) +by (cut_facts_tac [prem] 1); +by (fast_tac (ZF_cs addSEs [mem_anti_refl]) 1); +val inj_succ_succD = result(); + +val [prem] = goalw Cardinal.thy [lepoll_def] + "m:nat ==> ALL n: nat. m lepoll n --> m le n"; +by (nat_ind_tac "m" [prem] 1); +by (fast_tac (ZF_cs addSIs [nat_0_le]) 1); +br 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 addSIs [succ_leI] addSDs [inj_succ_succD]) 1); +val nat_lepoll_imp_le_lemma = result(); +val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp |> standard; + +goal Cardinal.thy + "!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n"; +br iffI 1; +by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); +by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_asym] addSEs [eqpollE]) 1); +val nat_eqpoll_iff = result(); + +goalw Cardinal.thy [Card_def,cardinal_def] + "!!n. n: nat ==> Card(n)"; +br (Least_equality RS ssubst) 1; +by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl])); +by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1); +by (fast_tac (ZF_cs addSEs [lt_anti_refl]) 1); +val nat_into_Card = result(); + +val Card_0 = nat_0I RS nat_into_Card; + +(*Part of Kunen's Lemma 10.6*) +goal Cardinal.thy "!!n. [| succ(n) lepoll n; n:nat |] ==> P"; +br (nat_lepoll_imp_le RS lt_anti_refl) 1; +by (REPEAT (ares_tac [nat_succI] 1)); +val succ_lepoll_natE = result(); + + +(*** The first infinite cardinal: Omega, or nat ***) + +(*This implies Kunen's Lemma 10.6*) +goal Cardinal.thy "!!n. [| n ~ i lepoll n"; +br notI 1; +by (rtac succ_lepoll_natE 1 THEN assume_tac 2); +by (rtac lepoll_trans 1 THEN assume_tac 2); +be ltE 1; +by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1)); +val lt_not_lepoll = result(); + +goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)"; +br (Least_equality RS ssubst) 1; +by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl])); +be ltE 1; +by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1); +val Card_nat = result(); + +goal Cardinal.thy "!!i n. [| Ord(i); n:nat |] ==> i eqpoll n <-> i=n"; +br iffI 1; +by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); +by (rtac Ord_linear_lt 1); +by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord])); +by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN + REPEAT (assume_tac 1)); +by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1))); +be eqpoll_imp_lepoll 1; +val Ord_nat_eqpoll_iff = result(); + + diff -r 89d45187f04d -r ca5356bd315a src/ZF/Cardinal.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Cardinal.thy Tue Jun 21 17:20:34 1994 +0200 @@ -0,0 +1,33 @@ +(* Title: ZF/Cardinal.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Cardinals in Zermelo-Fraenkel Set Theory +*) + +Cardinal = OrderType + Fixedpt + Nat + Sum + +consts + Least :: "(i=>o) => i" (binder "LEAST " 10) + eqpoll, lepoll :: "[i,i] => o" (infixl 50) + "cardinal" :: "i=>i" ("|_|") + Card :: "i=>o" + + swap :: "[i,i,i]=>i" (*not used; useful??*) + +rules + + (*least ordinal operator*) + Least_def "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j ~P(j))" + + eqpoll_def "A eqpoll B == EX f. f: bij(A,B)" + + lepoll_def "A lepoll B == EX f. f: inj(A,B)" + + cardinal_def "|A| == LEAST i. i eqpoll A" + + Card_def "Card(i) == ( i = |i| )" + + swap_def "swap(A,x,y) == (lam z:A. if(z=x, y, if(z=y, x, z)))" + +end diff -r 89d45187f04d -r ca5356bd315a src/ZF/Fin.ML --- a/src/ZF/Fin.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Fin.ML Tue Jun 21 17:20:34 1994 +0200 @@ -1,12 +1,10 @@ -(* Title: ZF/ex/fin.ML +(* Title: ZF/ex/Fin.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Finite powerset operator -could define cardinality? - prove X:Fin(A) ==> EX n:nat. EX f. f:bij(X,n) card(0)=0 [| a~:b; b: Fin(A) |] ==> card(cons(a,b)) = succ(card(b)) diff -r 89d45187f04d -r ca5356bd315a src/ZF/Fin.thy --- a/src/ZF/Fin.thy Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Fin.thy Tue Jun 21 17:20:34 1994 +0200 @@ -1,3 +1,3 @@ (*Dummy theory to document dependencies *) -fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities" +Fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities" diff -r 89d45187f04d -r ca5356bd315a src/ZF/List.ML --- a/src/ZF/List.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/List.ML Tue Jun 21 17:20:34 1994 +0200 @@ -1,4 +1,4 @@ -(* Title: ZF/list.ML +(* Title: ZF/List.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge @@ -36,6 +36,14 @@ rename_last_tac a ["1"] (i+2), ares_tac prems i]; +goal List.thy "list(A) = {0} + (A * list(A))"; +by (rtac (List.unfold RS trans) 1); +bws List.con_defs; +by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs) + addDs [List.dom_subset RS subsetD] + addEs [A_into_univ]) 1); +val list_unfold = result(); + (** Lemmas to justify using "list" in other recursive type definitions **) goalw List.thy List.defs "!!A B. A<=B ==> list(A) <= list(B)"; @@ -54,6 +62,10 @@ val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans); +goal List.thy "!!l A B. [| l: list(A); A <= univ(B) |] ==> l: univ(B)"; +by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1)); +val list_into_univ = result(); + val major::prems = goal List.thy "[| l: list(A); \ \ c: C(Nil); \ diff -r 89d45187f04d -r ca5356bd315a src/ZF/List.thy --- a/src/ZF/List.thy Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/List.thy Tue Jun 21 17:20:34 1994 +0200 @@ -1,3 +1,3 @@ (*Dummy theory to document dependencies *) -list = Univ + "Datatype" + "intr_elim" +List = Univ + "Datatype" + "intr_elim" diff -r 89d45187f04d -r ca5356bd315a src/ZF/Makefile --- a/src/ZF/Makefile Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Makefile Tue Jun 21 17:20:34 1994 +0200 @@ -22,8 +22,11 @@ func.ML simpdata.ML Bool.thy Bool.ML \ Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \ ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \ - equalities.ML Perm.thy Perm.ML Trancl.thy Trancl.ML \ - WF.thy WF.ML Ord.thy Ord.ML Nat.thy Nat.ML \ + equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \ + WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \ + OrderType.thy OrderType.ML OrderArith.thy OrderArith.ML \ + Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \ + Nat.thy Nat.ML \ Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ QUniv.thy QUniv.ML constructor.ML Datatype.ML \ Fin.ML List.ML ListFn.thy ListFn.ML @@ -44,7 +47,8 @@ poly*) cp $(BIN)/FOL $(BIN)/ZF;\ echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\ sml*) echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\ - *) echo Bad value for ISABELLECOMP;;\ + *) echo Bad value for ISABELLECOMP: \ + $(COMP) is not poly or sml;;\ esac $(BIN)/FOL: @@ -54,7 +58,8 @@ case "$(COMP)" in \ poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/ZF ;;\ sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/ZF;;\ - *) echo Bad value for ISABELLECOMP;;\ + *) echo Bad value for ISABELLECOMP: \ + $(COMP) is not poly or sml;;\ esac .PRECIOUS: $(BIN)/FOL $(BIN)/ZF diff -r 89d45187f04d -r ca5356bd315a src/ZF/Nat.ML --- a/src/ZF/Nat.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Nat.ML Tue Jun 21 17:20:34 1994 +0200 @@ -68,10 +68,12 @@ val prems = goal Nat.thy "n: nat ==> Ord(n)"; by (nat_ind_tac "n" prems 1); by (REPEAT (ares_tac [Ord_0, Ord_succ] 1)); -val naturals_are_ordinals = result(); +val nat_into_Ord = result(); (* i: nat ==> 0 le i *) -val nat_0_le = naturals_are_ordinals RS Ord_0_le; +val nat_0_le = nat_into_Ord RS Ord_0_le; + +val nat_le_refl = nat_into_Ord RS le_refl; goal Nat.thy "!!n. n: nat ==> n=0 | 0:n"; by (etac nat_induct 1); @@ -81,18 +83,23 @@ goal Nat.thy "Ord(nat)"; by (rtac OrdI 1); -by (etac (naturals_are_ordinals RS Ord_is_Transset) 2); +by (etac (nat_into_Ord RS Ord_is_Transset) 2); by (rewtac Transset_def); by (rtac ballI 1); by (etac nat_induct 1); by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1)); val Ord_nat = result(); +goalw Nat.thy [Limit_def] "Limit(nat)"; +by (safe_tac (ZF_cs addSIs [ltI, nat_0I, nat_1I, nat_succI, Ord_nat])); +by (etac ltD 1); +val Limit_nat = result(); + (* succ(i): nat ==> i: nat *) val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans; (* [| succ(i): k; k: nat |] ==> i: k *) -val succ_in_naturalD = [succI1, asm_rl, naturals_are_ordinals] MRS Ord_trans; +val succ_in_naturalD = [succI1, asm_rl, nat_into_Ord] MRS Ord_trans; goal Nat.thy "!!m n. [| m m: nat"; by (etac ltE 1); diff -r 89d45187f04d -r ca5356bd315a src/ZF/Nat.thy --- a/src/ZF/Nat.thy Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Nat.thy Tue Jun 21 17:20:34 1994 +0200 @@ -1,12 +1,12 @@ -(* Title: ZF/nat.thy +(* Title: ZF/Nat.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge + Copyright 1994 University of Cambridge Natural numbers in Zermelo-Fraenkel Set Theory *) -Nat = Ord + Bool + "mono" + +Nat = Ordinal + Bool + "mono" + consts nat :: "i" nat_case :: "[i, i=>i, i]=>i" diff -r 89d45187f04d -r ca5356bd315a src/ZF/Order.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Order.ML Tue Jun 21 17:20:34 1994 +0200 @@ -0,0 +1,185 @@ +(* Title: ZF/Order.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +For Order.thy. Orders in Zermelo-Fraenkel Set Theory +*) + +(*TO PURE/TACTIC.ML*) +fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops); + + +open Order; + +val bij_apply_cs = ZF_cs addSEs [bij_converse_bij] + addIs [bij_is_fun, apply_type]; + +val bij_inverse_ss = + ZF_ss addsimps [bij_is_fun RS apply_type, + bij_converse_bij RS bij_is_fun RS apply_type, + left_inverse_bij, right_inverse_bij]; + +(** Basic properties of the definitions **) + +(*needed????*) +goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, asym_def] + "!!r. part_ord(A,r) ==> asym(r Int A*A)"; +by (fast_tac ZF_cs 1); +val part_ord_Imp_asym = result(); + +(** Order-isomorphisms **) + +goalw Order.thy [ord_iso_def] + "!!f. f: ord_iso(A,r,B,s) ==> f: bij(A,B)"; +by (etac CollectD1 1); +val ord_iso_is_bij = result(); + +goalw Order.thy [ord_iso_def] + "!!f. [| f: ord_iso(A,r,B,s); : r; x:A; y:A |] ==> \ +\ : s"; +by (fast_tac ZF_cs 1); +val ord_iso_apply = result(); + +goalw Order.thy [ord_iso_def] + "!!f. [| f: ord_iso(A,r,B,s); : s; x:B; y:B |] ==> \ +\ : r"; +be CollectE 1; +be (bspec RS bspec RS iffD2) 1; +by (REPEAT (eresolve_tac [asm_rl, + bij_converse_bij RS bij_is_fun RS apply_type] 1)); +by (asm_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1); +val ord_iso_converse = result(); + +val major::premx::premy::prems = goalw Order.thy [linear_def] + "[| linear(A,r); x:A; y:A; \ +\ :r ==> P; x=y ==> P; :r ==> P |] ==> P"; +by (cut_facts_tac [major,premx,premy] 1); +by (REPEAT_FIRST (eresolve_tac [ballE,disjE])); +by (EVERY1 (map etac prems)); +by (ALLGOALS contr_tac); +val linearE = result(); + +(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*) +val linear_case_tac = + SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1, + REPEAT_SOME assume_tac]); + +(*Inductive argument for proving Kunen's Lemma 6.1*) +goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def, pred_def] + "!!r. [| well_ord(A,r); x: A; f: ord_iso(A, r, pred(A,x,r), r); y: A |] \ +\ ==> f`y = y"; +by (safe_tac ZF_cs); +by (wf_on_ind_tac "y" [] 1); +by (forward_tac [ord_iso_is_bij] 1); +by (subgoal_tac "f`y1 : {y: A . : r}" 1); +by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type]) 2); +(*Now we know f`y1 : A and : r *) +by (etac CollectE 1); +by (linear_case_tac 1); +(*Case : r *) (*use induction hyp*) +by (dtac bspec 1 THEN mp_tac 2 THEN assume_tac 1); +by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); +by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); +(*The case : r *) +by (subgoal_tac " : r" 1); +by (fast_tac (ZF_cs addSEs [trans_onD]) 2); +by (dtac ord_iso_converse 1 THEN assume_tac 1 THEN fast_tac ZF_cs 2); +by (fast_tac ZF_cs 1); +by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); +(*now use induction hyp*) +by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); +by (dres_inst_tac [("t", "op `(f)")] subst_context 1); +by (asm_full_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1); +val not_well_ord_iso_pred_lemma = result(); + + +(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment + of a well-ordering*) +goal Order.thy + "!!r. [| well_ord(A,r); x:A |] ==> \ +\ ALL f. f ~: ord_iso(A, r, pred(A,x,r), r)"; +by (safe_tac ZF_cs); +by (metacut_tac not_well_ord_iso_pred_lemma 1); +by (REPEAT_SOME assume_tac); +(*Now we know f`x = x*) +by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type), + assume_tac]); +(*Now we know f`x : pred(A,x,r) *) +by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, pred_def]) 1); +by (fast_tac (ZF_cs addSEs [wf_on_not_refl RS notE]) 1); +val not_well_ord_iso_pred = result(); + + +(*Inductive argument for proving Kunen's Lemma 6.2*) +goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def] + "!!r. [| well_ord(A,r); well_ord(B,s); \ +\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s); y: A |] \ +\ ==> f`y = g`y"; +by (safe_tac ZF_cs); +by (wf_on_ind_tac "y" [] 1); +by (subgoals_tac ["f: bij(A,B)", "g: bij(A,B)", "f`y1 : B", "g`y1 : B"] 1); +by (REPEAT (fast_tac (bij_apply_cs addSEs [ord_iso_is_bij]) 2)); +by (linear_case_tac 1); +(*The case : s *) +by (forw_inst_tac [("f","g")] ord_iso_converse 1 THEN REPEAT (assume_tac 1)); +by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); +by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); +by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); +by (dres_inst_tac [("t", "op `(g)")] subst_context 1); +by (asm_full_simp_tac bij_inverse_ss 1); +(*The case : s *) +by (forw_inst_tac [("f","f")] ord_iso_converse 1 THEN REPEAT (assume_tac 1)); +by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); +by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); +by (dres_inst_tac [("t", "op `(converse(g))")] subst_context 1); +by (dres_inst_tac [("t", "op `(f)")] subst_context 1); +by (asm_full_simp_tac bij_inverse_ss 1); +val well_ord_iso_unique_lemma = result(); + + +(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*) +goal Order.thy + "!!r. [| well_ord(A,r); well_ord(B,s); \ +\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s) |] ==> f = g"; +br fun_extension 1; +be (ord_iso_is_bij RS bij_is_fun) 1; +be (ord_iso_is_bij RS bij_is_fun) 1; +br well_ord_iso_unique_lemma 1; +by (REPEAT_SOME assume_tac); +val well_ord_iso_unique = result(); + + +goalw Order.thy [irrefl_def, part_ord_def, tot_ord_def, + trans_on_def, well_ord_def] + "!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"; +by (asm_simp_tac (ZF_ss addsimps [wf_on_not_refl]) 1); +by (safe_tac ZF_cs); +by (linear_case_tac 1); +(*case x=xb*) +by (fast_tac (ZF_cs addSEs [wf_on_anti_sym]) 1); +(*case x wf[A](r)"; +by (safe_tac ZF_cs); +val well_ord_is_wf = result(); + + +(*** Derived rules for pred(A,x,r) ***) + +val [major,minor] = goalw Order.thy [pred_def] + "[| y: pred(A,x,r); [| y:A; :r |] ==> P |] ==> P"; +br (major RS CollectE) 1; +by (REPEAT (ares_tac [minor] 1)); +val predE = result(); + +goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}"; +by (fast_tac ZF_cs 1); +val pred_subset_under = result(); + +goalw Order.thy [pred_def] "pred(A,x,r) <= A"; +by (fast_tac ZF_cs 1); +val pred_subset = result(); diff -r 89d45187f04d -r ca5356bd315a src/ZF/Order.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Order.thy Tue Jun 21 17:20:34 1994 +0200 @@ -0,0 +1,31 @@ +(* Title: ZF/Order.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Orders in Zermelo-Fraenkel Set Theory +*) + +Order = WF + Perm + +consts + part_ord :: "[i,i]=>o" (*Strict partial ordering*) + linear, tot_ord :: "[i,i]=>o" (*Strict total ordering*) + well_ord :: "[i,i]=>o" (*Well-ordering*) + ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*) + pred :: "[i,i,i]=>i" (*Set of predecessors*) + +rules + part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)" + + linear_def "linear(A,r) == (ALL x:A. ALL y:A. :r | x=y | :r)" + + tot_ord_def "tot_ord(A,r) == part_ord(A,r) & linear(A,r)" + + well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)" + + ord_iso_def "ord_iso(A,r,B,s) == \ +\ {f: bij(A,B). ALL x:A. ALL y:A. :r <-> :s}" + + pred_def "pred(A,x,r) == {y:A. :r}" + +end diff -r 89d45187f04d -r ca5356bd315a src/ZF/OrderType.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/OrderType.ML Tue Jun 21 17:20:34 1994 +0200 @@ -0,0 +1,132 @@ +(* Title: ZF/OrderType.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +For OrderType.thy. Order types in Zermelo-Fraenkel Set Theory +*) + + +(*Requires Ordinal.thy as parent; otherwise could be in Order.ML*) +goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))"; +br well_ordI 1; +br (wf_Memrel RS wf_imp_wf_on) 1; +by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1); +by (REPEAT (resolve_tac [ballI, Ord_linear] 1));; +by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));; +val well_ord_Memrel = result(); + +open OrderType; + +(** Unfolding of ordermap **) + +goalw OrderType.thy [ordermap_def, pred_def] + "!!r. [| wf[A](r); x:A |] ==> \ +\ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"; +by (asm_simp_tac ZF_ss 1); +be (wfrec_on RS trans) 1; +ba 1; +by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam, + vimage_singleton_iff]) 1); +val ordermap_pred_unfold = result(); + +(*pred-unfolded version. NOT suitable for rewriting -- loops!*) +val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold; + +goalw OrderType.thy [ordermap_def,ordertype_def] + "ordermap(A,r) : A -> ordertype(A,r)"; +br lam_type 1; +by (rtac (lamI RS imageI) 1); +by (REPEAT (assume_tac 1)); +val ordermap_type = result(); + +(** Showing that ordermap, ordertype yield ordinals **) + +fun ordermap_elim_tac i = + EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i, + assume_tac (i+1), + assume_tac i]; + +goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def] + "!!r. [| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)"; +by (safe_tac ZF_cs); +by (wf_on_ind_tac "x" [] 1); +by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1); +by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); +bws [pred_def,Transset_def]; +by (fast_tac ZF_cs 2); +by (safe_tac ZF_cs); +by (ordermap_elim_tac 1); +by (fast_tac (ZF_cs addSEs [trans_onD]) 1); +val Ord_ordermap = result(); + +goalw OrderType.thy [ordertype_def] + "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))"; +by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1); +by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); +by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2); +bws [Transset_def,well_ord_def]; +by (safe_tac ZF_cs); +by (ordermap_elim_tac 1); +by (fast_tac ZF_cs 1); +val Ord_ordertype = result(); + +(** ordermap preserves the orderings in both directions **) + +goal OrderType.thy + "!!r. [| : r; wf[A](r); w: A; x: A |] ==> \ +\ ordermap(A,r)`w : ordermap(A,r)`x"; +by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1); +ba 1; +by (fast_tac ZF_cs 1); +val less_imp_ordermap_in = result(); + +(*linearity of r is crucial here*) +goalw OrderType.thy [well_ord_def, tot_ord_def] + "!!r. [| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \ +\ w: A; x: A |] ==> : r"; +by (safe_tac ZF_cs); +by (linear_case_tac 1); +by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1); +bd less_imp_ordermap_in 1; +by (REPEAT_SOME assume_tac); +be mem_anti_sym 1; +ba 1; +val ordermap_in_imp_less = result(); + +val ordermap_surj = + (ordermap_type RS surj_image) |> + rewrite_rule [symmetric ordertype_def] |> + standard; + +goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def] + "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"; +by (safe_tac ZF_cs); +br ordermap_type 1; +br ordermap_surj 2; +by (linear_case_tac 1); +(*The two cases yield similar contradictions*) +by (ALLGOALS (dtac less_imp_ordermap_in)); +by (REPEAT_SOME assume_tac); +by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl]))); +val ordertype_bij = result(); + +goalw OrderType.thy [ord_iso_def] + "!!r. well_ord(A,r) ==> \ +\ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"; +by (safe_tac ZF_cs); +br ordertype_bij 1; +ba 1; +by (fast_tac (ZF_cs addSEs [MemrelE, ordermap_in_imp_less]) 2); +bw well_ord_def; +by (fast_tac (ZF_cs addSIs [MemrelI, less_imp_ordermap_in, + ordermap_type RS apply_type]) 1); +val ordertype_ord_iso = result(); + + +(** Unfolding of ordertype **) + +goalw OrderType.thy [ordertype_def] + "ordertype(A,r) = {ordermap(A,r)`y . y : A}"; +by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1); +val ordertype_unfold = result(); diff -r 89d45187f04d -r ca5356bd315a src/ZF/OrderType.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/OrderType.thy Tue Jun 21 17:20:34 1994 +0200 @@ -0,0 +1,22 @@ +(* Title: ZF/OrderType.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Order types. + +The order type of a well-ordering is the least ordinal isomorphic to it. +*) + +OrderType = Order + Ordinal + +consts + ordermap :: "[i,i]=>i" + ordertype :: "[i,i]=>i" + +rules + ordermap_def + "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))" + + ordertype_def "ordertype(A,r) == ordermap(A,r)``A" + +end diff -r 89d45187f04d -r ca5356bd315a src/ZF/Ordinal.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Ordinal.ML Tue Jun 21 17:20:34 1994 +0200 @@ -0,0 +1,619 @@ +(* Title: ZF/Ordinal.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +For Ordinal.thy. Ordinals in Zermelo-Fraenkel Set Theory +*) + +open Ordinal; + +(*** Rules for Transset ***) + +(** Two neat characterisations of Transset **) + +goalw Ordinal.thy [Transset_def] "Transset(A) <-> A<=Pow(A)"; +by (fast_tac ZF_cs 1); +val Transset_iff_Pow = result(); + +goalw Ordinal.thy [Transset_def] "Transset(A) <-> Union(succ(A)) = A"; +by (fast_tac (eq_cs addSEs [equalityE]) 1); +val Transset_iff_Union_succ = result(); + +(** Consequences of downwards closure **) + +goalw Ordinal.thy [Transset_def] + "!!C a b. [| Transset(C); {a,b}: C |] ==> a:C & b: C"; +by (fast_tac ZF_cs 1); +val Transset_doubleton_D = result(); + +val [prem1,prem2] = goalw Ordinal.thy [Pair_def] + "[| Transset(C); : C |] ==> a:C & b: C"; +by (cut_facts_tac [prem2] 1); +by (fast_tac (ZF_cs addSDs [prem1 RS Transset_doubleton_D]) 1); +val Transset_Pair_D = result(); + +val prem1::prems = goal Ordinal.thy + "[| Transset(C); A*B <= C; b: B |] ==> A <= C"; +by (cut_facts_tac prems 1); +by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1); +val Transset_includes_domain = result(); + +val prem1::prems = goal Ordinal.thy + "[| Transset(C); A*B <= C; a: A |] ==> B <= C"; +by (cut_facts_tac prems 1); +by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1); +val Transset_includes_range = result(); + +val [prem1,prem2] = goalw (merge_theories(Ordinal.thy,Sum.thy)) [sum_def] + "[| Transset(C); A+B <= C |] ==> A <= C & B <= C"; +by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1); +by (REPEAT (etac (prem1 RS Transset_includes_range) 1 + ORELSE resolve_tac [conjI, singletonI] 1)); +val Transset_includes_summands = result(); + +val [prem] = goalw (merge_theories(Ordinal.thy,Sum.thy)) [sum_def] + "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)"; +by (rtac (Int_Un_distrib RS ssubst) 1); +by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1); +val Transset_sum_Int_subset = result(); + +(** Closure properties **) + +goalw Ordinal.thy [Transset_def] "Transset(0)"; +by (fast_tac ZF_cs 1); +val Transset_0 = result(); + +goalw Ordinal.thy [Transset_def] + "!!i j. [| Transset(i); Transset(j) |] ==> Transset(i Un j)"; +by (fast_tac ZF_cs 1); +val Transset_Un = result(); + +goalw Ordinal.thy [Transset_def] + "!!i j. [| Transset(i); Transset(j) |] ==> Transset(i Int j)"; +by (fast_tac ZF_cs 1); +val Transset_Int = result(); + +goalw Ordinal.thy [Transset_def] "!!i. Transset(i) ==> Transset(succ(i))"; +by (fast_tac ZF_cs 1); +val Transset_succ = result(); + +goalw Ordinal.thy [Transset_def] "!!i. Transset(i) ==> Transset(Pow(i))"; +by (fast_tac ZF_cs 1); +val Transset_Pow = result(); + +goalw Ordinal.thy [Transset_def] "!!A. Transset(A) ==> Transset(Union(A))"; +by (fast_tac ZF_cs 1); +val Transset_Union = result(); + +val [Transprem] = goalw Ordinal.thy [Transset_def] + "[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))"; +by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1); +val Transset_Union_family = result(); + +val [prem,Transprem] = goalw Ordinal.thy [Transset_def] + "[| j:A; !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))"; +by (cut_facts_tac [prem] 1); +by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1); +val Transset_Inter_family = result(); + +(*** Natural Deduction rules for Ord ***) + +val prems = goalw Ordinal.thy [Ord_def] + "[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i) "; +by (REPEAT (ares_tac (prems@[ballI,conjI]) 1)); +val OrdI = result(); + +val [major] = goalw Ordinal.thy [Ord_def] + "Ord(i) ==> Transset(i)"; +by (rtac (major RS conjunct1) 1); +val Ord_is_Transset = result(); + +val [major,minor] = goalw Ordinal.thy [Ord_def] + "[| Ord(i); j:i |] ==> Transset(j) "; +by (rtac (minor RS (major RS conjunct2 RS bspec)) 1); +val Ord_contains_Transset = result(); + +(*** Lemmas for ordinals ***) + +goalw Ordinal.thy [Ord_def,Transset_def] "!!i j.[| Ord(i); j:i |] ==> Ord(j)"; +by (fast_tac ZF_cs 1); +val Ord_in_Ord = result(); + +(* Ord(succ(j)) ==> Ord(j) *) +val Ord_succD = succI1 RSN (2, Ord_in_Ord); + +goal Ordinal.thy "!!i j. [| Ord(i); Transset(j); j<=i |] ==> Ord(j)"; +by (REPEAT (ares_tac [OrdI] 1 + ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1)); +val Ord_subset_Ord = result(); + +goalw Ordinal.thy [Ord_def,Transset_def] "!!i j. [| j:i; Ord(i) |] ==> j<=i"; +by (fast_tac ZF_cs 1); +val OrdmemD = result(); + +goal Ordinal.thy "!!i j k. [| i:j; j:k; Ord(k) |] ==> i:k"; +by (REPEAT (ares_tac [OrdmemD RS subsetD] 1)); +val Ord_trans = result(); + +goal Ordinal.thy "!!i j. [| i:j; Ord(j) |] ==> succ(i) <= j"; +by (REPEAT (ares_tac [OrdmemD RSN (2,succ_subsetI)] 1)); +val Ord_succ_subsetI = result(); + + +(*** The construction of ordinals: 0, succ, Union ***) + +goal Ordinal.thy "Ord(0)"; +by (REPEAT (ares_tac [OrdI,Transset_0] 1 ORELSE etac emptyE 1)); +val Ord_0 = result(); + +goal Ordinal.thy "!!i. Ord(i) ==> Ord(succ(i))"; +by (REPEAT (ares_tac [OrdI,Transset_succ] 1 + ORELSE eresolve_tac [succE,ssubst,Ord_is_Transset, + Ord_contains_Transset] 1)); +val Ord_succ = result(); + +goal Ordinal.thy "Ord(succ(i)) <-> Ord(i)"; +by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1); +val Ord_succ_iff = result(); + +goalw Ordinal.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Un j)"; +by (fast_tac (ZF_cs addSIs [Transset_Un]) 1); +val Ord_Un = result(); + +goalw Ordinal.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Int j)"; +by (fast_tac (ZF_cs addSIs [Transset_Int]) 1); +val Ord_Int = result(); + +val nonempty::prems = goal Ordinal.thy + "[| j:A; !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))"; +by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1); +by (rtac Ord_is_Transset 1); +by (REPEAT (ares_tac ([Ord_contains_Transset,nonempty]@prems) 1 + ORELSE etac InterD 1)); +val Ord_Inter = result(); + +val jmemA::prems = goal Ordinal.thy + "[| j:A; !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"; +by (rtac (jmemA RS RepFunI RS Ord_Inter) 1); +by (etac RepFunE 1); +by (etac ssubst 1); +by (eresolve_tac prems 1); +val Ord_INT = result(); + +(*There is no set of all ordinals, for then it would contain itself*) +goal Ordinal.thy "~ (ALL i. i:X <-> Ord(i))"; +by (rtac notI 1); +by (forw_inst_tac [("x", "X")] spec 1); +by (safe_tac (ZF_cs addSEs [mem_anti_refl])); +by (swap_res_tac [Ord_is_Transset RSN (2,OrdI)] 1); +by (fast_tac ZF_cs 2); +bw Transset_def; +by (safe_tac ZF_cs); +by (asm_full_simp_tac ZF_ss 1); +by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); +val ON_class = result(); + +(*** < is 'less than' for ordinals ***) + +goalw Ordinal.thy [lt_def] "!!i j. [| i:j; Ord(j) |] ==> i P |] ==> P"; +by (rtac (major RS conjE) 1); +by (REPEAT (ares_tac (prems@[Ord_in_Ord]) 1)); +val ltE = result(); + +goal Ordinal.thy "!!i j. i i:j"; +by (etac ltE 1); +by (assume_tac 1); +val ltD = result(); + +goalw Ordinal.thy [lt_def] "~ i<0"; +by (fast_tac ZF_cs 1); +val not_lt0 = result(); + +(* i<0 ==> R *) +val lt0E = standard (not_lt0 RS notE); + +goal Ordinal.thy "!!i j k. [| i i P"; +by (REPEAT (eresolve_tac [asm_rl, conjE, mem_anti_sym] 1)); +val lt_anti_sym = result(); + +val lt_anti_refl = prove_goal Ordinal.thy "i P" + (fn [major]=> [ (rtac (major RS (major RS lt_anti_sym)) 1) ]); + +val lt_not_refl = prove_goal Ordinal.thy "~ i [ (rtac notI 1), (etac lt_anti_refl 1) ]); + +(** le is less than or equals; recall i le j abbrevs i i i le j"; +by (asm_simp_tac (ZF_ss addsimps [le_iff]) 1); +val leI = result(); + +goal Ordinal.thy "!!i. [| i=j; Ord(j) |] ==> i le j"; +by (asm_simp_tac (ZF_ss addsimps [le_iff]) 1); +val le_eqI = result(); + +val le_refl = refl RS le_eqI; + +val [prem] = goal Ordinal.thy "(~ (i=j & Ord(j)) ==> i i le j"; +by (rtac (disjCI RS (le_iff RS iffD2)) 1); +by (etac prem 1); +val leCI = result(); + +val major::prems = goal Ordinal.thy + "[| i le j; i P; [| i=j; Ord(j) |] ==> P |] ==> P"; +by (rtac (major RS (le_iff RS iffD1 RS disjE)) 1); +by (DEPTH_SOLVE (ares_tac prems 1 ORELSE etac conjE 1)); +val leE = result(); + +goal Ordinal.thy "!!i j. [| i le j; j le i |] ==> i=j"; +by (asm_full_simp_tac (ZF_ss addsimps [le_iff]) 1); +by (fast_tac (ZF_cs addEs [lt_anti_sym]) 1); +val le_asym = result(); + +goal Ordinal.thy "i le 0 <-> i=0"; +by (fast_tac (ZF_cs addSIs [Ord_0 RS le_refl] addSEs [leE, lt0E]) 1); +val le0_iff = result(); + +val le0D = standard (le0_iff RS iffD1); + +val lt_cs = + ZF_cs addSIs [le_refl, leCI] + addSDs [le0D] + addSEs [lt_anti_refl, lt0E, leE]; + + +(*** Natural Deduction rules for Memrel ***) + +goalw Ordinal.thy [Memrel_def] " : Memrel(A) <-> a:b & a:A & b:A"; +by (fast_tac ZF_cs 1); +val Memrel_iff = result(); + +val prems = goal Ordinal.thy "[| a: b; a: A; b: A |] ==> : Memrel(A)"; +by (REPEAT (resolve_tac (prems@[conjI, Memrel_iff RS iffD2]) 1)); +val MemrelI = result(); + +val [major,minor] = goal Ordinal.thy + "[| : Memrel(A); \ +\ [| a: A; b: A; a:b |] ==> P \ +\ |] ==> P"; +by (rtac (major RS (Memrel_iff RS iffD1) RS conjE) 1); +by (etac conjE 1); +by (rtac minor 1); +by (REPEAT (assume_tac 1)); +val MemrelE = result(); + +(*The membership relation (as a set) is well-founded. + Proof idea: show A<=B by applying the foundation axiom to A-B *) +goalw Ordinal.thy [wf_def] "wf(Memrel(A))"; +by (EVERY1 [rtac (foundation RS disjE RS allI), + etac disjI1, + etac bexE, + rtac (impI RS allI RS bexI RS disjI2), + etac MemrelE, + etac bspec, + REPEAT o assume_tac]); +val wf_Memrel = result(); + +(*Transset(i) does not suffice, though ALL j:i.Transset(j) does*) +goalw Ordinal.thy [Ord_def, Transset_def, trans_def] + "!!i. Ord(i) ==> trans(Memrel(i))"; +by (fast_tac (ZF_cs addSIs [MemrelI] addSEs [MemrelE]) 1); +val trans_Memrel = result(); + +(*If Transset(A) then Memrel(A) internalizes the membership relation below A*) +goalw Ordinal.thy [Transset_def] + "!!A. Transset(A) ==> : Memrel(A) <-> a:b & b:A"; +by (fast_tac (ZF_cs addSIs [MemrelI] addSEs [MemrelE]) 1); +val Transset_Memrel_iff = result(); + + +(*** Transfinite induction ***) + +(*Epsilon induction over a transitive set*) +val major::prems = goalw Ordinal.thy [Transset_def] + "[| i: k; Transset(k); \ +\ !!x.[| x: k; ALL y:x. P(y) |] ==> P(x) \ +\ |] ==> P(i)"; +by (rtac (major RS (wf_Memrel RS wf_induct2)) 1); +by (fast_tac (ZF_cs addEs [MemrelE]) 1); +by (resolve_tac prems 1); +by (assume_tac 1); +by (cut_facts_tac prems 1); +by (fast_tac (ZF_cs addIs [MemrelI]) 1); +val Transset_induct = result(); + +(*Induction over an ordinal*) +val Ord_induct = Ord_is_Transset RSN (2, Transset_induct); + +(*Induction over the class of ordinals -- a useful corollary of Ord_induct*) +val [major,indhyp] = goal Ordinal.thy + "[| Ord(i); \ +\ !!x.[| Ord(x); ALL y:x. P(y) |] ==> P(x) \ +\ |] ==> P(i)"; +by (rtac (major RS Ord_succ RS (succI1 RS Ord_induct)) 1); +by (rtac indhyp 1); +by (rtac (major RS Ord_succ RS Ord_in_Ord) 1); +by (REPEAT (assume_tac 1)); +val trans_induct = result(); + +(*Perform induction on i, then prove the Ord(i) subgoal using prems. *) +fun trans_ind_tac a prems i = + EVERY [res_inst_tac [("i",a)] trans_induct i, + rename_last_tac a ["1"] (i+1), + ares_tac prems i]; + + +(*** Fundamental properties of the epsilon ordering (< on ordinals) ***) + +(*Finds contradictions for the following proof*) +val Ord_trans_tac = EVERY' [etac notE, etac Ord_trans, REPEAT o atac]; + +(** Proving that < is a linear ordering on the ordinals **) + +val prems = goal Ordinal.thy + "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)"; +by (trans_ind_tac "i" prems 1); +by (rtac (impI RS allI) 1); +by (trans_ind_tac "j" [] 1); +by (DEPTH_SOLVE (step_tac eq_cs 1 ORELSE Ord_trans_tac 1)); +val Ord_linear_lemma = result(); +val Ord_linear = standard (Ord_linear_lemma RS spec RS mp); + +(*The trichotomy law for ordinals!*) +val ordi::ordj::prems = goalw Ordinal.thy [lt_def] + "[| Ord(i); Ord(j); i P; i=j ==> P; j P |] ==> P"; +by (rtac ([ordi,ordj] MRS Ord_linear RS disjE) 1); +by (etac disjE 2); +by (DEPTH_SOLVE (ares_tac ([ordi,ordj,conjI] @ prems) 1)); +val Ord_linear_lt = result(); + +val prems = goal Ordinal.thy + "[| Ord(i); Ord(j); i P; j le i ==> P |] ==> P"; +by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); +by (DEPTH_SOLVE (ares_tac ([leI, sym RS le_eqI] @ prems) 1)); +val Ord_linear2 = result(); + +val prems = goal Ordinal.thy + "[| Ord(i); Ord(j); i le j ==> P; j le i ==> P |] ==> P"; +by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); +by (DEPTH_SOLVE (ares_tac ([leI,le_eqI] @ prems) 1)); +val Ord_linear_le = result(); + +goal Ordinal.thy "!!i j. j le i ==> ~ i j le i"; +by (res_inst_tac [("i","i"),("j","j")] Ord_linear2 1); +by (REPEAT (SOMEGOAL assume_tac)); +by (fast_tac (lt_cs addEs [lt_anti_sym]) 1); +val not_lt_imp_le = result(); + +goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> ~ i j le i"; +by (REPEAT (ares_tac [iffI, le_imp_not_lt, not_lt_imp_le] 1)); +val not_lt_iff_le = result(); + +goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> ~ i le j <-> j 0 le i"; +by (etac (not_lt_iff_le RS iffD1) 1); +by (REPEAT (resolve_tac [Ord_0, not_lt0] 1)); +val Ord_0_le = result(); + +goal Ordinal.thy "!!i. [| Ord(i); i~=0 |] ==> 0 j le i"; +by (rtac (not_lt_iff_le RS iffD1) 1); +by (assume_tac 1); +by (assume_tac 1); +by (fast_tac (ZF_cs addEs [ltE, mem_anti_refl]) 1); +val subset_imp_le = result(); + +goal Ordinal.thy "!!i j. i le j ==> i<=j"; +by (etac leE 1); +by (fast_tac ZF_cs 2); +by (fast_tac (subset_cs addIs [OrdmemD] addEs [ltE]) 1); +val le_imp_subset = result(); + +goal Ordinal.thy "j le i <-> j<=i & Ord(i) & Ord(j)"; +by (fast_tac (ZF_cs addSEs [subset_imp_le, le_imp_subset] + addEs [ltE, make_elim Ord_succD]) 1); +val le_subset_iff = result(); + +goal Ordinal.thy "i le succ(j) <-> i le j | i=succ(j) & Ord(i)"; +by (simp_tac (ZF_ss addsimps [le_iff]) 1); +by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1); +val le_succ_iff = result(); + +(*Just a variant of subset_imp_le*) +val [ordi,ordj,minor] = goal Ordinal.thy + "[| Ord(i); Ord(j); !!x. x x j le i"; +by (REPEAT_FIRST (ares_tac [notI RS not_lt_imp_le, ordi, ordj])); +be (minor RS lt_anti_refl) 1; +val all_lt_imp_le = result(); + +(** Transitive laws **) + +goal Ordinal.thy "!!i j. [| i le j; j i i i le k"; +by (REPEAT (ares_tac [lt_trans1] 1)); +val le_trans = result(); + +goal Ordinal.thy "!!i j. i succ(i) le j"; +by (rtac (not_lt_iff_le RS iffD1) 1); +by (fast_tac (lt_cs addEs [lt_anti_sym]) 3); +by (ALLGOALS (fast_tac (ZF_cs addEs [ltE] addIs [Ord_succ]))); +val succ_leI = result(); + +goal Ordinal.thy "!!i j. succ(i) le j ==> i i i le i Un j"; +by (rtac (Un_upper1 RS subset_imp_le) 1); +by (REPEAT (ares_tac [Ord_Un] 1)); +val Un_upper1_le = result(); + +goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> j le i Un j"; +by (rtac (Un_upper2 RS subset_imp_le) 1); +by (REPEAT (ares_tac [Ord_Un] 1)); +val Un_upper2_le = result(); + +(*Replacing k by succ(k') yields the similar rule for le!*) +goal Ordinal.thy "!!i j k. [| i i Un j < k"; +by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); +by (rtac (Un_commute RS ssubst) 4); +by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 4); +by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 3); +by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); +val Un_least_lt = result(); + +goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> i Un j < k <-> i i Un j : k <-> i:k & j:k"; +by (cut_facts_tac [[ordi,ordj] MRS + read_instantiate [("k","k")] Un_least_lt_iff] 1); +by (asm_full_simp_tac (ZF_ss addsimps [lt_def,ordi,ordj,ordk]) 1); +val Un_least_mem_iff = result(); + +(*Replacing k by succ(k') yields the similar rule for le!*) +goal Ordinal.thy "!!i j k. [| i i Int j < k"; +by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); +by (rtac (Int_commute RS ssubst) 4); +by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 4); +by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 3); +by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); +val Int_greatest_lt = result(); + +(*FIXME: the Intersection duals are missing!*) + + +(*** Results about limits ***) + +val prems = goal Ordinal.thy "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))"; +by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1); +by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1)); +val Ord_Union = result(); + +val prems = goal Ordinal.thy + "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))"; +by (rtac Ord_Union 1); +by (etac RepFunE 1); +by (etac ssubst 1); +by (eresolve_tac prems 1); +val Ord_UN = result(); + +(* No < version; consider (UN i:nat.i)=nat *) +val [ordi,limit] = goal Ordinal.thy + "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i"; +by (rtac (le_imp_subset RS UN_least RS subset_imp_le) 1); +by (REPEAT (ares_tac [ordi, Ord_UN, limit] 1 ORELSE etac (limit RS ltE) 1)); +val UN_least_le = result(); + +val [jlti,limit] = goal Ordinal.thy + "[| j b(x) (UN x:A. succ(b(x))) < i"; +by (rtac (jlti RS ltE) 1); +by (rtac (UN_least_le RS lt_trans2) 1); +by (REPEAT (ares_tac [jlti, succ_leI, limit] 1)); +val UN_succ_least_lt = result(); + +val prems = goal Ordinal.thy + "[| a: A; i le b(a); !!x. x:A ==> Ord(b(x)) |] ==> i le (UN x:A. b(x))"; +by (resolve_tac (prems RL [ltE]) 1); +by (rtac (le_imp_subset RS subset_trans RS subset_imp_le) 1); +by (REPEAT (ares_tac (prems @ [UN_upper, Ord_UN]) 1)); +val UN_upper_le = result(); + +goal Ordinal.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i"; +by (fast_tac (eq_cs addEs [Ord_trans]) 1); +val Ord_equality = result(); + +(*Holds for all transitive sets, not just ordinals*) +goal Ordinal.thy "!!i. Ord(i) ==> Union(i) <= i"; +by (fast_tac (ZF_cs addSEs [Ord_trans]) 1); +val Ord_Union_subset = result(); + + +(*** Limit ordinals -- general properties ***) + +goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i"; +by (fast_tac (eq_cs addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1); +val Limit_Union_eq = result(); + +goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)"; +by (etac conjunct1 1); +val Limit_is_Ord = result(); + +goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> 0 < i"; +by (etac (conjunct2 RS conjunct1) 1); +val Limit_has_0 = result(); + +goalw Ordinal.thy [Limit_def] "!!i. [| Limit(i); j succ(j) < i"; +by (fast_tac ZF_cs 1); +val Limit_has_succ = result(); + +goalw Ordinal.thy [Limit_def] + "!!i. [| 0 Limit(i)"; +by (safe_tac subset_cs); +by (rtac (not_le_iff_lt RS iffD1) 2); +by (fast_tac (lt_cs addEs [lt_anti_sym]) 4); +by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1)); +val non_succ_LimitI = result(); + +goal Ordinal.thy "!!i. Limit(succ(i)) ==> P"; +br lt_anti_refl 1; +br Limit_has_succ 1; +ba 1; +be (Limit_is_Ord RS Ord_succD RS le_refl) 1; +val succ_LimitE = result(); + +goal Ordinal.thy "!!i. [| Limit(i); i le succ(j) |] ==> i le j"; +by (safe_tac (ZF_cs addSEs [succ_LimitE, leE])); +val Limit_le_succD = result(); + + diff -r 89d45187f04d -r ca5356bd315a src/ZF/Ordinal.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Ordinal.thy Tue Jun 21 17:20:34 1994 +0200 @@ -0,0 +1,28 @@ +(* Title: ZF/Ordinal.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Ordinals in Zermelo-Fraenkel Set Theory +*) + +Ordinal = WF + "simpdata" + "equalities" + +consts + Memrel :: "i=>i" + Transset,Ord :: "i=>o" + "<" :: "[i,i] => o" (infixl 50) (*less than on ordinals*) + "le" :: "[i,i] => o" (infixl 50) (*less than or equals*) + Limit :: "i=>o" + +translations + "x le y" == "x < succ(y)" + +rules + Memrel_def "Memrel(A) == {z: A*A . EX x y. z= & x:y }" + Transset_def "Transset(i) == ALL x:i. x<=i" + Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))" + lt_def "i succ(y) id(A): inj(A,B)"; by (REPEAT (ares_tac [CollectI,lam_type] 1)); +by (etac subsetD 1 THEN assume_tac 1); by (simp_tac ZF_ss 1); -val id_inj = result(); +val id_subset_inj = result(); + +val id_inj = subset_refl RS id_subset_inj; goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)"; by (fast_tac (ZF_cs addIs [lam_type,beta]) 1); @@ -111,24 +114,32 @@ by (fast_tac (ZF_cs addIs (prems@[apply_Pair,apply_equality,converseI])) 1); val left_inverse_lemma = result(); -val prems = goal Perm.thy - "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a"; -by (fast_tac (ZF_cs addIs (prems@ - [left_inverse_lemma,inj_converse_fun,inj_is_fun])) 1); +goal Perm.thy + "!!f. [| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a"; +by (fast_tac (ZF_cs addIs [left_inverse_lemma,inj_converse_fun,inj_is_fun]) 1); val left_inverse = result(); +val left_inverse_bij = bij_is_inj RS left_inverse; + val prems = goal Perm.thy "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b"; by (rtac (apply_Pair RS (converseD RS apply_equality)) 1); by (REPEAT (resolve_tac prems 1)); val right_inverse_lemma = result(); -val prems = goal Perm.thy - "[| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b"; +goal Perm.thy + "!!f. [| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b"; by (rtac right_inverse_lemma 1); -by (REPEAT (resolve_tac (prems@ [inj_converse_fun,inj_is_fun]) 1)); +by (REPEAT (ares_tac [inj_converse_fun,inj_is_fun] 1)); val right_inverse = result(); +goalw Perm.thy [bij_def] + "!!f. [| f: bij(A,B); b: B |] ==> f`(converse(f)`b) = b"; +by (EVERY1 [etac IntE, etac right_inverse, + etac (surj_range RS ssubst), + assume_tac]); +val right_inverse_bij = result(); + val prems = goal Perm.thy "f: inj(A,B) ==> converse(f): inj(range(f), A)"; bw inj_def; (*rewrite subgoal but not prems!!*) @@ -236,22 +247,22 @@ by (REPEAT (ares_tac [PiI,comp_rel,ex1I,compI] 1 ORELSE eresolve_tac [fun_is_rel,apply_Pair,apply_type] 1)); by (fast_tac (comp_cs addDs [apply_equality]) 1); -val comp_func = result(); +val comp_fun = result(); goal Perm.thy "!!f g. [| g: A->B; f: B->C; a:A |] ==> (f O g)`a = f`(g`a)"; -by (REPEAT (ares_tac [comp_func,apply_equality,compI, +by (REPEAT (ares_tac [comp_fun,apply_equality,compI, apply_Pair,apply_type] 1)); -val comp_func_apply = result(); +val comp_fun_apply = result(); goalw Perm.thy [inj_def] "!!f g. [| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)"; by (REPEAT (eresolve_tac [bspec RS bspec RS mp, box_equals] 1 - ORELSE step_tac (ZF_cs addSIs [comp_func,apply_type,comp_func_apply]) 1)); + ORELSE step_tac (ZF_cs addSIs [comp_fun,apply_type,comp_fun_apply]) 1)); val comp_inj = result(); goalw Perm.thy [surj_def] "!!f g. [| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)"; -by (best_tac (ZF_cs addSIs [comp_func,comp_func_apply]) 1); +by (best_tac (ZF_cs addSIs [comp_fun,comp_fun_apply]) 1); val comp_surj = result(); goalw Perm.thy [bij_def] @@ -268,7 +279,7 @@ "!!f g. [| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)"; by (safe_tac comp_cs); by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1)); -by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1); +by (asm_simp_tac (FOL_ss addsimps [comp_fun_apply]) 1); val comp_mem_injD1 = result(); goalw Perm.thy [inj_def,surj_def] @@ -280,24 +291,24 @@ by (safe_tac comp_cs); by (res_inst_tac [("t", "op `(g)")] subst_context 1); by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1)); -by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1); +by (asm_simp_tac (FOL_ss addsimps [comp_fun_apply]) 1); val comp_mem_injD2 = result(); goalw Perm.thy [surj_def] "!!f g. [| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)"; -by (fast_tac (comp_cs addSIs [comp_func_apply RS sym, apply_type]) 1); +by (fast_tac (comp_cs addSIs [comp_fun_apply RS sym, apply_type]) 1); val comp_mem_surjD1 = result(); goal Perm.thy "!!f g. [| (f O g)`a = c; g: A->B; f: B->C; a:A |] ==> f`(g`a) = c"; -by (REPEAT (ares_tac [comp_func_apply RS sym RS trans] 1)); -val comp_func_applyD = result(); +by (REPEAT (ares_tac [comp_fun_apply RS sym RS trans] 1)); +val comp_fun_applyD = result(); goalw Perm.thy [inj_def,surj_def] "!!f g. [| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)"; by (safe_tac comp_cs); by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1); -by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_func_applyD 1)); +by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1)); by (best_tac (comp_cs addSIs [apply_type]) 1); val comp_mem_surjD2 = result(); @@ -325,6 +336,49 @@ by (best_tac (comp_cs addIs [apply_Pair]) 1); val right_comp_inverse = result(); +(** Proving that a function is a bijection **) + +val prems = +goalw Perm.thy [bij_def, inj_def, surj_def] + "[| !!x. x:A ==> c(x): B; \ +\ !!y. y:B ==> d(y): A; \ +\ !!x. x:A ==> d(c(x)) = x; \ +\ !!y. y:B ==> c(d(y)) = y \ +\ |] ==> (lam x:A.c(x)) : bij(A,B)"; +by (simp_tac (ZF_ss addsimps ([lam_type]@prems)) 1); +by (safe_tac ZF_cs); +(*Apply d to both sides then simplify (type constraint is essential) *) +by (dres_inst_tac [("t", "d::i=>i")] subst_context 1); +by (asm_full_simp_tac (ZF_ss addsimps prems) 1); +by (fast_tac (ZF_cs addIs prems) 1); +val lam_bijective = result(); + +goalw Perm.thy [id_def] + "!!f A B. [| f: A->B; g: B->A |] ==> \ +\ f O g = id(B) <-> (ALL y:B. f`(g`y)=y)"; +by (safe_tac ZF_cs); +by (dres_inst_tac [("t", "%h.h`y ")] subst_context 1); +by (asm_full_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1); +br fun_extension 1; +by (REPEAT (ares_tac [comp_fun, lam_type] 1)); +by (asm_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1); +val comp_eq_id_iff = result(); + +goalw Perm.thy [bij_def, inj_def, surj_def] + "!!f A B. [| f: A->B; g: B->A; f O g = id(B); g O f = id(A) \ +\ |] ==> f : bij(A,B)"; +by (asm_full_simp_tac (ZF_ss addsimps [comp_eq_id_iff]) 1); +by (safe_tac ZF_cs); +(*Apply g to both sides then simplify*) +by (dres_inst_tac [("t", "op `(g)"), ("a", "f`x")] subst_context 1); +by (asm_full_simp_tac ZF_ss 1); +by (fast_tac (ZF_cs addIs [apply_type]) 1); +val fg_imp_bijective = result(); + +goal Perm.thy "!!f A. [| f: A->A; f O f = id(A) |] ==> f : bij(A,A)"; +by (REPEAT (ares_tac [fg_imp_bijective] 1)); +val nilpotent_imp_bijective = result(); + (*Injective case applies converse(f) to both sides then simplifies using left_inverse_lemma*) goalw Perm.thy [bij_def,inj_def,surj_def] diff -r 89d45187f04d -r ca5356bd315a src/ZF/QPair.thy --- a/src/ZF/QPair.thy Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/QPair.thy Tue Jun 21 17:20:34 1994 +0200 @@ -18,7 +18,7 @@ qfsplit :: "[[i,i] => o, i] => o" qconverse :: "i => i" "@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10) - " <*>" :: "[i, i] => i" ("(_ <*>/ _)" [81, 80] 80) + "<*>" :: "[i, i] => i" ("(_ <*>/ _)" [81, 80] 80) QSigma :: "[i, i => i] => i" "<+>" :: "[i,i]=>i" (infixr 65) diff -r 89d45187f04d -r ca5356bd315a src/ZF/ROOT.ML --- a/src/ZF/ROOT.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/ROOT.ML Tue Jun 21 17:20:34 1994 +0200 @@ -28,6 +28,7 @@ print_depth 1; +use_thy "CardinalArith"; use_thy "Fin"; use_thy "ListFn"; diff -r 89d45187f04d -r ca5356bd315a src/ZF/Rel.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Rel.ML Tue Jun 21 17:20:34 1994 +0200 @@ -0,0 +1,60 @@ +(* Title: ZF/Rel.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +For Rel.thy. Relations in Zermelo-Fraenkel Set Theory +*) + +open Rel; + +(*** Some properties of relations -- useful? ***) + +(* irreflexivity *) + +val prems = goalw Rel.thy [irrefl_def] + "[| !!x. x:A ==> ~: r |] ==> irrefl(A,r)"; +by (REPEAT (ares_tac (prems @ [ballI]) 1)); +val irreflI = result(); + +val prems = goalw Rel.thy [irrefl_def] + "[| irrefl(A,r); x:A |] ==> ~: r"; +by (rtac (prems MRS bspec) 1); +val irreflE = result(); + +(* symmetry *) + +val prems = goalw Rel.thy [sym_def] + "[| !!x y.: r ==> : r |] ==> sym(r)"; +by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); +val symI = result(); + +goalw Rel.thy [sym_def] "!!r. [| sym(r); : r |] ==> : r"; +by (fast_tac ZF_cs 1); +val symE = result(); + +(* antisymmetry *) + +val prems = goalw Rel.thy [antisym_def] + "[| !!x y.[| : r; : r |] ==> x=y |] ==> \ +\ antisym(r)"; +by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); +val antisymI = result(); + +val prems = goalw Rel.thy [antisym_def] + "!!r. [| antisym(r); : r; : r |] ==> x=y"; +by (fast_tac ZF_cs 1); +val antisymE = result(); + +(* transitivity *) + +goalw Rel.thy [trans_def] + "!!r. [| trans(r); :r; :r |] ==> :r"; +by (fast_tac ZF_cs 1); +val transD = result(); + +goalw Rel.thy [trans_on_def] + "!!r. [| trans[A](r); :r; :r; a:A; b:A; c:A |] ==> :r"; +by (fast_tac ZF_cs 1); +val trans_onD = result(); + diff -r 89d45187f04d -r ca5356bd315a src/ZF/Rel.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Rel.thy Tue Jun 21 17:20:34 1994 +0200 @@ -0,0 +1,33 @@ +(* Title: ZF/Rel.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Relations in Zermelo-Fraenkel Set Theory +*) + +Rel = ZF + +consts + refl,irrefl,equiv :: "[i,i]=>o" + sym,asym,antisym,trans :: "i=>o" + trans_on :: "[i,i]=>o" ("trans[_]'(_')") + +rules + refl_def "refl(A,r) == (ALL x: A. : r)" + + irrefl_def "irrefl(A,r) == ALL x: A. ~: r" + + sym_def "sym(r) == ALL x y. : r --> : r" + + asym_def "asym(r) == ALL x y. :r --> ~ :r" + + antisym_def "antisym(r) == ALL x y.:r --> :r --> x=y" + + trans_def "trans(r) == ALL x y z. : r --> : r --> : r" + + trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. \ +\ : r --> : r --> : r" + + equiv_def "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)" + +end diff -r 89d45187f04d -r ca5356bd315a src/ZF/Sum.ML --- a/src/ZF/Sum.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Sum.ML Tue Jun 21 17:20:34 1994 +0200 @@ -35,19 +35,19 @@ (** Injection and freeness equivalences, for rewriting **) goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b"; -by (simp_tac (ZF_ss addsimps [Pair_iff]) 1); +by (simp_tac ZF_ss 1); val Inl_iff = result(); goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b"; -by (simp_tac (ZF_ss addsimps [Pair_iff]) 1); +by (simp_tac ZF_ss 1); val Inr_iff = result(); goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False"; -by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0 RS not_sym]) 1); +by (simp_tac (ZF_ss addsimps [one_not_0 RS not_sym]) 1); val Inl_Inr_iff = result(); goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False"; -by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0]) 1); +by (simp_tac (ZF_ss addsimps [one_not_0]) 1); val Inr_Inl_iff = result(); (*Injection and freeness rules*) @@ -60,6 +60,9 @@ val sum_cs = ZF_cs addSIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl] addSDs [Inl_inject,Inr_inject]; +val sum_ss = ZF_ss addsimps [InlI, InrI, Inl_iff, Inr_iff, + Inl_Inr_iff, Inr_Inl_iff]; + goal Sum.thy "!!A B. Inl(a): A+B ==> a: A"; by (fast_tac sum_cs 1); val InlD = result(); @@ -104,6 +107,19 @@ (prems@[case_Inl,case_Inr])))); val case_type = result(); +goal Sum.thy + "!!u. u: A+B ==> \ +\ R(case(c,d,u)) <-> \ +\ ((ALL x:A. u = Inl(x) --> R(c(x))) & \ +\ (ALL y:B. u = Inr(y) --> R(d(y))))"; +by (etac sumE 1); +by (asm_simp_tac (ZF_ss addsimps [case_Inl]) 1); +by (fast_tac sum_cs 1); +by (asm_simp_tac (ZF_ss addsimps [case_Inr]) 1); +by (fast_tac sum_cs 1); +val expand_case = result(); + + (** Rules for the Part primitive **) goalw Sum.thy [Part_def] diff -r 89d45187f04d -r ca5356bd315a src/ZF/Trancl.ML --- a/src/ZF/Trancl.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Trancl.ML Tue Jun 21 17:20:34 1994 +0200 @@ -8,12 +8,6 @@ open Trancl; -val major::prems = goalw Trancl.thy [trans_def] - "[| trans(r); :r; :r |] ==> :r"; -by (rtac (major RS spec RS spec RS spec RS mp RS mp) 1); -by (REPEAT (resolve_tac prems 1)); -val transD = result(); - goal Trancl.thy "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))"; by (rtac bnd_monoI 1); by (REPEAT (ares_tac [subset_refl, Un_mono, comp_mono] 2)); diff -r 89d45187f04d -r ca5356bd315a src/ZF/Trancl.thy --- a/src/ZF/Trancl.thy Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Trancl.thy Tue Jun 21 17:20:34 1994 +0200 @@ -6,16 +6,12 @@ Transitive closure of a relation *) -Trancl = Fixedpt + Perm + "mono" + +Trancl = Fixedpt + Perm + "mono" + Rel + consts - "rtrancl" :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*) - "trancl" :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*) - "trans" :: "i=>o" (*transitivity predicate*) + rtrancl :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*) + trancl :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*) rules - trans_def "trans(r) == ALL x y z. : r --> : r --> : r" - rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))" - trancl_def "r^+ == r O r^*" end diff -r 89d45187f04d -r ca5356bd315a src/ZF/Univ.ML --- a/src/ZF/Univ.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Univ.ML Tue Jun 21 17:20:34 1994 +0200 @@ -1,7 +1,7 @@ -(* Title: ZF/univ +(* Title: ZF/Univ ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge + Copyright 1994 University of Cambridge The cumulative hierarchy and a small universe for recursive types *) @@ -161,37 +161,6 @@ by (fast_tac ZF_cs 1); val Vfrom_Union = result(); -(*** Limit ordinals -- general properties ***) - -goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i"; -by (fast_tac (eq_cs addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1); -val Limit_Union_eq = result(); - -goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)"; -by (etac conjunct1 1); -val Limit_is_Ord = result(); - -goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> 0 < i"; -by (etac (conjunct2 RS conjunct1) 1); -val Limit_has_0 = result(); - -goalw Univ.thy [Limit_def] "!!i. [| Limit(i); j succ(j) < i"; -by (fast_tac ZF_cs 1); -val Limit_has_succ = result(); - -goalw Univ.thy [Limit_def] "Limit(nat)"; -by (safe_tac (ZF_cs addSIs (ltI::nat_typechecks))); -by (etac ltD 1); -val Limit_nat = result(); - -goalw Univ.thy [Limit_def] - "!!i. [| 0 Limit(i)"; -by (safe_tac subset_cs); -by (rtac (not_le_iff_lt RS iffD1) 2); -by (fast_tac (lt_cs addEs [lt_anti_sym]) 4); -by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1)); -val non_succ_LimitI = result(); - goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)"; by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_lt]) 1); val Ord_cases_lemma = result(); @@ -284,7 +253,7 @@ by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1); val Transset_Vfrom_succ = result(); -goalw Ord.thy [Pair_def,Transset_def] +goalw Ordinal.thy [Pair_def,Transset_def] "!!C. [| <= C; Transset(C) |] ==> a: C & b: C"; by (fast_tac ZF_cs 1); val Transset_Pair_subset = result(); diff -r 89d45187f04d -r ca5356bd315a src/ZF/Univ.thy --- a/src/ZF/Univ.thy Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/Univ.thy Tue Jun 21 17:20:34 1994 +0200 @@ -10,18 +10,15 @@ Univ = Arith + Sum + "mono" + consts - Limit :: "i=>o" - Vfrom :: "[i,i]=>i" - Vset :: "i=>i" - Vrec :: "[i, [i,i]=>i] =>i" - univ :: "i=>i" + Vfrom :: "[i,i]=>i" + Vset :: "i=>i" + Vrec :: "[i, [i,i]=>i] =>i" + univ :: "i=>i" translations "Vset(x)" == "Vfrom(0,x)" rules - Limit_def "Limit(i) == Ord(i) & 0 succ(y) wf[A](r)"; +by (fast_tac ZF_cs 1); +val wf_imp_wf_on = result(); + +goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)"; +by (fast_tac ZF_cs 1); +val wf_on_field_imp_wf = result(); + +goal WF.thy "wf(r) <-> wf[field(r)](r)"; +by (fast_tac (ZF_cs addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1); +val wf_iff_wf_on_field = result(); -(*If every subset of field(r) possesses an r-minimal element then wf(r). - Seems impossible to prove this for domain(r) or range(r) instead... - Consider in particular finite wf relations!*) -val [prem1,prem2] = goalw WF.thy [wf_def] - "[| field(r)<=A; \ -\ !!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. :r |] ==> False |] \ -\ ==> wf(r)"; +goalw WF.thy [wf_on_def, wf_def] "!!A B r. [| wf[A](r); B<=A |] ==> wf[B](r)"; +by (fast_tac ZF_cs 1); +val wf_on_subset_A = result(); + +goalw WF.thy [wf_on_def, wf_def] "!!A r s. [| wf[A](r); s<=r |] ==> wf[A](s)"; +by (fast_tac ZF_cs 1); +val wf_on_subset_r = result(); + +(** Introduction rules for wf_on **) + +(*If every non-empty subset of A has an r-minimal element then wf[A](r).*) +val [prem] = goalw WF.thy [wf_on_def, wf_def] + "[| !!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. :r |] ==> False |] \ +\ ==> wf[A](r)"; by (rtac (equals0I RS disjCI RS allI) 1); -by (rtac prem2 1); -by (res_inst_tac [ ("B1", "Z") ] (prem1 RS (Int_lower1 RS subset_trans)) 1); -by (fast_tac ZF_cs 1); -by (fast_tac ZF_cs 1); -val wfI = result(); +by (res_inst_tac [ ("Z", "Z") ] prem 1); +by (ALLGOALS (fast_tac ZF_cs)); +val wf_onI = result(); -(*If r allows well-founded induction then wf(r)*) -val [prem1,prem2] = goal WF.thy - "[| field(r)<=A; \ -\ !!B. ALL x:A. (ALL y. : r --> y:B) --> x:B ==> A<=B |] \ -\ ==> wf(r)"; -by (rtac (prem1 RS wfI) 1); -by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1); -by (fast_tac ZF_cs 3); +(*If r allows well-founded induction over A then wf[A](r) + Premise is equivalent to + !!B. ALL x:A. (ALL y. : r --> y:B) --> x:B ==> A<=B *) +val [prem] = goal WF.thy + "[| !!y B. [| ALL x:A. (ALL y:A. :r --> y:B) --> x:B; y:A \ +\ |] ==> y:B |] \ +\ ==> wf[A](r)"; +br wf_onI 1; +by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1); +by (contr_tac 3); by (fast_tac ZF_cs 2); by (fast_tac ZF_cs 1); -val wfI2 = result(); +val wf_onI2 = result(); (** Well-founded Induction **) @@ -88,29 +107,100 @@ by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1); val wf_induct2 = result(); -val prems = goal WF.thy "[| wf(r); :r; :r |] ==> False"; -by (subgoal_tac "ALL x. :r --> :r --> False" 1); -by (wf_ind_tac "a" prems 2); +goal ZF.thy "!!r A. field(r Int A*A) <= A"; +by (fast_tac ZF_cs 1); +val field_Int_square = result(); + +val wfr::amem::prems = goalw WF.thy [wf_on_def] + "[| wf[A](r); a:A; \ +\ !!x.[| x: A; ALL y:A. : r --> P(y) |] ==> P(x) \ +\ |] ==> P(a)"; +by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1); +by (REPEAT (ares_tac prems 1)); +by (fast_tac ZF_cs 1); +val wf_on_induct = result(); + +fun wf_on_ind_tac a prems i = + EVERY [res_inst_tac [("a",a)] wf_on_induct i, + rename_last_tac a ["1"] (i+2), + REPEAT (ares_tac prems i)]; + +(*If r allows well-founded induction then wf(r)*) +val [subs,indhyp] = goal WF.thy + "[| field(r)<=A; \ +\ !!y B. [| ALL x:A. (ALL y:A. :r --> y:B) --> x:B; y:A \ +\ |] ==> y:B |] \ +\ ==> wf(r)"; +br ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1; +by (REPEAT (ares_tac [indhyp] 1)); +val wfI2 = result(); + + +(*** Properties of well-founded relations ***) + +goal WF.thy "!!r. wf(r) ==> ~: r"; +by (wf_ind_tac "a" [] 1); +by (fast_tac ZF_cs 1); +val wf_not_refl = result(); + +goal WF.thy "!!r. [| wf(r); :r; :r |] ==> P"; +by (subgoal_tac "ALL x. :r --> :r --> P" 1); +by (wf_ind_tac "a" [] 2); by (fast_tac ZF_cs 2); -by (fast_tac (FOL_cs addIs prems) 1); +by (fast_tac FOL_cs 1); val wf_anti_sym = result(); -(*transitive closure of a WF relation is WF!*) -val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; -by (rtac (trancl_type RS field_rel_subset RS wfI2) 1); -by (rtac subsetI 1); -(*must retain the universal formula for later use!*) -by (rtac (bspec RS mp) 1 THEN assume_tac 1 THEN assume_tac 1); -by (eres_inst_tac [("a","x")] (prem RS wf_induct2) 1); -by (rtac subset_refl 1); -by (rtac (impI RS allI) 1); +goal WF.thy "!!r. [| wf[A](r); a: A |] ==> ~: r"; +by (wf_on_ind_tac "a" [] 1); +by (fast_tac ZF_cs 1); +val wf_on_not_refl = result(); + +goal WF.thy "!!r. [| wf[A](r); :r; :r; a:A; b:A |] ==> P"; +by (subgoal_tac "ALL y:A. :r --> :r --> P" 1); +by (wf_on_ind_tac "a" [] 2); +by (fast_tac ZF_cs 2); +by (fast_tac ZF_cs 1); +val wf_on_anti_sym = result(); + +(*Needed to prove well_ordI. Could also reason that wf[A](r) means + wf(r Int A*A); thus wf( (r Int A*A)^+ ) and use wf_not_refl *) +goal WF.thy + "!!r. [| wf[A](r); :r; :r; :r; a:A; b:A; c:A |] ==> P"; +by (subgoal_tac + "ALL y:A. ALL z:A. :r --> :r --> :r --> P" 1); +by (wf_on_ind_tac "a" [] 2); +by (fast_tac ZF_cs 2); +by (fast_tac ZF_cs 1); +val wf_on_chain3 = result(); + + +(*retains the universal formula for later use!*) +val bchain_tac = EVERY' [rtac (bspec RS mp), assume_tac, assume_tac ]; + +(*transitive closure of a WF relation is WF provided A is downwards closed*) +val [wfr,subs] = goal WF.thy + "[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)"; +br wf_onI2 1; +by (bchain_tac 1); +by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1); +by (rtac (impI RS ballI) 1); by (etac tranclE 1); -by (etac (bspec RS mp) 1); -by (etac fieldI1 1); +by (etac (bspec RS mp) 1 THEN assume_tac 1); by (fast_tac ZF_cs 1); +by (cut_facts_tac [subs] 1); +(*astar_tac is slightly faster*) +by (best_tac ZF_cs 1); +val wf_on_trancl = result(); + +goal WF.thy "!!r. wf(r) ==> wf(r^+)"; +by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1); +br (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1; +be wf_on_trancl 1; by (fast_tac ZF_cs 1); val wf_trancl = result(); + + (** r-``{a} is the set of everything under a in r **) val underI = standard (vimage_singleton_iff RS iffD2); @@ -247,3 +337,12 @@ by (REPEAT (ares_tac (prems@[lam_type]) 1 ORELSE eresolve_tac [spec RS mp, underD] 1)); val wfrec_type = result(); + + +goalw WF.thy [wf_on_def, wfrec_on_def] + "!!A r. [| wf[A](r); a: A |] ==> \ +\ wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))"; +be (wfrec RS trans) 1; +by (asm_simp_tac (ZF_ss addsimps [vimage_Int_square, cons_subset_iff]) 1); +val wfrec_on = result(); + diff -r 89d45187f04d -r ca5356bd315a src/ZF/WF.thy --- a/src/ZF/WF.thy Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/WF.thy Tue Jun 21 17:20:34 1994 +0200 @@ -1,22 +1,28 @@ (* Title: ZF/wf.thy ID: $Id$ Author: Tobias Nipkow and Lawrence C Paulson - Copyright 1992 University of Cambridge + Copyright 1994 University of Cambridge Well-founded Recursion *) -WF = Trancl + "mono" + +WF = Trancl + "mono" + "equalities" + consts - wf :: "i=>o" - wftrec,wfrec :: "[i, i, [i,i]=>i] =>i" - is_recfun :: "[i, i, [i,i]=>i, i] =>o" - the_recfun :: "[i, i, [i,i]=>i] =>i" + wf :: "i=>o" + wf_on :: "[i,i]=>o" ("wf[_]'(_')") + + wftrec,wfrec :: "[i, i, [i,i]=>i] =>i" + wfrec_on :: "[i, i, i, [i,i]=>i] =>i" ("wfrec[_]'(_,_,_')") + is_recfun :: "[i, i, [i,i]=>i, i] =>o" + the_recfun :: "[i, i, [i,i]=>i] =>i" rules (*r is a well-founded relation*) wf_def "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. :r --> ~ y:Z)" + (*r is well-founded relation over A*) + wf_on_def "wf_on(A,r) == wf(r Int A*A)" + is_recfun_def "is_recfun(r,a,H,f) == \ \ (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))" @@ -27,4 +33,6 @@ (*public version. Does not require r to be transitive*) wfrec_def "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))" + wfrec_on_def "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)" + end diff -r 89d45187f04d -r ca5356bd315a src/ZF/ZF.ML --- a/src/ZF/ZF.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/ZF.ML Tue Jun 21 17:20:34 1994 +0200 @@ -1,7 +1,7 @@ (* Title: ZF/zf.ML ID: $Id$ Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory - Copyright 1992 University of Cambridge + Copyright 1994 University of Cambridge Basic introduction and elimination rules for Zermelo-Fraenkel Set Theory *) @@ -10,63 +10,66 @@ signature ZF_LEMMAS = sig - val ballE : thm - val ballI : thm - val ball_cong : thm - val ball_simp : thm - val ball_tac : int -> tactic - val bexCI : thm - val bexE : thm - val bexI : thm - val bex_cong : thm - val bspec : thm - val CollectD1 : thm - val CollectD2 : thm - val CollectE : thm - val CollectI : thm - val Collect_cong : thm - val emptyE : thm - val empty_subsetI : thm - val equalityCE : thm - val equalityD1 : thm - val equalityD2 : thm - val equalityE : thm - val equalityI : thm - val equality_iffI : thm - val equals0D : thm - val equals0I : thm - val ex1_functional : thm - val InterD : thm - val InterE : thm - val InterI : thm - val INT_E : thm - val INT_I : thm - val lemmas_cs : claset - val PowD : thm - val PowI : thm - val RepFunE : thm - val RepFunI : thm - val RepFun_eqI : thm - val RepFun_cong : thm - val ReplaceE : thm - val ReplaceI : thm - val Replace_iff : thm - val Replace_cong : thm - val rev_ballE : thm - val rev_bspec : thm - val rev_subsetD : thm - val separation : thm - val setup_induction : thm - val set_mp_tac : int -> tactic - val subsetCE : thm - val subsetD : thm - val subsetI : thm - val subset_refl : thm - val subset_trans : thm - val UnionE : thm - val UnionI : thm - val UN_E : thm - val UN_I : thm + val ballE : thm + val ballI : thm + val ball_cong : thm + val ball_simp : thm + val ball_tac : int -> tactic + val bexCI : thm + val bexE : thm + val bexI : thm + val bex_cong : thm + val bspec : thm + val CollectD1 : thm + val CollectD2 : thm + val CollectE : thm + val CollectI : thm + val Collect_cong : thm + val emptyE : thm + val empty_subsetI : thm + val equalityCE : thm + val equalityD1 : thm + val equalityD2 : thm + val equalityE : thm + val equalityI : thm + val equality_iffI : thm + val equals0D : thm + val equals0I : thm + val ex1_functional : thm + val InterD : thm + val InterE : thm + val InterI : thm + val INT_E : thm + val INT_I : thm + val INT_cong : thm + val lemmas_cs : claset + val PowD : thm + val PowI : thm + val RepFunE : thm + val RepFunI : thm + val RepFun_eqI : thm + val RepFun_cong : thm + val ReplaceE : thm + val ReplaceI : thm + val Replace_iff : thm + val Replace_cong : thm + val rev_ballE : thm + val rev_bspec : thm + val rev_subsetD : thm + val separation : thm + val setup_induction : thm + val set_mp_tac : int -> tactic + val subsetCE : thm + val subsetD : thm + val subsetI : thm + val subset_iff : thm + val subset_refl : thm + val subset_trans : thm + val UnionE : thm + val UnionI : thm + val UN_E : thm + val UN_I : thm + val UN_cong : thm end; @@ -175,6 +178,11 @@ val subset_trans = prove_goal ZF.thy "[| A<=B; B<=C |] ==> A<=C" (fn prems=> [ (REPEAT (ares_tac ([subsetI]@(prems RL [subsetD])) 1)) ]); +(*Useful for proving A<=B by rewriting in some cases*) +val subset_iff = prove_goalw ZF.thy [subset_def,Ball_def] + "A<=B <-> (ALL x. x:A --> x:B)" + (fn _=> [ (rtac iff_refl 1) ]); + (*** Rules for equality ***) @@ -379,6 +387,10 @@ [ (rtac (major RS UnionE) 1), (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]); +val UN_cong = prove_goal ZF.thy + "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A.C(x)) = (UN x:B.D(x))" + (fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]); + (*** Rules for Intersections of families ***) (* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *) @@ -395,6 +407,10 @@ [ (rtac (major RS InterD) 1), (rtac (minor RS RepFunI) 1) ]); +val INT_cong = prove_goal ZF.thy + "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A.C(x)) = (INT x:B.D(x))" + (fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]); + (*** Rules for Powersets ***) diff -r 89d45187f04d -r ca5356bd315a src/ZF/equalities.ML --- a/src/ZF/equalities.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/equalities.ML Tue Jun 21 17:20:34 1994 +0200 @@ -58,6 +58,10 @@ by (fast_tac (eq_cs addSEs [equalityE]) 1); val subset_Int_iff = result(); +goal ZF.thy "A<=B <-> B Int A = A"; +by (fast_tac (eq_cs addSEs [equalityE]) 1); +val subset_Int_iff2 = result(); + (** Binary Union **) goal ZF.thy "0 Un A = A"; @@ -88,6 +92,10 @@ by (fast_tac (eq_cs addSEs [equalityE]) 1); val subset_Un_iff = result(); +goal ZF.thy "A<=B <-> B Un A = B"; +by (fast_tac (eq_cs addSEs [equalityE]) 1); +val subset_Un_iff2 = result(); + (** Simple properties of Diff -- set difference **) goal ZF.thy "A-A = 0"; @@ -161,6 +169,10 @@ by (fast_tac eq_cs 1); val Union_Un_distrib = result(); +goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)"; +by (fast_tac ZF_cs 1); +val Union_Int_subset = result(); + goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)"; by (fast_tac (eq_cs addSEs [equalityE]) 1); val Union_disjoint = result(); @@ -208,15 +220,13 @@ by (fast_tac eq_cs 1); val Un_INT_distrib2 = result(); -goal ZF.thy "!!A. [| a: A; ALL y:A. b(y)=b(a) |] ==> (UN y:A. b(y)) = b(a)"; -by (fast_tac (eq_cs addSEs [equalityE]) 1); -val UN_singleton_lemma = result(); -val UN_singleton = ballI RSN (2,UN_singleton_lemma); +goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c"; +by (fast_tac eq_cs 1); +val UN_constant = result(); -goal ZF.thy "!!A. [| a: A; ALL y:A. b(y)=b(a) |] ==> (INT y:A. b(y)) = b(a)"; -by (fast_tac (eq_cs addSEs [equalityE]) 1); -val INT_singleton_lemma = result(); -val INT_singleton = ballI RSN (2,INT_singleton_lemma); +goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c"; +by (fast_tac eq_cs 1); +val INT_constant = result(); (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: Union of a family of unions **) @@ -292,7 +302,7 @@ val range_Un_eq = result(); goal ZF.thy "range(A Int B) <= range(A) Int range(B)"; -by (fast_tac eq_cs 1); +by (fast_tac ZF_cs 1); val range_Int_subset = result(); goal ZF.thy "range(A) - range(B) <= range(A - B)"; @@ -312,6 +322,52 @@ val field_diff_subset = result(); +(** Image **) + +goal ZF.thy "r``0 = 0"; +by (fast_tac eq_cs 1); +val image_empty = result(); + +goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)"; +by (fast_tac eq_cs 1); +val image_Un = result(); + +goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)"; +by (fast_tac ZF_cs 1); +val image_Int_subset = result(); + +goal ZF.thy "(r Int A*A)``B <= (r``B) Int A"; +by (fast_tac ZF_cs 1); +val image_Int_square_subset = result(); + +goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A"; +by (fast_tac eq_cs 1); +val image_Int_square = result(); + + +(** Inverse Image **) + +goal ZF.thy "r-``0 = 0"; +by (fast_tac eq_cs 1); +val vimage_empty = result(); + +goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)"; +by (fast_tac eq_cs 1); +val vimage_Un = result(); + +goal ZF.thy "r-``(A Int B) <= (r-``A) Int (r-``B)"; +by (fast_tac ZF_cs 1); +val vimage_Int_subset = result(); + +goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A"; +by (fast_tac ZF_cs 1); +val vimage_Int_square_subset = result(); + +goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A"; +by (fast_tac eq_cs 1); +val vimage_Int_square = result(); + + (** Converse **) goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)"; @@ -351,3 +407,4 @@ goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))"; by (fast_tac eq_cs 1); val INT_Pow_subset = result(); + diff -r 89d45187f04d -r ca5356bd315a src/ZF/func.ML --- a/src/ZF/func.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/func.ML Tue Jun 21 17:20:34 1994 +0200 @@ -223,6 +223,19 @@ val Pi_lamE = result(); +(** Images of functions **) + +goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}"; +by (fast_tac eq_cs 1); +val image_lam = result(); + +goal ZF.thy "!!C A. [| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}"; +be (eta RS subst) 1; +by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff] + addcongs [RepFun_cong]) 1); +val image_fun = result(); + + (*** properties of "restrict" ***) goalw ZF.thy [restrict_def,lam_def] diff -r 89d45187f04d -r ca5356bd315a src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/ind_syntax.ML Tue Jun 21 17:20:34 1994 +0200 @@ -89,7 +89,6 @@ val Trueprop = Const("Trueprop",oT-->propT); fun mk_tprop P = Trueprop $ P; -fun dest_tprop (Const("Trueprop",_) $ P) = P; (*Prove a goal stated as a term, with exception handling*) fun prove_term sign defs (P,tacsf) = @@ -113,9 +112,14 @@ (*Return the conclusion of a rule, of the form t:X*) fun rule_concl rl = - case dest_tprop (Logic.strip_imp_concl rl) of - Const("op :",_) $ t $ X => (t,X) - | _ => error "Conclusion of rule should be a set membership"; + let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = + Logic.strip_imp_concl rl + in (t,X) end; + +(*As above, but return error message if bad*) +fun rule_concl_msg sign rl = rule_concl rl + handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ + Sign.string_of_term sign rl); (*For deriving cases rules. CollectD2 discards the domain, which is redundant; read_instantiate replaces a propositional variable by a formula variable*) diff -r 89d45187f04d -r ca5356bd315a src/ZF/intr_elim.ML --- a/src/ZF/intr_elim.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/intr_elim.ML Tue Jun 21 17:20:34 1994 +0200 @@ -119,7 +119,7 @@ val intr_tms = map (term_of o rd propT) sintrs; local (*Checking the introduction rules*) - val intr_sets = map (#2 o rule_concl) intr_tms; + val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; fun intr_ok set = case head_of set of Const(a,recT) => a mem rec_names | _ => false; @@ -154,6 +154,10 @@ | chk_prem rec_hd t = deny (rec_hd occs t) "Recursion term in side formula"; +fun dest_tprop (Const("Trueprop",_) $ P) = P + | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ + Sign.string_of_term sign Q); + (*Makes a disjunct from an introduction rule*) fun lfp_part intr = (*quantify over rule's free vars except parameters*) let val prems = map dest_tprop (strip_imp_prems intr) @@ -213,7 +217,7 @@ val prove = prove_term (sign_of thy); (********) -val dummy = writeln "Proving monotonocity..."; +val dummy = writeln "Proving monotonicity..."; val bnd_mono = prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs), diff -r 89d45187f04d -r ca5356bd315a src/ZF/pair.ML --- a/src/ZF/pair.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/pair.ML Tue Jun 21 17:20:34 1994 +0200 @@ -103,7 +103,7 @@ val split = prove_goalw ZF.thy [split_def] "split(%x y.c(x,y), ) = c(a,b)" (fn _ => - [ (fast_tac (upair_cs addIs [the_equality] addEs [Pair_inject]) 1) ]); + [ (fast_tac (upair_cs addIs [the_equality] addSEs [Pair_inject]) 1) ]); val split_type = prove_goal ZF.thy "[| p:Sigma(A,B); \ @@ -114,6 +114,16 @@ (etac ssubst 1), (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]); + +goal ZF.thy + "!!u. u: A*B ==> \ +\ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = --> R(c(x,y)))"; +by (etac SigmaE 1); +by (asm_simp_tac (FOL_ss addsimps [split]) 1); +by (fast_tac (upair_cs addSEs [Pair_inject]) 1); +val expand_split = result(); + + (*** conversions for fst and snd ***) val fst_conv = prove_goalw ZF.thy [fst_def] "fst() = a" diff -r 89d45187f04d -r ca5356bd315a src/ZF/simpdata.ML --- a/src/ZF/simpdata.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/simpdata.ML Tue Jun 21 17:20:34 1994 +0200 @@ -79,15 +79,18 @@ Some rls => flat (map atomize ([th] RL rls)) | None => [th]) | _ => [th] - in case concl_of th of (*The operator below is Trueprop*) - _ $ (Const("op :",_) $ a $ b) => tryrules atomize_mem_pairs b - | _ $ (Const("True",_)) => [] (*True is DELETED*) - | _ $ (Const("False",_)) => [] (*should False do something??*) - | _ $ A => tryrules atomize_pairs A + in case concl_of th of + Const("Trueprop",_) $ P => + (case P of + Const("op :",_) $ a $ b => tryrules atomize_mem_pairs b + | Const("True",_) => [] + | Const("False",_) => [] + | A => tryrules atomize_pairs A) + | _ => [th] end; val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, - beta, eta, restrict, fst_conv, snd_conv, split]; + beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff]; (*Sigma_cong, Pi_cong NOT included by default since they cause flex-flex pairs and the "Check your prover" error -- because most diff -r 89d45187f04d -r ca5356bd315a src/ZF/upair.ML --- a/src/ZF/upair.ML Tue Jun 21 16:26:34 1994 +0200 +++ b/src/ZF/upair.ML Tue Jun 21 17:20:34 1994 +0200 @@ -167,6 +167,15 @@ (resolve_tac [major RS the_equality2 RS ssubst] 1), (REPEAT (assume_tac 1)) ]); +(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then + (THE x.P(x)) rewrites to (THE x. Q(x)) *) + +(*If it's "undefined", it's zero!*) +val the_0 = prove_goalw ZF.thy [the_def] + "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0" + (fn _ => + [ (fast_tac (lemmas_cs addIs [equalityI]) 1) ]); + (*** if -- a conditional expression for formulae ***) @@ -226,6 +235,10 @@ val mem_not_refl = prove_goal ZF.thy "a~:a" (K [ (rtac notI 1), (etac mem_anti_refl 1) ]); +(*Good for proving inequalities by rewriting*) +val mem_imp_not_eq = prove_goal ZF.thy "!!a A. a:A ==> a ~= A" + (fn _=> [ fast_tac (lemmas_cs addSEs [mem_anti_refl]) 1 ]); + (*** Rules for succ ***) val succI1 = prove_goalw ZF.thy [succ_def] "i : succ(i)"