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