--- a/src/ZF/CardinalArith.thy Wed May 08 09:14:56 2002 +0200
+++ b/src/ZF/CardinalArith.thy Wed May 08 10:12:57 2002 +0200
@@ -40,6 +40,42 @@
"op |*|" :: "[i,i] => i" (infixl "\<otimes>" 70)
+(*** The following really belong early in the development ***)
+
+lemma relation_converse_converse [simp]:
+ "relation(r) ==> converse(converse(r)) = r"
+by (simp add: relation_def, blast)
+
+lemma relation_restrict [simp]: "relation(restrict(r,A))"
+by (simp add: restrict_def relation_def, blast)
+
+(*** The following really belong in Order ***)
+
+lemma subset_ord_iso_Memrel:
+ "\<lbrakk>f: ord_iso(A,Memrel(B),C,r); A<=B\<rbrakk> \<Longrightarrow> f: ord_iso(A,Memrel(A),C,r)"
+apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel])
+apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption)
+apply (simp add: right_comp_id)
+done
+
+lemma restrict_ord_iso:
+ "\<lbrakk>f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r); a \<in> A; j < i;
+ trans[A](r)\<rbrakk>
+ \<Longrightarrow> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
+apply (frule ltD)
+apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
+apply (frule ord_iso_restrict_pred, assumption)
+apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel)
+apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI])
+done
+
+lemma restrict_ord_iso2:
+ "\<lbrakk>f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i)); a \<in> A;
+ j < i; trans[A](r)\<rbrakk>
+ \<Longrightarrow> converse(restrict(converse(f), j))
+ \<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"
+by (blast intro: restrict_ord_iso ord_iso_sym ltI)
+
(*** The following really belong in OrderType ***)
lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0"
--- a/src/ZF/OrdQuant.thy Wed May 08 09:14:56 2002 +0200
+++ b/src/ZF/OrdQuant.thy Wed May 08 10:12:57 2002 +0200
@@ -62,6 +62,33 @@
declare Ord_UN [intro,simp,TC]
declare Ord_Union [intro,simp,TC]
+(** Now some very basic ZF theorems **)
+
+lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
+by blast
+
+lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
+by blast
+
+lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
+by (unfold trans_def trans_on_def, blast)
+
+lemma image_is_UN: "\<lbrakk>function(g); x <= domain(g)\<rbrakk> \<Longrightarrow> g``x = (UN k:x. {g`k})"
+by (blast intro: function_apply_equality [THEN sym] function_apply_Pair)
+
+lemma functionI:
+ "\<lbrakk>!!x y y'. \<lbrakk><x,y>:r; <x,y'>:r\<rbrakk> \<Longrightarrow> y=y'\<rbrakk> \<Longrightarrow> function(r)"
+by (simp add: function_def, blast)
+
+lemma function_lam: "function (lam x:A. b(x))"
+by (simp add: function_def lam_def)
+
+lemma relation_lam: "relation (lam x:A. b(x))"
+by (simp add: relation_def lam_def, blast)
+
+lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"
+by (simp add: restrict_def)
+
(** These mostly belong to theory Ordinal **)
lemma Union_upper_le: