# HG changeset patch
# User paulson
# Date 1030532930 -7200
# Node ID 895994073bdf007a1abd735baa782e3bcb9bc826
# Parent  2b3c7e319d82da39d33d2a18a341f420fc1465ee
various new lemmas for Constructible

diff -r 2b3c7e319d82 -r 895994073bdf src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Wed Aug 28 13:08:34 2002 +0200
+++ b/src/ZF/IsaMakefile	Wed Aug 28 13:08:50 2002 +0200
@@ -80,7 +80,7 @@
 $(LOG)/ZF-Constructible.gz: $(OUT)/ZF  Constructible/ROOT.ML \
   Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy\
   Constructible/Formula.thy Constructible/Internalize.thy \
-  Constructible/Relative.thy \
+  Constructible/AC_in_L.thy Constructible/Relative.thy \
   Constructible/L_axioms.thy    Constructible/Wellorderings.thy \
   Constructible/MetaExists.thy  Constructible/Normal.thy \
   Constructible/Rec_Separation.thy Constructible/Separation.thy \
diff -r 2b3c7e319d82 -r 895994073bdf src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Wed Aug 28 13:08:34 2002 +0200
+++ b/src/ZF/OrderArith.thy	Wed Aug 28 13:08:50 2002 +0200
@@ -356,7 +356,6 @@
 
 subsubsection{*Well-foundedness*}
 
-(*Not sure if wf_on_rvimage could be proved from this!*)
 lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))"
 apply (simp (no_asm_use) add: rvimage_def wf_eq_minimal)
 apply clarify
@@ -368,6 +367,8 @@
 apply blast 
 done
 
+text{*But note that the combination of @{text wf_imp_wf_on} and
+ @{text wf_rvimage} gives @{term "wf(r) ==> wf[C](rvimage(A,f,r))"}*}
 lemma wf_on_rvimage: "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
 apply (rule wf_onI2)
 apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba")
@@ -397,7 +398,34 @@
 by (unfold ord_iso_def rvimage_def, blast)
 
 
-subsubsection{*Other Results*}
+subsection{*Other Results*}
+
+lemma wf_times: "A Int B = 0 ==> wf(A*B)"
+by (simp add: wf_def, blast)
+
+text{*Could also be used to prove @{text wf_radd}*}
+lemma wf_Un:
+     "[| range(r) Int domain(s) = 0; wf(r);  wf(s) |] ==> wf(r Un s)"
+apply (simp add: wf_def, clarify) 
+apply (rule equalityI) 
+ prefer 2 apply blast 
+apply clarify 
+apply (drule_tac x=Z in spec)
+apply (drule_tac x="Z Int domain(s)" in spec)
+apply simp 
+apply (blast intro: elim: equalityE) 
+done
+
+subsubsection{*The Empty Relation*}
+
+lemma wf0: "wf(0)"
+by (simp add: wf_def, blast)
+
+lemma linear0: "linear(0,0)"
+by (simp add: linear_def)
+
+lemma well_ord0: "well_ord(0,0)"
+by (blast intro: wf_imp_wf_on well_ordI wf0 linear0)
 
 subsubsection{*The "measure" relation is useful with wfrec*}
 
@@ -414,6 +442,31 @@
 lemma measure_iff [iff]: "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)"
 by (simp (no_asm) add: measure_def)
 
+lemma linear_measure: 
+ assumes Ordf: "!!x. x \<in> A ==> Ord(f(x))"
+     and inj:  "!!x y. [|x \<in> A; y \<in> A; f(x) = f(y) |] ==> x=y"
+ shows "linear(A, measure(A,f))"
+apply (auto simp add: linear_def) 
+apply (rule_tac i="f(x)" and j="f(y)" in Ord_linear_lt) 
+    apply (simp_all add: Ordf) 
+apply (blast intro: inj) 
+done
+
+lemma wf_on_measure: "wf[B](measure(A,f))"
+by (rule wf_imp_wf_on [OF wf_measure])
+
+lemma well_ord_measure: 
+ assumes Ordf: "!!x. x \<in> A ==> Ord(f(x))"
+     and inj:  "!!x y. [|x \<in> A; y \<in> A; f(x) = f(y) |] ==> x=y"
+ shows "well_ord(A, measure(A,f))"
+apply (rule well_ordI)
+apply (rule wf_on_measure) 
+apply (blast intro: linear_measure Ordf inj) 
+done
+
+lemma measure_type: "measure(A,f) <= A*A"
+by (auto simp add: measure_def)
+
 subsubsection{*Well-foundedness of Unions*}
 
 lemma wf_on_Union:
