author | huffman |
Sun, 25 Mar 2012 20:15:39 +0200 | |
changeset 47108 | 2a1953f0d20d |
parent 39272 | 0b61951d2682 |
child 47125 | a3a64240cd98 |
permissions | -rw-r--r-- |
24999 | 1 |
(* Title: HOL/Library/Code_Integer.thy |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Pretty integer literals for code generation *} |
|
6 |
||
7 |
theory Code_Integer |
|
37968 | 8 |
imports Main Code_Natural |
24999 | 9 |
begin |
10 |
||
11 |
text {* |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
12 |
Representation-ignorant code equations for conversions. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
13 |
*} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
14 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
15 |
lemma nat_code [code]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
16 |
"nat k = (if k \<le> 0 then 0 else |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
17 |
let |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
18 |
(l, j) = divmod_int k 2; |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
19 |
l' = 2 * nat l |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
20 |
in if j = 0 then l' else Suc l')" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
21 |
proof - |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
22 |
have "2 = nat 2" by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
23 |
show ?thesis |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
24 |
apply (auto simp add: Let_def divmod_int_mod_div not_le |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
25 |
nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
26 |
apply (unfold `2 = nat 2`) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
27 |
apply (subst nat_mod_distrib [symmetric]) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
28 |
apply simp_all |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
29 |
done |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
30 |
qed |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
31 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
32 |
lemma (in ring_1) of_int_code: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
33 |
"of_int k = (if k = 0 then 0 |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
34 |
else if k < 0 then - of_int (- k) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
35 |
else let |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
36 |
(l, j) = divmod_int k 2; |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
37 |
l' = 2 * of_int l |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
38 |
in if j = 0 then l' else l' + 1)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
39 |
proof - |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
40 |
from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
41 |
show ?thesis |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
42 |
by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
43 |
of_int_add [symmetric]) (simp add: * mult_commute) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
44 |
qed |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
45 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
46 |
declare of_int_code [code] |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
47 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
48 |
text {* |
24999 | 49 |
HOL numeral expressions are mapped to integer literals |
50 |
in target languages, using predefined target language |
|
51 |
operations for abstract integer operations. |
|
52 |
*} |
|
53 |
||
54 |
code_type int |
|
55 |
(SML "IntInf.int") |
|
56 |
(OCaml "Big'_int.big'_int") |
|
57 |
(Haskell "Integer") |
|
34899 | 58 |
(Scala "BigInt") |
38053 | 59 |
(Eval "int") |
24999 | 60 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38773
diff
changeset
|
61 |
code_instance int :: equal |
24999 | 62 |
(Haskell -) |
63 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
64 |
code_const "0::int" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
65 |
(SML "0") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
66 |
(OCaml "Big'_int.zero'_big'_int") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
67 |
(Haskell "0") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
68 |
(Scala "BigInt(0)") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
69 |
|
24999 | 70 |
setup {* |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
71 |
fold (Numeral.add_code @{const_name Int.Pos} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
72 |
false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
24999 | 73 |
*} |
74 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
75 |
setup {* |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
76 |
fold (Numeral.add_code @{const_name Int.Neg} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
77 |
true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
78 |
*} |
24999 | 79 |
|
80 |
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
81 |
(SML "IntInf.+ ((_), (_))") |
|
82 |
(OCaml "Big'_int.add'_big'_int") |
|
83 |
(Haskell infixl 6 "+") |
|
34899 | 84 |
(Scala infixl 7 "+") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
85 |
(Eval infixl 8 "+") |
24999 | 86 |
|
87 |
code_const "uminus \<Colon> int \<Rightarrow> int" |
|
88 |
(SML "IntInf.~") |
|
89 |
(OCaml "Big'_int.minus'_big'_int") |
|
90 |
(Haskell "negate") |
|
34899 | 91 |
(Scala "!(- _)") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
92 |
(Eval "~/ _") |
24999 | 93 |
|
94 |
code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
95 |
(SML "IntInf.- ((_), (_))") |
|
96 |
(OCaml "Big'_int.sub'_big'_int") |
|
97 |
(Haskell infixl 6 "-") |
|
34899 | 98 |
(Scala infixl 7 "-") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
99 |
(Eval infixl 8 "-") |
24999 | 100 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
101 |
code_const Int.dup |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
102 |
(SML "IntInf.*/ (2,/ (_))") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
103 |
(OCaml "Big'_int.mult'_big'_int/ 2") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
104 |
(Haskell "!(2 * _)") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
105 |
(Scala "!(2 * _)") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
106 |
(Eval "!(2 * _)") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
107 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
108 |
code_const Int.sub |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
109 |
(SML "!(raise/ Fail/ \"sub\")") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
110 |
(OCaml "failwith/ \"sub\"") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
111 |
(Haskell "error/ \"sub\"") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
112 |
(Scala "!error(\"sub\")") |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
113 |
|
24999 | 114 |
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
115 |
(SML "IntInf.* ((_), (_))") |
|
116 |
(OCaml "Big'_int.mult'_big'_int") |
|
117 |
(Haskell infixl 7 "*") |
|
34899 | 118 |
(Scala infixl 8 "*") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
119 |
(Eval infixl 9 "*") |
24999 | 120 |
|
29936 | 121 |
code_const pdivmod |
34899 | 122 |
(SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
123 |
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") |
|
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34899
diff
changeset
|
124 |
(Haskell "divMod/ (abs _)/ (abs _)") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
125 |
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
126 |
(Eval "Integer.div'_mod/ (abs _)/ (abs _)") |
29936 | 127 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38773
diff
changeset
|
128 |
code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
24999 | 129 |
(SML "!((_ : IntInf.int) = _)") |
130 |
(OCaml "Big'_int.eq'_big'_int") |
|
39272 | 131 |
(Haskell infix 4 "==") |
34899 | 132 |
(Scala infixl 5 "==") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
133 |
(Eval infixl 6 "=") |
24999 | 134 |
|
135 |
code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
136 |
(SML "IntInf.<= ((_), (_))") |
|
137 |
(OCaml "Big'_int.le'_big'_int") |
|
138 |
(Haskell infix 4 "<=") |
|
34899 | 139 |
(Scala infixl 4 "<=") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
140 |
(Eval infixl 6 "<=") |
24999 | 141 |
|
142 |
code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
143 |
(SML "IntInf.< ((_), (_))") |
|
144 |
(OCaml "Big'_int.lt'_big'_int") |
|
145 |
(Haskell infix 4 "<") |
|
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
146 |
(Scala infixl 4 "<") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
147 |
(Eval infixl 6 "<") |
24999 | 148 |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
149 |
code_const Code_Numeral.int_of |
31192 | 150 |
(SML "IntInf.fromInt") |
31377 | 151 |
(OCaml "_") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
152 |
(Haskell "toInteger") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
153 |
(Scala "!_.as'_BigInt") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
154 |
(Eval "_") |
24999 | 155 |
|
32657 | 156 |
code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term" |
31192 | 157 |
(Eval "HOLogic.mk'_number/ HOLogic.intT") |
28228 | 158 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
39272
diff
changeset
|
159 |
end |