author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 48891  c0eafbd55de3 
child 51717  9e7d1c139569 
permissions  rwrr 
41777  1 
(* Title: ZF/pair.thy 
13240  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 
Copyright 1992 University of Cambridge 

4 
*) 

5 

13357  6 
header{*Ordered Pairs*} 
7 

16417  8 
theory pair imports upair 
42455  9 
begin 
10 

48891  11 
ML_file "simpdata.ML" 
12 

42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42794
diff
changeset

13 
setup {* 
45625
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset

14 
Simplifier.map_simpset_global 
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset

15 
(Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)) 
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset

16 
#> Simplifier.add_cong @{thm if_weak_cong}) 
42794  17 
*} 
18 

19 
ML {* val ZF_ss = @{simpset} *} 

20 

46820  21 
simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = {* 
42455  22 
let 
23 
val unfold_bex_tac = unfold_tac @{thms Bex_def}; 

24 
fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; 

42459  25 
in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end 
42455  26 
*} 
27 

46820  28 
simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {* 
42455  29 
let 
30 
val unfold_ball_tac = unfold_tac @{thms Ball_def}; 

31 
fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; 

42459  32 
in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end 
42455  33 
*} 
34 

13240  35 

36 
(** Lemmas for showing that <a,b> uniquely determines a and b **) 

37 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

38 
lemma singleton_eq_iff [iff]: "{a} = {b} \<longleftrightarrow> a=b" 
13240  39 
by (rule extension [THEN iff_trans], blast) 
40 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

41 
lemma doubleton_eq_iff: "{a,b} = {c,d} \<longleftrightarrow> (a=c & b=d)  (a=d & b=c)" 
13240  42 
by (rule extension [THEN iff_trans], blast) 
43 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

44 
lemma Pair_iff [simp]: "<a,b> = <c,d> \<longleftrightarrow> a=c & b=d" 
13240  45 
by (simp add: Pair_def doubleton_eq_iff, blast) 
46 

45602  47 
lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!] 
13240  48 

45602  49 
lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1] 
50 
lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2] 

13240  51 

46820  52 
lemma Pair_not_0: "<a,b> \<noteq> 0" 
13240  53 
apply (unfold Pair_def) 
54 
apply (blast elim: equalityE) 

55 
done 

56 

45602  57 
lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!] 
13240  58 

59 
declare sym [THEN Pair_neq_0, elim!] 

60 

61 
lemma Pair_neq_fst: "<a,b>=a ==> P" 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

62 
proof (unfold Pair_def) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

63 
assume eq: "{{a, a}, {a, b}} = a" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

64 
have "{a, a} \<in> {{a, a}, {a, b}}" by (rule consI1) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

65 
hence "{a, a} \<in> a" by (simp add: eq) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

66 
moreover have "a \<in> {a, a}" by (rule consI1) 
46953  67 
ultimately show "P" by (rule mem_asym) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

68 
qed 
13240  69 

70 
lemma Pair_neq_snd: "<a,b>=b ==> P" 

46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

71 
proof (unfold Pair_def) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

72 
assume eq: "{{a, a}, {a, b}} = b" 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

73 
have "{a, b} \<in> {{a, a}, {a, b}}" by blast 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

74 
hence "{a, b} \<in> b" by (simp add: eq) 
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

75 
moreover have "b \<in> {a, b}" by blast 
46953  76 
ultimately show "P" by (rule mem_asym) 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

77 
qed 
13240  78 

79 

13357  80 
subsection{*Sigma: Disjoint Union of a Family of Sets*} 
81 

82 
text{*Generalizes Cartesian product*} 

13240  83 

46953  84 
lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) \<longleftrightarrow> a \<in> A & b \<in> B(a)" 
13240  85 
by (simp add: Sigma_def) 
86 

