author | wenzelm |
Fri, 04 Sep 2015 19:22:13 +0200 | |
changeset 61115 | 3a4400985780 |
parent 61076 | bdc1e2f0a86a |
child 61433 | a4c0de1df3d8 |
permissions | -rw-r--r-- |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
47108
diff
changeset
|
1 |
(* Title: HOL/Library/Code_Binary_Nat.thy |
51113
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
50023
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen |
47108 | 3 |
*) |
4 |
||
60500 | 5 |
section \<open>Implementation of natural numbers as binary numerals\<close> |
47108 | 6 |
|
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
47108
diff
changeset
|
7 |
theory Code_Binary_Nat |
51113
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
50023
diff
changeset
|
8 |
imports Code_Abstract_Nat |
47108 | 9 |
begin |
10 |
||
60500 | 11 |
text \<open> |
47108 | 12 |
When generating code for functions on natural numbers, the |
13 |
canonical representation using @{term "0::nat"} and |
|
14 |
@{term Suc} is unsuitable for computations involving large |
|
15 |
numbers. This theory refines the representation of |
|
16 |
natural numbers for code generation to use binary |
|
17 |
numerals, which do not grow linear in size but logarithmic. |
|
60500 | 18 |
\<close> |
47108 | 19 |
|
60500 | 20 |
subsection \<open>Representation\<close> |
47108 | 21 |
|
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
47108
diff
changeset
|
22 |
code_datatype "0::nat" nat_of_num |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
47108
diff
changeset
|
23 |
|
47108 | 24 |
lemma [code]: |
25 |
"num_of_nat 0 = Num.One" |
|
26 |
"num_of_nat (nat_of_num k) = k" |
|
27 |
by (simp_all add: nat_of_num_inverse) |
|
28 |
||
29 |
lemma [code]: |
|
61076 | 30 |
"(1::nat) = Numeral1" |
47108 | 31 |
by simp |
32 |
||
61076 | 33 |
lemma [code_abbrev]: "Numeral1 = (1::nat)" |
47108 | 34 |
by simp |
35 |
||
36 |
lemma [code]: |
|
37 |
"Suc n = n + 1" |
|
38 |
by simp |
|
39 |
||
40 |
||
60500 | 41 |
subsection \<open>Basic arithmetic\<close> |
47108 | 42 |
|
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
61076
diff
changeset
|
43 |
context |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
61076
diff
changeset
|
44 |
begin |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
61076
diff
changeset
|
45 |
|
47108 | 46 |
lemma [code, code del]: |
47 |
"(plus :: nat \<Rightarrow> _) = plus" .. |
|
48 |
||
49 |
lemma plus_nat_code [code]: |
|
50 |
"nat_of_num k + nat_of_num l = nat_of_num (k + l)" |
|
51 |
"m + 0 = (m::nat)" |
|
52 |
"0 + n = (n::nat)" |
|
53 |
by (simp_all add: nat_of_num_numeral) |
|
54 |
||
60500 | 55 |
text \<open>Bounded subtraction needs some auxiliary\<close> |
47108 | 56 |
|
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
61076
diff
changeset
|
57 |
qualified definition dup :: "nat \<Rightarrow> nat" where |
47108 | 58 |
"dup n = n + n" |
59 |
||
60 |
lemma dup_code [code]: |
|
61 |
"dup 0 = 0" |
|
62 |
"dup (nat_of_num k) = nat_of_num (Num.Bit0 k)" |
|
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
47108
diff
changeset
|
63 |
by (simp_all add: dup_def numeral_Bit0) |
47108 | 64 |
|
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
61076
diff
changeset
|
65 |
qualified definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where |
47108 | 66 |
"sub k l = (if k \<ge> l then Some (numeral k - numeral l) else None)" |
67 |
||
68 |
lemma sub_code [code]: |
|
69 |
"sub Num.One Num.One = Some 0" |
|
70 |
"sub (Num.Bit0 m) Num.One = Some (nat_of_num (Num.BitM m))" |
|
71 |
"sub (Num.Bit1 m) Num.One = Some (nat_of_num (Num.Bit0 m))" |
|
72 |
"sub Num.One (Num.Bit0 n) = None" |
|
73 |
"sub Num.One (Num.Bit1 n) = None" |
|
55466 | 74 |
"sub (Num.Bit0 m) (Num.Bit0 n) = map_option dup (sub m n)" |
75 |
"sub (Num.Bit1 m) (Num.Bit1 n) = map_option dup (sub m n)" |
|
76 |
"sub (Num.Bit1 m) (Num.Bit0 n) = map_option (\<lambda>q. dup q + 1) (sub m n)" |
|
47108 | 77 |
"sub (Num.Bit0 m) (Num.Bit1 n) = (case sub m n of None \<Rightarrow> None |
78 |
| Some q \<Rightarrow> if q = 0 then None else Some (dup q - 1))" |
|
79 |
apply (auto simp add: nat_of_num_numeral |
|
80 |
Num.dbl_def Num.dbl_inc_def Num.dbl_dec_def |
|
81 |
Let_def le_imp_diff_is_add BitM_plus_one sub_def dup_def) |
|
82 |
apply (simp_all add: sub_non_positive) |
|
83 |
apply (simp_all add: sub_non_negative [symmetric, where ?'a = int]) |
|
84 |
done |
|
85 |
||
86 |
lemma [code, code del]: |
|
87 |
"(minus :: nat \<Rightarrow> _) = minus" .. |
|
88 |
||
89 |
lemma minus_nat_code [code]: |
|
90 |
"nat_of_num k - nat_of_num l = (case sub k l of None \<Rightarrow> 0 | Some j \<Rightarrow> j)" |
|
91 |
"m - 0 = (m::nat)" |
|
92 |
"0 - n = (0::nat)" |
|
93 |
by (simp_all add: nat_of_num_numeral sub_non_positive sub_def) |
|
94 |
||
95 |
lemma [code, code del]: |
|
96 |
"(times :: nat \<Rightarrow> _) = times" .. |
|
97 |
||
98 |
lemma times_nat_code [code]: |
|
99 |
"nat_of_num k * nat_of_num l = nat_of_num (k * l)" |
|
100 |
"m * 0 = (0::nat)" |
|
101 |
"0 * n = (0::nat)" |
|
102 |
by (simp_all add: nat_of_num_numeral) |
|
103 |
||
104 |
lemma [code, code del]: |
|
105 |
"(HOL.equal :: nat \<Rightarrow> _) = HOL.equal" .. |
|
106 |
||
107 |
lemma equal_nat_code [code]: |
|
108 |
"HOL.equal 0 (0::nat) \<longleftrightarrow> True" |
|
109 |
"HOL.equal 0 (nat_of_num l) \<longleftrightarrow> False" |
|
110 |
"HOL.equal (nat_of_num k) 0 \<longleftrightarrow> False" |
|
111 |
"HOL.equal (nat_of_num k) (nat_of_num l) \<longleftrightarrow> HOL.equal k l" |
|
112 |
by (simp_all add: nat_of_num_numeral equal) |
|
113 |
||
114 |
lemma equal_nat_refl [code nbe]: |
|
115 |
"HOL.equal (n::nat) n \<longleftrightarrow> True" |
|
116 |
by (rule equal_refl) |
|
117 |
||
118 |
lemma [code, code del]: |
|
119 |
"(less_eq :: nat \<Rightarrow> _) = less_eq" .. |
|
120 |
||
121 |
lemma less_eq_nat_code [code]: |
|
122 |
"0 \<le> (n::nat) \<longleftrightarrow> True" |
|
123 |
"nat_of_num k \<le> 0 \<longleftrightarrow> False" |
|
124 |
"nat_of_num k \<le> nat_of_num l \<longleftrightarrow> k \<le> l" |
|
125 |
by (simp_all add: nat_of_num_numeral) |
|
126 |
||
127 |
lemma [code, code del]: |
|
128 |
"(less :: nat \<Rightarrow> _) = less" .. |
|
129 |
||
130 |
lemma less_nat_code [code]: |
|
131 |
"(m::nat) < 0 \<longleftrightarrow> False" |
|
132 |
"0 < nat_of_num l \<longleftrightarrow> True" |
|
133 |
"nat_of_num k < nat_of_num l \<longleftrightarrow> k < l" |
|
134 |
by (simp_all add: nat_of_num_numeral) |
|
135 |
||
53069
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset
|
136 |
lemma [code, code del]: |
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset
|
137 |
"divmod_nat = divmod_nat" .. |
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset
|
138 |
|
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset
|
139 |
lemma divmod_nat_code [code]: |
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset
|
140 |
"divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l" |
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset
|
141 |
"divmod_nat m 0 = (0, m)" |
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset
|
142 |
"divmod_nat 0 n = (0, 0)" |
60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60500
diff
changeset
|
143 |
by (simp_all add: prod_eq_iff nat_of_num_numeral) |
53069
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset
|
144 |
|
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
61076
diff
changeset
|
145 |
end |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
61076
diff
changeset
|
146 |
|
47108 | 147 |
|
60500 | 148 |
subsection \<open>Conversions\<close> |
47108 | 149 |
|
150 |
lemma [code, code del]: |
|
151 |
"of_nat = of_nat" .. |
|
152 |
||
153 |
lemma of_nat_code [code]: |
|
154 |
"of_nat 0 = 0" |
|
155 |
"of_nat (nat_of_num k) = numeral k" |
|
156 |
by (simp_all add: nat_of_num_numeral) |
|
157 |
||
158 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
159 |
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
|
160 |
code_module Code_Binary_Nat \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
161 |
(SML) Arith and (OCaml) Arith and (Haskell) Arith |
47108 | 162 |
|
163 |
end |