src/ZF/pair.thy
author paulson
Sun Jun 23 10:14:13 2002 +0200 (2002-06-23)
changeset 13240 bb5f4faea1f3
parent 11694 4c6e9d800628
child 13357 6f54e992777e
permissions -rw-r--r--
conversion of Sum, pair to Isar script
paulson@13240
     1
(*  Title:      ZF/pair
paulson@13240
     2
    ID:         $Id$
paulson@13240
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13240
     4
    Copyright   1992  University of Cambridge
paulson@13240
     5
paulson@13240
     6
Ordered pairs in Zermelo-Fraenkel Set Theory 
paulson@13240
     7
*)
paulson@13240
     8
paulson@9570
     9
theory pair = upair
wenzelm@11694
    10
files "simpdata.ML":
paulson@13240
    11
paulson@13240
    12
(** Lemmas for showing that <a,b> uniquely determines a and b **)
paulson@13240
    13
paulson@13240
    14
lemma singleton_eq_iff [iff]: "{a} = {b} <-> a=b"
paulson@13240
    15
by (rule extension [THEN iff_trans], blast)
paulson@13240
    16
paulson@13240
    17
lemma doubleton_eq_iff: "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
paulson@13240
    18
by (rule extension [THEN iff_trans], blast)
paulson@13240
    19
paulson@13240
    20
lemma Pair_iff [simp]: "<a,b> = <c,d> <-> a=c & b=d"
paulson@13240
    21
by (simp add: Pair_def doubleton_eq_iff, blast)
paulson@13240
    22
paulson@13240
    23
lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, standard, elim!]
paulson@13240
    24
paulson@13240
    25
lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1, standard]
paulson@13240
    26
lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2, standard]
paulson@13240
    27
paulson@13240
    28
lemma Pair_not_0: "<a,b> ~= 0"
paulson@13240
    29
apply (unfold Pair_def)
paulson@13240
    30
apply (blast elim: equalityE)
paulson@13240
    31
done
paulson@13240
    32
paulson@13240
    33
lemmas Pair_neq_0 = Pair_not_0 [THEN notE, standard, elim!]
paulson@13240
    34
paulson@13240
    35
declare sym [THEN Pair_neq_0, elim!]
paulson@13240
    36
paulson@13240
    37
lemma Pair_neq_fst: "<a,b>=a ==> P"
paulson@13240
    38
apply (unfold Pair_def)
paulson@13240
    39
apply (rule consI1 [THEN mem_asym, THEN FalseE])
paulson@13240
    40
apply (erule subst)
paulson@13240
    41
apply (rule consI1)
paulson@13240
    42
done
paulson@13240
    43
paulson@13240
    44
lemma Pair_neq_snd: "<a,b>=b ==> P"
paulson@13240
    45
apply (unfold Pair_def)
paulson@13240
    46
apply (rule consI1 [THEN consI2, THEN mem_asym, THEN FalseE])
paulson@13240
    47
apply (erule subst)
paulson@13240
    48
apply (rule consI1 [THEN consI2])
paulson@13240
    49
done
paulson@13240
    50
paulson@13240
    51
paulson@13240
    52
(*** Sigma: Disjoint union of a family of sets
paulson@13240
    53
     Generalizes Cartesian product ***)
paulson@13240
    54
paulson@13240
    55
lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
paulson@13240
    56
by (simp add: Sigma_def)
paulson@13240
    57
paulson@13240
    58
lemma SigmaI [TC,intro!]: "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
paulson@13240
    59
by simp
paulson@13240
    60
paulson@13240
    61
lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1, standard]
paulson@13240
    62
lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2, standard]
paulson@13240
    63
paulson@13240
    64
(*The general elimination rule*)
paulson@13240
    65
lemma SigmaE [elim!]:
paulson@13240
    66
    "[| c: Sigma(A,B);   
paulson@13240
    67
        !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P  
paulson@13240
    68
     |] ==> P"
paulson@13240
    69
apply (unfold Sigma_def, blast) 
paulson@13240
    70
done
paulson@13240
    71
paulson@13240
    72
lemma SigmaE2 [elim!]:
paulson@13240
    73
    "[| <a,b> : Sigma(A,B);     
paulson@13240
    74
        [| a:A;  b:B(a) |] ==> P    
paulson@13240
    75
     |] ==> P"
paulson@13240
    76
apply (unfold Sigma_def, blast) 
paulson@13240
    77
done
paulson@13240
    78
paulson@13240
    79
lemma Sigma_cong:
paulson@13240
    80
    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==>  
paulson@13240
    81
     Sigma(A,B) = Sigma(A',B')"
paulson@13240
    82
by (simp add: Sigma_def)
paulson@13240
    83
paulson@13240
    84
(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
paulson@13240
    85
  flex-flex pairs and the "Check your prover" error.  Most
paulson@13240
    86
  Sigmas and Pis are abbreviated as * or -> *)
paulson@13240
    87
paulson@13240
    88
lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0"
paulson@13240
    89
by blast
paulson@13240
    90
paulson@13240
    91
lemma Sigma_empty2 [simp]: "A*0 = 0"
paulson@13240
    92
by blast
paulson@13240
    93
paulson@13240
    94
lemma Sigma_empty_iff: "A*B=0 <-> A=0 | B=0"
paulson@13240
    95
