Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
authorpaulson
Wed Jun 05 15:34:55 2002 +0200 (2002-06-05)
changeset 13203fac77a839aa2
parent 13202 53022e5f73ff
child 13204 9dbee7f2aff7
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
src/ZF/Epsilon.thy
src/ZF/Finite.thy
src/ZF/Main.thy
src/ZF/Nat.thy
src/ZF/Ordinal.thy
src/ZF/Univ.thy
src/ZF/WF.thy
src/ZF/equalities.thy
     1.1 --- a/src/ZF/Epsilon.thy	Wed Jun 05 12:24:14 2002 +0200
     1.2 +++ b/src/ZF/Epsilon.thy	Wed Jun 05 15:34:55 2002 +0200
     1.3 @@ -66,7 +66,9 @@
     1.4     [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
     1.5     |] ==> P(a) 
     1.6  *)
     1.7 -lemmas eclose_induct = Transset_induct [OF _ Transset_eclose]
     1.8 +lemmas eclose_induct =
     1.9 +     Transset_induct [OF _ Transset_eclose, induct set: eclose]
    1.10 +
    1.11  
    1.12  (*Epsilon induction*)
    1.13  lemma eps_induct:
    1.14 @@ -105,6 +107,9 @@
    1.15  apply (blast intro: arg_subset_eclose [THEN subsetD])
    1.16  done
    1.17  
    1.18 +(*fixed up for induct method*)
    1.19 +lemmas eclose_induct_down = eclose_induct_down [consumes 1]
    1.20 +
    1.21  lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
    1.22  apply (erule equalityI [OF eclose_least arg_subset_eclose])
    1.23  apply (rule subset_refl)
    1.24 @@ -327,6 +332,13 @@
    1.25  apply (auto simp add: OUnion_def); 
    1.26  done
    1.27  
    1.28 +lemma def_transrec2:
    1.29 +     "(!!x. f(x)==transrec2(x,a,b))
    1.30 +      ==> f(0) = a & 
    1.31 +          f(succ(i)) = b(i, f(i)) & 
    1.32 +          (Limit(K) --> f(K) = (UN j<K. f(j)))"
    1.33 +by (simp add: transrec2_Limit)
    1.34 +
    1.35  
    1.36  (** recursor -- better than nat_rec; the succ case has no type requirement! **)
    1.37  
     2.1 --- a/src/ZF/Finite.thy	Wed Jun 05 12:24:14 2002 +0200
     2.2 +++ b/src/ZF/Finite.thy	Wed Jun 05 15:34:55 2002 +0200
     2.3 @@ -67,17 +67,22 @@
     2.4  apply simp
     2.5  done
     2.6  
     2.7 +(*fixed up for induct method*)
     2.8 +lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin]
     2.9 +
    2.10 +
    2.11  (** Simplification for Fin **)
    2.12  declare Fin.intros [simp]
    2.13  
    2.14 +lemma Fin_0: "Fin(0) = {0}"
    2.15 +by (blast intro: Fin.emptyI dest: FinD)
    2.16 +
    2.17  (*The union of two finite sets is finite.*)
    2.18 -lemma Fin_UnI: "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)"
    2.19 +lemma Fin_UnI [simp]: "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)"
    2.20  apply (erule Fin_induct)
    2.21  apply (simp_all add: Un_cons)
    2.22  done
    2.23  
    2.24 -declare Fin_UnI [simp]
    2.25 -
    2.26  
    2.27  (*The union of a set of finite sets is finite.*)
    2.28  lemma Fin_UnionI: "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"
     3.1 --- a/src/ZF/Main.thy	Wed Jun 05 12:24:14 2002 +0200
     3.2 +++ b/src/ZF/Main.thy	Wed Jun 05 15:34:55 2002 +0200
     3.3 @@ -9,20 +9,11 @@
     3.4    and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1]
     3.5    and rtrancl_full_induct = rtrancl_full_induct [case_names initial step, consumes 1]
     3.6  
     3.7 -(* belongs to theory WF *)
     3.8 -lemmas wf_induct = wf_induct [induct set: wf]
     3.9 -  and wf_induct_rule = wf_induct [rule_format, induct set: wf]
    3.10 -  and wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on]
    3.11 -  and wf_on_induct_rule = wf_on_induct [rule_format, consumes 2, induct set: wf_on]
    3.12 -
    3.13 -(* belongs to theory Nat *)
    3.14 -lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat]
    3.15 -  and complete_induct = complete_induct [case_names less, consumes 1]
    3.16 -  and complete_induct_rule = complete_induct [rule_format, case_names less, consumes 1]
    3.17 -  and diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2]
    3.18  
    3.19  
    3.20 -
    3.21 +(*The theory of "iterates" logically belongs to Nat, but can't go there because
    3.22 +  primrec isn't available into after Datatype.  The only theories defined
    3.23 +  after Datatype are List and the Integ theories.*)
    3.24  subsection{* Iteration of the function @{term F} *}
    3.25  
    3.26  consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)
    3.27 @@ -60,15 +51,6 @@
    3.28  (* belongs to theory Cardinal *)
    3.29  declare Ord_Least [intro,simp,TC]
    3.30  
    3.31 -(* belongs to theory Epsilon *)
    3.32 -lemmas eclose_induct = eclose_induct [induct set: eclose]
    3.33 -  and eclose_induct_down = eclose_induct_down [consumes 1]
    3.34 -
    3.35 -(* belongs to theory Finite *)
    3.36 -lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin]
    3.37 -
    3.38 -(* belongs to theory CardinalArith *)
    3.39 -lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]
    3.40  
    3.41  (* belongs to theory List *)
    3.42  lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]
    3.43 @@ -78,16 +60,9 @@
    3.44    and negDivAlg_induct = negDivAlg_induct [consumes 2]
    3.45  
    3.46  
    3.47 -(* belongs to theory Epsilon *)
    3.48 +(* belongs to theory CardinalArith *)
    3.49  
    3.50 -lemma def_transrec2:
    3.51 -     "(!!x. f(x)==transrec2(x,a,b))
    3.52 -      ==> f(0) = a & 
    3.53 -          f(succ(i)) = b(i, f(i)) & 
    3.54 -          (Limit(K) --> f(K) = (UN j<K. f(j)))"
    3.55 -by (simp add: transrec2_Limit)
    3.56 -
    3.57 -(* belongs to theory CardinalArith *)
    3.58 +lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]
    3.59  
    3.60  lemma InfCard_square_eqpoll: "InfCard(K) ==> K \<times> K \<approx> K"
    3.61  apply (rule well_ord_InfCard_square_eq)  
     4.1 --- a/src/ZF/Nat.thy	Wed Jun 05 12:24:14 2002 +0200
     4.2 +++ b/src/ZF/Nat.thy	Wed Jun 05 15:34:55 2002 +0200
     4.3 @@ -83,13 +83,14 @@
     4.4  (*Mathematical induction*)
     4.5  lemma nat_induct:
     4.6      "[| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)"
     4.7 -apply (erule def_induct [OF nat_def nat_bnd_mono], blast)
     4.8 -done
     4.9 +by (erule def_induct [OF nat_def nat_bnd_mono], blast)
    4.10 +
    4.11 +(*fixed up for induct method*)
    4.12 +lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat]
    4.13  
    4.14  lemma natE:
    4.15      "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
    4.16 -apply (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) 
    4.17 -done
    4.18 +by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) 
    4.19  
    4.20  lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
    4.21  by (erule nat_induct, auto)
    4.22 @@ -145,7 +146,12 @@
    4.23  (** Variations on mathematical induction **)
    4.24  
    4.25  (*complete induction*)
    4.26 -lemmas complete_induct = Ord_induct [OF _ Ord_nat]
    4.27 +
    4.28 +lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1]
    4.29 +
    4.30 +lemmas complete_induct_rule =  
    4.31 +	complete_induct [rule_format, case_names less, consumes 1]
    4.32 +
    4.33  
    4.34  lemma nat_induct_from_lemma [rule_format]: 
    4.35      "[| n: nat;  m: nat;   
    4.36 @@ -178,6 +184,9 @@
    4.37  apply (erule_tac n=j in nat_induct, auto)  
    4.38  done
    4.39  
    4.40 +(*fixed up for induct method*)
    4.41 +lemmas diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2]
    4.42 +
    4.43  (** Induction principle analogous to trancl_induct **)
    4.44  
    4.45  lemma succ_lt_induct_lemma [rule_format]:
    4.46 @@ -268,6 +277,7 @@
    4.47  lemma nat_nonempty [simp]: "nat ~= 0"
    4.48  by blast
    4.49  
    4.50 +
    4.51  ML
    4.52  {*
    4.53  val Le_def = thm "Le_def";
     5.1 --- a/src/ZF/Ordinal.thy	Wed Jun 05 12:24:14 2002 +0200
     5.2 +++ b/src/ZF/Ordinal.thy	Wed Jun 05 15:34:55 2002 +0200
     5.3 @@ -97,8 +97,17 @@
     5.4  by (unfold Transset_def, blast)
     5.5  
     5.6  lemma Transset_Inter_family: 
     5.7 -    "[| j:A;  !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))"
     5.8 -by (unfold Transset_def, blast)
     5.9 +    "[| !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))"
    5.10 +by (unfold Inter_def Transset_def, blast)
    5.11 +
    5.12 +lemma Transset_UN:
    5.13 +     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (UN x:A. B(x))"
    5.14 +by (rule Transset_Union_family, auto) 
    5.15 +
    5.16 +lemma Transset_INT:
    5.17 +     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (INT x:A. B(x))"
    5.18 +by (rule Transset_Inter_family, auto) 
    5.19 +
    5.20  
    5.21  (*** Natural Deduction rules for Ord ***)
    5.22  
    5.23 @@ -157,18 +166,6 @@
    5.24  apply (blast intro!: Transset_Int)
    5.25  done
    5.26  
    5.27 -
    5.28 -lemma Ord_Inter:
    5.29 -    "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))"
    5.30 -apply (rule Transset_Inter_family [THEN OrdI], assumption)
    5.31 -apply (blast intro: Ord_is_Transset) 
    5.32 -apply (blast intro: Ord_contains_Transset) 
    5.33 -done
    5.34 -
    5.35 -lemma Ord_INT:
    5.36 -    "[| j:A;  !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"
    5.37 -by (rule RepFunI [THEN Ord_Inter], assumption, blast) 
    5.38 -
    5.39  (*There is no set of all ordinals, for then it would contain itself*)
    5.40  lemma ON_class: "~ (ALL i. i:X <-> Ord(i))"
    5.41  apply (rule notI)
    5.42 @@ -532,8 +529,6 @@
    5.43  by (blast intro: Ord_trans)
    5.44  
    5.45  
    5.46 -(*FIXME: the Intersection duals are missing!*)
    5.47 -
    5.48  (*** Results about limits ***)
    5.49  
    5.50  lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))"
    5.51 @@ -545,6 +540,19 @@
    5.52       "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))"
    5.53  by (rule Ord_Union, blast)
    5.54  
    5.55 +lemma Ord_Inter [intro,simp,TC]:
    5.56 +    "[| !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))" 
    5.57 +apply (rule Transset_Inter_family [THEN OrdI])
    5.58 +apply (blast intro: Ord_is_Transset) 
    5.59 +apply (simp add: Inter_def) 
    5.60 +apply (blast intro: Ord_contains_Transset) 
    5.61 +done
    5.62 +
    5.63 +lemma Ord_INT [intro,simp,TC]:
    5.64 +    "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"
    5.65 +by (rule Ord_Inter, blast) 
    5.66 +
    5.67 +
    5.68  (* No < version; consider (UN i:nat.i)=nat *)
    5.69  lemma UN_least_le:
    5.70      "[| Ord(i);  !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i"
     6.1 --- a/src/ZF/Univ.thy	Wed Jun 05 12:24:14 2002 +0200
     6.2 +++ b/src/ZF/Univ.thy	Wed Jun 05 15:34:55 2002 +0200
     6.3 @@ -53,6 +53,9 @@
     6.4  apply (erule UN_mono, blast) 
     6.5  done
     6.6  
     6.7 +lemma VfromI: "[| a: Vfrom(A,j);  j<i |] ==> a : Vfrom(A,i)"
     6.8 +by (blast dest: Vfrom_mono [OF subset_refl le_imp_subset [OF leI]]) 
     6.9 +
    6.10  
    6.11  subsubsection{* A fundamental equality: Vfrom does not require ordinals! *}
    6.12  
    6.13 @@ -178,20 +181,15 @@
    6.14  apply (simp add: Limit_Union_eq) 
    6.15  done
    6.16  
    6.17 -lemma Limit_VfromI: "[| a: Vfrom(A,j);  Limit(i);  j<i |] ==> a : Vfrom(A,i)"
    6.18 -apply (rule Limit_Vfrom_eq [THEN equalityD2, THEN subsetD], assumption)
    6.19 -apply (blast intro: ltD) 
    6.20 -done
    6.21 -
    6.22  lemma Limit_VfromE:
    6.23      "[| a: Vfrom(A,i);  ~R ==> Limit(i);
    6.24          !!x. [| x<i;  a: Vfrom(A,x) |] ==> R
    6.25       |] ==> R"
    6.26  apply (rule classical)
    6.27  apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
    6.28 -prefer 2 apply assumption
    6.29 -apply blast 
    6.30 -apply (blast intro: ltI  Limit_is_Ord)
    6.31 +  prefer 2 apply assumption
    6.32 + apply blast 
    6.33 +apply (blast intro: ltI Limit_is_Ord)
    6.34  done
    6.35  
    6.36  lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
    6.37 @@ -199,7 +197,7 @@
    6.38  lemma singleton_in_VLimit:
    6.39      "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)"
    6.40  apply (erule Limit_VfromE, assumption)
    6.41 -apply (erule singleton_in_Vfrom [THEN Limit_VfromI], assumption)
    6.42 +apply (erule singleton_in_Vfrom [THEN VfromI])
    6.43  apply (blast intro: Limit_has_succ) 
    6.44  done
    6.45  
    6.46 @@ -213,7 +211,7 @@
    6.47      "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> {a,b} : Vfrom(A,i)"
    6.48  apply (erule Limit_VfromE, assumption)
    6.49  apply (erule Limit_VfromE, assumption)
    6.50 -apply (blast intro:  Limit_VfromI [OF doubleton_in_Vfrom]
    6.51 +apply (blast intro:  VfromI [OF doubleton_in_Vfrom]
    6.52                       Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
    6.53  done
    6.54  
    6.55 @@ -223,8 +221,8 @@
    6.56  apply (erule Limit_VfromE, assumption)
    6.57  apply (erule Limit_VfromE, assumption)
    6.58  txt{*Infer that succ(succ(x Un xa)) < i *}
    6.59 -apply (blast intro:  Limit_VfromI [OF Pair_in_Vfrom]
    6.60 -                     Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
    6.61 +apply (blast intro: VfromI [OF Pair_in_Vfrom]
    6.62 +                    Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
    6.63  done
    6.64  
    6.65  lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) <= Vfrom(A,i)"
    6.66 @@ -303,7 +301,7 @@
    6.67  lemma Union_in_VLimit:
    6.68       "[| X: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Union(X) : Vfrom(A,i)"
    6.69  apply (rule Limit_VfromE, assumption+)
    6.70 -apply (blast intro: Limit_has_succ Limit_VfromI Union_in_Vfrom)
    6.71 +apply (blast intro: Limit_has_succ VfromI Union_in_Vfrom)
    6.72  done
    6.73  
    6.74  
    6.75 @@ -324,9 +322,8 @@
    6.76  apply (drule_tac x=a in spec) 
    6.77  apply (drule_tac x=b in spec) 
    6.78  apply (drule_tac x="x Un xa Un 2" in spec) 
    6.79 -txt{*FIXME: can do better using simprule about Un and <*}
    6.80 -apply (simp add: Vfrom_UnI2 [THEN Vfrom_UnI1] Vfrom_UnI1 [THEN Vfrom_UnI1]) 
    6.81 -apply (blast intro: Limit_has_0 Limit_has_succ Un_least_lt Limit_VfromI)
    6.82 +apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2) 
    6.83 +apply (blast intro: Limit_has_0 Limit_has_succ VfromI)
    6.84  done
    6.85  
    6.86  subsubsection{* products *}
    6.87 @@ -401,7 +398,7 @@
    6.88  
    6.89  lemma Pow_in_VLimit:
    6.90       "[| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)"
    6.91 -by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom Limit_VfromI)
    6.92 +by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI)
    6.93  
    6.94  
    6.95  subsection{* The set Vset(i) *}
    6.96 @@ -684,7 +681,7 @@
    6.97  apply (rule Limit_nat [THEN Fin_VLimit])
    6.98  done
    6.99  
   6.100 -subsubsection{* Closure under finite powers (functions from a fixed natural number) *}
   6.101 +subsubsection{* Closure under finite powers: functions from a natural number *}
   6.102  
   6.103  lemma nat_fun_VLimit:
   6.104       "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"
   6.105 @@ -793,8 +790,6 @@
   6.106  val Vfrom_succ = thm "Vfrom_succ";
   6.107  val Vfrom_Union = thm "Vfrom_Union";
   6.108  val Limit_Vfrom_eq = thm "Limit_Vfrom_eq";
   6.109 -val Limit_VfromI = thm "Limit_VfromI";
   6.110 -val Limit_VfromE = thm "Limit_VfromE";
   6.111  val zero_in_VLimit = thm "zero_in_VLimit";
   6.112  val singleton_in_VLimit = thm "singleton_in_VLimit";
   6.113  val Vfrom_UnI1 = thm "Vfrom_UnI1";
   6.114 @@ -814,7 +809,6 @@
   6.115  val Transset_Vfrom = thm "Transset_Vfrom";
   6.116  val Transset_Vfrom_succ = thm "Transset_Vfrom_succ";
   6.117  val Transset_Pair_subset = thm "Transset_Pair_subset";
   6.118 -val Transset_Pair_subset_VLimit = thm "Transset_Pair_subset_VLimit";
   6.119  val Union_in_Vfrom = thm "Union_in_Vfrom";
   6.120  val Union_in_VLimit = thm "Union_in_VLimit";
   6.121  val in_VLimit = thm "in_VLimit";
     7.1 --- a/src/ZF/WF.thy	Wed Jun 05 12:24:14 2002 +0200
     7.2 +++ b/src/ZF/WF.thy	Wed Jun 05 15:34:55 2002 +0200
     7.3 @@ -103,6 +103,10 @@
     7.4  apply blast 
     7.5  done
     7.6  
     7.7 +(*fixed up for induct method*)
     7.8 +lemmas wf_induct = wf_induct [induct set: wf]
     7.9 +  and wf_induct_rule = wf_induct [rule_format, induct set: wf]
    7.10 +
    7.11  (*The form of this rule is designed to match wfI*)
    7.12  lemma wf_induct2:
    7.13      "[| wf(r);  a:A;  field(r)<=A;
    7.14 @@ -124,6 +128,12 @@
    7.15  apply (rule field_Int_square, blast)
    7.16  done
    7.17  
    7.18 +(*fixed up for induct method*)
    7.19 +lemmas wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on]
    7.20 +   and wf_on_induct_rule = 
    7.21 +	 wf_on_induct [rule_format, consumes 2, induct set: wf_on]
    7.22 +
    7.23 +
    7.24  (*If r allows well-founded induction then wf(r)*)
    7.25  lemma wfI:
    7.26      "[| field(r)<=A;
     8.1 --- a/src/ZF/equalities.thy	Wed Jun 05 12:24:14 2002 +0200
     8.2 +++ b/src/ZF/equalities.thy	Wed Jun 05 15:34:55 2002 +0200
     8.3 @@ -794,6 +794,10 @@
     8.4       "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"
     8.5  by blast
     8.6  
     8.7 +lemma Collect_Union_eq [simp]:
     8.8 +     "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
     8.9 +by blast
    8.10 +
    8.11  ML
    8.12  {*
    8.13  val ZF_cs = claset() delrules [equalityI];