src/HOL/Decision_Procs/ferrante_rackoff_data.ML
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 37744 3daaf23b9ab4
child 55506 46f3e31c5a87
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
     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   val setup: theory -> theory
    21 end;
    22 
    23 structure Ferrante_Rackoff_Data: FERRANTE_RACKOF_DATA = 
    24 struct
    25 
    26 (* data *)
    27 
    28 datatype ord = Lt | Le | Gt | Ge | Eq | NEq | Nox
    29 
    30 type entry = 
    31   {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list,  
    32    ld: thm list, qe: thm, atoms : cterm list} *
    33    {isolate_conv: Proof.context -> cterm list -> cterm -> thm, 
    34     whatis : cterm -> cterm -> ord, 
    35     simpset : simpset};
    36 
    37 val eq_key = Thm.eq_thm;
    38 fun eq_data arg = eq_fst eq_key arg;
    39 
    40 structure Data = Generic_Data
    41 (
    42   type T = (thm * entry) list;
    43   val empty = [];
    44   val extend = I;
    45   fun merge data : T = AList.merge eq_key (K true) data;
    46 );
    47 
    48 val get = Data.get o Context.Proof;
    49 
    50 fun del_data key = remove eq_data (key, []);
    51 
    52 val del = Thm.declaration_attribute (Data.map o del_data);
    53 
    54 fun add entry = 
    55     Thm.declaration_attribute (fn key => fn context => context |> Data.map 
    56       (del_data key #> cons (key, entry)));
    57 
    58 
    59 (* extra-logical functions *)
    60 
    61 fun funs raw_key {isolate_conv = icv, whatis = wi, simpset = ss} phi = Data.map (fn data =>
    62   let
    63     val key = Morphism.thm phi raw_key;
    64     val _ = AList.defined eq_key data key orelse
    65       raise THM ("No data entry for structure key", 0, [key]);
    66     val fns = {isolate_conv = icv phi, whatis = wi phi, simpset = ss phi};
    67   in AList.map_entry eq_key key (apsnd (K fns)) data end);
    68 
    69 fun match ctxt tm =
    70   let
    71     fun match_inst
    72         ({minf, pinf, nmi, npi, ld, qe, atoms},
    73          fns as {isolate_conv, whatis, simpset}) pat =
    74        let
    75         fun h instT =
    76           let
    77             val substT = Thm.instantiate (instT, []);
    78             val substT_cterm = Drule.cterm_rule substT;
    79 
    80             val minf' = map substT minf
    81             val pinf' = map substT pinf
    82             val nmi' = map substT nmi
    83             val npi' = map substT npi
    84             val ld' = map substT ld
    85             val qe' = substT qe
    86             val atoms' = map substT_cterm atoms
    87             val result = ({minf = minf', pinf = pinf', nmi = nmi', npi = npi', 
    88                            ld = ld', qe = qe', atoms = atoms'}, fns)
    89           in SOME result end
    90       in (case try Thm.match (pat, tm) of
    91            NONE => NONE
    92          | SOME (instT, _) => h instT)
    93       end;
    94 
    95     fun match_struct (_,
    96         entry as ({atoms = atoms, ...}, _): entry) =
    97       get_first (match_inst entry) atoms;
    98   in get_first match_struct (get ctxt) end;
    99 
   100 
   101 (* concrete syntax *)
   102 
   103 local
   104 val minfN = "minf";
   105 val pinfN = "pinf";
   106 val nmiN = "nmi";
   107 val npiN = "npi";
   108 val lin_denseN = "lindense";
   109 val qeN = "qe"
   110 val atomsN = "atoms"
   111 val simpsN = "simps"
   112 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   113 val any_keyword =
   114   keyword minfN || keyword pinfN || keyword nmiN 
   115 || keyword npiN || keyword lin_denseN || keyword qeN 
   116 || keyword atomsN || keyword simpsN;
   117 
   118 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   119 val terms = thms >> map Drule.dest_term;
   120 in
   121 
   122 val ferrak_setup =
   123   Attrib.setup @{binding ferrack}
   124     ((keyword minfN |-- thms)
   125      -- (keyword pinfN |-- thms)
   126      -- (keyword nmiN |-- thms)
   127      -- (keyword npiN |-- thms)
   128      -- (keyword lin_denseN |-- thms)
   129      -- (keyword qeN |-- thms)
   130      -- (keyword atomsN |-- terms) >>
   131        (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> 
   132        if length qe = 1 then
   133          add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
   134               qe = hd qe, atoms = atoms},
   135              {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
   136        else error "only one theorem for qe!"))
   137     "Ferrante Rackoff data";
   138 
   139 end;
   140 
   141 
   142 (* theory setup *)
   143 
   144 val setup = ferrak_setup;
   145 
   146 end;