src/HOL/Decision_Procs/langford_data.ML
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 55792 687240115804
child 61476 1884c40f1539
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     1 signature LANGFORD_DATA =
     2 sig
     3   type entry
     4   val get: Proof.context -> simpset * (thm * entry) list
     5   val add: entry -> attribute
     6   val del: attribute
     7   val match: Proof.context -> cterm -> entry option
     8 end;
     9 
    10 structure Langford_Data: LANGFORD_DATA =
    11 struct
    12 
    13 (* data *)
    14 
    15 type entry =
    16   {qe_bnds: thm, qe_nolb : thm , qe_noub: thm,
    17    gs : thm list, gst : thm, atoms: cterm list};
    18 
    19 val eq_key = Thm.eq_thm;
    20 fun eq_data arg = eq_fst eq_key arg;
    21 
    22 structure Data = Generic_Data
    23 (
    24   type T = simpset * (thm * entry) list;
    25   val empty = (HOL_basic_ss, []);
    26   val extend = I;
    27   fun merge ((ss1, es1), (ss2, es2)) : T =
    28     (merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2));
    29 );
    30 
    31 val get = Data.get o Context.Proof;
    32 
    33 fun del_data key = apsnd (remove eq_data (key, []));
    34 
    35 val del = Thm.declaration_attribute (Data.map o del_data);
    36 
    37 fun add entry =
    38   Thm.declaration_attribute (fn key => fn context => context |> Data.map
    39     (del_data key #> apsnd (cons (key, entry))));
    40 
    41 val add_simp = Thm.declaration_attribute (fn th => fn context =>
    42   (Data.map o apfst) (simpset_map (Context.proof_of context) (Simplifier.add_simp th)) context);
    43 
    44 val del_simp = Thm.declaration_attribute (fn th => fn context =>
    45   (Data.map o apfst) (simpset_map (Context.proof_of context) (Simplifier.del_simp th)) context);
    46 
    47 fun match ctxt tm =
    48   let
    49     fun match_inst {qe_bnds, qe_nolb, qe_noub, gs, gst, atoms} pat =
    50       let
    51         fun h instT =
    52           let
    53             val substT = Thm.instantiate (instT, []);
    54             val substT_cterm = Drule.cterm_rule substT;
    55 
    56             val qe_bnds' = substT qe_bnds;
    57             val qe_nolb' = substT qe_nolb;
    58             val qe_noub' = substT qe_noub;
    59             val gs' = map substT gs;
    60             val gst' = substT gst;
    61             val atoms' = map substT_cterm atoms;
    62             val result =
    63              {qe_bnds = qe_bnds', qe_nolb = qe_nolb',
    64               qe_noub = qe_noub', gs = gs', gst = gst',
    65               atoms = atoms'};
    66           in SOME result end;
    67       in
    68         (case try Thm.match (pat, tm) of
    69           NONE => NONE
    70         | SOME (instT, _) => h instT)
    71       end;
    72 
    73     fun match_struct (_, entry as ({atoms = atoms, ...}): entry) =
    74       get_first (match_inst entry) atoms;
    75   in get_first match_struct (snd (get ctxt)) end;
    76 
    77 
    78 (* concrete syntax *)
    79 
    80 local
    81   val qeN = "qe";
    82   val gatherN = "gather";
    83   val atomsN = "atoms"
    84   fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
    85   val any_keyword = keyword qeN || keyword gatherN || keyword atomsN;
    86 
    87   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    88   val terms = thms >> map Drule.dest_term;
    89 in
    90 
    91 val _ =
    92   Theory.setup
    93     (Attrib.setup @{binding langford}
    94       ((keyword qeN |-- thms) --
    95        (keyword gatherN |-- thms) --
    96        (keyword atomsN |-- terms) >> (fn ((qes, gs), atoms) =>
    97           if length qes = 3 andalso length gs > 1 then
    98             let
    99               val [q1, q2, q3] = qes;
   100               val gst :: gss = gs;
   101               val entry =
   102                {qe_bnds = q1, qe_nolb = q2,
   103                 qe_noub = q3, gs = gss, gst = gst, atoms = atoms};
   104             in add entry end
   105           else error "Need 3 theorems for qe and at least one for gs"))
   106       "Langford data");
   107 end;
   108 
   109 val _ =
   110   Theory.setup
   111     (Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset");
   112 
   113 end;