author | wenzelm |
Tue, 11 Jul 2006 12:16:54 +0200 | |
changeset 20071 | 8f3e1ddb50e6 |
parent 19889 | 2202a5648897 |
child 20105 | 454f4be984b7 |
permissions | -rw-r--r-- |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/EfficientNat.thy |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
3 |
Author: Stefan Berghofer, TU Muenchen |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
4 |
*) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
5 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
6 |
header {* Implementation of natural numbers by integers *} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
7 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
8 |
theory EfficientNat |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
9 |
imports Main |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
10 |
begin |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
11 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
12 |
text {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
13 |
When generating code for functions on natural numbers, the canonical |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
14 |
representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
15 |
computations involving large numbers. The efficiency of the generated |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
16 |
code can be improved drastically by implementing natural numbers by |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
17 |
integers. To do this, just include this theory. |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
18 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
19 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
20 |
subsection {* Basic functions *} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
21 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
22 |
text {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
23 |
The implementation of @{term "0::nat"} and @{term "Suc"} using the |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
24 |
ML integers is straightforward. Since natural numbers are implemented |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
25 |
using integers, the coercion function @{term "int"} of type |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
26 |
@{typ "nat \<Rightarrow> int"} is simply implemented by the identity function. |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
27 |
For the @{term "nat"} function for converting an integer to a natural |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
28 |
number, we give a specific implementation using an ML function that |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
29 |
returns its input value, provided that it is non-negative, and otherwise |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
30 |
returns @{text "0"}. |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
31 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
32 |
|
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
33 |
types_code |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
34 |
nat ("int") |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
35 |
attach (term_of) {* |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
36 |
fun term_of_nat 0 = Const ("0", HOLogic.natT) |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
37 |
| term_of_nat 1 = Const ("1", HOLogic.natT) |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
38 |
| term_of_nat i = HOLogic.number_of_const HOLogic.natT $ |
19481
a6205c6203ea
renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum
paulson
parents:
19137
diff
changeset
|
39 |
HOLogic.mk_binum (IntInf.fromInt i); |
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
40 |
*} |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
41 |
attach (test) {* |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
42 |
fun gen_nat i = random_range 0 i; |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
43 |
*} |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
44 |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
45 |
consts_code |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
46 |
0 :: nat ("0") |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
47 |
Suc ("(_ + 1)") |
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
48 |
nat ("\<module>nat") |
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
49 |
attach {* |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
50 |
fun nat i = if i < 0 then 0 else i; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
51 |
*} |
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16295
diff
changeset
|
52 |
int ("(_)") |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
53 |
|
19889 | 54 |
code_typapp nat |
55 |
ml (target_atom "IntInf.int") |
|
56 |
haskell (target_atom "Integer") |
|
57 |
||
58 |
definition |
|
59 |
"nat_of_int (k::int) = (if k < 0 then - k else k)" |
|
18851 | 60 |
|
19889 | 61 |
lemma |
62 |
"nat_of_int = abs" |
|
63 |
by (simp add: expand_fun_eq nat_of_int_def zabs_def) |
|
64 |
||
65 |
code_generate (ml, haskell) "abs :: int \<Rightarrow> int" |
|
66 |
||
67 |
code_constapp |
|
19791 | 68 |
nat |
69 |
ml ("{* abs :: int \<Rightarrow> int *}") |
|
70 |
haskell ("{* abs :: int \<Rightarrow> int *}") |
|
71 |
int |
|
72 |
ml ("_") |
|
73 |
haskell ("_") |
|
18702 | 74 |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
75 |
text {* |
19889 | 76 |
Eliminate @{const "0::nat"} and @{const "Suc"} |
77 |
by unfolding in place. |
|
78 |
*} |
|
79 |
||
80 |
lemma [code unfolt]: |
|
81 |
"0 = nat 0" |
|
82 |
"Suc = (op +) 1" |
|
83 |
by (simp_all add: expand_fun_eq) |
|
84 |
||
85 |
declare elim_one_nat [code nofold] |
|
86 |
||
87 |
text {* |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
88 |
Case analysis on natural numbers is rephrased using a conditional |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
89 |
expression: |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
90 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
91 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
92 |
lemma [code unfold]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
93 |
apply (rule eq_reflection ext)+ |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
94 |
apply (case_tac n) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
95 |
apply simp_all |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
96 |
done |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
97 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
98 |
text {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
99 |
Most standard arithmetic functions on natural numbers are implemented |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
100 |
using their counterparts on the integers: |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
101 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
102 |
|
19791 | 103 |
lemma [code]: "m + n = nat (int m + int n)" |
104 |
by arith |
|
105 |
lemma [code]: "m - n = nat (int m - int n)" |
|
106 |
by arith |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
107 |
lemma [code]: "m * n = nat (int m * int n)" |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
108 |
by (simp add: zmult_int) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
109 |
lemma [code]: "m div n = nat (int m div int n)" |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
110 |
by (simp add: zdiv_int [symmetric]) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
111 |
lemma [code]: "m mod n = nat (int m mod int n)" |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
112 |
by (simp add: zmod_int [symmetric]) |
16295 | 113 |
lemma [code]: "(m < n) = (int m < int n)" |
114 |
by simp |
|
19791 | 115 |
lemma [code fun]: |
116 |
"(m = n) = (int m = int n)" |
|
19889 | 117 |
by simp |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
118 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
119 |
subsection {* Preprocessors *} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
120 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
121 |
text {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
122 |
In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
123 |
a constructor term. Therefore, all occurrences of this term in a position |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
124 |
where a pattern is expected (i.e.\ on the left-hand side of a recursion |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
125 |
equation or in the arguments of an inductive relation in an introduction |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
126 |
rule) must be eliminated. |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
127 |
This can be accomplished by applying the following transformation rules: |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
128 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
129 |
|
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
130 |
theorem Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow> |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
131 |
f n = (if n = 0 then g else h (n - 1))" |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
132 |
by (case_tac n) simp_all |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
133 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
134 |
theorem Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n" |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
135 |
by (case_tac n) simp_all |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
136 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
137 |
text {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
138 |
The rules above are built into a preprocessor that is plugged into |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
139 |
the code generator. Since the preprocessor for introduction rules |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
140 |
does not know anything about modes, some of the modes that worked |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
141 |
for the canonical representation of natural numbers may no longer work. |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
142 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
143 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
144 |
(*<*) |
19791 | 145 |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
146 |
ML {* |
19791 | 147 |
local |
148 |
val Suc_if_eq = thm "Suc_if_eq"; |
|
149 |
val Suc_clause = thm "Suc_clause"; |
|
150 |
fun contains_suc t = member (op =) (term_consts t) "Suc"; |
|
151 |
in |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
152 |
|
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
153 |
fun remove_suc thy thms = |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
154 |
let |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
155 |
val Suc_if_eq' = Thm.transfer thy Suc_if_eq; |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19889
diff
changeset
|
156 |
val vname = Name.variant (map fst |
16861 | 157 |
(fold (add_term_varnames o Thm.full_prop_of) thms [])) "x"; |
158 |
val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT)); |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
159 |
fun lhs_of th = snd (Thm.dest_comb |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
160 |
(fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))))); |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
161 |
fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th)))); |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
162 |
fun find_vars ct = (case term_of ct of |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
163 |
(Const ("Suc", _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
164 |
| _ $ _ => |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
165 |
let val (ct1, ct2) = Thm.dest_comb ct |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
166 |
in |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
167 |
map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @ |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
168 |
map (apfst (Thm.capply ct1)) (find_vars ct2) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
169 |
end |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
170 |
| _ => []); |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
171 |
val eqs = List.concat (map |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
172 |
(fn th => map (pair th) (find_vars (lhs_of th))) thms); |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
173 |
fun mk_thms (th, (ct, cv')) = |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
174 |
let |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
175 |
val th' = |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
176 |
Thm.implies_elim |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
177 |
(Drule.fconv_rule (Thm.beta_conversion true) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
178 |
(Drule.instantiate' |
15531 | 179 |
[SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct), |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
180 |
SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv'] |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
181 |
Suc_if_eq')) (Thm.forall_intr cv' th) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
182 |
in |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
183 |
case List.mapPartial (fn th'' => |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
184 |
SOME (th'', standard (Drule.freeze_all th'' RS th')) |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
185 |
handle THM _ => NONE) thms of |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
186 |
[] => NONE |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
187 |
| thps => |
19791 | 188 |
let val (ths1, ths2) = split_list thps |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
189 |
in SOME (gen_rems eq_thm (thms, th :: ths1) @ ths2) end |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
190 |
end |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
191 |
in |
19791 | 192 |
case get_first mk_thms eqs of |
16900
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
193 |
NONE => thms |
e294033d1c0f
Rewrote function remove_suc, since it failed on some equations
berghofe
parents:
16861
diff
changeset
|
194 |
| SOME x => remove_suc thy x |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
195 |
end; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
196 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
197 |
fun eqn_suc_preproc thy ths = |
19791 | 198 |
let |
199 |
val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
200 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
201 |
if forall (can dest) ths andalso |
19791 | 202 |
exists (contains_suc o dest) ths |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
203 |
then remove_suc thy ths else ths |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
204 |
end; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
205 |
|
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
206 |
fun remove_suc_clause thy thms = |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
207 |
let |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
208 |
val Suc_clause' = Thm.transfer thy Suc_clause; |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19889
diff
changeset
|
209 |
val vname = Name.variant (map fst |
16861 | 210 |
(fold (add_term_varnames o Thm.full_prop_of) thms [])) "x"; |
15531 | 211 |
fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v) |
212 |
| find_var (t $ u) = (case find_var t of NONE => find_var u | x => x) |
|
213 |
| find_var _ = NONE; |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
214 |
fun find_thm th = |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
215 |
let val th' = ObjectLogic.atomize_thm th |
15570 | 216 |
in Option.map (pair (th, th')) (find_var (prop_of th')) end |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
217 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
218 |
case get_first find_thm thms of |
15531 | 219 |
NONE => thms |
220 |
| SOME ((th, th'), (Sucv, v)) => |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
221 |
let |
16861 | 222 |
val cert = cterm_of (Thm.theory_of_thm th); |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
223 |
val th'' = ObjectLogic.rulify (Thm.implies_elim |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
224 |
(Drule.fconv_rule (Thm.beta_conversion true) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
225 |
(Drule.instantiate' [] |
15531 | 226 |
[SOME (cert (lambda v (Abs ("x", HOLogic.natT, |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
227 |
abstract_over (Sucv, |
19828 | 228 |
HOLogic.dest_Trueprop (prop_of th')))))), |
15531 | 229 |
SOME (cert v)] Suc_clause')) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
230 |
(Thm.forall_intr (cert v) th')) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
231 |
in |
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
232 |
remove_suc_clause thy (map (fn th''' => |
19617 | 233 |
if (op = o pairself prop_of) (th''', th) then th'' else th''') thms) |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
234 |
end |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
235 |
end; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
236 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
237 |
fun clause_suc_preproc thy ths = |
19791 | 238 |
let |
19828 | 239 |
val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
240 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
241 |
if forall (can (dest o concl_of)) ths andalso |
19791 | 242 |
exists (fn th => member (op =) (foldr add_term_consts |
243 |
[] (List.mapPartial (try dest) (concl_of th :: prems_of th))) "Suc") ths |
|
15396
0a36ccb79481
Preprocessors now transfer theorems to current theory in order to
berghofe
parents:
15323
diff
changeset
|
244 |
then remove_suc_clause thy ths else ths |
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
245 |
end; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
246 |
|
19791 | 247 |
end; (*local*) |
248 |
||
249 |
fun lift_obj_eq f thy = |
|
250 |
map (fn thm => thm RS meta_eq_to_obj_eq) |
|
251 |
#> f thy |
|
252 |
#> map (fn thm => thm RS HOL.eq_reflection) |
|
253 |
*} |
|
254 |
||
255 |
setup {* |
|
19603 | 256 |
Codegen.add_preprocessor eqn_suc_preproc |
257 |
#> Codegen.add_preprocessor clause_suc_preproc |
|
19791 | 258 |
#> CodegenTheorems.add_preproc (lift_obj_eq eqn_suc_preproc) |
259 |
#> CodegenTheorems.add_preproc (lift_obj_eq clause_suc_preproc) |
|
15323
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
260 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
261 |
(*>*) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
262 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
263 |
end |