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