34 |
34 |
35 translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)" |
35 translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)" |
36 |
36 |
37 typed_print_translation {* |
37 typed_print_translation {* |
38 let |
38 let |
39 fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_,[T,_]))] = |
39 fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] = |
40 Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T; |
40 Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T; |
41 in [(@{const_syntax card}, card_univ_tr')] |
41 in [(@{const_syntax card}, card_univ_tr')] |
42 end |
42 end |
43 *} |
43 *} |
44 |
44 |
45 lemma card_unit [simp]: "CARD(unit) = 1" |
45 lemma card_unit [simp]: "CARD(unit) = 1" |
387 "_NumeralType1" == (type) "num1" |
387 "_NumeralType1" == (type) "num1" |
388 "_NumeralType0" == (type) "num0" |
388 "_NumeralType0" == (type) "num0" |
389 |
389 |
390 parse_translation {* |
390 parse_translation {* |
391 let |
391 let |
392 |
392 (* FIXME @{type_syntax} *) |
393 val num1_const = Syntax.const "Numeral_Type.num1"; |
393 val num1_const = Syntax.const "Numeral_Type.num1"; |
394 val num0_const = Syntax.const "Numeral_Type.num0"; |
394 val num0_const = Syntax.const "Numeral_Type.num0"; |
395 val B0_const = Syntax.const "Numeral_Type.bit0"; |
395 val B0_const = Syntax.const "Numeral_Type.bit0"; |
396 val B1_const = Syntax.const "Numeral_Type.bit1"; |
396 val B1_const = Syntax.const "Numeral_Type.bit1"; |
397 |
397 |
409 |
409 |
410 fun numeral_tr (*"_NumeralType"*) [Const (str, _)] = |
410 fun numeral_tr (*"_NumeralType"*) [Const (str, _)] = |
411 mk_bintype (the (Int.fromString str)) |
411 mk_bintype (the (Int.fromString str)) |
412 | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts); |
412 | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts); |
413 |
413 |
414 in [("_NumeralType", numeral_tr)] end; |
414 in [(@{syntax_const "_NumeralType"}, numeral_tr)] end; |
415 *} |
415 *} |
416 |
416 |
417 print_translation {* |
417 print_translation {* |
418 let |
418 let |
419 fun int_of [] = 0 |
419 fun int_of [] = 0 |
420 | int_of (b :: bs) = b + 2 * int_of bs; |
420 | int_of (b :: bs) = b + 2 * int_of bs; |
421 |
421 |
|
422 (* FIXME @{type_syntax} *) |
422 fun bin_of (Const ("num0", _)) = [] |
423 fun bin_of (Const ("num0", _)) = [] |
423 | bin_of (Const ("num1", _)) = [1] |
424 | bin_of (Const ("num1", _)) = [1] |
424 | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs |
425 | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs |
425 | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs |
426 | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs |
426 | bin_of t = raise TERM("bin_of", [t]); |
427 | bin_of t = raise TERM("bin_of", [t]); |
433 in |
434 in |
434 Syntax.const "_NumeralType" $ Syntax.free num |
435 Syntax.const "_NumeralType" $ Syntax.free num |
435 end |
436 end |
436 | bit_tr' b _ = raise Match; |
437 | bit_tr' b _ = raise Match; |
437 |
438 |
|
439 (* FIXME @{type_syntax} *) |
438 in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end; |
440 in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end; |
439 *} |
441 *} |
440 |
442 |
441 subsection {* Examples *} |
443 subsection {* Examples *} |
442 |
444 |