equal
deleted
inserted
replaced
20 |
20 |
21 lemma [code]: |
21 lemma [code]: |
22 "char_of_nat = char_of_int o int" |
22 "char_of_nat = char_of_int o int" |
23 unfolding char_of_int_def by (simp add: expand_fun_eq) |
23 unfolding char_of_int_def by (simp add: expand_fun_eq) |
24 |
24 |
25 lemmas [code del] = char.recs char.cases char.size |
|
26 |
|
27 lemma [code, code_unfold]: |
|
28 "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))" |
|
29 by (cases c) (auto simp add: nibble_pair_of_nat_char) |
|
30 |
|
31 lemma [code, code_unfold]: |
|
32 "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))" |
|
33 by (cases c) (auto simp add: nibble_pair_of_nat_char) |
|
34 |
|
35 lemma [code]: |
|
36 "size (c\<Colon>char) = 0" |
|
37 by (cases c) auto |
|
38 |
|
39 code_const int_of_char and char_of_int |
25 code_const int_of_char and char_of_int |
40 (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)") |
26 (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)") |
41 (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)") |
27 (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)") |
42 (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)") |
28 (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | (0 <= k && k < 256) = toEnum k :: Char in chr . fromInteger)") |
|
29 (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))") |
43 |
30 |
44 end |
31 end |