new lemmas
authorpaulson
Wed May 08 10:12:57 2002 +0200 (2002-05-08)
changeset 13118336b0bcbd27c
parent 13117 0b233f430076
child 13119 6f7526467e5a
new lemmas
src/ZF/CardinalArith.thy
src/ZF/OrdQuant.thy
     1.1 --- a/src/ZF/CardinalArith.thy	Wed May 08 09:14:56 2002 +0200
     1.2 +++ b/src/ZF/CardinalArith.thy	Wed May 08 10:12:57 2002 +0200
     1.3 @@ -40,6 +40,42 @@
     1.4    "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
     1.5  
     1.6  
     1.7 +(*** The following really belong early in the development ***)
     1.8 +
     1.9 +lemma relation_converse_converse [simp]:
    1.10 +     "relation(r) ==> converse(converse(r)) = r"
    1.11 +by (simp add: relation_def, blast) 
    1.12 +
    1.13 +lemma relation_restrict [simp]:  "relation(restrict(r,A))"
    1.14 +by (simp add: restrict_def relation_def, blast) 
    1.15 +
    1.16 +(*** The following really belong in Order ***)
    1.17 +
    1.18 +lemma subset_ord_iso_Memrel:
    1.19 +     "\<lbrakk>f: ord_iso(A,Memrel(B),C,r); A<=B\<rbrakk> \<Longrightarrow> f: ord_iso(A,Memrel(A),C,r)"
    1.20 +apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel]) 
    1.21 +apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption) 
    1.22 +apply (simp add: right_comp_id) 
    1.23 +done
    1.24 +
    1.25 +lemma restrict_ord_iso:
    1.26 +     "\<lbrakk>f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r);  a \<in> A; j < i; 
    1.27 +       trans[A](r)\<rbrakk>
    1.28 +      \<Longrightarrow> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
    1.29 +apply (frule ltD) 
    1.30 +apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) 
    1.31 +apply (frule ord_iso_restrict_pred, assumption) 
    1.32 +apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel)
    1.33 +apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI]) 
    1.34 +done
    1.35 +
    1.36 +lemma restrict_ord_iso2:
    1.37 +     "\<lbrakk>f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i));  a \<in> A; 
    1.38 +       j < i; trans[A](r)\<rbrakk>
    1.39 +      \<Longrightarrow> converse(restrict(converse(f), j)) 
    1.40 +          \<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"
    1.41 +by (blast intro: restrict_ord_iso ord_iso_sym ltI)
    1.42 +
    1.43  (*** The following really belong in OrderType ***)
    1.44  
    1.45  lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0"
     2.1 --- a/src/ZF/OrdQuant.thy	Wed May 08 09:14:56 2002 +0200
     2.2 +++ b/src/ZF/OrdQuant.thy	Wed May 08 10:12:57 2002 +0200
     2.3 @@ -62,6 +62,33 @@
     2.4  declare Ord_UN [intro,simp,TC]
     2.5  declare Ord_Union [intro,simp,TC]
     2.6  
     2.7 +(** Now some very basic ZF theorems **)
     2.8 +
     2.9 +lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
    2.10 +by blast
    2.11 +
    2.12 +lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
    2.13 +by blast
    2.14 +
    2.15 +lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
    2.16 +by (unfold trans_def trans_on_def, blast)
    2.17 +
    2.18 +lemma image_is_UN: "\<lbrakk>function(g); x <= domain(g)\<rbrakk> \<Longrightarrow> g``x = (UN k:x. {g`k})"
    2.19 +by (blast intro: function_apply_equality [THEN sym] function_apply_Pair) 
    2.20 +
    2.21 +lemma functionI: 
    2.22 +     "\<lbrakk>!!x y y'. \<lbrakk><x,y>:r; <x,y'>:r\<rbrakk> \<Longrightarrow> y=y'\<rbrakk> \<Longrightarrow> function(r)"
    2.23 +by (simp add: function_def, blast) 
    2.24 +
    2.25 +lemma function_lam: "function (lam x:A. b(x))"
    2.26 +by (simp add: function_def lam_def) 
    2.27 +
    2.28 +lemma relation_lam: "relation (lam x:A. b(x))"  
    2.29 +by (simp add: relation_def lam_def, blast) 
    2.30 +
    2.31 +lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"
    2.32 +by (simp add: restrict_def) 
    2.33 +
    2.34  (** These mostly belong to theory Ordinal **)
    2.35  
    2.36  lemma Union_upper_le: