author | berghofe |
Wed, 24 Nov 2004 10:30:19 +0100 | |
changeset 15324 | c27165172e30 |
parent 15323 | 6c10fe1c0e17 |
child 15396 | 0a36ccb79481 |
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 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
33 |
types_code nat ("int") |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
34 |
consts_code |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
35 |
0 :: nat ("0") |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
36 |
Suc ("(_ + 1)") |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
37 |
nat ("nat") |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
38 |
int ("(_)") |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
39 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
40 |
ML {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
41 |
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
|
42 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
43 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
44 |
text {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
45 |
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
|
46 |
expression: |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
47 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
48 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
49 |
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
|
50 |
apply (rule eq_reflection ext)+ |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
51 |
apply (case_tac n) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
52 |
apply simp_all |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
53 |
done |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
54 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
55 |
text {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
56 |
Most standard arithmetic functions on natural numbers are implemented |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
57 |
using their counterparts on the integers: |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
58 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
59 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
60 |
lemma [code]: "m - n = nat (int m - int n)" by arith |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
61 |
lemma [code]: "m + n = nat (int m + int n)" by arith |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
62 |
lemma [code]: "m * n = nat (int m * int n)" |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
63 |
by (simp add: zmult_int) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
64 |
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
|
65 |
by (simp add: zdiv_int [symmetric]) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
66 |
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
|
67 |
by (simp add: zmod_int [symmetric]) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
68 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
69 |
subsection {* Preprocessors *} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
70 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
71 |
text {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
72 |
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
|
73 |
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
|
74 |
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
|
75 |
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
|
76 |
rule) must be eliminated. |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
77 |
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
|
78 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
79 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
80 |
theorem Suc_if_eq: "f 0 = g \<Longrightarrow> (\<And>n. f (Suc n) = h n) \<Longrightarrow> |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
81 |
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
|
82 |
by (case_tac n) simp_all |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
83 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
84 |
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
|
85 |
by (case_tac n) simp_all |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
86 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
87 |
text {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
88 |
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
|
89 |
the code generator. Since the preprocessor for introduction rules |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
90 |
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
|
91 |
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
|
92 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
93 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
94 |
(*<*) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
95 |
ML {* |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
96 |
val Suc_if_eq = thm "Suc_if_eq"; |
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 |
fun remove_suc thms = |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
99 |
let |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
100 |
val ctzero = cterm_of (sign_of Main.thy) HOLogic.zero; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
101 |
val vname = variant (map fst |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
102 |
(foldl add_term_varnames ([], map prop_of thms))) "x"; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
103 |
val cv = cterm_of (sign_of Main.thy) (Var ((vname, 0), HOLogic.natT)); |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
104 |
fun lhs_of th = snd (Thm.dest_comb |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
105 |
(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
|
106 |
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
|
107 |
fun find_vars ct = (case term_of ct of |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
108 |
(Const ("Suc", _) $ Var _) => [((cv, ctzero), snd (Thm.dest_comb ct))] |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
109 |
| _ $ _ => |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
110 |
let val (ct1, ct2) = Thm.dest_comb ct |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
111 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
112 |
map (apfst (pairself (fn ct => Thm.capply ct ct2))) (find_vars ct1) @ |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
113 |
map (apfst (pairself (Thm.capply ct1))) (find_vars ct2) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
114 |
end |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
115 |
| _ => []); |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
116 |
val eqs1 = flat (map |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
117 |
(fn th => map (pair th) (find_vars (lhs_of th))) thms); |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
118 |
val eqs2 = map (fn x as (_, ((_, ctzero), _)) => (x, mapfilter (fn th => |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
119 |
Some (th, Thm.cterm_match (lhs_of th, ctzero)) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
120 |
handle Pattern.MATCH => None) thms)) eqs1; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
121 |
fun distinct_vars vs = forall is_Var vs andalso null (duplicates vs); |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
122 |
val eqs2' = map (apsnd (filter (fn (_, (_, s)) => |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
123 |
distinct_vars (map (term_of o snd) s)))) eqs2; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
124 |
fun mk_thms b ((th, ((ct, _), cv')), (th', s) :: _) = |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
125 |
let |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
126 |
val th'' = Thm.instantiate s th'; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
127 |
val th''' = |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
128 |
Thm.implies_elim (Thm.implies_elim |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
129 |
(Drule.fconv_rule Drule.beta_eta_conversion |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
130 |
(Drule.instantiate' |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
131 |
[Some (ctyp_of_term ct)] [Some (Thm.cabs cv ct), |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
132 |
Some (rhs_of th''), Some (Thm.cabs cv' (rhs_of th)), Some cv'] |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
133 |
Suc_if_eq)) th'') (Thm.forall_intr cv' th) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
134 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
135 |
mapfilter (fn thm => |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
136 |
if thm = th then Some th''' |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
137 |
else if b andalso thm = th' then None |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
138 |
else Some thm) thms |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
139 |
end |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
140 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
141 |
case Library.find_first (not o null o snd) eqs2' of |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
142 |
None => (case Library.find_first (not o null o snd) eqs2 of |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
143 |
None => thms |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
144 |
| Some x => remove_suc (mk_thms false x)) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
145 |
| Some x => remove_suc (mk_thms true x) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
146 |
end; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
147 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
148 |
fun eqn_suc_preproc thy ths = |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
149 |
let val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
150 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
151 |
if forall (can dest) ths andalso |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
152 |
exists (fn th => "Suc" mem term_consts (dest th)) ths |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
153 |
then remove_suc ths else ths |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
154 |
end; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
155 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
156 |
val Suc_clause = thm "Suc_clause"; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
157 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
158 |
fun remove_suc_clause thms = |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
159 |
let |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
160 |
val vname = variant (map fst |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
161 |
(foldl add_term_varnames ([], map prop_of thms))) "x"; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
162 |
fun find_var (t as Const ("Suc", _) $ (v as Var _)) = Some (t, v) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
163 |
| find_var (t $ u) = (case find_var t of None => find_var u | x => x) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
164 |
| find_var _ = None; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
165 |
fun find_thm th = |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
166 |
let val th' = ObjectLogic.atomize_thm th |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
167 |
in apsome (pair (th, th')) (find_var (prop_of th')) end |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
168 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
169 |
case get_first find_thm thms of |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
170 |
None => thms |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
171 |
| Some ((th, th'), (Sucv, v)) => |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
172 |
let |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
173 |
val cert = cterm_of (sign_of_thm th); |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
174 |
val th'' = ObjectLogic.rulify (Thm.implies_elim |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
175 |
(Drule.fconv_rule Drule.beta_eta_conversion |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
176 |
(Drule.instantiate' [] |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
177 |
[Some (cert (lambda v (Abs ("x", HOLogic.natT, |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
178 |
abstract_over (Sucv, |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
179 |
HOLogic.dest_Trueprop (prop_of th')))))), |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
180 |
Some (cert v)] Suc_clause)) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
181 |
(Thm.forall_intr (cert v) th')) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
182 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
183 |
remove_suc_clause (map (fn th''' => |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
184 |
if th''' = th then th'' else th''') thms) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
185 |
end |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
186 |
end; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
187 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
188 |
fun clause_suc_preproc thy ths = |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
189 |
let val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
190 |
in |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
191 |
if forall (can (dest o concl_of)) ths andalso |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
192 |
exists (fn th => "Suc" mem foldr add_term_consts |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
193 |
(mapfilter (try dest) (concl_of th :: prems_of th), [])) ths |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
194 |
then remove_suc_clause ths else ths |
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 |
val suc_preproc_setup = |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
198 |
[Codegen.add_preprocessor eqn_suc_preproc, |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
199 |
Codegen.add_preprocessor clause_suc_preproc]; |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
200 |
*} |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
201 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
202 |
setup suc_preproc_setup |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
203 |
(*>*) |
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
204 |
|
6c10fe1c0e17
Code generator plug-in for implementing natural numbers by integers.
berghofe
parents:
diff
changeset
|
205 |
end |