# HG changeset patch
# User chaieb
# Date 1181552756 -7200
# Node ID b1eb911bf22f96519080dc96cdfdfc780536b74b
# Parent  22ddaef5fb920ecc4121840d34e407fbf90bb4b0
Context Data for the new presburger Method

diff -r 22ddaef5fb92 -r b1eb911bf22f src/HOL/Tools/Presburger/cooper_data.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Presburger/cooper_data.ML	Mon Jun 11 11:05:56 2007 +0200
@@ -0,0 +1,86 @@
+(*  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;