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