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>)"
    1.32 +by (simp add: restrict_def) 
    1.33 +
    1.34  (** These mostly belong to theory Ordinal **)
    1.35  
    1.36  lemma Union_upper_le: