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
```