|
24584
|
1 |
(* Title: HOL/Tools/Qelim/cooper_data.ML
|
|
23466
|
2 |
ID: $Id$
|
|
|
3 |
Author: Amine Chaieb, TU Muenchen
|
|
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
signature COOPER_DATA =
|
|
|
7 |
sig
|
|
|
8 |
type entry
|
|
|
9 |
val get: Proof.context -> entry
|
|
|
10 |
val del: term list -> attribute
|
|
|
11 |
val add: term list -> attribute
|
|
|
12 |
val setup: theory -> theory
|
|
|
13 |
end;
|
|
|
14 |
|
|
|
15 |
structure CooperData : COOPER_DATA =
|
|
|
16 |
struct
|
|
|
17 |
|
|
|
18 |
type entry = simpset * (term list);
|
|
|
19 |
val start_ss = HOL_ss (* addsimps @{thms "Groebner_Basis.comp_arith"}
|
|
|
20 |
addcongs [if_weak_cong, @{thm "let_weak_cong"}];*)
|
|
|
21 |
val allowed_consts =
|
|
|
22 |
[@{term "op + :: int => _"}, @{term "op + :: nat => _"},
|
|
|
23 |
@{term "op - :: int => _"}, @{term "op - :: nat => _"},
|
|
|
24 |
@{term "op * :: int => _"}, @{term "op * :: nat => _"},
|
|
|
25 |
@{term "op div :: int => _"}, @{term "op div :: nat => _"},
|
|
|
26 |
@{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
|
|
|
27 |
@{term "Numeral.Bit"},
|
|
|
28 |
@{term "op &"}, @{term "op |"}, @{term "op -->"},
|
|
|
29 |
@{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
|
|
|
30 |
@{term "op < :: int => _"}, @{term "op < :: nat => _"},
|
|
|
31 |
@{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
|
|
|
32 |
@{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"},
|
|
23879
|
33 |
@{term "abs :: int => _"}, (*@ {term "abs :: nat => _"}, *)
|
|
23466
|
34 |
@{term "max :: int => _"}, @{term "max :: nat => _"},
|
|
|
35 |
@{term "min :: int => _"}, @{term "min :: nat => _"},
|
|
|
36 |
@{term "HOL.uminus :: int => _"}, @{term "HOL.uminus :: nat => _"},
|
|
|
37 |
@{term "Not"}, @{term "Suc"},
|
|
|
38 |
@{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
|
|
|
39 |
@{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
|
|
|
40 |
@{term "nat"}, @{term "int"},
|
|
|
41 |
@{term "Numeral.bit.B0"},@{term "Numeral.bit.B1"},
|
|
|
42 |
@{term "Numeral.Bit"}, @{term "Numeral.Pls"}, @{term "Numeral.Min"},
|
|
|
43 |
@{term "Numeral.number_of :: int => int"}, @{term "Numeral.number_of :: int => nat"},
|
|
|
44 |
@{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
|
|
|
45 |
@{term "True"}, @{term "False"}];
|
|
|
46 |
|
|
|
47 |
structure Data = GenericDataFun
|
|
|
48 |
(
|
|
|
49 |
type T = simpset * (term list);
|
|
|
50 |
val empty = (start_ss, allowed_consts);
|
|
23474
|
51 |
val extend = I;
|
|
23466
|
52 |
fun merge _ ((ss1, ts1), (ss2, ts2)) =
|
|
|
53 |
(merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
|
|
|
54 |
);
|
|
|
55 |
|
|
|
56 |
val get = Data.get o Context.Proof;
|
|
|
57 |
|
|
|
58 |
fun add ts = Thm.declaration_attribute (fn th => fn context =>
|
|
|
59 |
context |> Data.map (fn (ss,ts') =>
|
|
|
60 |
(ss addsimps [th], merge (op aconv) (ts',ts) )))
|
|
|
61 |
|
|
|
62 |
fun del ts = Thm.declaration_attribute (fn th => fn context =>
|
|
|
63 |
context |> Data.map (fn (ss,ts') =>
|
|
|
64 |
(ss delsimps [th], subtract (op aconv) ts' ts )))
|
|
|
65 |
|
|
|
66 |
|
|
|
67 |
(* concrete syntax *)
|
|
|
68 |
|
|
|
69 |
local
|
|
|
70 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
|
|
|
71 |
|
|
|
72 |
val constsN = "consts";
|
|
|
73 |
val any_keyword = keyword constsN
|
|
|
74 |
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
|
|
|
75 |
val terms = thms >> map (term_of o Drule.dest_term);
|
|
|
76 |
|
|
|
77 |
fun optional scan = Scan.optional scan [];
|
|
|
78 |
|
|
|
79 |
in
|
|
|
80 |
fun att_syntax src = src |> Attrib.syntax
|
|
|
81 |
((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
|
|
|
82 |
optional (keyword constsN |-- terms) >> add)
|
|
|
83 |
end;
|
|
|
84 |
|
|
|
85 |
|
|
|
86 |
(* theory setup *)
|
|
|
87 |
|
|
|
88 |
val setup =
|
|
|
89 |
Attrib.add_attributes [("presburger", att_syntax, "Cooper data")];
|
|
|
90 |
|
|
|
91 |
end;
|