356 For datatypes, instances of @{class eq} are implicitly derived |
356 For datatypes, instances of @{class eq} are implicitly derived |
357 when possible. For other types, you may instantiate @{text eq} |
357 when possible. For other types, you may instantiate @{text eq} |
358 manually like any other type class. |
358 manually like any other type class. |
359 |
359 |
360 Though this @{text eq} class is designed to get rarely in |
360 Though this @{text eq} class is designed to get rarely in |
361 the way, a subtlety |
361 the way, in some cases the automatically derived code equations |
362 enters the stage when definitions of overloaded constants |
|
363 are dependent on operational equality. For example, let |
|
364 us define a lexicographic ordering on tuples |
|
365 (also see theory @{theory Product_ord}): |
|
366 *} |
|
367 |
|
368 instantiation %quote "*" :: (order, order) order |
|
369 begin |
|
370 |
|
371 definition %quote [code del]: |
|
372 "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y" |
|
373 |
|
374 definition %quote [code del]: |
|
375 "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" |
|
376 |
|
377 instance %quote proof |
|
378 qed (auto simp: less_eq_prod_def less_prod_def intro: order_less_trans) |
|
379 |
|
380 end %quote |
|
381 |
|
382 lemma %quote order_prod [code]: |
|
383 "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow> |
|
384 x1 < x2 \<or> x1 = x2 \<and> y1 < y2" |
|
385 "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow> |
|
386 x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2" |
|
387 by (simp_all add: less_prod_def less_eq_prod_def) |
|
388 |
|
389 text {* |
|
390 \noindent Then code generation will fail. Why? The definition |
|
391 of @{term "op \<le>"} depends on equality on both arguments, |
|
392 which are polymorphic and impose an additional @{class eq} |
|
393 class constraint, which the preprocessor does not propagate |
|
394 (for technical reasons). |
|
395 |
|
396 The solution is to add @{class eq} explicitly to the first sort arguments in the |
|
397 code theorems: |
|
398 *} |
|
399 |
|
400 lemma %quote order_prod_code [code]: |
|
401 "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow> |
|
402 x1 < x2 \<or> x1 = x2 \<and> y1 < y2" |
|
403 "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow> |
|
404 x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2" |
|
405 by (simp_all add: less_prod_def less_eq_prod_def) |
|
406 |
|
407 text {* |
|
408 \noindent Then code generation succeeds: |
|
409 *} |
|
410 |
|
411 text %quote {*@{code_stmts "op \<le> \<Colon> _ \<times> _ \<Rightarrow> _ \<times> _ \<Rightarrow> bool" (SML)}*} |
|
412 |
|
413 text {* |
|
414 In some cases, the automatically derived code equations |
|
415 for equality on a particular type may not be appropriate. |
362 for equality on a particular type may not be appropriate. |
416 As example, watch the following datatype representing |
363 As example, watch the following datatype representing |
417 monomorphic parametric types (where type constructors |
364 monomorphic parametric types (where type constructors |
418 are referred to by natural numbers): |
365 are referred to by natural numbers): |
419 *} |
366 *} |