# HG changeset patch # User wenzelm # Date 1030439375 -7200 # Node ID 007559e981c7920b5ded325b875c9dc3eb6e4d7b # Parent ca6debb89d77e66fd6b04ecd570b6922a557330a *** empty log message *** diff -r ca6debb89d77 -r 007559e981c7 src/ZF/AC/AC15_WO6.thy --- a/src/ZF/AC/AC15_WO6.thy Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/AC/AC15_WO6.thy Tue Aug 27 11:09:35 2002 +0200 @@ -145,7 +145,7 @@ lemma OUN_eq_UN: "Ord(x) ==> (\aa \ x. F(a))" by (fast intro!: ltI dest!: ltD) -lemma lemma1: +lemma AC15_WO6_aux1: "\x \ Pow(A)-{0}. f`x\0 & f`x \ x & f`x \ m ==> (\ix \ Pow(A)-{0}. f`x\0 & f`x \ x & f`x \ m ==> \x < (LEAST x. HH(f,A,x)={A}). HH(f,A,x) \ m" apply (rule oallI) @@ -163,7 +163,7 @@ apply (frule HH_subset_imp_eq) apply (erule ssubst) apply (blast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2]) - (*but can't use del: DiffE despite the obvious conflictc*) + (*but can't use del: DiffE despite the obvious conflict*) done theorem AC15_WO6: "AC15 ==> WO6" @@ -178,7 +178,7 @@ apply (rule_tac x = "\j \ (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI) apply (simp_all add: ltD) apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun] - elim!: less_Least_subset_x lemma1 lemma2) + elim!: less_Least_subset_x AC15_WO6_aux1 AC15_WO6_aux2) done diff -r ca6debb89d77 -r 007559e981c7 src/ZF/AC/AC17_AC1.thy --- a/src/ZF/AC/AC17_AC1.thy Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/AC/AC17_AC1.thy Tue Aug 27 11:09:35 2002 +0200 @@ -78,7 +78,7 @@ apply (blast intro: lam_type) done -lemma lemma1: +lemma AC17_AC1_aux1: "[| \f \ Pow(x) - {0} -> x. \u \ Pow(x) - {0}. f`u\u; \f \ Pow(x)-{0}->x. x - (\a \ (LEAST i. HH(\X \ Pow(x)-{0}. {f`X},x,i)={x}). @@ -94,18 +94,18 @@ apply (blast dest: apply_type) done -lemma lemma2: +lemma AC17_AC1_aux2: "~ (\f \ Pow(x)-{0}->x. x - F(f) = 0) ==> (\f \ Pow(x)-{0}->x . x - F(f)) \ (Pow(x) -{0} -> x) -> Pow(x) - {0}" by (fast intro!: lam_type dest!: Diff_eq_0_iff [THEN iffD1]) -lemma lemma3: +lemma AC17_AC1_aux3: "[| f`Z \ Z; Z \ Pow(x)-{0} |] ==> (\X \ Pow(x)-{0}. {f`X})`Z \ Pow(Z)-{0}" by auto -lemma lemma4: +lemma AC17_AC1_aux4: "\f \ F. f`((\f \ F. Q(f))`f) \ (\f \ F. Q(f))`f ==> \f \ F. f`Q(f) \ Q(f)" by simp @@ -117,15 +117,15 @@ apply (case_tac "\f \ Pow(x)-{0} -> x. x - (\a \ (LEAST i. HH (\X \ Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\X \ Pow (x) -{0}. {f`X},x,a)) = 0") -apply (erule lemma1, assumption) -apply (drule lemma2) +apply (erule AC17_AC1_aux1, assumption) +apply (drule AC17_AC1_aux2) apply (erule allE) apply (drule bspec, assumption) -apply (drule lemma4) +apply (drule AC17_AC1_aux4) apply (erule bexE) apply (drule apply_type, assumption) apply (simp add: HH_Least_eq_x del: Diff_iff ) -apply (drule lemma3, assumption) +apply (drule AC17_AC1_aux3, assumption) apply (fast dest!: subst_elem [OF _ HH_Least_eq_x [symmetric]] f_subset_imp_HH_subset elim!: mem_irrefl) done @@ -142,11 +142,11 @@ (* AC1 ==> AC2 *) (* ********************************************************************** *) -lemma lemma1: +lemma AC1_AC2_aux1: "[| f:(\X \ A. X); B \ A; 0\A |] ==> {f`B} \ B Int {f`C. C \ A}" by (fast elim!: apply_type) -lemma lemma2: +lemma AC1_AC2_aux2: "[| pairwise_disjoint(A); B \ A; C \ A; D \ B; D \ C |] ==> f`B = f`C" by (unfold pairwise_disjoint_def, fast) @@ -156,8 +156,8 @@ apply (rule impI) apply (elim asm_rl conjE allE exE impE, assumption) apply (intro exI ballI equalityI) -prefer 2 apply (rule lemma1, assumption+) -apply (fast elim!: lemma2 elim: apply_type) +prefer 2 apply (rule AC1_AC2_aux1, assumption+) +apply (fast elim!: AC1_AC2_aux2 elim: apply_type) done @@ -165,30 +165,30 @@ (* AC2 ==> AC1 *) (* ********************************************************************** *) -lemma lemma1: "0\A ==> 0 \ {B*{B}. B \ A}" +lemma AC2_AC1_aux1: "0\A ==> 0 \ {B*{B}. B \ A}" by (fast dest!: sym [THEN Sigma_empty_iff [THEN iffD1]]) -lemma lemma2: "[| X*{X} Int C = {y}; X \ A |] +lemma AC2_AC1_aux2: "[| X*{X} Int C = {y}; X \ A |] ==> (THE y. X*{X} Int C = {y}): X*A" apply (rule subst_elem [of y]) apply (blast elim!: equalityE) apply (auto simp add: singleton_eq_iff) done -lemma lemma3: +lemma AC2_AC1_aux3: "\D \ {E*{E}. E \ A}. \y. D Int C = {y} ==> (\x \ A. fst(THE z. (x*{x} Int C = {z}))) \ (\X \ A. X)" apply (rule lam_type) apply (drule bspec, blast) -apply (blast intro: lemma2 fst_type) +apply (blast intro: AC2_AC1_aux2 fst_type) done lemma AC2_AC1: "AC2 ==> AC1" apply (unfold AC1_def AC2_def pairwise_disjoint_def) apply (intro allI impI) apply (elim allE impE) -prefer 2 apply (fast elim!: lemma3) -apply (blast intro!: lemma1) +prefer 2 apply (fast elim!: AC2_AC1_aux3) +apply (blast intro!: AC2_AC1_aux1) done @@ -211,21 +211,21 @@ (* AC4 ==> AC3 *) (* ********************************************************************** *) -lemma lemma1: "f \ A->B ==> (\z \ A. {z}*f`z) \ A*Union(B)" +lemma AC4_AC3_aux1: "f \ A->B ==> (\z \ A. {z}*f`z) \ A*Union(B)" by (fast dest!: apply_type) -lemma lemma2: "domain(\z \ A. {z}*f(z)) = {a \ A. f(a)\0}" +lemma AC4_AC3_aux2: "domain(\z \ A. {z}*f(z)) = {a \ A. f(a)\0}" by blast -lemma lemma3: "x \ A ==> (\z \ A. {z}*f(z))``{x} = f(x)" +lemma AC4_AC3_aux3: "x \ A ==> (\z \ A. {z}*f(z))``{x} = f(x)" by fast lemma AC4_AC3: "AC4 ==> AC3" apply (unfold AC3_def AC4_def) apply (intro allI ballI) apply (elim allE impE) -apply (erule lemma1) -apply (simp add: lemma2 lemma3 cong add: Pi_cong) +apply (erule AC4_AC3_aux1) +apply (simp add: AC4_AC3_aux2 AC4_AC3_aux3 cong add: Pi_cong) done (* ********************************************************************** *) @@ -264,18 +264,18 @@ (* AC5 ==> AC4, Rubin & Rubin, p. 11 *) (* ********************************************************************** *) -lemma lemma1: "R \ A*B ==> (\x \ R. fst(x)) \ R -> A" +lemma AC5_AC4_aux1: "R \ A*B ==> (\x \ R. fst(x)) \ R -> A" by (fast intro!: lam_type fst_type) -lemma lemma2: "R \ A*B ==> range(\x \ R. fst(x)) = domain(R)" +lemma AC5_AC4_aux2: "R \ A*B ==> range(\x \ R. fst(x)) = domain(R)" by (unfold lam_def, force) -lemma lemma3: "[| \f \ A->C. P(f,domain(f)); A=B |] ==> \f \ B->C. P(f,B)" +lemma AC5_AC4_aux3: "[| \f \ A->C. P(f,domain(f)); A=B |] ==> \f \ B->C. P(f,B)" apply (erule bexE) apply (frule domain_of_fun, fast) done -lemma lemma4: "[| R \ A*B; g \ C->R; \x \ C. (\z \ R. fst(z))` (g`x) = x |] +lemma AC5_AC4_aux4: "[| R \ A*B; g \ C->R; \x \ C. (\z \ R. fst(z))` (g`x) = x |] ==> (\x \ C. snd(g`x)): (\x \ C. R``{x})" apply (rule lam_type) apply (force dest: apply_type) @@ -284,9 +284,9 @@ lemma AC5_AC4: "AC5 ==> AC4" apply (unfold AC4_def AC5_def, clarify) apply (elim allE ballE) -apply (drule lemma3 [OF _ lemma2], assumption) -apply (fast elim!: lemma4) -apply (blast intro: lemma1) +apply (drule AC5_AC4_aux3 [OF _ AC5_AC4_aux2], assumption) +apply (fast elim!: AC5_AC4_aux4) +apply (blast intro: AC5_AC4_aux1) done diff -r ca6debb89d77 -r 007559e981c7 src/ZF/Constructible/Formula.thy --- a/src/ZF/Constructible/Formula.thy Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/Constructible/Formula.thy Tue Aug 27 11:09:35 2002 +0200 @@ -164,11 +164,6 @@ ==> (P | Q) <-> sats(A, Or(p,q), env)" by (simp add: sats_Or_iff) -lemma imp_iff_sats: - "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \ list(A)|] - ==> (P --> Q) <-> sats(A, Implies(p,q), env)" -by (simp add: sats_Forall_iff) - lemma iff_iff_sats: "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \ list(A)|] ==> (P <-> Q) <-> sats(A, Iff(p,q), env)" @@ -819,8 +814,6 @@ apply (blast intro: doubleton_in_Lset) done -lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard] - lemma singleton_in_LLimit: "[| a: Lset(i); Limit(i) |] ==> {a} : Lset(i)" apply (erule Limit_LsetE, assumption) @@ -974,7 +967,7 @@ done text{*Kunen's VI, 1.12 *} -lemma Lset_subset_Vset: "i \ nat ==> Lset(i) = Vset(i)"; +lemma Lset_subset_Vset': "i \ nat ==> Lset(i) = Vset(i)"; apply (erule nat_induct) apply (simp add: Vfrom_0) apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow) diff -r ca6debb89d77 -r 007559e981c7 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Tue Aug 27 11:09:35 2002 +0200 @@ -802,14 +802,6 @@ ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')" by (simp add: is_nat_case_def) -lemma (in M_triv_axioms) Inl_in_M_iff [iff]: - "M(Inl(a)) <-> M(a)" -by (simp add: Inl_def) - -lemma (in M_triv_axioms) Inr_in_M_iff [iff]: - "M(Inr(a)) <-> M(a)" -by (simp add: Inr_def) - subsection{*Absoluteness for Ordinals*} text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*} diff -r ca6debb89d77 -r 007559e981c7 src/ZF/Constructible/Satisfies_absolute.thy --- a/src/ZF/Constructible/Satisfies_absolute.thy Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/Constructible/Satisfies_absolute.thy Tue Aug 27 11:09:35 2002 +0200 @@ -595,8 +595,8 @@ done lemmas (in M_satisfies) - satisfies_closed = Formula_Rec.formula_rec_closed [OF Formula_Rec_M] -and satisfies_abs = Formula_Rec.formula_rec_abs [OF Formula_Rec_M] + satisfies_closed' = Formula_Rec.formula_rec_closed [OF Formula_Rec_M] +and satisfies_abs' = Formula_Rec.formula_rec_abs [OF Formula_Rec_M] lemma (in M_satisfies) satisfies_closed: diff -r ca6debb89d77 -r 007559e981c7 src/ZF/Induct/FoldSet.ML --- a/src/ZF/Induct/FoldSet.ML Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/Induct/FoldSet.ML Tue Aug 27 11:09:35 2002 +0200 @@ -301,7 +301,7 @@ by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); by (etac Finite_induct 1); by Auto_tac; -qed "setsum_0"; +qed "setsum_K0"; (*The reversed orientation looks more natural, but LOOPS as a simprule!*) Goal "[| Finite(C); Finite(D) |] \ diff -r ca6debb89d77 -r 007559e981c7 src/ZF/Induct/Multiset.ML --- a/src/ZF/Induct/Multiset.ML Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/Induct/Multiset.ML Tue Aug 27 11:09:35 2002 +0200 @@ -206,7 +206,7 @@ by (res_inst_tac [("x", "{x:A . 0 multiset(M -# N)"; -by (res_inst_tac [("A", "mset_of(M)")] normalize_multiset 1); +by (res_inst_tac [("A", "mset_of(M)")] multiset_normalize 1); by (asm_simp_tac (simpset() addsimps [multiset_set_of_Finite]) 2); by (auto_tac (claset(), simpset() addsimps [mset_of_def, multiset_def])); by (auto_tac (claset() addSIs [lam_type], diff -r ca6debb89d77 -r 007559e981c7 src/ZF/Induct/Tree_Forest.thy --- a/src/ZF/Induct/Tree_Forest.thy Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/Induct/Tree_Forest.thy Tue Aug 27 11:09:35 2002 +0200 @@ -45,7 +45,7 @@ apply (rule Part_subset) done -lemma treeI [TC]: "x \ forest(A) ==> x \ tree_forest(A)" +lemma treeI' [TC]: "x \ forest(A) ==> x \ tree_forest(A)" by (rule forest_subset_TF [THEN subsetD]) lemma TF_equals_Un: "tree(A) \ forest(A) = tree_forest(A)" diff -r ca6debb89d77 -r 007559e981c7 src/ZF/Integ/Bin.ML --- a/src/ZF/Integ/Bin.ML Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/Integ/Bin.ML Tue Aug 27 11:09:35 2002 +0200 @@ -412,10 +412,6 @@ Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT]; -bind_thms ("NCons_simps", - [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]); - - bind_thms ("bin_arith_extra_simps", [integ_of_add RS sym, (*invoke bin_add*) integ_of_minus RS sym, (*invoke bin_minus*) diff -r ca6debb89d77 -r 007559e981c7 src/ZF/UNITY/WFair.ML --- a/src/ZF/UNITY/WFair.ML Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/UNITY/WFair.ML Tue Aug 27 11:09:35 2002 +0200 @@ -387,7 +387,7 @@ by (blast_tac (claset() addIs leadsTo_refl::prems) 1); by (rtac (major RS leadsTo_induct) 1); by (REPEAT (blast_tac (claset() addIs prems) 1)); -qed "lemma"; +qed "leadsTo_induct_pre_aux"; val [major, zb_prem, basis_prem, union_prem] = Goal @@ -399,7 +399,7 @@ by (cut_facts_tac [major] 1); by (subgoal_tac "(F : za leadsTo zb) & P(za)" 1); by (etac conjunct2 1); -by (rtac (major RS lemma) 1); +by (rtac (major RS leadsTo_induct_pre_aux) 1); by (blast_tac (claset() addDs [leadsToD2] addIs [leadsTo_Union,union_prem]) 3); by (blast_tac (claset() addIs [leadsTo_Trans,basis_prem, leadsTo_Basis]) 2); @@ -501,7 +501,7 @@ by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1); by (auto_tac (claset() addIs [leadsTo_UN], simpset() delsimps UN_simps addsimps [Int_UN_distrib])); -qed "lemma1"; +qed "leadsTo_wf_induct_aux"; (** Meta or object quantifier ? **) Goal "[| wf(r); \ @@ -515,7 +515,7 @@ by (res_inst_tac [("I", "I")] leadsTo_UN 2); by (REPEAT (assume_tac 2)); by (Clarify_tac 2); -by (eres_inst_tac [("I", "I")] lemma1 2); +by (eres_inst_tac [("I", "I")] leadsTo_wf_induct_aux 2); by (REPEAT (assume_tac 2)); by (rtac equalityI 1); by Safe_tac; @@ -602,7 +602,7 @@ \ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"; by (Clarify_tac 1); by (Blast_tac 1); -qed "lemma1"; +qed "leadsTo_123_aux"; (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) (* slightly different from the HOL one: B here is bounded *) @@ -615,7 +615,7 @@ (*Trans*) by (Clarify_tac 1); by (res_inst_tac [("x", "Ba Un Bb")] bexI 1); -by (blast_tac (claset() addIs [lemma1,leadsTo_Un_Un, leadsTo_cancel1, +by (blast_tac (claset() addIs [leadsTo_123_aux,leadsTo_Un_Un, leadsTo_cancel1, leadsTo_Un_duplicate]) 1); by (Blast_tac 1); (*Union*) diff -r ca6debb89d77 -r 007559e981c7 src/ZF/ex/Limit.thy --- a/src/ZF/ex/Limit.thy Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/ex/Limit.thy Tue Aug 27 11:09:35 2002 +0200 @@ -542,12 +542,12 @@ matrix_chain_lub isub_lemma) done -lemma lemma1: +lemma lub_matrix_diag_aux1: "lub(D,(\n \ nat. lub(D,\m \ nat. M`n`m))) = (THE x. islub(D, (\n \ nat. lub(D,\m \ nat. M`n`m)), x))" by (simp add: lub_def) -lemma lemma2: +lemma lub_matrix_diag_aux2: "lub(D,(\n \ nat. M`n`n)) = (THE x. islub(D, (\n \ nat. M`n`n), x))" by (simp add: lub_def) @@ -556,7 +556,7 @@ "[|matrix(D,M); cpo(D)|] ==> lub(D,(\n \ nat. lub(D,\m \ nat. M`n`m))) = lub(D,(\n \ nat. M`n`n))" -apply (simp (no_asm) add: lemma1 lemma2) +apply (simp (no_asm) add: lub_matrix_diag_aux1 lub_matrix_diag_aux2) apply (simp add: islub_def isub_eq) done @@ -876,7 +876,7 @@ lemmas id_comp = fun_is_rel [THEN left_comp_id] and comp_id = fun_is_rel [THEN right_comp_id] -lemma lemma1: +lemma projpair_unique_aux1: "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p'); rel(cf(D,E),e,e')|] ==> rel(cf(E,D),p',p)" apply (rule_tac b=p' in @@ -899,7 +899,7 @@ text{*Proof's very like the previous one. Is there a pattern that could be exploited?*} -lemma lemma2: +lemma projpair_unique_aux2: "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p'); rel(cf(E,D),p',p)|] ==> rel(cf(D,E),e,e')" apply (rule_tac b=e @@ -923,7 +923,7 @@ lemma projpair_unique: "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p')|] ==> (e=e')<->(p=p')" -by (blast intro: cpo_antisym lemma1 lemma2 cpo_cf cont_cf +by (blast intro: cpo_antisym projpair_unique_aux1 projpair_unique_aux2 cpo_cf cont_cf dest: projpair_ep_cont) (* Slightly different, more asms, since THE chooses the unique element. *) @@ -1763,7 +1763,7 @@ (* 32 vs 61, using safe_tac with imp in asm would be unfortunate (5steps) *) -lemma lemma1: +lemma eps1_aux1: "[|m le n; emb_chain(DD,ee); x \ set(Dinf(DD,ee)); m \ nat; n \ nat|] ==> rel(DD`n,e_less(DD,ee,m,n)`(x`m),x`n)" apply (erule rev_mp) (* For induction proof *) @@ -1807,7 +1807,7 @@ (* 18 vs 40 *) -lemma lemma2: +lemma eps1_aux2: "[|n le m; emb_chain(DD,ee); x \ set(Dinf(DD,ee)); m \ nat; n \ nat|] ==> rel(DD`n,e_gr(DD,ee,m,n)`(x`m),x`n)" apply (erule rev_mp) (* For induction proof *) @@ -1835,7 +1835,7 @@ "[|emb_chain(DD,ee); x \ set(Dinf(DD,ee)); m \ nat; n \ nat|] ==> rel(DD`n,eps(DD,ee,m,n)`(x`m),x`n)" apply (simp add: eps_def) -apply (blast intro: lemma1 not_le_iff_lt [THEN iffD1, THEN leI, THEN lemma2] +apply (blast intro: eps1_aux1 not_le_iff_lt [THEN iffD1, THEN leI, THEN eps1_aux2] nat_into_Ord) done @@ -1894,7 +1894,7 @@ "[| emb_chain(DD,ee); n \ nat |] ==> emb(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))" by (auto simp add: emb_def intro: exI rho_projpair) -lemma commuteI: "[| emb_chain(DD,ee); n \ nat |] +lemma rho_proj_cont: "[| emb_chain(DD,ee); n \ nat |] ==> rho_proj(DD,ee,n) \ cont(Dinf(DD,ee),DD`n)" by (auto intro: rho_projpair projpair_p_cont)