--- 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 \
--- 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:
--- 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
--- 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
--- 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)"
--- 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
--- 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"