author | wenzelm |
Sat, 26 Jan 2008 17:08:38 +0100 | |
changeset 25979 | 3297781f8141 |
parent 25254 | 0216ca99a599 |
child 30528 | 7173bf123335 |
permissions | -rw-r--r-- |
23252 | 1 |
(* Title: HOL/Tools/Groebner_Basis/normalizer_data.ML |
2 |
ID: $Id$ |
|
3 |
Author: Amine Chaieb, TU Muenchen |
|
4 |
||
5 |
Ring normalization data. |
|
6 |
*) |
|
7 |
||
8 |
signature NORMALIZER_DATA = |
|
9 |
sig |
|
10 |
type entry |
|
23581 | 11 |
val get: Proof.context -> simpset * (thm * entry) list |
23252 | 12 |
val match: Proof.context -> cterm -> entry option |
13 |
val del: attribute |
|
25254
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
14 |
val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list, ideal: thm list} |
23252 | 15 |
-> attribute |
16 |
val funs: thm -> {is_const: morphism -> cterm -> bool, |
|
17 |
dest_const: morphism -> cterm -> Rat.rat, |
|
18 |
mk_const: morphism -> ctyp -> Rat.rat -> cterm, |
|
24020 | 19 |
conv: morphism -> Proof.context -> cterm -> thm} -> declaration |
23252 | 20 |
val setup: theory -> theory |
21 |
end; |
|
22 |
||
23 |
structure NormalizerData: NORMALIZER_DATA = |
|
24 |
struct |
|
25 |
||
26 |
(* data *) |
|
27 |
||
28 |
type entry = |
|
29 |
{vars: cterm list, |
|
30 |
semiring: cterm list * thm list, |
|
31 |
ring: cterm list * thm list, |
|
25254
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
32 |
idom: thm list, |
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
33 |
ideal: thm list} * |
23252 | 34 |
{is_const: cterm -> bool, |
35 |
dest_const: cterm -> Rat.rat, |
|
36 |
mk_const: ctyp -> Rat.rat -> cterm, |
|
23330
01c09922ce59
Conversion for computation on constants now depends on the context
chaieb
parents:
23260
diff
changeset
|
37 |
conv: Proof.context -> cterm -> thm}; |
23252 | 38 |
|
39 |
val eq_key = Thm.eq_thm; |
|
40 |
fun eq_data arg = eq_fst eq_key arg; |
|
41 |
||
42 |
structure Data = GenericDataFun |
|
43 |
( |
|
23581 | 44 |
type T = simpset * (thm * entry) list; |
23335
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
45 |
val empty = (HOL_basic_ss, []); |
23252 | 46 |
val extend = I; |
23581 | 47 |
fun merge _ ((ss, e), (ss', e')) = |
48 |
(merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e')); |
|
23252 | 49 |
); |
50 |
||
51 |
val get = Data.get o Context.Proof; |
|
52 |
||
53 |
||
54 |
(* match data *) |
|
55 |
||
56 |
fun match ctxt tm = |
|
57 |
let |
|
58 |
fun match_inst |
|
25254
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
59 |
({vars, semiring = (sr_ops, sr_rules), |
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
60 |
ring = (r_ops, r_rules), idom, ideal}, |
23252 | 61 |
fns as {is_const, dest_const, mk_const, conv}) pat = |
62 |
let |
|
63 |
fun h instT = |
|
64 |
let |
|
65 |
val substT = Thm.instantiate (instT, []); |
|
66 |
val substT_cterm = Drule.cterm_rule substT; |
|
67 |
||
68 |
val vars' = map substT_cterm vars; |
|
69 |
val semiring' = (map substT_cterm sr_ops, map substT sr_rules); |
|
70 |
val ring' = (map substT_cterm r_ops, map substT r_rules); |
|
71 |
val idom' = map substT idom; |
|
25254
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
72 |
val ideal' = map substT ideal; |
23252 | 73 |
|
25254
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
74 |
val result = ({vars = vars', semiring = semiring', |
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
75 |
ring = ring', idom = idom', ideal = ideal'}, fns); |
23252 | 76 |
in SOME result end |
77 |
in (case try Thm.match (pat, tm) of |
|
78 |
NONE => NONE |
|
79 |
| SOME (instT, _) => h instT) |
|
80 |
end; |
|
81 |
||
82 |
fun match_struct (_, |
|
83 |
entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) = |
|
84 |
get_first (match_inst entry) (sr_ops @ r_ops); |
|
23335
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
85 |
in get_first match_struct (snd (get ctxt)) end; |
23252 | 86 |
|
87 |
||
88 |
(* logical content *) |
|
89 |
||
90 |
val semiringN = "semiring"; |
|
91 |
val ringN = "ring"; |
|
92 |
val idomN = "idom"; |
|
25254
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
93 |
val idealN = "ideal"; |
23252 | 94 |
|
95 |
fun undefined _ = raise Match; |
|
96 |
||
23335
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
97 |
fun del_data key = apsnd (remove eq_data (key, [])); |
23252 | 98 |
|
99 |
val del = Thm.declaration_attribute (Data.map o del_data); |
|
23335
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
100 |
val add_ss = Thm.declaration_attribute |
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
101 |
(fn th => Data.map (fn (ss,data) => (ss addsimps [th], data))); |
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
102 |
|
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
103 |
val del_ss = Thm.declaration_attribute |
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
104 |
(fn th => Data.map (fn (ss,data) => (ss delsimps [th], data))); |
23252 | 105 |
|
25254
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
106 |
fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom, ideal} = |
23252 | 107 |
Thm.declaration_attribute (fn key => fn context => context |> Data.map |
108 |
let |
|
109 |
val ctxt = Context.proof_of context; |
|
110 |
||
111 |
fun check kind name xs n = |
|
112 |
null xs orelse length xs = n orelse |
|
113 |
error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); |
|
114 |
val check_ops = check "operations"; |
|
115 |
val check_rules = check "rules"; |
|
116 |
||
117 |
val _ = |
|
118 |
check_ops semiringN sr_ops 5 andalso |
|
119 |
check_rules semiringN sr_rules 37 andalso |
|
120 |
check_ops ringN r_ops 2 andalso |
|
121 |
check_rules ringN r_rules 2 andalso |
|
122 |
check_rules idomN idom 2; |
|
123 |
||
124 |
val mk_meta = LocalDefs.meta_rewrite_rule ctxt; |
|
125 |
val sr_rules' = map mk_meta sr_rules; |
|
126 |
val r_rules' = map mk_meta r_rules; |
|
127 |
||
128 |
fun rule i = nth sr_rules' (i - 1); |
|
129 |
||
130 |
val (cx, cy) = Thm.dest_binop (hd sr_ops); |
|
131 |
val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; |
|
132 |
val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; |
|
133 |
val ((clx, crx), (cly, cry)) = |
|
134 |
rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; |
|
135 |
val ((ca, cb), (cc, cd)) = |
|
136 |
rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; |
|
137 |
val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; |
|
138 |
val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg; |
|
139 |
||
140 |
val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; |
|
141 |
val semiring = (sr_ops, sr_rules'); |
|
142 |
val ring = (r_ops, r_rules'); |
|
25254
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
143 |
val ideal' = map (symmetric o mk_meta) ideal |
23252 | 144 |
in |
145 |
del_data key #> |
|
25254
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
146 |
apsnd (cons (key, ({vars = vars, semiring = semiring, |
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
147 |
ring = ring, idom = idom, ideal = ideal'}, |
23335
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
148 |
{is_const = undefined, dest_const = undefined, mk_const = undefined, |
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
149 |
conv = undefined}))) |
23252 | 150 |
end); |
151 |
||
152 |
||
153 |
(* extra-logical functions *) |
|
154 |
||
23335
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
155 |
fun funs raw_key {is_const, dest_const, mk_const, conv} phi = |
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
156 |
(Data.map o apsnd) (fn data => |
23252 | 157 |
let |
158 |
val key = Morphism.thm phi raw_key; |
|
159 |
val _ = AList.defined eq_key data key orelse |
|
160 |
raise THM ("No data entry for structure key", 0, [key]); |
|
161 |
val fns = {is_const = is_const phi, dest_const = dest_const phi, |
|
162 |
mk_const = mk_const phi, conv = conv phi}; |
|
163 |
in AList.map_entry eq_key key (apsnd (K fns)) data end); |
|
164 |
||
165 |
||
166 |
(* concrete syntax *) |
|
167 |
||
168 |
local |
|
169 |
||
170 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
|
171 |
fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K (); |
|
172 |
fun keyword3 k1 k2 k3 = |
|
173 |
Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K (); |
|
174 |
||
175 |
val opsN = "ops"; |
|
176 |
val rulesN = "rules"; |
|
177 |
||
178 |
val normN = "norm"; |
|
179 |
val constN = "const"; |
|
180 |
val delN = "del"; |
|
181 |
||
182 |
val any_keyword = |
|
183 |
keyword2 semiringN opsN || keyword2 semiringN rulesN || |
|
184 |
keyword2 ringN opsN || keyword2 ringN rulesN || |
|
25254
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
185 |
keyword2 idomN rulesN || keyword2 idealN rulesN; |
23252 | 186 |
|
187 |
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
|
188 |
val terms = thms >> map Drule.dest_term; |
|
189 |
||
190 |
fun optional scan = Scan.optional scan []; |
|
191 |
||
192 |
in |
|
193 |
||
25979
3297781f8141
tuned attribute syntax -- no need for eta-expansion;
wenzelm
parents:
25254
diff
changeset
|
194 |
val att_syntax = Attrib.syntax |
23252 | 195 |
(Scan.lift (Args.$$$ delN >> K del) || |
196 |
((keyword2 semiringN opsN |-- terms) -- |
|
197 |
(keyword2 semiringN rulesN |-- thms)) -- |
|
198 |
(optional (keyword2 ringN opsN |-- terms) -- |
|
199 |
optional (keyword2 ringN rulesN |-- thms)) -- |
|
25254
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
200 |
optional (keyword2 idomN rulesN |-- thms) -- |
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
201 |
optional (keyword2 idealN rulesN |-- thms) |
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
202 |
>> (fn (((sr, r), id), idl) => |
0216ca99a599
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb
parents:
24020
diff
changeset
|
203 |
add {semiring = sr, ring = r, idom = id, ideal = idl})); |
23252 | 204 |
|
205 |
end; |
|
206 |
||
207 |
||
208 |
(* theory setup *) |
|
209 |
||
210 |
val setup = |
|
23335
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
211 |
Attrib.add_attributes |
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
212 |
[("normalizer", att_syntax, "semiring normalizer data"), |
42b827dfa86b
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
chaieb
parents:
23330
diff
changeset
|
213 |
("algebra", Attrib.add_del_args add_ss del_ss, "Pre-simplification for algebra")]; |
23252 | 214 |
|
215 |
end; |