46953  87 
lemma SigmaI [TC,intro!]: "[ a \<in> A; b \<in> B(a) ] ==> <a,b> \<in> Sigma(A,B)" 
13240  88 
by simp 
89 

45602  90 
lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1] 
91 
lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2] 

13240  92 

93 
(*The general elimination rule*) 

94 
lemma SigmaE [elim!]: 

46953  95 
"[ c \<in> Sigma(A,B); 
96 
!!x y.[ x \<in> A; y \<in> B(x); c=<x,y> ] ==> P 

13240  97 
] ==> P" 
46953  98 
by (unfold Sigma_def, blast) 
13240  99 

100 
lemma SigmaE2 [elim!]: 

46953  101 
"[ <a,b> \<in> Sigma(A,B); 
102 
[ a \<in> A; b \<in> B(a) ] ==> P 

13240  103 
] ==> P" 
46953  104 
by (unfold Sigma_def, blast) 
13240  105 

106 
lemma Sigma_cong: 

46953  107 
"[ A=A'; !!x. x \<in> A' ==> B(x)=B'(x) ] ==> 
13240  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 
flexflex 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 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

121 
lemma Sigma_empty_iff: "A*B=0 \<longleftrightarrow> A=0  B=0" 
13240  122 
by blast 
123 

124 

13357  125 
subsection{*Projections @{term fst} and @{term snd}*} 
13240  126 

127 
lemma fst_conv [simp]: "fst(<a,b>) = a" 

13544  128 
by (simp add: fst_def) 
13240  129 

130 
lemma snd_conv [simp]: "snd(<a,b>) = b" 

13544  131 
by (simp add: snd_def) 
13240  132 

46953  133 
lemma fst_type [TC]: "p \<in> Sigma(A,B) ==> fst(p) \<in> A" 
13240  134 
by auto 
135 

46953  136 
lemma snd_type [TC]: "p \<in> Sigma(A,B) ==> snd(p) \<in> B(fst(p))" 
13240  137 
by auto 
138 

46953  139 
lemma Pair_fst_snd_eq: "a \<in> Sigma(A,B) ==> <fst(a),snd(a)> = a" 
13240  140 
by auto 
141 

142 

13357  143 
subsection{*The Eliminator, @{term split}*} 
13240  144 

145 
(*A METAequality, 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]: 

46953  150 
"[ p \<in> Sigma(A,B); 
151 
!!x y.[ x \<in> A; y \<in> B(x) ] ==> c(x,y):C(<x,y>) 

46820  152 
] ==> split(%x y. c(x,y), p) \<in> C(p)" 
46953  153 
by (erule SigmaE, auto) 
13240  154 

46953  155 
lemma expand_split: 
156 
"u \<in> A*B ==> 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

157 
R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))" 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

158 
by (auto simp add: split_def) 
13240  159 

160 

13357  161 
subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*} 
13240  162 

163 
lemma splitI: "R(a,b) ==> split(R, <a,b>)" 

164 
by (simp add: split_def) 

165 

166 
lemma splitE: 

46953  167 
"[ split(R,z); z \<in> Sigma(A,B); 
168 
!!x y. [ z = <x,y>; R(x,y) ] ==> P 

13240  169 
] ==> P" 
46841
49b91b716cbe
Structured and calculationbased proofs (with new trans rules!)
paulson
parents:
46821
diff
changeset

170 
by (auto simp add: split_def) 
13240  171 

172 
lemma splitD: "split(R,<a,b>) ==> R(a,b)" 

173 
by (simp add: split_def) 

174 

14864  175 
text {* 
176 
\bigskip Complex rules for Sigma. 

177 
*} 

178 

179 
lemma split_paired_Bex_Sigma [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

180 
"(\<exists>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))" 
14864  181 
by blast 
182 

183 
lemma split_paired_Ball_Sigma [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

184 
"(\<forall>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))" 
14864  185 
by blast 
186 

9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
2469
diff
changeset

187 
end 
124  188 

2469  189 