src/ZF/pair.thy
changeset 13240 bb5f4faea1f3
parent 11694 4c6e9d800628
child 13357 6f54e992777e
     1.1 --- a/src/ZF/pair.thy	Sat Jun 22 18:28:46 2002 +0200
     1.2 +++ b/src/ZF/pair.thy	Sun Jun 23 10:14:13 2002 +0200
     1.3 @@ -1,5 +1,189 @@
     1.4 +(*  Title:      ZF/pair
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +Ordered pairs in Zermelo-Fraenkel Set Theory 
    1.10 +*)
    1.11 +
    1.12  theory pair = upair
    1.13  files "simpdata.ML":
    1.14 +
    1.15 +(** Lemmas for showing that <a,b> uniquely determines a and b **)
    1.16 +
    1.17 +lemma singleton_eq_iff [iff]: "{a} = {b} <-> a=b"
    1.18 +by (rule extension [THEN iff_trans], blast)
    1.19 +
    1.20 +lemma doubleton_eq_iff: "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
    1.21 +by (rule extension [THEN iff_trans], blast)
    1.22 +
    1.23 +lemma Pair_iff [simp]: "<a,b> = <c,d> <-> a=c & b=d"
    1.24 +by (simp add: Pair_def doubleton_eq_iff, blast)
    1.25 +
    1.26 +lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, standard, elim!]
    1.27 +
    1.28 +lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1, standard]
    1.29 +lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2, standard]
    1.30 +
    1.31 +lemma Pair_not_0: "<a,b> ~= 0"
    1.32 +apply (unfold Pair_def)
    1.33 +apply (blast elim: equalityE)
    1.34 +done
    1.35 +
    1.36 +lemmas Pair_neq_0 = Pair_not_0 [THEN notE, standard, elim!]
    1.37 +
    1.38 +declare sym [THEN Pair_neq_0, elim!]
    1.39 +
    1.40 +lemma Pair_neq_fst: "<a,b>=a ==> P"
    1.41 +apply (unfold Pair_def)
    1.42 +apply (rule consI1 [THEN mem_asym, THEN FalseE])
    1.43 +apply (erule subst)
    1.44 +apply (rule consI1)
    1.45 +done
    1.46 +
    1.47 +lemma Pair_neq_snd: "<a,b>=b ==> P"
    1.48 +apply (unfold Pair_def)
    1.49 +apply (rule consI1 [THEN consI2, THEN mem_asym, THEN FalseE])
    1.50 +apply (erule subst)
    1.51 +apply (rule consI1 [THEN consI2])
    1.52 +done
    1.53 +
    1.54 +
    1.55 +(*** Sigma: Disjoint union of a family of sets
    1.56 +     Generalizes Cartesian product ***)
    1.57 +
    1.58 +lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
    1.59 +by (simp add: Sigma_def)
    1.60 +
    1.61 +lemma SigmaI [TC,intro!]: "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
    1.62 +by simp
    1.63 +
    1.64 +lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1, standard]
    1.65 +lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2, standard]
    1.66 +
    1.67 +(*The general elimination rule*)
    1.68 +lemma SigmaE [elim!]:
    1.69 +    "[| c: Sigma(A,B);   
    1.70 +        !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P  
    1.71 +     |] ==> P"
    1.72 +apply (unfold Sigma_def, blast) 
    1.73 +done
    1.74 +
    1.75 +lemma SigmaE2 [elim!]:
    1.76 +    "[| <a,b> : Sigma(A,B);     
    1.77 +        [| a:A;  b:B(a) |] ==> P    
    1.78 +     |] ==> P"
    1.79 +apply (unfold Sigma_def, blast) 
    1.80 +done
    1.81 +
    1.82 +lemma Sigma_cong:
    1.83 +    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==>  
    1.84 +     Sigma(A,B) = Sigma(A',B')"
    1.85 +by (simp add: Sigma_def)
    1.86 +
    1.87 +(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
    1.88 +  flex-flex pairs and the "Check your prover" error.  Most
    1.89 +  Sigmas and Pis are abbreviated as * or -> *)
    1.90 +
    1.91 +lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0"
    1.92 +by blast
    1.93 +
    1.94 +lemma Sigma_empty2 [simp]: "A*0 = 0"
    1.95 +by blast
    1.96 +
    1.97 +lemma Sigma_empty_iff: "A*B=0 <-> A=0 | B=0"
    1.98 +by blast
    1.99 +
   1.100 +
   1.101 +(*** Projections: fst, snd ***)
   1.102 +
   1.103 +lemma fst_conv [simp]: "fst(<a,b>) = a"
   1.104 +by (simp add: fst_def, blast)
   1.105 +
   1.106 +lemma snd_conv [simp]: "snd(<a,b>) = b"
   1.107 +by (simp add: snd_def, blast)
   1.108 +
   1.109 +lemma fst_type [TC]: "p:Sigma(A,B) ==> fst(p) : A"
   1.110 +by auto
   1.111 +
   1.112 +lemma snd_type [TC]: "p:Sigma(A,B) ==> snd(p) : B(fst(p))"
   1.113 +by auto
   1.114 +
   1.115 +lemma Pair_fst_snd_eq: "a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
   1.116 +by auto
   1.117 +
   1.118 +
   1.119 +(*** Eliminator - split ***)
   1.120 +
   1.121 +(*A META-equality, so that it applies to higher types as well...*)
   1.122 +lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
   1.123 +by (simp add: split_def)
   1.124 +
   1.125 +lemma split_type [TC]:
   1.126 +    "[|  p:Sigma(A,B);    
   1.127 +         !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>)  
   1.128 +     |] ==> split(%x y. c(x,y), p) : C(p)"
   1.129 +apply (erule SigmaE, auto) 
   1.130 +done
   1.131 +
   1.132 +lemma expand_split: 
   1.133 +  "u: A*B ==>    
   1.134 +        R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"
   1.135 +apply (simp add: split_def, auto)
   1.136 +done
   1.137 +
   1.138 +
   1.139 +(*** split for predicates: result type o ***)
   1.140 +
   1.141 +lemma splitI: "R(a,b) ==> split(R, <a,b>)"
   1.142 +by (simp add: split_def)
   1.143 +
   1.144 +lemma splitE:
   1.145 +    "[| split(R,z);  z:Sigma(A,B);                       
   1.146 +        !!x y. [| z = <x,y>;  R(x,y) |] ==> P            
   1.147 +     |] ==> P"
   1.148 +apply (simp add: split_def)
   1.149 +apply (erule SigmaE, force) 
   1.150 +done
   1.151 +
   1.152 +lemma splitD: "split(R,<a,b>) ==> R(a,b)"
   1.153 +by (simp add: split_def)
   1.154 +
   1.155 +ML
   1.156 +{*
   1.157 +val singleton_eq_iff = thm "singleton_eq_iff";
   1.158 +val doubleton_eq_iff = thm "doubleton_eq_iff";
   1.159 +val Pair_iff = thm "Pair_iff";
   1.160 +val Pair_inject = thm "Pair_inject";
   1.161 +val Pair_inject1 = thm "Pair_inject1";
   1.162 +val Pair_inject2 = thm "Pair_inject2";
   1.163 +val Pair_not_0 = thm "Pair_not_0";
   1.164 +val Pair_neq_0 = thm "Pair_neq_0";
   1.165 +val Pair_neq_fst = thm "Pair_neq_fst";
   1.166 +val Pair_neq_snd = thm "Pair_neq_snd";
   1.167 +val Sigma_iff = thm "Sigma_iff";
   1.168 +val SigmaI = thm "SigmaI";
   1.169 +val SigmaD1 = thm "SigmaD1";
   1.170 +val SigmaD2 = thm "SigmaD2";
   1.171 +val SigmaE = thm "SigmaE";
   1.172 +val SigmaE2 = thm "SigmaE2";
   1.173 +val Sigma_cong = thm "Sigma_cong";
   1.174 +val Sigma_empty1 = thm "Sigma_empty1";
   1.175 +val Sigma_empty2 = thm "Sigma_empty2";
   1.176 +val Sigma_empty_iff = thm "Sigma_empty_iff";
   1.177 +val fst_conv = thm "fst_conv";
   1.178 +val snd_conv = thm "snd_conv";
   1.179 +val fst_type = thm "fst_type";
   1.180 +val snd_type = thm "snd_type";
   1.181 +val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
   1.182 +val split = thm "split";
   1.183 +val split_type = thm "split_type";
   1.184 +val expand_split = thm "expand_split";
   1.185 +val splitI = thm "splitI";
   1.186 +val splitE = thm "splitE";
   1.187 +val splitD = thm "splitD";
   1.188 +*}
   1.189 +
   1.190  end
   1.191  
   1.192