(* Title: HOL/Tools/Presburger/cooper_data.ML
ID: $Id$
Author: Amine Chaieb, TU Muenchen
*)
signature COOPER_DATA =
sig
type entry
val get: Proof.context -> entry
val del: term list -> attribute
val add: term list -> attribute
val setup: theory -> theory
end;
structure Cooper_Data : COOPER_DATA =
struct
type entry = simpset* (term list);
val start_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"}
addcongs [if_weak_cong, @{thm "let_weak_cong"}];
val allowed_consts =
[@{term "op + :: int => _"}, @{term "op + :: nat => _"},
@{term "op - :: int => _"}, @{term "op - :: nat => _"},
@{term "op * :: int => _"}, @{term "op * :: nat => _"},
@{term "op div :: int => _"}, @{term "op div :: nat => _"},
@{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
@{term "Numeral.Bit"},
@{term "op &"}, @{term "op |"}, @{term "op -->"},
@{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
@{term "op < :: int => _"}, @{term "op < :: nat => _"},
@{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
@{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"},
@{term "abs :: int => _"}, @{term "abs :: nat => _"},
@{term "max :: int => _"}, @{term "max :: nat => _"},
@{term "min :: int => _"}, @{term "min :: nat => _"},
@{term "HOL.uminus :: int => _"}, @{term "HOL.uminus :: nat => _"},
@{term "Not"}, @{term "Suc"},
@{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
@{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
@{term "nat"}, @{term "int"},
@{term "Numeral.bit.B0"},@{term "Numeral.bit.B1"},
@{term "Numeral.Bit"}, @{term "Numeral.Pls"}, @{term "Numeral.Min"},
@{term "Numeral.number_of :: int => int"}, @{term "Numeral.number_of :: int => nat"},
@{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
@{term "True"}, @{term "False"}];
structure Data = GenericDataFun
(
val name = "Cooper-Data";
type T = simpset * (term list)
val empty = (start_ss, allowed_consts);
fun extend (ss,ts) = (MetaSimplifier.inherit_context empty_ss ss, ts);
fun merge _ ((ss1,ts1), (ss2,ts2)) = (merge_ss (ss1,ss2),
Library.merge (op aconv) (ts1,ts2)));
val get = Data.get o Context.Proof;
fun add ts = Thm.declaration_attribute (fn th => fn context =>
context |> Data.map (fn (ss,ts') =>
(ss addsimps [th], Library.merge (op aconv) (ts',ts) )))
fun del ts = Thm.declaration_attribute (fn th => fn context =>
context |> Data.map (fn (ss,ts') =>
(ss delsimps [th], Library.subtract (op aconv) ts' ts )))
(* concrete syntax *)
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
val constsN = "consts";
val any_keyword = keyword constsN
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
val terms = thms >> map (term_of o Drule.dest_term);
fun optional scan = Scan.optional scan [];
fun att_syntax src = src |> Attrib.syntax
((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
optional (keyword constsN |-- terms) >> add);
(* theory setup *)
val setup =
Attrib.add_attributes [("presburger", att_syntax, "Cooper data")];
end;