86 |
87 |
87 lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f" |
88 lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f" |
88 by (rule ext) simp |
89 by (rule ext) simp |
89 |
90 |
90 |
91 |
|
92 text {* code generator setup *} |
|
93 |
|
94 instance unit :: eq .. |
|
95 |
|
96 lemma [code func]: |
|
97 "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+ |
|
98 |
|
99 code_type unit |
|
100 (SML "unit") |
|
101 (OCaml "unit") |
|
102 (Haskell "()") |
|
103 |
|
104 code_instance unit :: eq |
|
105 (Haskell -) |
|
106 |
|
107 code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool" |
|
108 (Haskell infixl 4 "==") |
|
109 |
|
110 code_const Unity |
|
111 (SML "()") |
|
112 (OCaml "()") |
|
113 (Haskell "()") |
|
114 |
|
115 code_reserved SML |
|
116 unit |
|
117 |
|
118 code_reserved OCaml |
|
119 unit |
|
120 |
|
121 |
91 subsection {* Pairs *} |
122 subsection {* Pairs *} |
92 |
123 |
93 subsubsection {* Type definition *} |
124 subsubsection {* Product type, basic operations and concrete syntax *} |
94 |
125 |
95 constdefs |
126 definition |
96 Pair_Rep :: "['a, 'b] => ['a, 'b] => bool" |
127 Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
97 "Pair_Rep == (%a b. %x y. x=a & y=b)" |
128 where |
|
129 "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)" |
98 |
130 |
99 global |
131 global |
100 |
132 |
101 typedef (Prod) |
133 typedef (Prod) |
102 ('a, 'b) "*" (infixr "*" 20) |
134 ('a, 'b) "*" (infixr "*" 20) |
103 = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}" |
135 = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}" |
104 proof |
136 proof |
105 fix a b show "Pair_Rep a b : ?Prod" |
137 fix a b show "Pair_Rep a b \<in> ?Prod" |
106 by blast |
138 by rule+ |
107 qed |
139 qed |
108 |
140 |
109 syntax (xsymbols) |
141 syntax (xsymbols) |
110 "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) |
142 "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) |
111 syntax (HTML output) |
143 syntax (HTML output) |
112 "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) |
144 "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) |
113 |
145 |
114 local |
|
115 |
|
116 subsubsection {* Definitions *} |
|
117 |
|
118 global |
|
119 |
|
120 consts |
146 consts |
121 fst :: "'a * 'b => 'a" |
147 Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" |
122 snd :: "'a * 'b => 'b" |
148 fst :: "'a \<times> 'b \<Rightarrow> 'a" |
123 split :: "[['a, 'b] => 'c, 'a * 'b] => 'c" |
149 snd :: "'a \<times> 'b \<Rightarrow> 'b" |
124 curry :: "['a * 'b => 'c, 'a, 'b] => 'c" |
150 split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" |
125 prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd" |
151 curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" |
126 Pair :: "['a, 'b] => 'a * 'b" |
|
127 Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set" |
|
128 |
152 |
129 local |
153 local |
130 |
154 |
131 defs |
155 defs |
132 Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)" |
156 Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)" |
133 fst_def: "fst p == THE a. EX b. p = Pair a b" |
157 fst_def: "fst p == THE a. EX b. p = Pair a b" |
134 snd_def: "snd p == THE b. EX a. p = Pair a b" |
158 snd_def: "snd p == THE b. EX a. p = Pair a b" |
135 split_def: "split == (%c p. c (fst p) (snd p))" |
159 split_def: "split == (%c p. c (fst p) (snd p))" |
136 curry_def: "curry == (%c x y. c (Pair x y))" |
160 curry_def: "curry == (%c x y. c (Pair x y))" |
137 prod_fun_def: "prod_fun f g == split (%x y. Pair (f x) (g y))" |
|
138 Sigma_def [code func]: "Sigma A B == UN x:A. UN y:B x. {Pair x y}" |
|
139 |
|
140 abbreviation |
|
141 Times :: "['a set, 'b set] => ('a * 'b) set" |
|
142 (infixr "<*>" 80) where |
|
143 "A <*> B == Sigma A (%_. B)" |
|
144 |
|
145 notation (xsymbols) |
|
146 Times (infixr "\<times>" 80) |
|
147 |
|
148 notation (HTML output) |
|
149 Times (infixr "\<times>" 80) |
|
150 |
|
151 |
|
152 subsubsection {* Concrete syntax *} |
|
153 |
161 |
154 text {* |
162 text {* |
155 Patterns -- extends pre-defined type @{typ pttrn} used in |
163 Patterns -- extends pre-defined type @{typ pttrn} used in |
156 abstractions. |
164 abstractions. |
157 *} |
165 *} |
164 "_tuple_arg" :: "'a => tuple_args" ("_") |
172 "_tuple_arg" :: "'a => tuple_args" ("_") |
165 "_tuple_args" :: "'a => tuple_args => tuple_args" ("_,/ _") |
173 "_tuple_args" :: "'a => tuple_args => tuple_args" ("_,/ _") |
166 "_pattern" :: "[pttrn, patterns] => pttrn" ("'(_,/ _')") |
174 "_pattern" :: "[pttrn, patterns] => pttrn" ("'(_,/ _')") |
167 "" :: "pttrn => patterns" ("_") |
175 "" :: "pttrn => patterns" ("_") |
168 "_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") |
176 "_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") |
169 "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10) |
|
170 |
177 |
171 translations |
178 translations |
172 "(x, y)" == "Pair x y" |
179 "(x, y)" == "Pair x y" |
173 "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" |
180 "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" |
174 "%(x,y,zs).b" == "split(%x (y,zs).b)" |
181 "%(x,y,zs).b" == "split(%x (y,zs).b)" |
175 "%(x,y).b" == "split(%x y. b)" |
182 "%(x,y).b" == "split(%x y. b)" |
176 "_abs (Pair x y) t" => "%(x,y).t" |
183 "_abs (Pair x y) t" => "%(x,y).t" |
177 (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
184 (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
178 The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) |
185 The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) |
179 "SIGMA x:A. B" == "Sigma A (%x. B)" |
|
180 |
186 |
181 (* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*) |
187 (* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*) |
182 (* works best with enclosing "let", if "let" does not avoid eta-contraction *) |
188 (* works best with enclosing "let", if "let" does not avoid eta-contraction *) |
183 print_translation {* |
189 print_translation {* |
184 let fun split_tr' [Abs (x,T,t as (Abs abs))] = |
190 let fun split_tr' [Abs (x,T,t as (Abs abs))] = |
230 in [("split", split_guess_names_tr')] |
236 in [("split", split_guess_names_tr')] |
231 end |
237 end |
232 *} |
238 *} |
233 |
239 |
234 |
240 |
235 subsubsection {* Lemmas and proof tool setup *} |
241 text {* Towards a datatype declaration *} |
236 |
242 |
237 lemma ProdI: "Pair_Rep a b : Prod" |
243 lemma surj_pair [simp]: "EX x y. p = (x, y)" |
238 unfolding Prod_def by blast |
244 apply (unfold Pair_def) |
239 |
245 apply (rule Rep_Prod [unfolded Prod_def, THEN CollectE]) |
240 lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' ==> a = a' & b = b'" |
246 apply (erule exE, erule exE, rule exI, rule exI) |
241 apply (unfold Pair_Rep_def) |
247 apply (rule Rep_Prod_inverse [symmetric, THEN trans]) |
242 apply (drule fun_cong [THEN fun_cong], blast) |
248 apply (erule arg_cong) |
243 done |
249 done |
|
250 |
|
251 lemma PairE [cases type: *]: |
|
252 obtains x y where "p = (x, y)" |
|
253 using surj_pair [of p] by blast |
|
254 |
|
255 |
|
256 lemma prod_induct [induct type: *]: "(\<And>a b. P (a, b)) \<Longrightarrow> P x" |
|
257 by (cases x) simp |
|
258 |
|
259 lemma ProdI: "Pair_Rep a b \<in> Prod" |
|
260 unfolding Prod_def by rule+ |
|
261 |
|
262 lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' \<Longrightarrow> a = a' \<and> b = b'" |
|
263 unfolding Pair_Rep_def by (drule fun_cong, drule fun_cong) blast |
244 |
264 |
245 lemma inj_on_Abs_Prod: "inj_on Abs_Prod Prod" |
265 lemma inj_on_Abs_Prod: "inj_on Abs_Prod Prod" |
246 apply (rule inj_on_inverseI) |
266 apply (rule inj_on_inverseI) |
247 apply (erule Abs_Prod_inverse) |
267 apply (erule Abs_Prod_inverse) |
248 done |
268 done |
263 unfolding fst_def by blast |
283 unfolding fst_def by blast |
264 |
284 |
265 lemma snd_conv [simp, code]: "snd (a, b) = b" |
285 lemma snd_conv [simp, code]: "snd (a, b) = b" |
266 unfolding snd_def by blast |
286 unfolding snd_def by blast |
267 |
287 |
|
288 rep_datatype prod |
|
289 inject Pair_eq |
|
290 induction prod_induct |
|
291 |
|
292 |
|
293 subsubsection {* Basic rules and proof tools *} |
|
294 |
268 lemma fst_eqD: "fst (x, y) = a ==> x = a" |
295 lemma fst_eqD: "fst (x, y) = a ==> x = a" |
269 by simp |
296 by simp |
270 |
297 |
271 lemma snd_eqD: "snd (x, y) = a ==> y = a" |
298 lemma snd_eqD: "snd (x, y) = a ==> y = a" |
272 by simp |
299 by simp |
273 |
300 |
274 lemma PairE_lemma: "EX x y. p = (x, y)" |
301 lemma pair_collapse [simp]: "(fst p, snd p) = p" |
275 apply (unfold Pair_def) |
|
276 apply (rule Rep_Prod [unfolded Prod_def, THEN CollectE]) |
|
277 apply (erule exE, erule exE, rule exI, rule exI) |
|
278 apply (rule Rep_Prod_inverse [symmetric, THEN trans]) |
|
279 apply (erule arg_cong) |
|
280 done |
|
281 |
|
282 lemma PairE [cases type: *]: "(!!x y. p = (x, y) ==> Q) ==> Q" |
|
283 using PairE_lemma [of p] by blast |
|
284 |
|
285 ML {* |
|
286 local val PairE = thm "PairE" in |
|
287 fun pair_tac s = |
|
288 EVERY' [res_inst_tac [("p", s)] PairE, hyp_subst_tac, K prune_params_tac]; |
|
289 end; |
|
290 *} |
|
291 |
|
292 lemma surjective_pairing: "p = (fst p, snd p)" |
|
293 -- {* Do not add as rewrite rule: invalidates some proofs in IMP *} |
|
294 by (cases p) simp |
302 by (cases p) simp |
295 |
303 |
296 lemmas pair_collapse = surjective_pairing [symmetric] |
304 lemmas surjective_pairing = pair_collapse [symmetric] |
297 declare pair_collapse [simp] |
|
298 |
|
299 lemma surj_pair [simp]: "EX x y. z = (x, y)" |
|
300 apply (rule exI) |
|
301 apply (rule exI) |
|
302 apply (rule surjective_pairing) |
|
303 done |
|
304 |
305 |
305 lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))" |
306 lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))" |
306 proof |
307 proof |
307 fix a b |
308 fix a b |
308 assume "!!x. PROP P x" |
309 assume "!!x. PROP P x" |
311 fix x |
312 fix x |
312 assume "!!a b. PROP P (a, b)" |
313 assume "!!a b. PROP P (a, b)" |
313 from `PROP P (fst x, snd x)` show "PROP P x" by simp |
314 from `PROP P (fst x, snd x)` show "PROP P x" by simp |
314 qed |
315 qed |
315 |
316 |
316 lemmas split_tupled_all = split_paired_all unit_all_eq2 |
|
317 |
|
318 text {* |
317 text {* |
319 The rule @{thm [source] split_paired_all} does not work with the |
318 The rule @{thm [source] split_paired_all} does not work with the |
320 Simplifier because it also affects premises in congrence rules, |
319 Simplifier because it also affects premises in congrence rules, |
321 where this can lead to premises of the form @{text "!!a b. ... = |
320 where this can lead to premises of the form @{text "!!a b. ... = |
322 ?P(a, b)"} which cannot be solved by reflexivity. |
321 ?P(a, b)"} which cannot be solved by reflexivity. |
323 *} |
322 *} |
324 |
323 |
325 ML {* |
324 lemmas split_tupled_all = split_paired_all unit_all_eq2 |
|
325 |
|
326 ML_setup {* |
326 (* replace parameters of product type by individual component parameters *) |
327 (* replace parameters of product type by individual component parameters *) |
327 val safe_full_simp_tac = generic_simp_tac true (true, false, false); |
328 val safe_full_simp_tac = generic_simp_tac true (true, false, false); |
328 local (* filtering with exists_paired_all is an essential optimization *) |
329 local (* filtering with exists_paired_all is an essential optimization *) |
329 fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) = |
330 fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) = |
330 can HOLogic.dest_prodT T orelse exists_paired_all t |
331 can HOLogic.dest_prodT T orelse exists_paired_all t |
350 |
351 |
351 lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))" |
352 lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))" |
352 -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *} |
353 -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *} |
353 by fast |
354 by fast |
354 |
355 |
|
356 lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))" |
|
357 by fast |
|
358 |
|
359 lemma Pair_fst_snd_eq: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t" |
|
360 by (cases s, cases t) simp |
|
361 |
|
362 lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q" |
|
363 by (simp add: Pair_fst_snd_eq) |
|
364 |
|
365 |
|
366 subsubsection {* @{text split} and @{text curry} *} |
|
367 |
|
368 lemma split_conv [simp, code func]: "split f (a, b) = f a b" |
|
369 by (simp add: split_def) |
|
370 |
|
371 lemma curry_conv [simp, code func]: "curry f a b = f (a, b)" |
|
372 by (simp add: curry_def) |
|
373 |
|
374 lemmas split = split_conv -- {* for backwards compatibility *} |
|
375 |
|
376 lemma splitI: "f a b \<Longrightarrow> split f (a, b)" |
|
377 by (rule split_conv [THEN iffD2]) |
|
378 |
|
379 lemma splitD: "split f (a, b) \<Longrightarrow> f a b" |
|
380 by (rule split_conv [THEN iffD1]) |
|
381 |
|
382 lemma curryI [intro!]: "f (a, b) \<Longrightarrow> curry f a b" |
|
383 by (simp add: curry_def) |
|
384 |
|
385 lemma curryD [dest!]: "curry f a b \<Longrightarrow> f (a, b)" |
|
386 by (simp add: curry_def) |
|
387 |
|
388 lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q" |
|
389 by (simp add: curry_def) |
|
390 |
355 lemma curry_split [simp]: "curry (split f) = f" |
391 lemma curry_split [simp]: "curry (split f) = f" |
356 by (simp add: curry_def split_def) |
392 by (simp add: curry_def split_def) |
357 |
393 |
358 lemma split_curry [simp]: "split (curry f) = f" |
394 lemma split_curry [simp]: "split (curry f) = f" |
359 by (simp add: curry_def split_def) |
395 by (simp add: curry_def split_def) |
360 |
396 |
361 lemma curryI [intro!]: "f (a,b) ==> curry f a b" |
397 lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id" |
362 by (simp add: curry_def) |
398 by (simp add: split_def id_def) |
363 |
399 |
364 lemma curryD [dest!]: "curry f a b ==> f (a,b)" |
400 lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f" |
365 by (simp add: curry_def) |
|
366 |
|
367 lemma curryE: "[| curry f a b ; f (a,b) ==> Q |] ==> Q" |
|
368 by (simp add: curry_def) |
|
369 |
|
370 lemma curry_conv [simp, code func]: "curry f a b = f (a,b)" |
|
371 by (simp add: curry_def) |
|
372 |
|
373 lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x" |
|
374 by fast |
|
375 |
|
376 rep_datatype prod |
|
377 inject Pair_eq |
|
378 induction prod_induct |
|
379 |
|
380 lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))" |
|
381 by fast |
|
382 |
|
383 lemma split_conv [simp, code func]: "split c (a, b) = c a b" |
|
384 by (simp add: split_def) |
|
385 |
|
386 lemmas split = split_conv -- {* for backwards compatibility *} |
|
387 |
|
388 lemmas splitI = split_conv [THEN iffD2, standard] |
|
389 lemmas splitD = split_conv [THEN iffD1, standard] |
|
390 |
|
391 lemma split_Pair_apply: "split (%x y. f (x, y)) = f" |
|
392 -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *} |
401 -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *} |
393 apply (rule ext) |
402 by (rule ext) auto |
394 apply (tactic {* pair_tac "x" 1 *}, simp) |
403 |
395 done |
404 lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)" |
|
405 by (cases x) simp |
|
406 |
|
407 lemma split_twice: "split f (split g p) = split (\<lambda>x y. split f (g x y)) p" |
|
408 unfolding split_def .. |
396 |
409 |
397 lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))" |
410 lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))" |
398 -- {* Can't be added to simpset: loops! *} |
411 -- {* Can't be added to simpset: loops! *} |
399 by (simp add: split_Pair_apply) |
412 by (simp add: split_eta) |
400 |
413 |
401 lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))" |
414 lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))" |
402 by (simp add: split_def) |
415 by (simp add: split_def) |
403 |
416 |
404 lemma Pair_fst_snd_eq: "!!s t. (s = t) = (fst s = fst t & snd s = snd t)" |
417 lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q" |
405 by (simp only: split_tupled_all, simp) |
|
406 |
|
407 lemma prod_eqI [intro?]: "fst p = fst q ==> snd p = snd q ==> p = q" |
|
408 by (simp add: Pair_fst_snd_eq) |
|
409 |
|
410 lemma split_weak_cong: "p = q ==> split c p = split c q" |
|
411 -- {* Prevents simplification of @{term c}: much faster *} |
418 -- {* Prevents simplification of @{term c}: much faster *} |
412 by (erule arg_cong) |
419 by (erule arg_cong) |
413 |
|
414 lemma split_eta: "(%(x, y). f (x, y)) = f" |
|
415 apply (rule ext) |
|
416 apply (simp only: split_tupled_all) |
|
417 apply (rule split_conv) |
|
418 done |
|
419 |
420 |
420 lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g" |
421 lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g" |
421 by (simp add: split_eta) |
422 by (simp add: split_eta) |
422 |
423 |
423 text {* |
424 text {* |
424 Simplification procedure for @{thm [source] cond_split_eta}. Using |
425 Simplification procedure for @{thm [source] cond_split_eta}. Using |
425 @{thm [source] split_eta} as a rewrite rule is not general enough, |
426 @{thm [source] split_eta} as a rewrite rule is not general enough, |
426 and using @{thm [source] cond_split_eta} directly would render some |
427 and using @{thm [source] cond_split_eta} directly would render some |
427 existing proofs very inefficient; similarly for @{text |
428 existing proofs very inefficient; similarly for @{text |
428 split_beta}. *} |
429 split_beta}. |
|
430 *} |
429 |
431 |
430 ML_setup {* |
432 ML_setup {* |
431 |
433 |
432 local |
434 local |
433 val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"] |
435 val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"] |
595 by (split_all_tac 1) |
602 by (split_all_tac 1) |
596 by (Asm_full_simp_tac 1) |
603 by (Asm_full_simp_tac 1) |
597 qed "The_split_eq"; |
604 qed "The_split_eq"; |
598 *) |
605 *) |
599 |
606 |
600 lemma injective_fst_snd: "!!x y. [|fst x = fst y; snd x = snd y|] ==> x = y" |
607 text {* |
|
608 Setup of internal @{text split_rule}. |
|
609 *} |
|
610 |
|
611 definition |
|
612 internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" |
|
613 where |
|
614 "internal_split == split" |
|
615 |
|
616 lemma internal_split_conv: "internal_split c (a, b) = c a b" |
|
617 by (simp only: internal_split_def split_conv) |
|
618 |
|
619 hide const internal_split |
|
620 |
|
621 use "Tools/split_rule.ML" |
|
622 setup SplitRule.setup |
|
623 |
|
624 lemmas prod_caseI = prod.cases [THEN iffD2, standard] |
|
625 |
|
626 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" |
601 by auto |
627 by auto |
602 |
628 |
603 |
629 lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x" |
604 text {* |
630 by (auto simp: split_tupled_all) |
605 \bigskip @{term prod_fun} --- action of the product functor upon |
631 |
|
632 lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" |
|
633 by (induct p) auto |
|
634 |
|
635 lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" |
|
636 by (induct p) auto |
|
637 |
|
638 lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))" |
|
639 by (simp add: expand_fun_eq) |
|
640 |
|
641 declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!] |
|
642 declare prod_caseE' [elim!] prod_caseE [elim!] |
|
643 |
|
644 lemma prod_case_split: |
|
645 "prod_case = split" |
|
646 by (auto simp add: expand_fun_eq) |
|
647 |
|
648 lemma prod_case_beta: |
|
649 "prod_case f p = f (fst p) (snd p)" |
|
650 unfolding prod_case_split split_beta .. |
|
651 |
|
652 |
|
653 subsection {* Further cases/induct rules for tuples *} |
|
654 |
|
655 lemma prod_cases3 [cases type]: |
|
656 obtains (fields) a b c where "y = (a, b, c)" |
|
657 by (cases y, case_tac b) blast |
|
658 |
|
659 lemma prod_induct3 [case_names fields, induct type]: |
|
660 "(!!a b c. P (a, b, c)) ==> P x" |
|
661 by (cases x) blast |
|
662 |
|
663 lemma prod_cases4 [cases type]: |
|
664 obtains (fields) a b c d where "y = (a, b, c, d)" |
|
665 by (cases y, case_tac c) blast |
|
666 |
|
667 lemma prod_induct4 [case_names fields, induct type]: |
|
668 "(!!a b c d. P (a, b, c, d)) ==> P x" |
|
669 by (cases x) blast |
|
670 |
|
671 lemma prod_cases5 [cases type]: |
|
672 obtains (fields) a b c d e where "y = (a, b, c, d, e)" |
|
673 by (cases y, case_tac d) blast |
|
674 |
|
675 lemma prod_induct5 [case_names fields, induct type]: |
|
676 "(!!a b c d e. P (a, b, c, d, e)) ==> P x" |
|
677 by (cases x) blast |
|
678 |
|
679 lemma prod_cases6 [cases type]: |
|
680 obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)" |
|
681 by (cases y, case_tac e) blast |
|
682 |
|
683 lemma prod_induct6 [case_names fields, induct type]: |
|
684 "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" |
|
685 by (cases x) blast |
|
686 |
|
687 lemma prod_cases7 [cases type]: |
|
688 obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)" |
|
689 by (cases y, case_tac f) blast |
|
690 |
|
691 lemma prod_induct7 [case_names fields, induct type]: |
|
692 "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" |
|
693 by (cases x) blast |
|
694 |
|
695 |
|
696 subsubsection {* Derived operations *} |
|
697 |
|
698 text {* |
|
699 The composition-uncurry combinator. |
|
700 *} |
|
701 |
|
702 definition |
|
703 mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o->" 60) |
|
704 where |
|
705 "f o-> g = (\<lambda>x. split g (f x))" |
|
706 |
|
707 notation (xsymbols) |
|
708 mbind (infixl "\<circ>\<rightarrow>" 60) |
|
709 |
|
710 notation (HTML output) |
|
711 mbind (infixl "\<circ>\<rightarrow>" 60) |
|
712 |
|
713 lemma mbind_apply: "(f \<circ>\<rightarrow> g) x = split g (f x)" |
|
714 by (simp add: mbind_def) |
|
715 |
|
716 lemma Pair_mbind: "Pair x \<circ>\<rightarrow> f = f x" |
|
717 by (simp add: expand_fun_eq mbind_apply) |
|
718 |
|
719 lemma mbind_Pair: "x \<circ>\<rightarrow> Pair = x" |
|
720 by (simp add: expand_fun_eq mbind_apply) |
|
721 |
|
722 lemma mbind_mbind: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)" |
|
723 by (simp add: expand_fun_eq split_twice mbind_def) |
|
724 |
|
725 lemma mbind_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)" |
|
726 by (simp add: expand_fun_eq mbind_apply fcomp_def split_def) |
|
727 |
|
728 lemma fcomp_mbind: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)" |
|
729 by (simp add: expand_fun_eq mbind_apply fcomp_apply) |
|
730 |
|
731 |
|
732 text {* |
|
733 @{term prod_fun} --- action of the product functor upon |
606 functions. |
734 functions. |
607 *} |
735 *} |
|
736 |
|
737 definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where |
|
738 [code func del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))" |
608 |
739 |
609 lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)" |
740 lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)" |
610 by (simp add: prod_fun_def) |
741 by (simp add: prod_fun_def) |
611 |
742 |
612 lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)" |
743 lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)" |
613 apply (rule ext) |
744 by (rule ext) auto |
614 apply (tactic {* pair_tac "x" 1 *}, simp) |
|
615 done |
|
616 |
745 |
617 lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)" |
746 lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)" |
618 apply (rule ext) |
747 by (rule ext) auto |
619 apply (tactic {* pair_tac "z" 1 *}, simp) |
|
620 done |
|
621 |
748 |
622 lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r" |
749 lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r" |
623 apply (rule image_eqI) |
750 apply (rule image_eqI) |
624 apply (rule prod_fun [symmetric], assumption) |
751 apply (rule prod_fun [symmetric], assumption) |
625 done |
752 done |
633 apply (rule cases) |
760 apply (rule cases) |
634 apply (blast intro: prod_fun) |
761 apply (blast intro: prod_fun) |
635 apply blast |
762 apply blast |
636 done |
763 done |
637 |
764 |
638 |
|
639 definition |
765 definition |
640 upd_fst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" |
766 apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" |
641 where |
767 where |
642 [code func del]: "upd_fst f = prod_fun f id" |
768 [code func del]: "apfst f = prod_fun f id" |
643 |
769 |
644 definition |
770 definition |
645 upd_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" |
771 apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" |
646 where |
772 where |
647 [code func del]: "upd_snd f = prod_fun id f" |
773 [code func del]: "apsnd f = prod_fun id f" |
648 |
774 |
649 lemma upd_fst_conv [simp, code]: |
775 lemma apfst_conv [simp, code]: |
650 "upd_fst f (x, y) = (f x, y)" |
776 "apfst f (x, y) = (f x, y)" |
651 by (simp add: upd_fst_def) |
777 by (simp add: apfst_def) |
652 |
778 |
653 lemma upd_snd_conv [simp, code]: |
779 lemma upd_snd_conv [simp, code]: |
654 "upd_snd f (x, y) = (x, f y)" |
780 "apsnd f (x, y) = (x, f y)" |
655 by (simp add: upd_snd_def) |
781 by (simp add: apsnd_def) |
656 |
782 |
657 text {* |
783 |
658 \bigskip Disjoint union of a family of sets -- Sigma. |
784 text {* |
659 *} |
785 Disjoint union of a family of sets -- Sigma. |
|
786 *} |
|
787 |
|
788 definition Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where |
|
789 Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}" |
|
790 |
|
791 abbreviation |
|
792 Times :: "['a set, 'b set] => ('a * 'b) set" |
|
793 (infixr "<*>" 80) where |
|
794 "A <*> B == Sigma A (%_. B)" |
|
795 |
|
796 notation (xsymbols) |
|
797 Times (infixr "\<times>" 80) |
|
798 |
|
799 notation (HTML output) |
|
800 Times (infixr "\<times>" 80) |
|
801 |
|
802 syntax |
|
803 "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10) |
|
804 |
|
805 translations |
|
806 "SIGMA x:A. B" == "Product_Type.Sigma A (%x. B)" |
660 |
807 |
661 lemma SigmaI [intro!]: "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B" |
808 lemma SigmaI [intro!]: "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B" |
662 by (unfold Sigma_def) blast |
809 by (unfold Sigma_def) blast |
663 |
810 |
664 lemma SigmaE [elim!]: |
811 lemma SigmaE [elim!]: |
775 |
918 |
776 lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)" |
919 lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)" |
777 by blast |
920 by blast |
778 |
921 |
779 |
922 |
780 lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A" |
923 subsubsection {* Code generator setup *} |
781 apply (rule_tac x = "(a, b)" in image_eqI) |
|
782 apply auto |
|
783 done |
|
784 |
|
785 |
|
786 text {* |
|
787 Setup of internal @{text split_rule}. |
|
788 *} |
|
789 |
|
790 definition |
|
791 internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" |
|
792 where |
|
793 "internal_split == split" |
|
794 |
|
795 lemma internal_split_conv: "internal_split c (a, b) = c a b" |
|
796 by (simp only: internal_split_def split_conv) |
|
797 |
|
798 hide const internal_split |
|
799 |
|
800 use "Tools/split_rule.ML" |
|
801 setup SplitRule.setup |
|
802 |
|
803 |
|
804 |
|
805 lemmas prod_caseI = prod.cases [THEN iffD2, standard] |
|
806 |
|
807 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" |
|
808 by auto |
|
809 |
|
810 lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x" |
|
811 by (auto simp: split_tupled_all) |
|
812 |
|
813 lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" |
|
814 by (induct p) auto |
|
815 |
|
816 lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" |
|
817 by (induct p) auto |
|
818 |
|
819 lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))" |
|
820 by (simp add: expand_fun_eq) |
|
821 |
|
822 declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!] |
|
823 declare prod_caseE' [elim!] prod_caseE [elim!] |
|
824 |
|
825 lemma prod_case_split: |
|
826 "prod_case = split" |
|
827 by (auto simp add: expand_fun_eq) |
|
828 |
|
829 lemma prod_case_beta: |
|
830 "prod_case f p = f (fst p) (snd p)" |
|
831 unfolding prod_case_split split_beta .. |
|
832 |
|
833 |
|
834 subsection {* Further cases/induct rules for tuples *} |
|
835 |
|
836 lemma prod_cases3 [cases type]: |
|
837 obtains (fields) a b c where "y = (a, b, c)" |
|
838 by (cases y, case_tac b) blast |
|
839 |
|
840 lemma prod_induct3 [case_names fields, induct type]: |
|
841 "(!!a b c. P (a, b, c)) ==> P x" |
|
842 by (cases x) blast |
|
843 |
|
844 lemma prod_cases4 [cases type]: |
|
845 obtains (fields) a b c d where "y = (a, b, c, d)" |
|
846 by (cases y, case_tac c) blast |
|
847 |
|
848 lemma prod_induct4 [case_names fields, induct type]: |
|
849 "(!!a b c d. P (a, b, c, d)) ==> P x" |
|
850 by (cases x) blast |
|
851 |
|
852 lemma prod_cases5 [cases type]: |
|
853 obtains (fields) a b c d e where "y = (a, b, c, d, e)" |
|
854 by (cases y, case_tac d) blast |
|
855 |
|
856 lemma prod_induct5 [case_names fields, induct type]: |
|
857 "(!!a b c d e. P (a, b, c, d, e)) ==> P x" |
|
858 by (cases x) blast |
|
859 |
|
860 lemma prod_cases6 [cases type]: |
|
861 obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)" |
|
862 by (cases y, case_tac e) blast |
|
863 |
|
864 lemma prod_induct6 [case_names fields, induct type]: |
|
865 "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" |
|
866 by (cases x) blast |
|
867 |
|
868 lemma prod_cases7 [cases type]: |
|
869 obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)" |
|
870 by (cases y, case_tac f) blast |
|
871 |
|
872 lemma prod_induct7 [case_names fields, induct type]: |
|
873 "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" |
|
874 by (cases x) blast |
|
875 |
|
876 |
|
877 subsection {* Further lemmas *} |
|
878 |
|
879 lemma |
|
880 split_Pair: "split Pair x = x" |
|
881 unfolding split_def by auto |
|
882 |
|
883 lemma |
|
884 split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)" |
|
885 by (cases x, simp) |
|
886 |
|
887 |
|
888 subsection {* Code generator setup *} |
|
889 |
|
890 instance unit :: eq .. |
|
891 |
|
892 lemma [code func]: |
|
893 "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+ |
|
894 |
|
895 code_type unit |
|
896 (SML "unit") |
|
897 (OCaml "unit") |
|
898 (Haskell "()") |
|
899 |
|
900 code_instance unit :: eq |
|
901 (Haskell -) |
|
902 |
|
903 code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool" |
|
904 (Haskell infixl 4 "==") |
|
905 |
|
906 code_const Unity |
|
907 (SML "()") |
|
908 (OCaml "()") |
|
909 (Haskell "()") |
|
910 |
|
911 code_reserved SML |
|
912 unit |
|
913 |
|
914 code_reserved OCaml |
|
915 unit |
|
916 |
924 |
917 instance * :: (eq, eq) eq .. |
925 instance * :: (eq, eq) eq .. |
918 |
926 |
919 lemma [code func]: |
927 lemma [code func]: |
920 "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto |
928 "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto |
1042 ML {* |
1050 ML {* |
1043 val Collect_split = thm "Collect_split"; |
1051 val Collect_split = thm "Collect_split"; |
1044 val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1"; |
1052 val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1"; |
1045 val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2"; |
1053 val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2"; |
1046 val PairE = thm "PairE"; |
1054 val PairE = thm "PairE"; |
1047 val PairE_lemma = thm "PairE_lemma"; |
|
1048 val Pair_Rep_inject = thm "Pair_Rep_inject"; |
1055 val Pair_Rep_inject = thm "Pair_Rep_inject"; |
1049 val Pair_def = thm "Pair_def"; |
1056 val Pair_def = thm "Pair_def"; |
1050 val Pair_eq = thm "Pair_eq"; |
1057 val Pair_eq = thm "Pair_eq"; |
1051 val Pair_fst_snd_eq = thm "Pair_fst_snd_eq"; |
1058 val Pair_fst_snd_eq = thm "Pair_fst_snd_eq"; |
1052 val Pair_inject = thm "Pair_inject"; |
|
1053 val ProdI = thm "ProdI"; |
1059 val ProdI = thm "ProdI"; |
1054 val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq"; |
1060 val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq"; |
1055 val SigmaD1 = thm "SigmaD1"; |
1061 val SigmaD1 = thm "SigmaD1"; |
1056 val SigmaD2 = thm "SigmaD2"; |
1062 val SigmaD2 = thm "SigmaD2"; |
1057 val SigmaE = thm "SigmaE"; |
1063 val SigmaE = thm "SigmaE"; |