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