author | wenzelm |
Sat, 10 Jun 2017 21:48:02 +0200 | |
changeset 66061 | 880db47fed30 |
parent 61476 | 1884c40f1539 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
23907 | 1 |
signature LANGFORD_DATA = |
2 |
sig |
|
3 |
type entry |
|
4 |
val get: Proof.context -> simpset * (thm * entry) list |
|
55792 | 5 |
val add: entry -> attribute |
23907 | 6 |
val del: attribute |
7 |
val match: Proof.context -> cterm -> entry option |
|
8 |
end; |
|
9 |
||
55792 | 10 |
structure Langford_Data: LANGFORD_DATA = |
23907 | 11 |
struct |
12 |
||
13 |
(* data *) |
|
55792 | 14 |
|
15 |
type entry = |
|
16 |
{qe_bnds: thm, qe_nolb : thm , qe_noub: thm, |
|
17 |
gs : thm list, gst : thm, atoms: cterm list}; |
|
18 |
||
23907 | 19 |
val eq_key = Thm.eq_thm; |
20 |
fun eq_data arg = eq_fst eq_key arg; |
|
21 |
||
33519 | 22 |
structure Data = Generic_Data |
23 |
( |
|
24 |
type T = simpset * (thm * entry) list; |
|
23907 | 25 |
val empty = (HOL_basic_ss, []); |
26 |
val extend = I; |
|
33519 | 27 |
fun merge ((ss1, es1), (ss2, es2)) : T = |
28 |
(merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2)); |
|
23907 | 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 |
||
55792 | 37 |
fun add entry = |
38 |
Thm.declaration_attribute (fn key => fn context => context |> Data.map |
|
39 |
(del_data key #> apsnd (cons (key, entry)))); |
|
23907 | 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 | 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 | 46 |
|
47 |
fun match ctxt tm = |
|
48 |
let |
|
55792 | 49 |
fun match_inst {qe_bnds, qe_nolb, qe_noub, gs, gst, atoms} pat = |
50 |
let |
|
23907 | 51 |
fun h instT = |
52 |
let |
|
53 |
val substT = Thm.instantiate (instT, []); |
|
54 |
val substT_cterm = Drule.cterm_rule substT; |
|
55 |
||
55792 | 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) |
|
23907 | 71 |
end; |
72 |
||
55792 | 73 |
fun match_struct (_, entry as ({atoms = atoms, ...}): entry) = |
23907 | 74 |
get_first (match_inst entry) atoms; |
75 |
in get_first match_struct (snd (get ctxt)) end; |
|
76 |
||
55792 | 77 |
|
23907 | 78 |
(* concrete syntax *) |
79 |
||
80 |
local |
|
55792 | 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; |
|
23907 | 86 |
|
61476 | 87 |
val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm); |
55792 | 88 |
val terms = thms >> map Drule.dest_term; |
23907 | 89 |
in |
90 |
||
55792 | 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"); |
|
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 | 113 |
end; |