src/ZF/OrdQuant.thy
 changeset 13118 336b0bcbd27c parent 12825 f1f7964ed05c child 13149 773657d466cb
```     1.1 --- a/src/ZF/OrdQuant.thy	Wed May 08 09:14:56 2002 +0200
1.2 +++ b/src/ZF/OrdQuant.thy	Wed May 08 10:12:57 2002 +0200
1.3 @@ -62,6 +62,33 @@
1.4  declare Ord_UN [intro,simp,TC]
1.5  declare Ord_Union [intro,simp,TC]
1.6
1.7 +(** Now some very basic ZF theorems **)
1.8 +
1.9 +lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
1.10 +by blast
1.11 +
1.12 +lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
1.13 +by blast
1.14 +
1.15 +lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
1.16 +by (unfold trans_def trans_on_def, blast)
1.17 +
1.18 +lemma image_is_UN: "\<lbrakk>function(g); x <= domain(g)\<rbrakk> \<Longrightarrow> g``x = (UN k:x. {g`k})"
1.19 +by (blast intro: function_apply_equality [THEN sym] function_apply_Pair)
1.20 +
1.21 +lemma functionI:
1.22 +     "\<lbrakk>!!x y y'. \<lbrakk><x,y>:r; <x,y'>:r\<rbrakk> \<Longrightarrow> y=y'\<rbrakk> \<Longrightarrow> function(r)"
1.23 +by (simp add: function_def, blast)
1.24 +
1.25 +lemma function_lam: "function (lam x:A. b(x))"
1.26 +by (simp add: function_def lam_def)
1.27 +
1.28 +lemma relation_lam: "relation (lam x:A. b(x))"
1.29 +by (simp add: relation_def lam_def, blast)
1.30 +
1.31 +lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"