author | haftmann |
Tue, 19 Nov 2013 10:05:53 +0100 | |
changeset 54489 | 03ff4d1e6784 |
parent 54227 | 63b441f49645 |
child 54796 | cdc6d8cbf770 |
permissions | -rw-r--r-- |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/Code_Target_Int.thy |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
3 |
*) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
4 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
5 |
header {* Implementation of integer numbers by target-language integers *} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
6 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
7 |
theory Code_Target_Int |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51114
diff
changeset
|
8 |
imports Main |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
9 |
begin |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
10 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
11 |
code_datatype int_of_integer |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
12 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
13 |
lemma [code, code del]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
14 |
"integer_of_int = integer_of_int" .. |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
15 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
16 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
17 |
"integer_of_int (int_of_integer k) = k" |
51114 | 18 |
by transfer rule |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
19 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
20 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
21 |
"Int.Pos = int_of_integer \<circ> integer_of_num" |
51114 | 22 |
by transfer (simp add: fun_eq_iff) |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
23 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
24 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
25 |
"Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num" |
51114 | 26 |
by transfer (simp add: fun_eq_iff) |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
27 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
28 |
lemma [code_abbrev]: |
51095
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
29 |
"int_of_integer (numeral k) = Int.Pos k" |
51114 | 30 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
31 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
32 |
lemma [code_abbrev]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54227
diff
changeset
|
33 |
"int_of_integer (- numeral k) = Int.Neg k" |
51114 | 34 |
by transfer simp |
51095
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
35 |
|
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
36 |
lemma [code, symmetric, code_post]: |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
37 |
"0 = int_of_integer 0" |
51114 | 38 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
39 |
|
51095
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
40 |
lemma [code, symmetric, code_post]: |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
41 |
"1 = int_of_integer 1" |
51114 | 42 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
43 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
44 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
45 |
"k + l = int_of_integer (of_int k + of_int l)" |
51114 | 46 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
47 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
48 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
49 |
"- k = int_of_integer (- of_int k)" |
51114 | 50 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
51 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
52 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
53 |
"k - l = int_of_integer (of_int k - of_int l)" |
51114 | 54 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
55 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
56 |
lemma [code]: |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51114
diff
changeset
|
57 |
"Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))" |
51114 | 58 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
59 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
60 |
lemma [code, code del]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
61 |
"Int.sub = Int.sub" .. |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
62 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
63 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
64 |
"k * l = int_of_integer (of_int k * of_int l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
65 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
66 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
67 |
lemma [code]: |
53069
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset
|
68 |
"Divides.divmod_abs k l = map_pair int_of_integer int_of_integer |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51114
diff
changeset
|
69 |
(Code_Numeral.divmod_abs (of_int k) (of_int l))" |
53069
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset
|
70 |
by (simp add: prod_eq_iff) |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
71 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
72 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
73 |
"k div l = int_of_integer (of_int k div of_int l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
74 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
75 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
76 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
77 |
"k mod l = int_of_integer (of_int k mod of_int l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
78 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
79 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
80 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
81 |
"HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)" |
51114 | 82 |
by transfer (simp add: equal) |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
83 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
84 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
85 |
"k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l" |
51114 | 86 |
by transfer rule |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
87 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
88 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
89 |
"k < l \<longleftrightarrow> (of_int k :: integer) < of_int l" |
51114 | 90 |
by transfer rule |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
91 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
92 |
lemma (in ring_1) of_int_code: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
93 |
"of_int k = (if k = 0 then 0 |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
94 |
else if k < 0 then - of_int (- k) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
95 |
else let |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
96 |
(l, j) = divmod_int k 2; |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
97 |
l' = 2 * of_int l |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
98 |
in if j = 0 then l' else l' + 1)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
99 |
proof - |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
100 |
from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
101 |
show ?thesis |
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
53069
diff
changeset
|
102 |
by (simp add: Let_def divmod_int_mod_div not_mod_2_eq_0_eq_1 |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
103 |
of_int_add [symmetric]) (simp add: * mult_commute) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
104 |
qed |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
105 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
106 |
declare of_int_code [code] |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
107 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
108 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
109 |
"nat = nat_of_integer \<circ> of_int" |
51114 | 110 |
by transfer (simp add: fun_eq_iff) |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
111 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
112 |
code_identifier |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
113 |
code_module Code_Target_Int \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
114 |
(SML) Arith and (OCaml) Arith and (Haskell) Arith |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
115 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
116 |
end |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
117 |