by blast
paulson@13240
    96
paulson@13240
    97
paulson@13240
    98
(*** Projections: fst, snd ***)
paulson@13240
    99
paulson@13240
   100
lemma fst_conv [simp]: "fst(<a,b>) = a"
paulson@13240
   101
by (simp add: fst_def, blast)
paulson@13240
   102
paulson@13240
   103
lemma snd_conv [simp]: "snd(<a,b>) = b"
paulson@13240
   104
by (simp add: snd_def, blast)
paulson@13240
   105
paulson@13240
   106
lemma fst_type [TC]: "p:Sigma(A,B) ==> fst(p) : A"
paulson@13240
   107
by auto
paulson@13240
   108
paulson@13240
   109
lemma snd_type [TC]: "p:Sigma(A,B) ==> snd(p) : B(fst(p))"
paulson@13240
   110
by auto
paulson@13240
   111
paulson@13240
   112
lemma Pair_fst_snd_eq: "a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
paulson@13240
   113
by auto
paulson@13240
   114
paulson@13240
   115
paulson@13240
   116
(*** Eliminator - split ***)
paulson@13240
   117
paulson@13240
   118
(*A META-equality, so that it applies to higher types as well...*)
paulson@13240
   119
lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
paulson@13240
   120
by (simp add: split_def)
paulson@13240
   121
paulson@13240
   122
lemma split_type [TC]:
paulson@13240
   123
    "[|  p:Sigma(A,B);    
paulson@13240
   124
         !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>)  
paulson@13240
   125
     |] ==> split(%x y. c(x,y), p) : C(p)"
paulson@13240
   126
apply (erule SigmaE, auto) 
paulson@13240
   127
done
paulson@13240
   128
paulson@13240
   129
lemma expand_split: 
paulson@13240
   130
  "u: A*B ==>    
paulson@13240
   131
        R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"
paulson@13240
   132
apply (simp add: split_def, auto)
paulson@13240
   133
done
paulson@13240
   134
paulson@13240
   135
paulson@13240
   136
(*** split for predicates: result type o ***)
paulson@13240
   137
paulson@13240
   138
lemma splitI: "R(a,b) ==> split(R, <a,b>)"
paulson@13240
   139
by (simp add: split_def)
paulson@13240
   140
paulson@13240
   141
lemma splitE:
paulson@13240
   142
    "[| split(R,z);  z:Sigma(A,B);                       
paulson@13240
   143
        !!x y. [| z = <x,y>;  R(x,y) |] ==> P            
paulson@13240
   144
     |] ==> P"
paulson@13240
   145
apply (simp add: split_def)
paulson@13240
   146
apply (erule SigmaE, force) 
paulson@13240
   147
done
paulson@13240
   148
paulson@13240
   149
lemma splitD: "split(R,<a,b>) ==> R(a,b)"
paulson@13240
   150
by (simp add: split_def)
paulson@13240
   151
paulson@13240
   152
ML
paulson@13240
   153
{*
paulson@13240
   154
val singleton_eq_iff = thm "singleton_eq_iff";
paulson@13240
   155
val doubleton_eq_iff = thm "doubleton_eq_iff";
paulson@13240
   156
val Pair_iff = thm "Pair_iff";
paulson@13240
   157
val Pair_inject = thm "Pair_inject";
paulson@13240
   158
val Pair_inject1 = thm "Pair_inject1";
paulson@13240
   159
val Pair_inject2 = thm "Pair_inject2";
paulson@13240
   160
val Pair_not_0 = thm "Pair_not_0";
paulson@13240
   161
val Pair_neq_0 = thm "Pair_neq_0";
paulson@13240
   162
val Pair_neq_fst = thm "Pair_neq_fst";
paulson@13240
   163
val Pair_neq_snd = thm "Pair_neq_snd";
paulson@13240
   164
val Sigma_iff = thm "Sigma_iff";
paulson@13240
   165
val SigmaI = thm "SigmaI";
paulson@13240
   166
val SigmaD1 = thm "SigmaD1";
paulson@13240
   167
val SigmaD2 = thm "SigmaD2";
paulson@13240
   168
val SigmaE = thm "SigmaE";
paulson@13240
   169
val SigmaE2 = thm "SigmaE2";
paulson@13240
   170
val Sigma_cong = thm "Sigma_cong";
paulson@13240
   171
val Sigma_empty1 = thm "Sigma_empty1";
paulson@13240
   172
val Sigma_empty2 = thm "Sigma_empty2";
paulson@13240
   173
val Sigma_empty_iff = thm "Sigma_empty_iff";
paulson@13240
   174
val fst_conv = thm "fst_conv";
paulson@13240
   175
val snd_conv = thm "snd_conv";
paulson@13240
   176
val fst_type = thm "fst_type";
paulson@13240
   177
val snd_type = thm "snd_type";
paulson@13240
   178
val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
paulson@13240
   179
val split = thm "split";
paulson@13240
   180
val split_type = thm "split_type";
paulson@13240
   181
val expand_split = thm "expand_split";
paulson@13240
   182
val splitI = thm "splitI";
paulson@13240
   183
val splitE = thm "splitE";
paulson@13240
   184
val splitD = thm "splitD";
paulson@13240
   185
*}
paulson@13240
   186
paulson@9570
   187
end
clasohm@124
   188
paulson@2469
   189