src/HOL/Decision_Procs/ferrante_rackoff_data.ML
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 55792 687240115804
child 61089 969eb24297af
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     1 (* Title:      HOL/Decision_Procs/ferrante_rackoff_data.ML
     2    Author:     Amine Chaieb, TU Muenchen
     3 
     4 Context data for Ferrante and Rackoff's algorithm for quantifier
     5 elimination in dense linear orders.
     6 *)
     7 
     8 signature FERRANTE_RACKOF_DATA =
     9 sig
    10   datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox
    11   type entry
    12   val get: Proof.context -> (thm * entry) list
    13   val del: attribute
    14   val add: entry -> attribute 
    15   val funs: thm -> 
    16     {isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm,
    17      whatis: morphism -> cterm -> cterm -> ord,
    18      simpset: morphism -> simpset} -> declaration
    19   val match: Proof.context -> cterm -> entry option
    20 end;
    21 
    22 structure Ferrante_Rackoff_Data: FERRANTE_RACKOF_DATA = 
    23 struct
    24 
    25 (* data *)
    26 
    27 datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox
    28 
    29 type entry = 
    30   {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list,  
    31    ld: thm list, qe: thm, atoms : cterm list} *
    32    {isolate_conv: Proof.context -> cterm list -> cterm -> thm, 
    33     whatis : cterm -> cterm -> ord, 
    34     simpset : simpset};
    35 
    36 val eq_key = Thm.eq_thm;
    37 fun eq_data arg = eq_fst eq_key arg;
    38 
    39 structure Data = Generic_Data
    40 (
    41   type T = (thm * entry) list;
    42   val empty = [];
    43   val extend = I;
    44   fun merge data : T = AList.merge eq_key (K true) data;
    45 );
    46 
    47 val get = Data.get o Context.Proof;
    48 
    49 fun del_data key = remove eq_data (key, []);
    50 
    51 val del = Thm.declaration_attribute (Data.map o del_data);
    52 
    53 fun add entry = 
    54     Thm.declaration_attribute (fn key => fn context => context |> Data.map 
    55       (del_data key #> cons (key, entry)));
    56 
    57 
    58 (* extra-logical functions *)
    59 
    60 fun funs raw_key {isolate_conv = icv, whatis = wi, simpset = ss} phi = Data.map (fn data =>
    61   let
    62     val key = Morphism.thm phi raw_key;
    63     val _ = AList.defined eq_key data key orelse
    64       raise THM ("No data entry for structure key", 0, [key]);
    65     val fns = {isolate_conv = icv phi, whatis = wi phi, simpset = ss phi};
    66   in AList.map_entry eq_key key (apsnd (K fns)) data end);
    67 
    68 fun match ctxt tm =
    69   let
    70     fun match_inst ({minf, pinf, nmi, npi, ld, qe, atoms}, fns) pat =
    71        let
    72         fun h instT =
    73           let
    74             val substT = Thm.instantiate (instT, []);
    75             val substT_cterm = Drule.cterm_rule substT;
    76 
    77             val minf' = map substT minf
    78             val pinf' = map substT pinf
    79             val nmi' = map substT nmi
    80             val npi' = map substT npi
    81             val ld' = map substT ld
    82             val qe' = substT qe
    83             val atoms' = map substT_cterm atoms
    84             val result = ({minf = minf', pinf = pinf', nmi = nmi', npi = npi', 
    85                            ld = ld', qe = qe', atoms = atoms'}, fns)
    86           in SOME result end
    87       in (case try Thm.match (pat, tm) of
    88            NONE => NONE
    89          | SOME (instT, _) => h instT)
    90       end;
    91 
    92     fun match_struct (_,
    93         entry as ({atoms = atoms, ...}, _): entry) =
    94       get_first (match_inst entry) atoms;
    95   in get_first match_struct (get ctxt) end;
    96 
    97 
    98 (* concrete syntax *)
    99 
   100 local
   101 val minfN = "minf";
   102 val pinfN = "pinf";
   103 val nmiN = "nmi";
   104 val npiN = "npi";
   105 val lin_denseN = "lindense";
   106 val qeN = "qe"
   107 val atomsN = "atoms"
   108 val simpsN = "simps"
   109 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   110 val any_keyword =
   111   keyword minfN || keyword pinfN || keyword nmiN 
   112 || keyword npiN || keyword lin_denseN || keyword qeN 
   113 || keyword atomsN || keyword simpsN;
   114 
   115 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   116 val terms = thms >> map Drule.dest_term;
   117 in
   118 
   119 val _ =
   120   Theory.setup
   121     (Attrib.setup @{binding ferrack}
   122       ((keyword minfN |-- thms)
   123        -- (keyword pinfN |-- thms)
   124        -- (keyword nmiN |-- thms)
   125        -- (keyword npiN |-- thms)
   126        -- (keyword lin_denseN |-- thms)
   127        -- (keyword qeN |-- thms)
   128        -- (keyword atomsN |-- terms) >>
   129          (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> 
   130          if length qe = 1 then
   131            add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
   132                 qe = hd qe, atoms = atoms},
   133                {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
   134          else error "only one theorem for qe!"))
   135       "Ferrante Rackoff data");
   136 
   137 end;
   138 
   139 end;