# HG changeset patch # User paulson # Date 1010502549 -3600 # Node ID 7e6eaaa125f2a3a9ccbdafff8d6175105808c1de # Parent 9842befead7ad3f9196431aedf4ef639d6d59113 Added some simprules proofs. Converted theories CardinalArith and OrdQuant to Isar style diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/AC/AC7_AC9.ML --- a/src/ZF/AC/AC7_AC9.ML Tue Jan 08 15:39:47 2002 +0100 +++ b/src/ZF/AC/AC7_AC9.ML Tue Jan 08 16:09:09 2002 +0100 @@ -161,7 +161,8 @@ \ B1: C; B2: C |] \ \ ==> B1 eqpoll B2"; by (blast_tac - (claset() addSIs [nat_lepoll_lemma, nat_cons_eqpoll RS eqpoll_trans, + (claset() delrules [eqpoll_refl] + addSIs [nat_lepoll_lemma, nat_cons_eqpoll RS eqpoll_trans, eqpoll_refl RSN (2, prod_eqpoll_cong)] addIs [eqpoll_trans, eqpoll_sym, Sigma_fun_space_eqpoll]) 1); val lemma1 = result(); diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/AC/AC_Equiv.ML --- a/src/ZF/AC/AC_Equiv.ML Tue Jan 08 15:39:47 2002 +0100 +++ b/src/ZF/AC/AC_Equiv.ML Tue Jan 08 16:09:09 2002 +0100 @@ -26,7 +26,7 @@ (* used in \\ AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) (*I don't know where to put this one.*) -goal Cardinal.thy +Goal "!!m A B. [| A lepoll succ(m); B \\ A; B\\0 |] ==> A-B lepoll m"; by (rtac not_emptyE 1 THEN (assume_tac 1)); by (ftac singleton_subsetI 1); @@ -65,7 +65,7 @@ qed "ordertype_Int"; (* used only in AC16_lemmas.ML *) -goalw CardinalArith.thy [InfCard_def] +Goalw [InfCard_def] "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; by (asm_simp_tac (simpset() addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); qed "Inf_Card_is_InfCard"; diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/AC/WO6_WO1.ML --- a/src/ZF/AC/WO6_WO1.ML Tue Jan 08 15:39:47 2002 +0100 +++ b/src/ZF/AC/WO6_WO1.ML Tue Jan 08 16:09:09 2002 +0100 @@ -290,6 +290,7 @@ uu_subset1 RSN (4, rel_is_fun)))] 1 THEN TRYALL assume_tac); by (rtac (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, supset_lepoll_imp_eq)) 1); +by (REPEAT_FIRST assume_tac); by (REPEAT (fast_tac (claset() addSIs [domain_uu_subset]) 1)); qed "uu_Least_is_fun"; diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/Cardinal.ML --- a/src/ZF/Cardinal.ML Tue Jan 08 15:39:47 2002 +0100 +++ b/src/ZF/Cardinal.ML Tue Jan 08 16:09:09 2002 +0100 @@ -57,6 +57,7 @@ (*A eqpoll A*) bind_thm ("eqpoll_refl", id_bij RS bij_imp_eqpoll); +Addsimps [eqpoll_refl]; Goalw [eqpoll_def] "X eqpoll Y ==> Y eqpoll X"; by (blast_tac (claset() addIs [bij_converse_bij]) 1); @@ -75,6 +76,7 @@ qed "subset_imp_lepoll"; bind_thm ("lepoll_refl", subset_refl RS subset_imp_lepoll); +Addsimps [lepoll_refl]; bind_thm ("le_imp_lepoll", le_imp_subset RS subset_imp_lepoll); diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/CardinalArith.ML --- a/src/ZF/CardinalArith.ML Tue Jan 08 15:39:47 2002 +0100 +++ b/src/ZF/CardinalArith.ML Tue Jan 08 16:09:09 2002 +0100 @@ -11,6 +11,14 @@ coincide with union (maximum). Either way we get most laws for free. *) +val InfCard_def = thm "InfCard_def"; +val cmult_def = thm "cmult_def"; +val cadd_def = thm "cadd_def"; +val csquare_rel_def = thm "csquare_rel_def"; +val jump_cardinal_def = thm "jump_cardinal_def"; +val csucc_def = thm "csucc_def"; + + (*** Cardinal addition ***) (** Cardinal addition is commutative **) diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/CardinalArith.thy --- a/src/ZF/CardinalArith.thy Tue Jan 08 15:39:47 2002 +0100 +++ b/src/ZF/CardinalArith.thy Tue Jan 08 16:09:09 2002 +0100 @@ -6,41 +6,100 @@ Cardinal Arithmetic *) -CardinalArith = Cardinal + OrderArith + ArithSimp + Finite + -consts +theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite: - InfCard :: i=>o - "|*|" :: [i,i]=>i (infixl 70) - "|+|" :: [i,i]=>i (infixl 65) - csquare_rel :: i=>i - jump_cardinal :: i=>i - csucc :: i=>i +constdefs -defs + InfCard :: "i=>o" + "InfCard(i) == Card(i) & nat le i" - InfCard_def "InfCard(i) == Card(i) & nat le i" - - cadd_def "i |+| j == |i+j|" - - cmult_def "i |*| j == |i*j|" + cmult :: "[i,i]=>i" (infixl "|*|" 70) + "i |*| j == |i*j|" + + cadd :: "[i,i]=>i" (infixl "|+|" 65) + "i |+| j == |i+j|" - csquare_rel_def - "csquare_rel(K) == - rvimage(K*K, - lam :K*K. , - rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))" + csquare_rel :: "i=>i" + "csquare_rel(K) == + rvimage(K*K, + lam :K*K. , + rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))" (*This def is more complex than Kunen's but it more easily proved to be a cardinal*) - jump_cardinal_def - "jump_cardinal(K) == + jump_cardinal :: "i=>i" + "jump_cardinal(K) == UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" - + (*needed because jump_cardinal(K) might not be the successor of K*) - csucc_def "csucc(K) == LEAST L. Card(L) & Ki" + "csucc(K) == LEAST L. Card(L) & K i (infixl "\\" 65) - "op |*|" :: [i,i] => i (infixl "\\" 70) + "op |+|" :: "[i,i] => i" (infixl "\" 65) + "op |*|" :: "[i,i] => i" (infixl "\" 70) + + +(*** The following really belong in OrderType ***) + +lemma oadd_eq_0_iff: "\Ord(i); Ord(j)\ \ (i ++ j) = 0 <-> i=0 & j=0" +apply (erule trans_induct3 [of j]) +apply (simp_all add: oadd_Limit) +apply (simp add: Union_empty_iff Limit_def lt_def) +apply blast +done + +lemma oadd_eq_lt_iff: "\Ord(i); Ord(j)\ \ 0 < (i ++ j) <-> 0 i < i++j" +apply (rule lt_trans2) +apply (erule le_refl) +apply (simp only: lt_Ord2 oadd_1 [of i, symmetric]) +apply (blast intro: succ_leI oadd_le_mono) +done + +lemma oadd_LimitI: "\Ord(i); Limit(j)\ \ Limit(i ++ j)" +apply (simp add: oadd_Limit) +apply (frule Limit_has_1 [THEN ltD]) +apply (rule increasing_LimitI) + apply (rule Ord_0_lt) + apply (blast intro: Ord_in_Ord [OF Limit_is_Ord]) + apply (force simp add: Union_empty_iff oadd_eq_0_iff + Limit_is_Ord [of j, THEN Ord_in_Ord]) +apply auto +apply (rule_tac x="succ(x)" in bexI) + apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord]) +apply (simp add: Limit_def lt_def) +done + +(*** The following really belong in Cardinal ***) + +lemma lesspoll_not_refl: "~ (i lesspoll i)" +by (simp add: lesspoll_def) + +lemma lesspoll_irrefl [elim!]: "i lesspoll i ==> P" +by (simp add: lesspoll_def) + +lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))" +apply (rule CardI) + apply (simp add: Card_is_Ord) +apply (clarify dest!: ltD) +apply (drule bspec, assumption) +apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) +apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll]) +apply (drule lesspoll_trans1, assumption) +apply (subgoal_tac "B lepoll \A") + apply (drule lesspoll_trans1, assumption, blast) +apply (blast intro: subset_imp_lepoll) +done + +lemma Card_UN: + "(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))" +by (blast intro: Card_Union) + +lemma Card_OUN [simp,intro,TC]: + "(!!x. x:A ==> Card(K(x))) ==> Card(UN x i" ("(3\_<_./ _)" 10) -declare Ord_Un [intro,simp] -declare Ord_UN [intro,simp] -declare Ord_Union [intro,simp] +declare Ord_Un [intro,simp,TC] +declare Ord_UN [intro,simp,TC] +declare Ord_Union [intro,simp,TC] (** These mostly belong to theory Ordinal **) @@ -49,6 +49,17 @@ apply auto done +lemma zero_not_Limit [iff]: "~ Limit(0)" +by (simp add: Limit_def) + +lemma Limit_has_1: "Limit(i) \ 1 < i" +by (blast intro: Limit_has_0 Limit_has_succ) + +lemma Limit_Union [rule_format]: "\I \ 0; \i\I. Limit(i)\ \ Limit(\I)" +apply (simp add: Limit_def lt_def) +apply (blast intro!: equalityI) +done + lemma increasing_LimitI: "\0x\l. \y\l. x \ Limit(l)" apply (simp add: Limit_def lt_Ord2) apply clarify diff -r 9842befead7a -r 7e6eaaa125f2 src/ZF/OrderType.ML --- a/src/ZF/OrderType.ML Tue Jan 08 15:39:47 2002 +0100 +++ b/src/ZF/OrderType.ML Tue Jan 08 16:09:09 2002 +0100 @@ -364,6 +364,7 @@ "[| Ord(i); Ord(j) |] ==> Ord(i++j)"; by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 1)); qed "Ord_oadd"; +Addsimps [Ord_oadd]; AddIs [Ord_oadd]; AddTCs [Ord_oadd]; (** Ordinal addition with zero **) @@ -495,9 +496,10 @@ Goal "[| Ord(i); Ord(j) |] ==> i++succ(j) = succ(i++j)"; (*FOL_ss prevents looping*) -by (asm_simp_tac (FOL_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1); -by (asm_simp_tac (simpset() addsimps [oadd_1, oadd_assoc, Ord_1]) 1); +by (asm_simp_tac (FOL_ss delsimps [oadd_1] + addsimps [Ord_oadd, oadd_1 RS sym, oadd_assoc, Ord_1]) 1); qed "oadd_succ"; +Addsimps [oadd_succ]; (** Ordinal addition with limit ordinals **) @@ -549,11 +551,13 @@ qed "oadd_lt_mono"; Goal "[| i' le i; j' le j |] ==> i'++j' le i++j"; -by (asm_simp_tac (simpset() addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1); +by (asm_simp_tac (simpset() delsimps [oadd_succ] + addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1); qed "oadd_le_mono"; Goal "[| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"; -by (asm_simp_tac (simpset() addsimps [oadd_lt_iff2, oadd_succ RS sym, +by (asm_simp_tac (simpset() delsimps [oadd_succ] + addsimps [oadd_lt_iff2, oadd_succ RS sym, Ord_succ]) 1); qed "oadd_le_iff2"; @@ -761,9 +765,8 @@ Goal "[| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i"; (*FOL_ss prevents looping*) -by (asm_simp_tac (FOL_ss addsimps [oadd_1 RS sym]) 1); -by (asm_simp_tac - (simpset() addsimps [omult_1, oadd_omult_distrib, Ord_1]) 1); +by (asm_simp_tac (FOL_ss addsimps [oadd_1 RS sym, omult_1, oadd_omult_distrib, + Ord_1]) 1); qed "omult_succ"; (** Associative law **)