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