author | haftmann |
Sat, 08 Aug 2015 10:51:33 +0200 | |
changeset 60868 | dd18c33c001e |
parent 60500 | 903bb1495239 |
child 61275 | 053ec04ea866 |
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 |
|
60500 | 5 |
section \<open>Implementation of integer numbers by target-language integers\<close> |
50023
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 |
|
54891
2f4491f15fe6
examples how to avoid the "code, code del" antipattern
haftmann
parents:
54796
diff
changeset
|
13 |
declare [[code drop: integer_of_int]] |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
14 |
|
55736
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54891
diff
changeset
|
15 |
context |
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54891
diff
changeset
|
16 |
includes integer.lifting |
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54891
diff
changeset
|
17 |
begin |
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54891
diff
changeset
|
18 |
|
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
19 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
20 |
"integer_of_int (int_of_integer k) = k" |
51114 | 21 |
by transfer rule |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
22 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
23 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
24 |
"Int.Pos = int_of_integer \<circ> integer_of_num" |
51114 | 25 |
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
|
26 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
27 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
28 |
"Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num" |
51114 | 29 |
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
|
30 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
31 |
lemma [code_abbrev]: |
51095
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
32 |
"int_of_integer (numeral k) = Int.Pos k" |
51114 | 33 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
34 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
35 |
lemma [code_abbrev]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54227
diff
changeset
|
36 |
"int_of_integer (- numeral k) = Int.Neg k" |
51114 | 37 |
by transfer simp |
51095
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
38 |
|
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
39 |
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
|
40 |
"0 = int_of_integer 0" |
51114 | 41 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
42 |
|
51095
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
43 |
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
|
44 |
"1 = int_of_integer 1" |
51114 | 45 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
46 |
|
58099
7f232ae7de7c
convenient printing of (- 1 :: integer) after code evaluation
haftmann
parents:
57512
diff
changeset
|
47 |
lemma [code_post]: |
7f232ae7de7c
convenient printing of (- 1 :: integer) after code evaluation
haftmann
parents:
57512
diff
changeset
|
48 |
"int_of_integer (- 1) = - 1" |
7f232ae7de7c
convenient printing of (- 1 :: integer) after code evaluation
haftmann
parents:
57512
diff
changeset
|
49 |
by simp |
7f232ae7de7c
convenient printing of (- 1 :: integer) after code evaluation
haftmann
parents:
57512
diff
changeset
|
50 |
|
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
51 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
52 |
"k + l = int_of_integer (of_int k + of_int l)" |
51114 | 53 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
54 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
55 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
56 |
"- k = int_of_integer (- of_int k)" |
51114 | 57 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
58 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
59 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
60 |
"k - l = int_of_integer (of_int k - of_int l)" |
51114 | 61 |
by transfer simp |
50023
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]: |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51114
diff
changeset
|
64 |
"Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))" |
51114 | 65 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
66 |
|
54891
2f4491f15fe6
examples how to avoid the "code, code del" antipattern
haftmann
parents:
54796
diff
changeset
|
67 |
declare [[code drop: Int.sub]] |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
68 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
69 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
70 |
"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
|
71 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
72 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
73 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
74 |
"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
|
75 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
76 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
77 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
78 |
"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
|
79 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
80 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
81 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
82 |
"HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)" |
51114 | 83 |
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
|
84 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
85 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
86 |
"k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l" |
51114 | 87 |
by transfer rule |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
88 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
89 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
90 |
"k < l \<longleftrightarrow> (of_int k :: integer) < of_int l" |
51114 | 91 |
by transfer rule |
55736
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54891
diff
changeset
|
92 |
end |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
93 |
|
54796 | 94 |
lemma (in ring_1) of_int_code_if: |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
95 |
"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
|
96 |
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
|
97 |
else let |
60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60500
diff
changeset
|
98 |
l = 2 * of_int (k div 2); |
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60500
diff
changeset
|
99 |
j = k mod 2 |
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60500
diff
changeset
|
100 |
in if j = 0 then l else l + 1)" |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
101 |
proof - |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
102 |
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
|
103 |
show ?thesis |
60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60500
diff
changeset
|
104 |
by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute) |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
105 |
qed |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
106 |
|
54796 | 107 |
declare of_int_code_if [code] |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
108 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
109 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
110 |
"nat = nat_of_integer \<circ> of_int" |
55736
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54891
diff
changeset
|
111 |
including integer.lifting 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
|
112 |
|
52435
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_identifier |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
114 |
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
|
115 |
(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
|
116 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
117 |
end |