src/HOL/Decision_Procs/ferrante_rackoff_data.ML
author nipkow
Tue Feb 23 16:25:08 2016 +0100 (2016-02-23)
changeset 62390 842917225d56
parent 61476 1884c40f1539
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more canonical names
     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 -> Proof.context -> 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 context =
    61   context |> 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 =
    67         {isolate_conv = icv phi, whatis = wi phi, simpset = ss phi (Context.proof_of context)};
    68     in AList.map_entry eq_key key (apsnd (K fns)) data end);
    69 
    70 fun match ctxt tm =
    71   let
    72     fun match_inst ({minf, pinf, nmi, npi, ld, qe, atoms}, fns) pat =
    73        let
    74         fun h instT =
    75           let
    76             val substT = Thm.instantiate (instT, []);
    77             val substT_cterm = Drule.cterm_rule substT;
    78 
    79             val minf' = map substT minf
    80             val pinf' = map substT pinf
    81             val nmi' = map substT nmi
    82             val npi' = map substT npi
    83             val ld' = map substT ld
    84             val qe' = substT qe
    85             val atoms' = map substT_cterm atoms
    86             val result = ({minf = minf', pinf = pinf', nmi = nmi', npi = npi', 
    87                            ld = ld', qe = qe', atoms = atoms'}, fns)
    88           in SOME result end
    89       in (case try Thm.match (pat, tm) of
    90            NONE => NONE
    91          | SOME (instT, _) => h instT)
    92       end;
    93 
    94     fun match_struct (_,
    95         entry as ({atoms = atoms, ...}, _): entry) =
    96       get_first (match_inst entry) atoms;
    97   in get_first match_struct (get ctxt) end;
    98 
    99 
   100 (* concrete syntax *)
   101 
   102 local
   103 val minfN = "minf";
   104 val pinfN = "pinf";
   105 val nmiN = "nmi";
   106 val npiN = "npi";
   107 val lin_denseN = "lindense";
   108 val qeN = "qe"
   109 val atomsN = "atoms"
   110 val simpsN = "simps"
   111 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   112 val any_keyword =
   113   keyword minfN || keyword pinfN || keyword nmiN 
   114 || keyword npiN || keyword lin_denseN || keyword qeN 
   115 || keyword atomsN || keyword simpsN;
   116 
   117 val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
   118 val terms = thms >> map Drule.dest_term;
   119 in
   120 
   121 val _ =
   122   Theory.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 end;