349 definition "enum_class.enum = [1 :: num1]" |
349 definition "enum_class.enum = [1 :: num1]" |
350 definition "enum_class.enum_all P = P (1 :: num1)" |
350 definition "enum_class.enum_all P = P (1 :: num1)" |
351 definition "enum_class.enum_ex P = P (1 :: num1)" |
351 definition "enum_class.enum_ex P = P (1 :: num1)" |
352 instance |
352 instance |
353 by intro_classes |
353 by intro_classes |
354 (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def, |
354 (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def, |
355 (metis (full_types) num1_eq_iff)+) |
355 (metis (full_types) num1_eq_iff)+) |
356 end |
356 end |
357 |
357 |
358 instantiation num0 and num1 :: card_UNIV begin |
358 instantiation num0 and num1 :: card_UNIV begin |
359 definition "finite_UNIV = Phantom(num0) False" |
359 definition "finite_UNIV = Phantom(num0) False" |
475 translations |
475 translations |
476 (type) "1" == (type) "num1" |
476 (type) "1" == (type) "num1" |
477 (type) "0" == (type) "num0" |
477 (type) "0" == (type) "num0" |
478 |
478 |
479 parse_translation {* |
479 parse_translation {* |
480 let |
480 let |
481 fun mk_bintype n = |
481 fun mk_bintype n = |
482 let |
482 let |
483 fun mk_bit 0 = Syntax.const @{type_syntax bit0} |
483 fun mk_bit 0 = Syntax.const @{type_syntax bit0} |
484 | mk_bit 1 = Syntax.const @{type_syntax bit1}; |
484 | mk_bit 1 = Syntax.const @{type_syntax bit1}; |
485 fun bin_of n = |
485 fun bin_of n = |
486 if n = 1 then Syntax.const @{type_syntax num1} |
486 if n = 1 then Syntax.const @{type_syntax num1} |
487 else if n = 0 then Syntax.const @{type_syntax num0} |
487 else if n = 0 then Syntax.const @{type_syntax num0} |
488 else if n = ~1 then raise TERM ("negative type numeral", []) |
488 else if n = ~1 then raise TERM ("negative type numeral", []) |
489 else |
489 else |
490 let val (q, r) = Integer.div_mod n 2; |
490 let val (q, r) = Integer.div_mod n 2; |
491 in mk_bit r $ bin_of q end; |
491 in mk_bit r $ bin_of q end; |
492 in bin_of n end; |
492 in bin_of n end; |
493 |
493 |
494 fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str)) |
494 fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str)) |
495 | numeral_tr ts = raise TERM ("numeral_tr", ts); |
495 | numeral_tr ts = raise TERM ("numeral_tr", ts); |
496 |
496 |
497 in [(@{syntax_const "_NumeralType"}, numeral_tr)] end; |
497 in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end; |
498 *} |
498 *} |
499 |
499 |
500 print_translation {* |
500 print_translation {* |
501 let |
501 let |
502 fun int_of [] = 0 |
502 fun int_of [] = 0 |
503 | int_of (b :: bs) = b + 2 * int_of bs; |
503 | int_of (b :: bs) = b + 2 * int_of bs; |
504 |
504 |
505 fun bin_of (Const (@{type_syntax num0}, _)) = [] |
505 fun bin_of (Const (@{type_syntax num0}, _)) = [] |
506 | bin_of (Const (@{type_syntax num1}, _)) = [1] |
506 | bin_of (Const (@{type_syntax num1}, _)) = [1] |
507 | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs |
507 | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs |
508 | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs |
508 | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs |
509 | bin_of t = raise TERM ("bin_of", [t]); |
509 | bin_of t = raise TERM ("bin_of", [t]); |
510 |
510 |
511 fun bit_tr' b [t] = |
511 fun bit_tr' b [t] = |
512 let |
512 let |
513 val rev_digs = b :: bin_of t handle TERM _ => raise Match |
513 val rev_digs = b :: bin_of t handle TERM _ => raise Match |
514 val i = int_of rev_digs; |
514 val i = int_of rev_digs; |
515 val num = string_of_int (abs i); |
515 val num = string_of_int (abs i); |
516 in |
516 in |
517 Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num |
517 Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num |
518 end |
518 end |
519 | bit_tr' b _ = raise Match; |
519 | bit_tr' b _ = raise Match; |
520 in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end; |
520 in |
|
521 [(@{type_syntax bit0}, K (bit_tr' 0)), |
|
522 (@{type_syntax bit1}, K (bit_tr' 1))] end; |
521 *} |
523 *} |
522 |
524 |
523 subsection {* Examples *} |
525 subsection {* Examples *} |
524 |
526 |
525 lemma "CARD(0) = 0" by simp |
527 lemma "CARD(0) = 0" by simp |