src/ZF/pair.thy
author wenzelm
Fri Apr 22 13:58:13 2011 +0200 (2011-04-22)
changeset 42455 6702c984bf5a
parent 41777 1f7cbe39d425
child 42456 13b4b6ba3593
permissions -rw-r--r--
modernized Quantifier1 simproc setup;
     1 (*  Title:      ZF/pair.thy
     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"
    11 begin
    12 
    13 simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {*
    14   let
    15     val unfold_bex_tac = unfold_tac @{thms Bex_def};
    16     fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    17   in
    18     fn _ => fn ss => fn ct =>
    19       Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
    20   end
    21 *}
    22 
    23 simproc_setup defined_Ball ("ALL x:A. P(x) --> Q(x)") = {*
    24   let
    25     val unfold_ball_tac = unfold_tac @{thms Ball_def};
    26     fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    27   in
    28     fn _ => fn ss => fn ct =>
    29       Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
    30   end
    31 *}
    32 
    33 
    34 (** Lemmas for showing that <a,b> uniquely determines a and b **)
    35 
    36 lemma singleton_eq_iff [iff]: "{a} = {b} <-> a=b"
    37 by (rule extension [THEN iff_trans], blast)
    38 
    39 lemma doubleton_eq_iff: "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
    40 by (rule extension [THEN iff_trans], blast)
    41 
    42 lemma Pair_iff [simp]: "<a,b> = <c,d> <-> a=c & b=d"
    43 by (simp add: Pair_def doubleton_eq_iff, blast)
    44 
    45 lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, standard, elim!]
    46 
    47 lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1, standard]
    48 lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2, standard]
    49 
    50 lemma Pair_not_0: "<a,b> ~= 0"
    51 apply (unfold Pair_def)
    52 apply (blast elim: equalityE)
    53 done
    54 
    55 lemmas Pair_neq_0 = Pair_not_0 [THEN notE, standard, elim!]
    56 
    57 declare sym [THEN Pair_neq_0, elim!]
    58 
    59 lemma Pair_neq_fst: "<a,b>=a ==> P"
    60 apply (unfold Pair_def)
    61 apply (rule consI1 [THEN mem_asym, THEN FalseE])
    62 apply (erule subst)
    63 apply (rule consI1)
    64 done
    65 
    66 lemma Pair_neq_snd: "<a,b>=b ==> P"
    67 apply (unfold Pair_def)
    68 apply (rule consI1 [THEN consI2, THEN mem_asym, THEN FalseE])
    69 apply (erule subst)
    70 apply (rule consI1 [THEN consI2])
    71 done
    72 
    73 
    74 subsection{*Sigma: Disjoint Union of a Family of Sets*}
    75 
    76 text{*Generalizes Cartesian product*}
    77 
    78 lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
    79 by (simp add: Sigma_def)
    80 
    81 lemma SigmaI [TC,intro!]: "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
    82 by simp
    83 
    84 lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1, standard]
    85 lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2, standard]
    86 
    87 (*The general elimination rule*)
    88 lemma SigmaE [elim!]:
    89     "[| c: Sigma(A,B);   
    90         !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P  
    91      |] ==> P"
    92 by (unfold Sigma_def, blast) 
    93 
    94 lemma SigmaE2 [elim!]:
    95     "[| <a,b> : Sigma(A,B);     
    96         [| a:A;  b:B(a) |] ==> P    
    97      |] ==> P"
    98 by (unfold Sigma_def, blast) 
    99 
   100 lemma Sigma_cong:
   101     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==>  
   102      Sigma(A,B) = Sigma(A',B')"
   103 by (simp add: Sigma_def)
   104 
   105 (*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
   106   flex-flex pairs and the "Check your prover" error.  Most
   107   Sigmas and Pis are abbreviated as * or -> *)
   108 
   109 lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0"
   110 by blast
   111 
   112 lemma Sigma_empty2 [simp]: "A*0 = 0"
   113 by blast
   114 
   115 lemma Sigma_empty_iff: "A*B=0 <-> A=0 | B=0"
   116 by blast
   117 
   118 
   119 subsection{*Projections @{term fst} and @{term snd}*}
   120 
   121 lemma fst_conv [simp]: "fst(<a,b>) = a"
   122 by (simp add: fst_def)
   123 
   124 lemma snd_conv [simp]: "snd(<a,b>) = b"
   125 by (simp add: snd_def)
   126 
   127 lemma fst_type [TC]: "p:Sigma(A,B) ==> fst(p) : A"
   128 by auto
   129 
   130 lemma snd_type [TC]: "p:Sigma(A,B) ==> snd(p) : B(fst(p))"
   131 by auto
   132 
   133 lemma Pair_fst_snd_eq: "a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
   134 by auto
   135 
   136 
   137 subsection{*The Eliminator, @{term split}*}
   138 
   139 (*A META-equality, so that it applies to higher types as well...*)
   140 lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
   141 by (simp add: split_def)
   142 
   143 lemma split_type [TC]:
   144     "[|  p:Sigma(A,B);    
   145          !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>)  
   146      |] ==> split(%x y. c(x,y), p) : C(p)"
   147 apply (erule SigmaE, auto) 
   148 done
   149 
   150 lemma expand_split: 
   151   "u: A*B ==>    
   152         R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"
   153 apply (simp add: split_def)
   154 apply auto
   155 done
   156 
   157 
   158 subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*}
   159 
   160 lemma splitI: "R(a,b) ==> split(R, <a,b>)"
   161 by (simp add: split_def)
   162 
   163 lemma splitE:
   164     "[| split(R,z);  z:Sigma(A,B);                       
   165         !!x y. [| z = <x,y>;  R(x,y) |] ==> P            
   166      |] ==> P"
   167 apply (simp add: split_def)
   168 apply (erule SigmaE, force) 
   169 done
   170 
   171 lemma splitD: "split(R,<a,b>) ==> R(a,b)"
   172 by (simp add: split_def)
   173 
   174 text {*
   175   \bigskip Complex rules for Sigma.
   176 *}
   177 
   178 lemma split_paired_Bex_Sigma [simp]:
   179      "(\<exists>z \<in> Sigma(A,B). P(z)) <-> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
   180 by blast
   181 
   182 lemma split_paired_Ball_Sigma [simp]:
   183      "(\<forall>z \<in> Sigma(A,B). P(z)) <-> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
   184 by blast
   185 
   186 end
   187 
   188