author | skalberg |
Mon, 15 Sep 2003 14:00:43 +0200 | |
changeset 14190 | 609c072edf90 |
parent 14189 | de58f4d939e1 |
child 14208 | 144f45277d5a |
permissions | -rw-r--r-- |
10213 | 1 |
(* Title: HOL/Product_Type.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1992 University of Cambridge |
|
11777 | 5 |
*) |
10213 | 6 |
|
11838 | 7 |
header {* Cartesian products *} |
10213 | 8 |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
9 |
theory Product_Type = Fun |
11838 | 10 |
files ("Tools/split_rule.ML"): |
11 |
||
12 |
subsection {* Unit *} |
|
13 |
||
14 |
typedef unit = "{True}" |
|
15 |
proof |
|
16 |
show "True : ?unit" by blast |
|
17 |
qed |
|
18 |
||
19 |
constdefs |
|
20 |
Unity :: unit ("'(')") |
|
21 |
"() == Abs_unit True" |
|
22 |
||
23 |
lemma unit_eq: "u = ()" |
|
24 |
by (induct u) (simp add: unit_def Unity_def) |
|
25 |
||
26 |
text {* |
|
27 |
Simplification procedure for @{thm [source] unit_eq}. Cannot use |
|
28 |
this rule directly --- it loops! |
|
29 |
*} |
|
30 |
||
31 |
ML_setup {* |
|
13462 | 32 |
val unit_eq_proc = |
33 |
let val unit_meta_eq = mk_meta_eq (thm "unit_eq") in |
|
34 |
Simplifier.simproc (Theory.sign_of (the_context ())) "unit_eq" ["x::unit"] |
|
35 |
(fn _ => fn _ => fn t => if HOLogic.is_unit t then None else Some unit_meta_eq) |
|
36 |
end; |
|
11838 | 37 |
|
38 |
Addsimprocs [unit_eq_proc]; |
|
39 |
*} |
|
40 |
||
41 |
lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()" |
|
42 |
by simp |
|
43 |
||
44 |
lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P" |
|
45 |
by (rule triv_forall_equality) |
|
46 |
||
47 |
lemma unit_induct [induct type: unit]: "P () ==> P x" |
|
48 |
by simp |
|
49 |
||
50 |
text {* |
|
51 |
This rewrite counters the effect of @{text unit_eq_proc} on @{term |
|
52 |
[source] "%u::unit. f u"}, replacing it by @{term [source] |
|
53 |
f} rather than by @{term [source] "%u. f ()"}. |
|
54 |
*} |
|
55 |
||
56 |
lemma unit_abs_eta_conv [simp]: "(%u::unit. f ()) = f" |
|
57 |
by (rule ext) simp |
|
10213 | 58 |
|
59 |
||
11838 | 60 |
subsection {* Pairs *} |
10213 | 61 |
|
11777 | 62 |
subsubsection {* Type definition *} |
10213 | 63 |
|
64 |
constdefs |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
65 |
Pair_Rep :: "['a, 'b] => ['a, 'b] => bool" |
11032 | 66 |
"Pair_Rep == (%a b. %x y. x=a & y=b)" |
10213 | 67 |
|
68 |
global |
|
69 |
||
70 |
typedef (Prod) |
|
11838 | 71 |
('a, 'b) "*" (infixr 20) |
11032 | 72 |
= "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}" |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
73 |
proof |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
74 |
fix a b show "Pair_Rep a b : ?Prod" |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
75 |
by blast |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
76 |
qed |
10213 | 77 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
11966
diff
changeset
|
78 |
syntax (xsymbols) |
11493 | 79 |
"*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) |
10213 | 80 |
syntax (HTML output) |
11493 | 81 |
"*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) |
10213 | 82 |
|
11777 | 83 |
local |
10213 | 84 |
|
11777 | 85 |
|
86 |
subsubsection {* Abstract constants and syntax *} |
|
87 |
||
88 |
global |
|
10213 | 89 |
|
90 |
consts |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
91 |
fst :: "'a * 'b => 'a" |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
92 |
snd :: "'a * 'b => 'b" |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
93 |
split :: "[['a, 'b] => 'c, 'a * 'b] => 'c" |
14189 | 94 |
curry :: "['a * 'b => 'c, 'a, 'b] => 'c" |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
95 |
prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd" |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
96 |
Pair :: "['a, 'b] => 'a * 'b" |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
97 |
Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set" |
10213 | 98 |
|
11777 | 99 |
local |
10213 | 100 |
|
11777 | 101 |
text {* |
102 |
Patterns -- extends pre-defined type @{typ pttrn} used in |
|
103 |
abstractions. |
|
104 |
*} |
|
10213 | 105 |
|
106 |
nonterminals |
|
107 |
tuple_args patterns |
|
108 |
||
109 |
syntax |
|
110 |
"_tuple" :: "'a => tuple_args => 'a * 'b" ("(1'(_,/ _'))") |
|
111 |
"_tuple_arg" :: "'a => tuple_args" ("_") |
|
112 |
"_tuple_args" :: "'a => tuple_args => tuple_args" ("_,/ _") |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
113 |
"_pattern" :: "[pttrn, patterns] => pttrn" ("'(_,/ _')") |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
114 |
"" :: "pttrn => patterns" ("_") |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
115 |
"_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
116 |
"@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
117 |
"@Times" ::"['a set, 'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80) |
10213 | 118 |
|
119 |
translations |
|
120 |
"(x, y)" == "Pair x y" |
|
121 |
"_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" |
|
122 |
"%(x,y,zs).b" == "split(%x (y,zs).b)" |
|
123 |
"%(x,y).b" == "split(%x y. b)" |
|
124 |
"_abs (Pair x y) t" => "%(x,y).t" |
|
125 |
(* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
|
126 |
The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) |
|
127 |
||
128 |
"SIGMA x:A. B" => "Sigma A (%x. B)" |
|
129 |
"A <*> B" => "Sigma A (_K B)" |
|
130 |
||
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
11966
diff
changeset
|
131 |
syntax (xsymbols) |
11493 | 132 |
"@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10) |
133 |
"@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80) |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
134 |
|
11032 | 135 |
print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *} |
10213 | 136 |
|
137 |
||
11777 | 138 |
subsubsection {* Definitions *} |
10213 | 139 |
|
140 |
defs |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
141 |
Pair_def: "Pair a b == Abs_Prod(Pair_Rep a b)" |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11425
diff
changeset
|
142 |
fst_def: "fst p == THE a. EX b. p = (a, b)" |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11425
diff
changeset
|
143 |
snd_def: "snd p == THE b. EX a. p = (a, b)" |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
144 |
split_def: "split == (%c p. c (fst p) (snd p))" |
14189 | 145 |
curry_def: "curry == (%c x y. c (x,y))" |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
146 |
prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))" |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
147 |
Sigma_def: "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" |
10213 | 148 |
|
149 |
||
11966 | 150 |
subsubsection {* Lemmas and proof tool setup *} |
11838 | 151 |
|
152 |
lemma ProdI: "Pair_Rep a b : Prod" |
|
153 |
by (unfold Prod_def) blast |
|
154 |
||
155 |
lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' ==> a = a' & b = b'" |
|
156 |
apply (unfold Pair_Rep_def) |
|
157 |
apply (drule fun_cong [THEN fun_cong]) |
|
158 |
apply blast |
|
159 |
done |
|
10213 | 160 |
|
11838 | 161 |
lemma inj_on_Abs_Prod: "inj_on Abs_Prod Prod" |
162 |
apply (rule inj_on_inverseI) |
|
163 |
apply (erule Abs_Prod_inverse) |
|
164 |
done |
|
165 |
||
166 |
lemma Pair_inject: |
|
167 |
"(a, b) = (a', b') ==> (a = a' ==> b = b' ==> R) ==> R" |
|
168 |
proof - |
|
169 |
case rule_context [unfolded Pair_def] |
|
170 |
show ?thesis |
|
171 |
apply (rule inj_on_Abs_Prod [THEN inj_onD, THEN Pair_Rep_inject, THEN conjE]) |
|
172 |
apply (rule rule_context ProdI)+ |
|
173 |
. |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
174 |
qed |
10213 | 175 |
|
11838 | 176 |
lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')" |
177 |
by (blast elim!: Pair_inject) |
|
178 |
||
179 |
lemma fst_conv [simp]: "fst (a, b) = a" |
|
180 |
by (unfold fst_def) blast |
|
181 |
||
182 |
lemma snd_conv [simp]: "snd (a, b) = b" |
|
183 |
by (unfold snd_def) blast |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
184 |
|
11838 | 185 |
lemma fst_eqD: "fst (x, y) = a ==> x = a" |
186 |
by simp |
|
187 |
||
188 |
lemma snd_eqD: "snd (x, y) = a ==> y = a" |
|
189 |
by simp |
|
190 |
||
191 |
lemma PairE_lemma: "EX x y. p = (x, y)" |
|
192 |
apply (unfold Pair_def) |
|
193 |
apply (rule Rep_Prod [unfolded Prod_def, THEN CollectE]) |
|
194 |
apply (erule exE, erule exE, rule exI, rule exI) |
|
195 |
apply (rule Rep_Prod_inverse [symmetric, THEN trans]) |
|
196 |
apply (erule arg_cong) |
|
197 |
done |
|
11032 | 198 |
|
11838 | 199 |
lemma PairE [cases type: *]: "(!!x y. p = (x, y) ==> Q) ==> Q" |
200 |
by (insert PairE_lemma [of p]) blast |
|
201 |
||
202 |
ML_setup {* |
|
203 |
local val PairE = thm "PairE" in |
|
204 |
fun pair_tac s = |
|
205 |
EVERY' [res_inst_tac [("p", s)] PairE, hyp_subst_tac, K prune_params_tac]; |
|
206 |
end; |
|
207 |
*} |
|
11032 | 208 |
|
11838 | 209 |
lemma surjective_pairing: "p = (fst p, snd p)" |
210 |
-- {* Do not add as rewrite rule: invalidates some proofs in IMP *} |
|
211 |
by (cases p) simp |
|
212 |
||
213 |
declare surjective_pairing [symmetric, simp] |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
214 |
|
11838 | 215 |
lemma surj_pair [simp]: "EX x y. z = (x, y)" |
216 |
apply (rule exI) |
|
217 |
apply (rule exI) |
|
218 |
apply (rule surjective_pairing) |
|
219 |
done |
|
220 |
||
221 |
lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))" |
|
11820
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset
|
222 |
proof |
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset
|
223 |
fix a b |
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset
|
224 |
assume "!!x. PROP P x" |
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset
|
225 |
thus "PROP P (a, b)" . |
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset
|
226 |
next |
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset
|
227 |
fix x |
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset
|
228 |
assume "!!a b. PROP P (a, b)" |
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset
|
229 |
hence "PROP P (fst x, snd x)" . |
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset
|
230 |
thus "PROP P x" by simp |
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset
|
231 |
qed |
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset
|
232 |
|
11838 | 233 |
lemmas split_tupled_all = split_paired_all unit_all_eq2 |
234 |
||
235 |
text {* |
|
236 |
The rule @{thm [source] split_paired_all} does not work with the |
|
237 |
Simplifier because it also affects premises in congrence rules, |
|
238 |
where this can lead to premises of the form @{text "!!a b. ... = |
|
239 |
?P(a, b)"} which cannot be solved by reflexivity. |
|
240 |
*} |
|
241 |
||
242 |
ML_setup " |
|
243 |
(* replace parameters of product type by individual component parameters *) |
|
244 |
val safe_full_simp_tac = generic_simp_tac true (true, false, false); |
|
245 |
local (* filtering with exists_paired_all is an essential optimization *) |
|
246 |
fun exists_paired_all (Const (\"all\", _) $ Abs (_, T, t)) = |
|
247 |
can HOLogic.dest_prodT T orelse exists_paired_all t |
|
248 |
| exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u |
|
249 |
| exists_paired_all (Abs (_, _, t)) = exists_paired_all t |
|
250 |
| exists_paired_all _ = false; |
|
251 |
val ss = HOL_basic_ss |
|
252 |
addsimps [thm \"split_paired_all\", thm \"unit_all_eq2\", thm \"unit_abs_eta_conv\"] |
|
253 |
addsimprocs [unit_eq_proc]; |
|
254 |
in |
|
255 |
val split_all_tac = SUBGOAL (fn (t, i) => |
|
256 |
if exists_paired_all t then safe_full_simp_tac ss i else no_tac); |
|
257 |
val unsafe_split_all_tac = SUBGOAL (fn (t, i) => |
|
258 |
if exists_paired_all t then full_simp_tac ss i else no_tac); |
|
259 |
fun split_all th = |
|
260 |
if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th; |
|
261 |
end; |
|
262 |
||
263 |
claset_ref() := claset() addSbefore (\"split_all_tac\", split_all_tac); |
|
264 |
" |
|
265 |
||
266 |
lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))" |
|
267 |
-- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *} |
|
268 |
by fast |
|
269 |
||
14189 | 270 |
lemma curry_split [simp]: "curry (split f) = f" |
271 |
by (simp add: curry_def split_def) |
|
272 |
||
273 |
lemma split_curry [simp]: "split (curry f) = f" |
|
274 |
by (simp add: curry_def split_def) |
|
275 |
||
276 |
lemma curryI [intro!]: "f (a,b) ==> curry f a b" |
|
277 |
by (simp add: curry_def) |
|
278 |
||
14190
609c072edf90
Fixed blunder in the setup of the classical reasoner wrt. the constant
skalberg
parents:
14189
diff
changeset
|
279 |
lemma curryD [dest!]: "curry f a b ==> f (a,b)" |
14189 | 280 |
by (simp add: curry_def) |
281 |
||
14190
609c072edf90
Fixed blunder in the setup of the classical reasoner wrt. the constant
skalberg
parents:
14189
diff
changeset
|
282 |
lemma curryE: "[| curry f a b ; f (a,b) ==> Q |] ==> Q" |
14189 | 283 |
by (simp add: curry_def) |
284 |
||
285 |
lemma curry_conv [simp]: "curry f a b = f (a,b)" |
|
286 |
by (simp add: curry_def) |
|
287 |
||
11838 | 288 |
lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x" |
289 |
by fast |
|
290 |
||
291 |
lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))" |
|
292 |
by fast |
|
293 |
||
294 |
lemma split_conv [simp]: "split c (a, b) = c a b" |
|
295 |
by (simp add: split_def) |
|
296 |
||
297 |
lemmas split = split_conv -- {* for backwards compatibility *} |
|
298 |
||
299 |
lemmas splitI = split_conv [THEN iffD2, standard] |
|
300 |
lemmas splitD = split_conv [THEN iffD1, standard] |
|
301 |
||
302 |
lemma split_Pair_apply: "split (%x y. f (x, y)) = f" |
|
303 |
-- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *} |
|
304 |
apply (rule ext) |
|
305 |
apply (tactic {* pair_tac "x" 1 *}) |
|
306 |
apply simp |
|
307 |
done |
|
308 |
||
309 |
lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))" |
|
310 |
-- {* Can't be added to simpset: loops! *} |
|
311 |
by (simp add: split_Pair_apply) |
|
312 |
||
313 |
lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))" |
|
314 |
by (simp add: split_def) |
|
315 |
||
316 |
lemma Pair_fst_snd_eq: "!!s t. (s = t) = (fst s = fst t & snd s = snd t)" |
|
317 |
apply (simp only: split_tupled_all) |
|
318 |
apply simp |
|
319 |
done |
|
320 |
||
321 |
lemma prod_eqI [intro?]: "fst p = fst q ==> snd p = snd q ==> p = q" |
|
322 |
by (simp add: Pair_fst_snd_eq) |
|
323 |
||
324 |
lemma split_weak_cong: "p = q ==> split c p = split c q" |
|
325 |
-- {* Prevents simplification of @{term c}: much faster *} |
|
326 |
by (erule arg_cong) |
|
327 |
||
328 |
lemma split_eta: "(%(x, y). f (x, y)) = f" |
|
329 |
apply (rule ext) |
|
330 |
apply (simp only: split_tupled_all) |
|
331 |
apply (rule split_conv) |
|
332 |
done |
|
333 |
||
334 |
lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g" |
|
335 |
by (simp add: split_eta) |
|
336 |
||
337 |
text {* |
|
338 |
Simplification procedure for @{thm [source] cond_split_eta}. Using |
|
339 |
@{thm [source] split_eta} as a rewrite rule is not general enough, |
|
340 |
and using @{thm [source] cond_split_eta} directly would render some |
|
341 |
existing proofs very inefficient; similarly for @{text |
|
342 |
split_beta}. *} |
|
343 |
||
344 |
ML_setup {* |
|
345 |
||
346 |
local |
|
347 |
val cond_split_eta = thm "cond_split_eta"; |
|
348 |
fun Pair_pat k 0 (Bound m) = (m = k) |
|
349 |
| Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso |
|
350 |
m = k+i andalso Pair_pat k (i-1) t |
|
351 |
| Pair_pat _ _ _ = false; |
|
352 |
fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t |
|
353 |
| no_args k i (t $ u) = no_args k i t andalso no_args k i u |
|
354 |
| no_args k i (Bound m) = m < k orelse m > k+i |
|
355 |
| no_args _ _ _ = true; |
|
356 |
fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then Some (i,t) else None |
|
357 |
| split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t |
|
358 |
| split_pat tp i _ = None; |
|
13480
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
359 |
fun metaeq sg lhs rhs = mk_meta_eq (Tactic.prove sg [] [] |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
360 |
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))) |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
361 |
(K (simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1))); |
11838 | 362 |
|
363 |
fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t |
|
364 |
| beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse |
|
365 |
(beta_term_pat k i t andalso beta_term_pat k i u) |
|
366 |
| beta_term_pat k i t = no_args k i t; |
|
367 |
fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg |
|
368 |
| eta_term_pat _ _ _ = false; |
|
369 |
fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t) |
|
370 |
| subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg |
|
371 |
else (subst arg k i t $ subst arg k i u) |
|
372 |
| subst arg k i t = t; |
|
373 |
fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) = |
|
374 |
(case split_pat beta_term_pat 1 t of |
|
375 |
Some (i,f) => Some (metaeq sg s (subst arg 0 i f)) |
|
376 |
| None => None) |
|
377 |
| beta_proc _ _ _ = None; |
|
378 |
fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) = |
|
379 |
(case split_pat eta_term_pat 1 t of |
|
380 |
Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end)) |
|
381 |
| None => None) |
|
382 |
| eta_proc _ _ _ = None; |
|
383 |
in |
|
13462 | 384 |
val split_beta_proc = Simplifier.simproc (Theory.sign_of (the_context ())) |
385 |
"split_beta" ["split f z"] beta_proc; |
|
386 |
val split_eta_proc = Simplifier.simproc (Theory.sign_of (the_context ())) |
|
387 |
"split_eta" ["split f"] eta_proc; |
|
11838 | 388 |
end; |
389 |
||
390 |
Addsimprocs [split_beta_proc, split_eta_proc]; |
|
391 |
*} |
|
392 |
||
393 |
lemma split_beta: "(%(x, y). P x y) z = P (fst z) (snd z)" |
|
394 |
by (subst surjective_pairing, rule split_conv) |
|
395 |
||
396 |
lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))" |
|
397 |
-- {* For use with @{text split} and the Simplifier. *} |
|
398 |
apply (subst surjective_pairing) |
|
399 |
apply (subst split_conv) |
|
400 |
apply blast |
|
401 |
done |
|
402 |
||
403 |
text {* |
|
404 |
@{thm [source] split_split} could be declared as @{text "[split]"} |
|
405 |
done after the Splitter has been speeded up significantly; |
|
406 |
precompute the constants involved and don't do anything unless the |
|
407 |
current goal contains one of those constants. |
|
408 |
*} |
|
409 |
||
410 |
lemma split_split_asm: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))" |
|
411 |
apply (subst split_split) |
|
412 |
apply simp |
|
413 |
done |
|
414 |
||
415 |
||
416 |
text {* |
|
417 |
\medskip @{term split} used as a logical connective or set former. |
|
418 |
||
419 |
\medskip These rules are for use with @{text blast}; could instead |
|
420 |
call @{text simp} using @{thm [source] split} as rewrite. *} |
|
421 |
||
422 |
lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p" |
|
423 |
apply (simp only: split_tupled_all) |
|
424 |
apply (simp (no_asm_simp)) |
|
425 |
done |
|
426 |
||
427 |
lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> split c p x" |
|
428 |
apply (simp only: split_tupled_all) |
|
429 |
apply (simp (no_asm_simp)) |
|
430 |
done |
|
431 |
||
432 |
lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" |
|
433 |
by (induct p) (auto simp add: split_def) |
|
434 |
||
435 |
lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" |
|
436 |
by (induct p) (auto simp add: split_def) |
|
437 |
||
438 |
lemma splitE2: |
|
439 |
"[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R" |
|
440 |
proof - |
|
441 |
assume q: "Q (split P z)" |
|
442 |
assume r: "!!x y. [|z = (x, y); Q (P x y)|] ==> R" |
|
443 |
show R |
|
444 |
apply (rule r surjective_pairing)+ |
|
445 |
apply (rule split_beta [THEN subst], rule q) |
|
446 |
done |
|
447 |
qed |
|
448 |
||
449 |
lemma splitD': "split R (a,b) c ==> R a b c" |
|
450 |
by simp |
|
451 |
||
452 |
lemma mem_splitI: "z: c a b ==> z: split c (a, b)" |
|
453 |
by simp |
|
454 |
||
455 |
lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: split c p" |
|
456 |
apply (simp only: split_tupled_all) |
|
457 |
apply simp |
|
458 |
done |
|
459 |
||
460 |
lemma mem_splitE: "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q" |
|
461 |
proof - |
|
462 |
case rule_context [unfolded split_def] |
|
463 |
show ?thesis by (rule rule_context surjective_pairing)+ |
|
464 |
qed |
|
465 |
||
466 |
declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!] |
|
467 |
declare mem_splitE [elim!] splitE' [elim!] splitE [elim!] |
|
468 |
||
469 |
ML_setup " |
|
470 |
local (* filtering with exists_p_split is an essential optimization *) |
|
471 |
fun exists_p_split (Const (\"split\",_) $ _ $ (Const (\"Pair\",_)$_$_)) = true |
|
472 |
| exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u |
|
473 |
| exists_p_split (Abs (_, _, t)) = exists_p_split t |
|
474 |
| exists_p_split _ = false; |
|
475 |
val ss = HOL_basic_ss addsimps [thm \"split_conv\"]; |
|
476 |
in |
|
477 |
val split_conv_tac = SUBGOAL (fn (t, i) => |
|
478 |
if exists_p_split t then safe_full_simp_tac ss i else no_tac); |
|
479 |
end; |
|
480 |
(* This prevents applications of splitE for already splitted arguments leading |
|
481 |
to quite time-consuming computations (in particular for nested tuples) *) |
|
482 |
claset_ref() := claset() addSbefore (\"split_conv_tac\", split_conv_tac); |
|
483 |
" |
|
484 |
||
485 |
lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P" |
|
486 |
apply (rule ext) |
|
487 |
apply fast |
|
488 |
done |
|
489 |
||
490 |
lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P" |
|
491 |
apply (rule ext) |
|
492 |
apply fast |
|
493 |
done |
|
494 |
||
495 |
lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)" |
|
496 |
-- {* Allows simplifications of nested splits in case of independent predicates. *} |
|
497 |
apply (rule ext) |
|
498 |
apply blast |
|
499 |
done |
|
500 |
||
14101 | 501 |
lemma split_comp_eq [simp]: |
502 |
"(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))" |
|
503 |
by (rule ext, auto) |
|
504 |
||
11838 | 505 |
lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)" |
506 |
by blast |
|
507 |
||
508 |
(* |
|
509 |
the following would be slightly more general, |
|
510 |
but cannot be used as rewrite rule: |
|
511 |
### Cannot add premise as rewrite rule because it contains (type) unknowns: |
|
512 |
### ?y = .x |
|
513 |
Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)" |
|
514 |
by (rtac some_equality 1); |
|
515 |
by ( Simp_tac 1); |
|
516 |
by (split_all_tac 1); |
|
517 |
by (Asm_full_simp_tac 1); |
|
518 |
qed "The_split_eq"; |
|
519 |
*) |
|
520 |
||
521 |
lemma injective_fst_snd: "!!x y. [|fst x = fst y; snd x = snd y|] ==> x = y" |
|
522 |
by auto |
|
523 |
||
524 |
||
525 |
text {* |
|
526 |
\bigskip @{term prod_fun} --- action of the product functor upon |
|
527 |
functions. |
|
528 |
*} |
|
529 |
||
530 |
lemma prod_fun [simp]: "prod_fun f g (a, b) = (f a, g b)" |
|
531 |
by (simp add: prod_fun_def) |
|
532 |
||
533 |
lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)" |
|
534 |
apply (rule ext) |
|
535 |
apply (tactic {* pair_tac "x" 1 *}) |
|
536 |
apply simp |
|
537 |
done |
|
538 |
||
539 |
lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)" |
|
540 |
apply (rule ext) |
|
541 |
apply (tactic {* pair_tac "z" 1 *}) |
|
542 |
apply simp |
|
543 |
done |
|
544 |
||
545 |
lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r" |
|
546 |
apply (rule image_eqI) |
|
547 |
apply (rule prod_fun [symmetric]) |
|
548 |
apply assumption |
|
549 |
done |
|
550 |
||
551 |
lemma prod_fun_imageE [elim!]: |
|
552 |
"[| c: (prod_fun f g)`r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P |
|
553 |
|] ==> P" |
|
554 |
proof - |
|
555 |
case rule_context |
|
556 |
assume major: "c: (prod_fun f g)`r" |
|
557 |
show ?thesis |
|
558 |
apply (rule major [THEN imageE]) |
|
559 |
apply (rule_tac p = x in PairE) |
|
560 |
apply (rule rule_context) |
|
561 |
prefer 2 |
|
562 |
apply blast |
|
563 |
apply (blast intro: prod_fun) |
|
564 |
done |
|
565 |
qed |
|
566 |
||
567 |
||
14101 | 568 |
constdefs |
569 |
upd_fst :: "('a => 'c) => 'a * 'b => 'c * 'b" |
|
570 |
"upd_fst f == prod_fun f id" |
|
571 |
||
572 |
upd_snd :: "('b => 'c) => 'a * 'b => 'a * 'c" |
|
573 |
"upd_snd f == prod_fun id f" |
|
574 |
||
575 |
lemma upd_fst_conv [simp]: "upd_fst f (x,y) = (f x,y)" |
|
576 |
by (simp add: upd_fst_def) |
|
577 |
||
578 |
lemma upd_snd_conv [simp]: "upd_snd f (x,y) = (x,f y)" |
|
579 |
by (simp add: upd_snd_def) |
|
580 |
||
11838 | 581 |
text {* |
582 |
\bigskip Disjoint union of a family of sets -- Sigma. |
|
583 |
*} |
|
584 |
||
585 |
lemma SigmaI [intro!]: "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B" |
|
586 |
by (unfold Sigma_def) blast |
|
587 |
||
588 |
||
589 |
lemma SigmaE: |
|
590 |
"[| c: Sigma A B; |
|
591 |
!!x y.[| x:A; y:B(x); c=(x,y) |] ==> P |
|
592 |
|] ==> P" |
|
593 |
-- {* The general elimination rule. *} |
|
594 |
by (unfold Sigma_def) blast |
|
595 |
||
596 |
text {* |
|
597 |
Elimination of @{term "(a, b) : A \<times> B"} -- introduces no |
|
598 |
eigenvariables. |
|
599 |
*} |
|
600 |
||
601 |
lemma SigmaD1: "(a, b) : Sigma A B ==> a : A" |
|
602 |
apply (erule SigmaE) |
|
603 |
apply blast |
|
604 |
done |
|
605 |
||
606 |
lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a" |
|
607 |
apply (erule SigmaE) |
|
608 |
apply blast |
|
609 |
done |
|
610 |
||
611 |
lemma SigmaE2: |
|
612 |
"[| (a, b) : Sigma A B; |
|
613 |
[| a:A; b:B(a) |] ==> P |
|
614 |
|] ==> P" |
|
615 |
by (blast dest: SigmaD1 SigmaD2) |
|
616 |
||
617 |
declare SigmaE [elim!] SigmaE2 [elim!] |
|
618 |
||
619 |
lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D" |
|
620 |
by blast |
|
621 |
||
622 |
lemma Sigma_empty1 [simp]: "Sigma {} B = {}" |
|
623 |
by blast |
|
624 |
||
625 |
lemma Sigma_empty2 [simp]: "A <*> {} = {}" |
|
626 |
by blast |
|
627 |
||
628 |
lemma UNIV_Times_UNIV [simp]: "UNIV <*> UNIV = UNIV" |
|
629 |
by auto |
|
630 |
||
631 |
lemma Compl_Times_UNIV1 [simp]: "- (UNIV <*> A) = UNIV <*> (-A)" |
|
632 |
by auto |
|
633 |
||
634 |
lemma Compl_Times_UNIV2 [simp]: "- (A <*> UNIV) = (-A) <*> UNIV" |
|
635 |
by auto |
|
636 |
||
637 |
lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))" |
|
638 |
by blast |
|
639 |
||
640 |
lemma Times_subset_cancel2: "x:C ==> (A <*> C <= B <*> C) = (A <= B)" |
|
641 |
by blast |
|
642 |
||
643 |
lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)" |
|
644 |
by (blast elim: equalityE) |
|
645 |
||
646 |
lemma SetCompr_Sigma_eq: |
|
647 |
"Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))" |
|
648 |
by blast |
|
649 |
||
650 |
text {* |
|
651 |
\bigskip Complex rules for Sigma. |
|
652 |
*} |
|
653 |
||
654 |
lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q" |
|
655 |
by blast |
|
656 |
||
657 |
lemma UN_Times_distrib: |
|
658 |
"(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)" |
|
659 |
-- {* Suggested by Pierre Chartier *} |
|
660 |
by blast |
|
661 |
||
662 |
lemma split_paired_Ball_Sigma [simp]: |
|
663 |
"(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))" |
|
664 |
by blast |
|
665 |
||
666 |
lemma split_paired_Bex_Sigma [simp]: |
|
667 |
"(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))" |
|
668 |
by blast |
|
669 |
||
670 |
lemma Sigma_Un_distrib1: "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))" |
|
671 |
by blast |
|
672 |
||
673 |
lemma Sigma_Un_distrib2: "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))" |
|
674 |
by blast |
|
675 |
||
676 |
lemma Sigma_Int_distrib1: "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))" |
|
677 |
by blast |
|
678 |
||
679 |
lemma Sigma_Int_distrib2: "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))" |
|
680 |
by blast |
|
681 |
||
682 |
lemma Sigma_Diff_distrib1: "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))" |
|
683 |
by blast |
|
684 |
||
685 |
lemma Sigma_Diff_distrib2: "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))" |
|
686 |
by blast |
|
687 |
||
688 |
lemma Sigma_Union: "Sigma (Union X) B = (UN A:X. Sigma A B)" |
|
689 |
by blast |
|
690 |
||
691 |
text {* |
|
692 |
Non-dependent versions are needed to avoid the need for higher-order |
|
693 |
matching, especially when the rules are re-oriented. |
|
694 |
*} |
|
695 |
||
696 |
lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)" |
|
697 |
by blast |
|
698 |
||
699 |
lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)" |
|
700 |
by blast |
|
701 |
||
702 |
lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)" |
|
703 |
by blast |
|
704 |
||
705 |
||
11493 | 706 |
lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A" |
11777 | 707 |
apply (rule_tac x = "(a, b)" in image_eqI) |
708 |
apply auto |
|
709 |
done |
|
710 |
||
11493 | 711 |
|
11838 | 712 |
text {* |
713 |
Setup of internal @{text split_rule}. |
|
714 |
*} |
|
715 |
||
11032 | 716 |
constdefs |
11425 | 717 |
internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c" |
11032 | 718 |
"internal_split == split" |
719 |
||
720 |
lemma internal_split_conv: "internal_split c (a, b) = c a b" |
|
721 |
by (simp only: internal_split_def split_conv) |
|
722 |
||
723 |
hide const internal_split |
|
724 |
||
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset
|
725 |
use "Tools/split_rule.ML" |
11032 | 726 |
setup SplitRule.setup |
10213 | 727 |
|
728 |
end |