# HG changeset patch # User paulson # Date 1023284095 -7200 # Node ID fac77a839aa2183dc0911d52f266b3099a4e98ec # Parent 53022e5f73ff72dd3b2e77605510483131ab143f Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files. diff -r 53022e5f73ff -r fac77a839aa2 src/ZF/Epsilon.thy --- a/src/ZF/Epsilon.thy Wed Jun 05 12:24:14 2002 +0200 +++ b/src/ZF/Epsilon.thy Wed Jun 05 15:34:55 2002 +0200 @@ -66,7 +66,9 @@ [| a: eclose(A); !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) |] ==> P(a) *) -lemmas eclose_induct = Transset_induct [OF _ Transset_eclose] +lemmas eclose_induct = + Transset_induct [OF _ Transset_eclose, induct set: eclose] + (*Epsilon induction*) lemma eps_induct: @@ -105,6 +107,9 @@ apply (blast intro: arg_subset_eclose [THEN subsetD]) done +(*fixed up for induct method*) +lemmas eclose_induct_down = eclose_induct_down [consumes 1] + lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X" apply (erule equalityI [OF eclose_least arg_subset_eclose]) apply (rule subset_refl) @@ -327,6 +332,13 @@ apply (auto simp add: OUnion_def); done +lemma def_transrec2: + "(!!x. f(x)==transrec2(x,a,b)) + ==> f(0) = a & + f(succ(i)) = b(i, f(i)) & + (Limit(K) --> f(K) = (UN j b Un c : Fin(A)" +lemma Fin_UnI [simp]: "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)" apply (erule Fin_induct) apply (simp_all add: Un_cons) done -declare Fin_UnI [simp] - (*The union of a set of finite sets is finite.*) lemma Fin_UnionI: "C : Fin(Fin(A)) ==> Union(C) : Fin(A)" diff -r 53022e5f73ff -r fac77a839aa2 src/ZF/Main.thy --- a/src/ZF/Main.thy Wed Jun 05 12:24:14 2002 +0200 +++ b/src/ZF/Main.thy Wed Jun 05 15:34:55 2002 +0200 @@ -9,20 +9,11 @@ and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1] and rtrancl_full_induct = rtrancl_full_induct [case_names initial step, consumes 1] -(* belongs to theory WF *) -lemmas wf_induct = wf_induct [induct set: wf] - and wf_induct_rule = wf_induct [rule_format, induct set: wf] - and wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on] - and wf_on_induct_rule = wf_on_induct [rule_format, consumes 2, induct set: wf_on] - -(* belongs to theory Nat *) -lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat] - and complete_induct = complete_induct [case_names less, consumes 1] - and complete_induct_rule = complete_induct [rule_format, case_names less, consumes 1] - and diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2] - +(*The theory of "iterates" logically belongs to Nat, but can't go there because + primrec isn't available into after Datatype. The only theories defined + after Datatype are List and the Integ theories.*) subsection{* Iteration of the function @{term F} *} consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60) @@ -60,15 +51,6 @@ (* belongs to theory Cardinal *) declare Ord_Least [intro,simp,TC] -(* belongs to theory Epsilon *) -lemmas eclose_induct = eclose_induct [induct set: eclose] - and eclose_induct_down = eclose_induct_down [consumes 1] - -(* belongs to theory Finite *) -lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin] - -(* belongs to theory CardinalArith *) -lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite] (* belongs to theory List *) lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1] @@ -78,16 +60,9 @@ and negDivAlg_induct = negDivAlg_induct [consumes 2] -(* belongs to theory Epsilon *) +(* belongs to theory CardinalArith *) -lemma def_transrec2: - "(!!x. f(x)==transrec2(x,a,b)) - ==> f(0) = a & - f(succ(i)) = b(i, f(i)) & - (Limit(K) --> f(K) = (UN j K \ K \ K" apply (rule well_ord_InfCard_square_eq) diff -r 53022e5f73ff -r fac77a839aa2 src/ZF/Nat.thy --- a/src/ZF/Nat.thy Wed Jun 05 12:24:14 2002 +0200 +++ b/src/ZF/Nat.thy Wed Jun 05 15:34:55 2002 +0200 @@ -83,13 +83,14 @@ (*Mathematical induction*) lemma nat_induct: "[| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)" -apply (erule def_induct [OF nat_def nat_bnd_mono], blast) -done +by (erule def_induct [OF nat_def nat_bnd_mono], blast) + +(*fixed up for induct method*) +lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat] lemma natE: "[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P" -apply (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) -done +by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)" by (erule nat_induct, auto) @@ -145,7 +146,12 @@ (** Variations on mathematical induction **) (*complete induction*) -lemmas complete_induct = Ord_induct [OF _ Ord_nat] + +lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1] + +lemmas complete_induct_rule = + complete_induct [rule_format, case_names less, consumes 1] + lemma nat_induct_from_lemma [rule_format]: "[| n: nat; m: nat; @@ -178,6 +184,9 @@ apply (erule_tac n=j in nat_induct, auto) done +(*fixed up for induct method*) +lemmas diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2] + (** Induction principle analogous to trancl_induct **) lemma succ_lt_induct_lemma [rule_format]: @@ -268,6 +277,7 @@ lemma nat_nonempty [simp]: "nat ~= 0" by blast + ML {* val Le_def = thm "Le_def"; diff -r 53022e5f73ff -r fac77a839aa2 src/ZF/Ordinal.thy --- a/src/ZF/Ordinal.thy Wed Jun 05 12:24:14 2002 +0200 +++ b/src/ZF/Ordinal.thy Wed Jun 05 15:34:55 2002 +0200 @@ -97,8 +97,17 @@ by (unfold Transset_def, blast) lemma Transset_Inter_family: - "[| j:A; !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))" -by (unfold Transset_def, blast) + "[| !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))" +by (unfold Inter_def Transset_def, blast) + +lemma Transset_UN: + "(!!x. x \ A ==> Transset(B(x))) ==> Transset (UN x:A. B(x))" +by (rule Transset_Union_family, auto) + +lemma Transset_INT: + "(!!x. x \ A ==> Transset(B(x))) ==> Transset (INT x:A. B(x))" +by (rule Transset_Inter_family, auto) + (*** Natural Deduction rules for Ord ***) @@ -157,18 +166,6 @@ apply (blast intro!: Transset_Int) done - -lemma Ord_Inter: - "[| j:A; !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))" -apply (rule Transset_Inter_family [THEN OrdI], assumption) -apply (blast intro: Ord_is_Transset) -apply (blast intro: Ord_contains_Transset) -done - -lemma Ord_INT: - "[| j:A; !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))" -by (rule RepFunI [THEN Ord_Inter], assumption, blast) - (*There is no set of all ordinals, for then it would contain itself*) lemma ON_class: "~ (ALL i. i:X <-> Ord(i))" apply (rule notI) @@ -532,8 +529,6 @@ by (blast intro: Ord_trans) -(*FIXME: the Intersection duals are missing!*) - (*** Results about limits ***) lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))" @@ -545,6 +540,19 @@ "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))" by (rule Ord_Union, blast) +lemma Ord_Inter [intro,simp,TC]: + "[| !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))" +apply (rule Transset_Inter_family [THEN OrdI]) +apply (blast intro: Ord_is_Transset) +apply (simp add: Inter_def) +apply (blast intro: Ord_contains_Transset) +done + +lemma Ord_INT [intro,simp,TC]: + "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))" +by (rule Ord_Inter, blast) + + (* No < version; consider (UN i:nat.i)=nat *) lemma UN_least_le: "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i" diff -r 53022e5f73ff -r fac77a839aa2 src/ZF/Univ.thy --- a/src/ZF/Univ.thy Wed Jun 05 12:24:14 2002 +0200 +++ b/src/ZF/Univ.thy Wed Jun 05 15:34:55 2002 +0200 @@ -53,6 +53,9 @@ apply (erule UN_mono, blast) done +lemma VfromI: "[| a: Vfrom(A,j); j a : Vfrom(A,i)" +by (blast dest: Vfrom_mono [OF subset_refl le_imp_subset [OF leI]]) + subsubsection{* A fundamental equality: Vfrom does not require ordinals! *} @@ -178,20 +181,15 @@ apply (simp add: Limit_Union_eq) done -lemma Limit_VfromI: "[| a: Vfrom(A,j); Limit(i); j a : Vfrom(A,i)" -apply (rule Limit_Vfrom_eq [THEN equalityD2, THEN subsetD], assumption) -apply (blast intro: ltD) -done - lemma Limit_VfromE: "[| a: Vfrom(A,i); ~R ==> Limit(i); !!x. [| x R |] ==> R" apply (rule classical) apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E]) -prefer 2 apply assumption -apply blast -apply (blast intro: ltI Limit_is_Ord) + prefer 2 apply assumption + apply blast +apply (blast intro: ltI Limit_is_Ord) done lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard] @@ -199,7 +197,7 @@ lemma singleton_in_VLimit: "[| a: Vfrom(A,i); Limit(i) |] ==> {a} : Vfrom(A,i)" apply (erule Limit_VfromE, assumption) -apply (erule singleton_in_Vfrom [THEN Limit_VfromI], assumption) +apply (erule singleton_in_Vfrom [THEN VfromI]) apply (blast intro: Limit_has_succ) done @@ -213,7 +211,7 @@ "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> {a,b} : Vfrom(A,i)" apply (erule Limit_VfromE, assumption) apply (erule Limit_VfromE, assumption) -apply (blast intro: Limit_VfromI [OF doubleton_in_Vfrom] +apply (blast intro: VfromI [OF doubleton_in_Vfrom] Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt) done @@ -223,8 +221,8 @@ apply (erule Limit_VfromE, assumption) apply (erule Limit_VfromE, assumption) txt{*Infer that succ(succ(x Un xa)) < i *} -apply (blast intro: Limit_VfromI [OF Pair_in_Vfrom] - Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt) +apply (blast intro: VfromI [OF Pair_in_Vfrom] + Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt) done lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) <= Vfrom(A,i)" @@ -303,7 +301,7 @@ lemma Union_in_VLimit: "[| X: Vfrom(A,i); Limit(i); Transset(A) |] ==> Union(X) : Vfrom(A,i)" apply (rule Limit_VfromE, assumption+) -apply (blast intro: Limit_has_succ Limit_VfromI Union_in_Vfrom) +apply (blast intro: Limit_has_succ VfromI Union_in_Vfrom) done @@ -324,9 +322,8 @@ apply (drule_tac x=a in spec) apply (drule_tac x=b in spec) apply (drule_tac x="x Un xa Un 2" in spec) -txt{*FIXME: can do better using simprule about Un and <*} -apply (simp add: Vfrom_UnI2 [THEN Vfrom_UnI1] Vfrom_UnI1 [THEN Vfrom_UnI1]) -apply (blast intro: Limit_has_0 Limit_has_succ Un_least_lt Limit_VfromI) +apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2) +apply (blast intro: Limit_has_0 Limit_has_succ VfromI) done subsubsection{* products *} @@ -401,7 +398,7 @@ lemma Pow_in_VLimit: "[| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)" -by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom Limit_VfromI) +by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI) subsection{* The set Vset(i) *} @@ -684,7 +681,7 @@ apply (rule Limit_nat [THEN Fin_VLimit]) done -subsubsection{* Closure under finite powers (functions from a fixed natural number) *} +subsubsection{* Closure under finite powers: functions from a natural number *} lemma nat_fun_VLimit: "[| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)" @@ -793,8 +790,6 @@ val Vfrom_succ = thm "Vfrom_succ"; val Vfrom_Union = thm "Vfrom_Union"; val Limit_Vfrom_eq = thm "Limit_Vfrom_eq"; -val Limit_VfromI = thm "Limit_VfromI"; -val Limit_VfromE = thm "Limit_VfromE"; val zero_in_VLimit = thm "zero_in_VLimit"; val singleton_in_VLimit = thm "singleton_in_VLimit"; val Vfrom_UnI1 = thm "Vfrom_UnI1"; @@ -814,7 +809,6 @@ val Transset_Vfrom = thm "Transset_Vfrom"; val Transset_Vfrom_succ = thm "Transset_Vfrom_succ"; val Transset_Pair_subset = thm "Transset_Pair_subset"; -val Transset_Pair_subset_VLimit = thm "Transset_Pair_subset_VLimit"; val Union_in_Vfrom = thm "Union_in_Vfrom"; val Union_in_VLimit = thm "Union_in_VLimit"; val in_VLimit = thm "in_VLimit"; diff -r 53022e5f73ff -r fac77a839aa2 src/ZF/WF.thy --- a/src/ZF/WF.thy Wed Jun 05 12:24:14 2002 +0200 +++ b/src/ZF/WF.thy Wed Jun 05 15:34:55 2002 +0200 @@ -103,6 +103,10 @@ apply blast done +(*fixed up for induct method*) +lemmas wf_induct = wf_induct [induct set: wf] + and wf_induct_rule = wf_induct [rule_format, induct set: wf] + (*The form of this rule is designed to match wfI*) lemma wf_induct2: "[| wf(r); a:A; field(r)<=A; @@ -124,6 +128,12 @@ apply (rule field_Int_square, blast) done +(*fixed up for induct method*) +lemmas wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on] + and wf_on_induct_rule = + wf_on_induct [rule_format, consumes 2, induct set: wf_on] + + (*If r allows well-founded induction then wf(r)*) lemma wfI: "[| field(r)<=A; diff -r 53022e5f73ff -r fac77a839aa2 src/ZF/equalities.thy --- a/src/ZF/equalities.thy Wed Jun 05 12:24:14 2002 +0200 +++ b/src/ZF/equalities.thy Wed Jun 05 15:34:55 2002 +0200 @@ -794,6 +794,10 @@ "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))" by blast +lemma Collect_Union_eq [simp]: + "Collect(\x\A. B(x), P) = (\x\A. Collect(B(x), P))" +by blast + ML {* val ZF_cs = claset() delrules [equalityI];