SSL ferrante_rackoff_data.ML Sprache: SML

(* Title:      HOL/Decision_Procs/ferrante_rackoff_data.ML
   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 -> Proof.context -> simpset} -> Morphism.declaration
  val match: Proof.context -> cterm -> entry option
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 = Generic_Data
(
  type T = (thm * entry) list;
  val empty = [];
  fun merge data : T = AList.merge eq_key (K true) data;
);

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 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 context =
  context |> 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 (Context.proof_of context)};
    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) pat =
       let
        fun h instT =
          let
            val substT = Thm.instantiate (instT, Vars.empty);
            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.repeats (Scan.unless any_keyword Attrib.multi_thm);
val terms = thms >> map Drule.dest_term;
in

val _ =
  Theory.setup
    (Attrib.setup \<^binding>\<open>ferrack\<close>
      ((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!"))
      "Ferrante Rackoff data");

end;

end;

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.