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