diff -r 2b3c7e319d82 -r 895994073bdf src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Wed Aug 28 13:08:34 2002 +0200
+++ b/src/ZF/Ordinal.thy	Wed Aug 28 13:08:50 2002 +0200
@@ -637,9 +637,18 @@
 apply (erule conjunct2 [THEN conjunct1])
 done
 
+lemma Limit_nonzero: "Limit(i) ==> i ~= 0"
+by (drule Limit_has_0, blast)
+
 lemma Limit_has_succ: "[| Limit(i);  j<i |] ==> succ(j) < i"
 by (unfold Limit_def, blast)
 
+lemma Limit_succ_lt_iff [simp]: "Limit(i) ==> succ(j) < i <-> (j<i)"
+apply (safe intro!: Limit_has_succ)
+apply (frule lt_Ord)
+apply (blast intro: lt_trans)   
+done
+
 lemma zero_not_Limit [iff]: "~ Limit(0)"
 by (simp add: Limit_def)
 
@@ -647,7 +656,7 @@
 by (blast intro: Limit_has_0 Limit_has_succ)
 
 lemma increasing_LimitI: "[| 0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y |] ==> Limit(l)"
-apply (simp add: Limit_def lt_Ord2, clarify)
+apply (unfold Limit_def, simp add: lt_Ord2, clarify)
 apply (drule_tac i=y in ltD) 
 apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2)
 done
diff -r 2b3c7e319d82 -r 895994073bdf src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Wed Aug 28 13:08:34 2002 +0200
+++ b/src/ZF/QPair.thy	Wed Aug 28 13:08:50 2002 +0200
@@ -126,10 +126,10 @@
 subsubsection{*Projections: qfst, qsnd*}
 
 lemma qfst_conv [simp]: "qfst(<a;b>) = a"
-by (simp add: qfst_def, blast)
+by (simp add: qfst_def)
 
 lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
-by (simp add: qsnd_def, blast)
+by (simp add: qsnd_def)
 
 lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A"
 by auto
diff -r 2b3c7e319d82 -r 895994073bdf src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Wed Aug 28 13:08:34 2002 +0200
+++ b/src/ZF/equalities.thy	Wed Aug 28 13:08:50 2002 +0200
@@ -576,6 +576,14 @@
 lemma SUM_eq_UN: "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))"
 by blast
 
+lemma times_subset_iff:
+     "(A'*B' <= A*B) <-> (A' = 0 | B' = 0 | (A'<=A) & (B'<=B))"
+by blast
+
+lemma Int_Sigma_eq:
+     "(\<Sigma>x \<in> A'. B'(x)) Int (\<Sigma>x \<in> A. B(x)) = (\<Sigma>x \<in> A' Int A. B'(x) Int B(x))"
+by blast
+
 (** Domain **)
 
 lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>: r)"
diff -r 2b3c7e319d82 -r 895994073bdf src/ZF/pair.thy
--- a/src/ZF/pair.thy	Wed Aug 28 13:08:34 2002 +0200
+++ b/src/ZF/pair.thy	Wed Aug 28 13:08:50 2002 +0200
@@ -98,10 +98,10 @@
 subsection{*Projections @{term fst} and @{term snd}*}
 
 lemma fst_conv [simp]: "fst(<a,b>) = a"
-by (simp add: fst_def, blast)
+by (simp add: fst_def)
 
 lemma snd_conv [simp]: "snd(<a,b>) = b"
-by (simp add: snd_def, blast)
+by (simp add: snd_def)
 
 lemma fst_type [TC]: "p:Sigma(A,B) ==> fst(p) : A"
 by auto
diff -r 2b3c7e319d82 -r 895994073bdf src/ZF/upair.thy
--- a/src/ZF/upair.thy	Wed Aug 28 13:08:34 2002 +0200
+++ b/src/ZF/upair.thy	Wed Aug 28 13:08:50 2002 +0200
@@ -210,6 +210,9 @@
 lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
 by blast
 
+lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a"
+by blast
+
 subsection{*Conditional Terms: @{text "if-then-else"}*}
 
 lemma if_true [simp]: "(if True then a else b) = a"