src/ZF/pair.thy
author wenzelm
Tue Aug 02 19:47:11 2005 +0200 (2005-08-02)
changeset 17001 51ff2bc32774
parent 16417 9bc16273c2d4
child 24893 b8ef7afe3a6b
permissions -rw-r--r--
tuned;
     1 (*  Title:      ZF/pair
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 *)
     7 
     8 header{*Ordered Pairs*}
     9 
    10 theory pair imports upair
    11 uses "simpdata.ML" begin
    12 
    13 (** Lemmas for showing that <a,b> uniquely determines a and b **)
    14 
    15 lemma singleton_eq_iff [iff]: "{a} = {b} <-> a=b"
    16 by (rule extension [THEN iff_trans], blast)
    17 
    18 lemma doubleton_eq_iff: "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
    19 by (rule extension [THEN iff_trans], blast)
    20 
    21 lemma Pair_iff [simp]: "<a,b> = <c,d> <-> a=c & b=d"
    22 by (simp add: Pair_def doubleton_eq_iff, blast)
    23 
    24 lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, standard, elim!]
    25 
    26 lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1, standard]
    27 lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2, standard]
    28 
    29 lemma Pair_not_0: "<a,b> ~= 0"
    30 apply (unfold Pair_def)
    31 apply (blast elim: equalityE)
    32 done
    33 
    34 lemmas Pair_neq_0 = Pair_not_0 [THEN notE, standard, elim!]
    35 
    36 declare sym [THEN Pair_neq_0, elim!]
    37 
    38 lemma Pair_neq_fst: "<a,b>=a ==> P"
    39 apply (unfold Pair_def)
    40 apply (rule consI1 [THEN mem_asym, THEN FalseE])
    41 apply (erule subst)
    42 apply (rule consI1)
    43 done
    44 
    45 lemma Pair_neq_snd: "<a,b>=b ==> P"
    46 apply (unfold Pair_def)
    47 apply (rule consI1 [THEN consI2, THEN mem_asym, THEN FalseE])
    48 apply (erule subst)
    49 apply (rule consI1 [THEN consI2])
    50 done
    51 
    52 
    53 subsection{*Sigma: Disjoint Union of a Family of Sets*}
    54 
    55 text{*Generalizes Cartesian product*}
    56 
    57 lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
    58 by (simp add: Sigma_def)
    59 
    60 lemma SigmaI [TC,intro!]: "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
    61 by simp
    62 
    63 lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1, standard]
    64 lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2, standard]
    65 
    66 (*The general elimination rule*)
    67 lemma SigmaE [elim!]:
    68     "[| c: Sigma(A,B);   
    69         !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P  
    70      |] ==> P"
    71 by (unfold Sigma_def, blast) 
    72 
    73 lemma SigmaE2 [elim!]:
    74     "[| <a,b> : Sigma(A,B);     
    75         [| a:A;  b:B(a) |] ==> P    
    76      |] ==> P"
    77 by (unfold Sigma_def, blast) 
    78 
    79 lemma Sigma_cong:
    80     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==>  
    81      Sigma(A,B) = Sigma(A',B')"
    82 by (simp add: Sigma_def)
    83 
    84 (*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
    85   flex-flex pairs and the "Check your prover" error.  Most
    86   Sigmas and Pis are abbreviated as * or -> *)
    87 
    88 lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0"
    89 by blast
    90 
    91 lemma Sigma_empty2 [simp]: "A*0 = 0"
    92 by blast
    93 
    94 lemma Sigma_empty_iff: "A*B=0 <-> A=0 | B=0"
    95 by blast
    96 
    97 
    98 subsection{*Projections @{term fst} and @{term snd}*}
    99 
   100 lemma fst_conv [simp]: "fst(<a,b>) = a"
   101 by (simp add: fst_def)
   102 
   103 lemma snd_conv [simp]: "snd(<a,b>) = b"
   104 by (simp add: snd_def)
   105 
   106 lemma fst_type [TC]: "p:Sigma(A,B) ==> fst(p) : A"
   107 by auto
   108 
   109 lemma snd_type [TC]: "p:Sigma(A,B) ==> snd(p) : B(fst(p))"
   110 by auto
   111 
   112 lemma Pair_fst_snd_eq: "a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
   113 by auto
   114 
   115 
   116 subsection{*The Eliminator, @{term split}*}
   117 
   118 (*A META-equality, so that it applies to higher types as well...*)
   119 lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
   120 by (simp add: split_def)
   121 
   122 lemma split_type [TC]:
   123     "[|  p:Sigma(A,B);    
   124          !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>)  
   125      |] ==> split(%x y. c(x,y), p) : C(p)"
   126 apply (erule SigmaE, auto) 
   127 done
   128 
   129 lemma expand_split: 
   130   "u: A*B ==>    
   131         R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"
   132 apply (simp add: split_def)
   133 apply auto
   134 done
   135 
   136 
   137 subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*}
   138 
   139 lemma splitI: "R(a,b) ==> split(R, <a,b>)"
   140 by (simp add: split_def)
   141 
   142 lemma splitE:
   143     "[| split(R,z);  z:Sigma(A,B);                       
   144         !!x y. [| z = <x,y>;  R(x,y) |] ==> P            
   145      |] ==> P"
   146 apply (simp add: split_def)
   147 apply (erule SigmaE, force) 
   148 done
   149 
   150 lemma splitD: "split(R,<a,b>) ==> R(a,b)"
   151 by (simp add: split_def)
   152 
   153 text {*
   154   \bigskip Complex rules for Sigma.
   155 *}
   156 
   157 lemma split_paired_Bex_Sigma [simp]:
   158      "(\<exists>z \<in> Sigma(A,B). P(z)) <-> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
   159 by blast
   160 
   161 lemma split_paired_Ball_Sigma [simp]:
   162      "(\<forall>z \<in> Sigma(A,B). P(z)) <-> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
   163 by blast
   164 
   165 ML
   166 {*
   167 val singleton_eq_iff = thm "singleton_eq_iff";
   168 val doubleton_eq_iff = thm "doubleton_eq_iff";
   169 val Pair_iff = thm "Pair_iff";
   170 val Pair_inject = thm "Pair_inject";
   171 val Pair_inject1 = thm "Pair_inject1";
   172 val Pair_inject2 = thm "Pair_inject2";
   173 val Pair_not_0 = thm "Pair_not_0";
   174 val Pair_neq_0 = thm "Pair_neq_0";
   175 val Pair_neq_fst = thm "Pair_neq_fst";
   176 val Pair_neq_snd = thm "Pair_neq_snd";
   177 val Sigma_iff = thm "Sigma_iff";
   178 val SigmaI = thm "SigmaI";
   179 val SigmaD1 = thm "SigmaD1";
   180 val SigmaD2 = thm "SigmaD2";
   181 val SigmaE = thm "SigmaE";
   182 val SigmaE2 = thm "SigmaE2";
   183 val Sigma_cong = thm "Sigma_cong";
   184 val Sigma_empty1 = thm "Sigma_empty1";
   185 val Sigma_empty2 = thm "Sigma_empty2";
   186 val Sigma_empty_iff = thm "Sigma_empty_iff";
   187 val fst_conv = thm "fst_conv";
   188 val snd_conv = thm "snd_conv";
   189 val fst_type = thm "fst_type";
   190 val snd_type = thm "snd_type";
   191 val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
   192 val split = thm "split";
   193 val split_type = thm "split_type";
   194 val expand_split = thm "expand_split";
   195 val splitI = thm "splitI";
   196 val splitE = thm "splitE";
   197 val splitD = thm "splitD";
   198 *}
   199 
   200 end
   201 
   202