author | nipkow |
Mon, 14 Jan 2019 16:10:56 +0100 | |
changeset 69655 | 2b56cbb02e8a |
parent 69593 | 3dda49e08b9d |
child 69946 | 494934c30f38 |
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_Nat.thy |
51113
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
51095
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen |
50023
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 natural 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_Nat |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51114
diff
changeset
|
8 |
imports Code_Abstract_Nat |
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 |
|
69593 | 11 |
subsection \<open>Implementation for \<^typ>\<open>nat\<close>\<close> |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
12 |
|
55736
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54796
diff
changeset
|
13 |
context |
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54796
diff
changeset
|
14 |
includes natural.lifting integer.lifting |
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54796
diff
changeset
|
15 |
begin |
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54796
diff
changeset
|
16 |
|
51114 | 17 |
lift_definition Nat :: "integer \<Rightarrow> nat" |
18 |
is nat |
|
19 |
. |
|
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
20 |
|
51095
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
21 |
lemma [code_post]: |
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
22 |
"Nat 0 = 0" |
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
23 |
"Nat 1 = 1" |
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
24 |
"Nat (numeral k) = numeral k" |
51114 | 25 |
by (transfer, simp)+ |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
26 |
|
51095
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
27 |
lemma [code_abbrev]: |
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
28 |
"integer_of_nat = of_nat" |
51114 | 29 |
by transfer rule |
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_unfold]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
32 |
"Int.nat (int_of_integer k) = nat_of_integer k" |
51114 | 33 |
by transfer rule |
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 abstype]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
36 |
"Code_Target_Nat.Nat (integer_of_nat n) = n" |
51114 | 37 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
38 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
39 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
40 |
"integer_of_nat (nat_of_integer k) = max 0 k" |
51114 | 41 |
by transfer auto |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
42 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
43 |
lemma [code_abbrev]: |
51095
7ae79f2e3cc7
explicit conversion integer_of_nat already in Code_Numeral_Types;
haftmann
parents:
50023
diff
changeset
|
44 |
"nat_of_integer (numeral k) = nat_of_num k" |
51114 | 45 |
by transfer (simp add: nat_of_num_numeral) |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
46 |
|
64997
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
47 |
context |
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
48 |
begin |
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
49 |
|
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
50 |
qualified definition natural :: "num \<Rightarrow> nat" |
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
51 |
where [simp]: "natural = nat_of_num" |
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
52 |
|
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
53 |
lemma [code_computation_unfold]: |
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
54 |
"numeral = natural" |
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
55 |
"nat_of_num = natural" |
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
56 |
by (simp_all add: nat_of_num_numeral) |
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
57 |
|
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
58 |
end |
067a6cca39f0
dedicated computation preprocessing rules for nat, int implemented by target language literals
haftmann
parents:
64242
diff
changeset
|
59 |
|
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
60 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
61 |
"integer_of_nat (nat_of_num n) = integer_of_num n" |
66190 | 62 |
by (simp add: nat_of_num_numeral integer_of_nat_numeral) |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
63 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
64 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
65 |
"integer_of_nat 0 = 0" |
51114 | 66 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
67 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
68 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
69 |
"integer_of_nat 1 = 1" |
51114 | 70 |
by transfer simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
71 |
|
51113
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
51095
diff
changeset
|
72 |
lemma [code]: |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
51095
diff
changeset
|
73 |
"Suc n = n + 1" |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
51095
diff
changeset
|
74 |
by simp |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
51095
diff
changeset
|
75 |
|
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
76 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
77 |
"integer_of_nat (m + n) = of_nat m + of_nat n" |
51114 | 78 |
by transfer simp |
50023
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 abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
81 |
"integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)" |
51114 | 82 |
by transfer simp |
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 abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
85 |
"integer_of_nat (m * n) = of_nat m * of_nat n" |
51114 | 86 |
by transfer (simp add: of_nat_mult) |
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 abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
89 |
"integer_of_nat (m div n) = of_nat m div of_nat n" |
51114 | 90 |
by transfer (simp add: zdiv_int) |
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 [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
93 |
"integer_of_nat (m mod n) = of_nat m mod of_nat n" |
51114 | 94 |
by transfer (simp add: zmod_int) |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
95 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
96 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
97 |
"Divides.divmod_nat m n = (m div n, m mod n)" |
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66190
diff
changeset
|
98 |
by (fact divmod_nat_def) |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
99 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
100 |
lemma [code]: |
61275
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
60500
diff
changeset
|
101 |
"divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)" |
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
60500
diff
changeset
|
102 |
by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv) |
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
60500
diff
changeset
|
103 |
(transfer, simp_all only: nat_div_distrib nat_mod_distrib |
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
60500
diff
changeset
|
104 |
zero_le_numeral nat_numeral) |
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
60500
diff
changeset
|
105 |
|
053ec04ea866
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
haftmann
parents:
60500
diff
changeset
|
106 |
lemma [code]: |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
107 |
"HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)" |
51114 | 108 |
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
|
109 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
110 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
111 |
"m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
112 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
113 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
114 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
115 |
"m < n \<longleftrightarrow> (of_nat m :: integer) < of_nat n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
116 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
117 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
118 |
lemma num_of_nat_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
119 |
"num_of_nat = num_of_integer \<circ> of_nat" |
51114 | 120 |
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
|
121 |
|
55736
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54796
diff
changeset
|
122 |
end |
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54796
diff
changeset
|
123 |
|
54796 | 124 |
lemma (in semiring_1) of_nat_code_if: |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
125 |
"of_nat n = (if n = 0 then 0 |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
126 |
else let |
61433
a4c0de1df3d8
qualify some names stemming from internal bootstrap constructions
haftmann
parents:
61275
diff
changeset
|
127 |
(m, q) = Divides.divmod_nat n 2; |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
128 |
m' = 2 * of_nat m |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
129 |
in if q = 0 then m' else m' + 1)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
130 |
proof - |
64242
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
61585
diff
changeset
|
131 |
from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
132 |
show ?thesis |
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66190
diff
changeset
|
133 |
by (simp add: Let_def divmod_nat_def of_nat_add [symmetric]) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55736
diff
changeset
|
134 |
(simp add: * mult.commute of_nat_mult add.commute) |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
135 |
qed |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
136 |
|
54796 | 137 |
declare of_nat_code_if [code] |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
138 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
139 |
definition int_of_nat :: "nat \<Rightarrow> int" where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
140 |
[code_abbrev]: "int_of_nat = of_nat" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
141 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
142 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
143 |
"int_of_nat n = int_of_integer (of_nat n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
144 |
by (simp add: int_of_nat_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
145 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
146 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
147 |
"integer_of_nat (nat k) = max 0 (integer_of_int k)" |
55736
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54796
diff
changeset
|
148 |
including integer.lifting by transfer auto |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
149 |
|
68028 | 150 |
definition char_of_nat :: "nat \<Rightarrow> char" |
151 |
where [code_abbrev]: "char_of_nat = char_of" |
|
152 |
||
153 |
definition nat_of_char :: "char \<Rightarrow> nat" |
|
154 |
where [code_abbrev]: "nat_of_char = of_char" |
|
155 |
||
156 |
lemma [code]: |
|
157 |
"char_of_nat = char_of_integer \<circ> integer_of_nat" |
|
158 |
including integer.lifting unfolding char_of_integer_def char_of_nat_def |
|
159 |
by transfer (simp add: fun_eq_iff) |
|
160 |
||
161 |
lemma [code abstract]: |
|
162 |
"integer_of_nat (nat_of_char c) = integer_of_char c" |
|
163 |
by (cases c) (simp add: nat_of_char_def integer_of_char_def integer_of_nat_eq_of_nat) |
|
164 |
||
53027
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
165 |
lemma term_of_nat_code [code]: |
69593 | 166 |
\<comment> \<open>Use \<^term>\<open>Code_Numeral.nat_of_integer\<close> in term reconstruction |
167 |
instead of \<^term>\<open>Code_Target_Nat.Nat\<close> such that reconstructed |
|
60500 | 168 |
terms can be fed back to the code generator\<close> |
53027
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
169 |
"term_of_class.term_of n = |
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
170 |
Code_Evaluation.App |
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
171 |
(Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'') |
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
172 |
(typerep.Typerep (STR ''fun'') |
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
173 |
[typerep.Typerep (STR ''Code_Numeral.integer'') [], |
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
174 |
typerep.Typerep (STR ''Nat.nat'') []])) |
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
175 |
(term_of_class.term_of (integer_of_nat n))" |
54796 | 176 |
by (simp add: term_of_anything) |
53027
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
177 |
|
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
178 |
lemma nat_of_integer_code_post [code_post]: |
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
179 |
"nat_of_integer 0 = 0" |
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
180 |
"nat_of_integer 1 = 1" |
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
181 |
"nat_of_integer (numeral k) = numeral k" |
55736
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
54796
diff
changeset
|
182 |
including integer.lifting by (transfer, simp)+ |
53027
1774d569b604
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
Andreas Lochbihler
parents:
52435
diff
changeset
|
183 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
184 |
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
|
185 |
code_module Code_Target_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
|
186 |
(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
|
187 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
188 |
end |