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