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