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