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