various new lemmas for Constructible
authorpaulson
Wed Aug 28 13:08:50 2002 +0200 (2002-08-28 ago)
changeset 13544895994073bdf
parent 13543 2b3c7e319d82
child 13545 fcdbd6cf5f9f
various new lemmas for Constructible
src/ZF/IsaMakefile
src/ZF/OrderArith.thy
src/ZF/Ordinal.thy
src/ZF/QPair.thy
src/ZF/equalities.thy
src/ZF/pair.thy
src/ZF/upair.thy
     1.1 --- a/src/ZF/IsaMakefile	Wed Aug 28 13:08:34 2002 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Wed Aug 28 13:08:50 2002 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4  $(LOG)/ZF-Constructible.gz: $(OUT)/ZF  Constructible/ROOT.ML \
     1.5    Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy\
     1.6    Constructible/Formula.thy Constructible/Internalize.thy \
     1.7 -  Constructible/Relative.thy \
     1.8 +  Constructible/AC_in_L.thy Constructible/Relative.thy \
     1.9    Constructible/L_axioms.thy    Constructible/Wellorderings.thy \
    1.10    Constructible/MetaExists.thy  Constructible/Normal.thy \
    1.11    Constructible/Rec_Separation.thy Constructible/Separation.thy \
     2.1 --- a/src/ZF/OrderArith.thy	Wed Aug 28 13:08:34 2002 +0200
     2.2 +++ b/src/ZF/OrderArith.thy	Wed Aug 28 13:08:50 2002 +0200
     2.3 @@ -356,7 +356,6 @@
     2.4  
     2.5  subsubsection{*Well-foundedness*}
     2.6  
     2.7 -(*Not sure if wf_on_rvimage could be proved from this!*)
     2.8  lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))"
     2.9  apply (simp (no_asm_use) add: rvimage_def wf_eq_minimal)
    2.10  apply clarify
    2.11 @@ -368,6 +367,8 @@
    2.12  apply blast 
    2.13  done
    2.14  
    2.15 +text{*But note that the combination of @{text wf_imp_wf_on} and
    2.16 + @{text wf_rvimage} gives @{term "wf(r) ==> wf[C](rvimage(A,f,r))"}*}
    2.17  lemma wf_on_rvimage: "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
    2.18  apply (rule wf_onI2)
    2.19  apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba")
    2.20 @@ -397,7 +398,34 @@
    2.21  by (unfold ord_iso_def rvimage_def, blast)
    2.22  
    2.23  
    2.24 -subsubsection{*Other Results*}
    2.25 +subsection{*Other Results*}
    2.26 +
    2.27 +lemma wf_times: "A Int B = 0 ==> wf(A*B)"
    2.28 +by (simp add: wf_def, blast)
    2.29 +
    2.30 +text{*Could also be used to prove @{text wf_radd}*}
    2.31 +lemma wf_Un:
    2.32 +     "[| range(r) Int domain(s) = 0; wf(r);  wf(s) |] ==> wf(r Un s)"
    2.33 +apply (simp add: wf_def, clarify) 
    2.34 +apply (rule equalityI) 
    2.35 + prefer 2 apply blast 
    2.36 +apply clarify 
    2.37 +apply (drule_tac x=Z in spec)
    2.38 +apply (drule_tac x="Z Int domain(s)" in spec)
    2.39 +apply simp 
    2.40 +apply (blast intro: elim: equalityE) 
    2.41 +done
    2.42 +
    2.43 +subsubsection{*The Empty Relation*}
    2.44 +
    2.45 +lemma wf0: "wf(0)"
    2.46 +by (simp add: wf_def, blast)
    2.47 +
    2.48 +lemma linear0: "linear(0,0)"
    2.49 +by (simp add: linear_def)
    2.50 +
    2.51 +lemma well_ord0: "well_ord(0,0)"
    2.52 +by (blast intro: wf_imp_wf_on well_ordI wf0 linear0)
    2.53  
    2.54  subsubsection{*The "measure" relation is useful with wfrec*}
    2.55  
    2.56 @@ -414,6 +442,31 @@
    2.57  lemma measure_iff [iff]: "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)"
    2.58  by (simp (no_asm) add: measure_def)
    2.59  
    2.60 +lemma linear_measure: 
    2.61 + assumes Ordf: "!!x. x \<in> A ==> Ord(f(x))"
    2.62 +     and inj:  "!!x y. [|x \<in> A; y \<in> A; f(x) = f(y) |] ==> x=y"
    2.63 + shows "linear(A, measure(A,f))"
    2.64 +apply (auto simp add: linear_def) 
    2.65 +apply (rule_tac i="f(x)" and j="f(y)" in Ord_linear_lt) 
    2.66 +    apply (simp_all add: Ordf) 
    2.67 +apply (blast intro: inj) 
    2.68 +done
    2.69 +
    2.70 +lemma wf_on_measure: "wf[B](measure(A,f))"
    2.71 +by (rule wf_imp_wf_on [OF wf_measure])
    2.72 +
    2.73 +lemma well_ord_measure: 
    2.74 + assumes Ordf: "!!x. x \<in> A ==> Ord(f(x))"
    2.75 +     and inj:  "!!x y. [|x \<in> A; y \<in> A; f(x) = f(y) |] ==> x=y"
    2.76 + shows "well_ord(A, measure(A,f))"
    2.77 +apply (rule well_ordI)
    2.78 +apply (rule wf_on_measure) 
    2.79 +apply (blast intro: linear_measure Ordf inj) 
    2.80 +done
    2.81 +
    2.82 +lemma measure_type: "measure(A,f) <= A*A"
    2.83 +by (auto simp add: measure_def)
    2.84 +
    2.85  subsubsection{*Well-foundedness of Unions*}
    2.86  
    2.87  lemma wf_on_Union:
     3.1 --- a/src/ZF/Ordinal.thy	Wed Aug 28 13:08:34 2002 +0200
     3.2 +++ b/src/ZF/Ordinal.thy	Wed Aug 28 13:08:50 2002 +0200
     3.3 @@ -637,9 +637,18 @@
     3.4  apply (erule conjunct2 [THEN conjunct1])
     3.5  done
     3.6  
     3.7 +lemma Limit_nonzero: "Limit(i) ==> i ~= 0"
     3.8 +by (drule Limit_has_0, blast)
     3.9 +
    3.10  lemma Limit_has_succ: "[| Limit(i);  j<i |] ==> succ(j) < i"
    3.11  by (unfold Limit_def, blast)
    3.12  
    3.13 +lemma Limit_succ_lt_iff [simp]: "Limit(i) ==> succ(j) < i <-> (j<i)"
    3.14 +apply (safe intro!: Limit_has_succ)
    3.15 +apply (frule lt_Ord)
    3.16 +apply (blast intro: lt_trans)   
    3.17 +done
    3.18 +
    3.19  lemma zero_not_Limit [iff]: "~ Limit(0)"
    3.20  by (simp add: Limit_def)
    3.21  
    3.22 @@ -647,7 +656,7 @@
    3.23  by (blast intro: Limit_has_0 Limit_has_succ)
    3.24  
    3.25  lemma increasing_LimitI: "[| 0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y |] ==> Limit(l)"
    3.26 -apply (simp add: Limit_def lt_Ord2, clarify)
    3.27 +apply (unfold Limit_def, simp add: lt_Ord2, clarify)
    3.28  apply (drule_tac i=y in ltD) 
    3.29  apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2)
    3.30  done
     4.1 --- a/src/ZF/QPair.thy	Wed Aug 28 13:08:34 2002 +0200
     4.2 +++ b/src/ZF/QPair.thy	Wed Aug 28 13:08:50 2002 +0200
     4.3 @@ -126,10 +126,10 @@
     4.4  subsubsection{*Projections: qfst, qsnd*}
     4.5  
     4.6  lemma qfst_conv [simp]: "qfst(<a;b>) = a"
     4.7 -by (simp add: qfst_def, blast)
     4.8 +by (simp add: qfst_def)
     4.9  
    4.10  lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
    4.11 -by (simp add: qsnd_def, blast)
    4.12 +by (simp add: qsnd_def)
    4.13  
    4.14  lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A"
    4.15  by auto
     5.1 --- a/src/ZF/equalities.thy	Wed Aug 28 13:08:34 2002 +0200
     5.2 +++ b/src/ZF/equalities.thy	Wed Aug 28 13:08:50 2002 +0200
     5.3 @@ -576,6 +576,14 @@
     5.4  lemma SUM_eq_UN: "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))"
     5.5  by blast
     5.6  
     5.7 +lemma times_subset_iff:
     5.8 +     "(A'*B' <= A*B) <-> (A' = 0 | B' = 0 | (A'<=A) & (B'<=B))"
     5.9 +by blast
    5.10 +
    5.11 +lemma Int_Sigma_eq:
    5.12 +     "(\<Sigma>x \<in> A'. B'(x)) Int (\<Sigma>x \<in> A. B(x)) = (\<Sigma>x \<in> A' Int A. B'(x) Int B(x))"
    5.13 +by blast
    5.14 +
    5.15  (** Domain **)
    5.16  
    5.17  lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>: r)"
     6.1 --- a/src/ZF/pair.thy	Wed Aug 28 13:08:34 2002 +0200
     6.2 +++ b/src/ZF/pair.thy	Wed Aug 28 13:08:50 2002 +0200
     6.3 @@ -98,10 +98,10 @@
     6.4  subsection{*Projections @{term fst} and @{term snd}*}
     6.5  
     6.6  lemma fst_conv [simp]: "fst(<a,b>) = a"
     6.7 -by (simp add: fst_def, blast)
     6.8 +by (simp add: fst_def)
     6.9  
    6.10  lemma snd_conv [simp]: "snd(<a,b>) = b"
    6.11 -by (simp add: snd_def, blast)
    6.12 +by (simp add: snd_def)
    6.13  
    6.14  lemma fst_type [TC]: "p:Sigma(A,B) ==> fst(p) : A"
    6.15  by auto
     7.1 --- a/src/ZF/upair.thy	Wed Aug 28 13:08:34 2002 +0200
     7.2 +++ b/src/ZF/upair.thy	Wed Aug 28 13:08:50 2002 +0200
     7.3 @@ -210,6 +210,9 @@
     7.4  lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
     7.5  by blast
     7.6  
     7.7 +lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a"
     7.8 +by blast
     7.9 +
    7.10  subsection{*Conditional Terms: @{text "if-then-else"}*}
    7.11  
    7.12  lemma if_true [simp]: "(if True then a else b) = a"