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