equal
deleted
inserted
replaced
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 code_datatype int_of_integer |
11 code_datatype int_of_integer |
12 |
12 |
13 lemma [code, code del]: |
13 declare [[code drop: integer_of_int]] |
14 "integer_of_int = integer_of_int" .. |
|
15 |
14 |
16 lemma [code]: |
15 lemma [code]: |
17 "integer_of_int (int_of_integer k) = k" |
16 "integer_of_int (int_of_integer k) = k" |
18 by transfer rule |
17 by transfer rule |
19 |
18 |
55 |
54 |
56 lemma [code]: |
55 lemma [code]: |
57 "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))" |
56 "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))" |
58 by transfer simp |
57 by transfer simp |
59 |
58 |
60 lemma [code, code del]: |
59 declare [[code drop: Int.sub]] |
61 "Int.sub = Int.sub" .. |
|
62 |
60 |
63 lemma [code]: |
61 lemma [code]: |
64 "k * l = int_of_integer (of_int k * of_int l)" |
62 "k * l = int_of_integer (of_int k * of_int l)" |
65 by simp |
63 by simp |
66 |
64 |