Context data for Ferrante-Rackoff quantifier elimination.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Ferrante_Rackoff/ferrante_rackoff_data.ML	Thu Jun 21 15:42:09 2007 +0200
@@ -0,0 +1,149 @@
+(* Title:      HOL/Tools/ferrante_rackoff_data.ML
+   ID:         $Id$
+   Author:     Amine Chaieb, TU Muenchen
+
+Context data for Ferrante and Rackoff's algorithm for quantifier
+elimination in dense linear orders.
+*)
+
+signature FERRANTE_RACKOF_DATA =
+sig
+  datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox
+  type entry
+  val get: Proof.context -> (thm * entry) list
+  val del: attribute
+  val add: entry -> attribute 
+  val funs: thm -> 
+    {isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm,
+     whatis: morphism -> cterm -> cterm -> ord,
+     simpset: morphism -> simpset}
+             -> morphism -> Context.generic -> Context.generic
+  val match: Proof.context -> cterm -> entry option
+  val setup: theory -> theory
+end;
+
+structure Ferrante_Rackoff_Data: FERRANTE_RACKOF_DATA = 
+struct
+
+(* data *)
+
+datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox
+
+type entry = 
+  {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list,  
+   ld: thm list, qe: thm, atoms : cterm list} *
+   {isolate_conv: Proof.context -> cterm list -> cterm -> thm, 
+    whatis : cterm -> cterm -> ord, 
+    simpset : simpset};
+
+val eq_key = Thm.eq_thm;
+fun eq_data arg = eq_fst eq_key arg;
+
+structure Data = GenericDataFun
+(
+  type T = (thm * entry) list;
+  val empty = [];
+  val extend = I;
+  fun merge _ = AList.merge eq_key (K true);
+);
+
+val get = Data.get o Context.Proof;
+
+fun del_data key = remove eq_data (key, []);
+
+val del = Thm.declaration_attribute (Data.map o del_data);
+
+fun undefined x = error "undefined";
+
+fun add entry = 
+    Thm.declaration_attribute (fn key => fn context => context |> Data.map 
+      (del_data key #> cons (key, entry)));
+
+
+(* extra-logical functions *)
+
+fun funs raw_key {isolate_conv = icv, whatis = wi, simpset = ss} phi = Data.map (fn data =>
+  let
+    val key = Morphism.thm phi raw_key;
+    val _ = AList.defined eq_key data key orelse
+      raise THM ("No data entry for structure key", 0, [key]);
+    val fns = {isolate_conv = icv phi, whatis = wi phi, simpset = ss phi};
+  in AList.map_entry eq_key key (apsnd (K fns)) data end);
+
+fun match ctxt tm =
+  let
+    fun match_inst
+        ({minf, pinf, nmi, npi, ld, qe, atoms},
+         fns as {isolate_conv, whatis, simpset}) pat =
+       let
+        fun h instT =
+          let
+            val substT = Thm.instantiate (instT, []);
+            val substT_cterm = Drule.cterm_rule substT;
+
+            val minf' = map substT minf
+            val pinf' = map substT pinf
+            val nmi' = map substT nmi
+            val npi' = map substT npi
+            val ld' = map substT ld
+            val qe' = substT qe
+            val atoms' = map substT_cterm atoms
+            val result = ({minf = minf', pinf = pinf', nmi = nmi', npi = npi', 
+                           ld = ld', qe = qe', atoms = atoms'}, fns)
+          in SOME result end
+      in (case try Thm.match (pat, tm) of
+           NONE => NONE
+         | SOME (instT, _) => h instT)
+      end;
+
+    fun match_struct (_,
+        entry as ({atoms = atoms, ...}, _): entry) =
+      get_first (match_inst entry) atoms;
+  in get_first match_struct (get ctxt) end;
+
+
+(* concrete syntax *)
+
+local
+val minfN = "minf";
+val pinfN = "pinf";
+val nmiN = "nmi";
+val npiN = "npi";
+val lin_denseN = "lindense";
+val qeN = "qe"
+val atomsN = "atoms"
+val simpsN = "simps"
+fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
+val any_keyword =
+  keyword minfN || keyword pinfN || keyword nmiN 
+|| keyword npiN || keyword lin_denseN || keyword qeN 
+|| keyword atomsN || keyword simpsN;
+
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val terms = thms >> map Drule.dest_term;
+in
+
+fun att_syntax src = src |> Attrib.syntax
+    ((keyword minfN |-- thms)
+     -- (keyword pinfN |-- thms)
+     -- (keyword nmiN |-- thms)
+     -- (keyword npiN |-- thms)
+     -- (keyword lin_denseN |-- thms)
+     -- (keyword qeN |-- thms)
+     -- (keyword atomsN |-- terms) >> 
+     (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> 
+     if length qe = 1 then
+       add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
+            qe = hd qe, atoms = atoms},
+           {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
+     else error "only one theorem for qe!"))
+
+end;
+
+
+(* theory setup *)
+
+val setup =
+  Attrib.add_attributes [("dlo", att_syntax, "Ferrante Rackoff data")];
+
+end;