src/HOL/Tools/Presburger/cooper_data.ML
author chaieb
Thu, 14 Jun 2007 22:59:40 +0200
changeset 23391 a7c128816edc
parent 23336 21a7433c4bd3
child 23461 9a586e80ce15
permissions -rw-r--r--
no computation rules in the pre-simplifiaction set

(*  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 *)
local
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 [];

in
fun att_syntax src = src |> Attrib.syntax
 ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
  optional (keyword constsN |-- terms) >> add)
end;


(* theory setup *)
 val setup =
  Attrib.add_attributes [("presburger", att_syntax, "Cooper data")];
end;