author | paulson <lp15@cam.ac.uk> |
Sun, 14 Aug 2022 23:51:47 +0100 | |
changeset 75864 | 3842556b757c |
parent 74561 | 8e6c973003c8 |
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, []); |
33519 | 26 |
fun merge ((ss1, es1), (ss2, es2)) : T = |
27 |
(merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2)); |
|
23907 | 28 |
); |
29 |
||
30 |
val get = Data.get o Context.Proof; |
|
31 |
||
32 |
fun del_data key = apsnd (remove eq_data (key, [])); |
|
33 |
||
34 |
val del = Thm.declaration_attribute (Data.map o del_data); |
|
35 |
||
55792 | 36 |
fun add entry = |
37 |
Thm.declaration_attribute (fn key => fn context => context |> Data.map |
|
38 |
(del_data key #> apsnd (cons (key, entry)))); |
|
23907 | 39 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
41226
diff
changeset
|
40 |
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
|
41 |
(Data.map o apfst) (simpset_map (Context.proof_of context) (Simplifier.add_simp th)) context); |
23907 | 42 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
41226
diff
changeset
|
43 |
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
|
44 |
(Data.map o apfst) (simpset_map (Context.proof_of context) (Simplifier.del_simp th)) context); |
23907 | 45 |
|
46 |
fun match ctxt tm = |
|
47 |
let |
|
55792 | 48 |
fun match_inst {qe_bnds, qe_nolb, qe_noub, gs, gst, atoms} pat = |
49 |
let |
|
23907 | 50 |
fun h instT = |
51 |
let |
|
74282 | 52 |
val substT = Thm.instantiate (instT, Vars.empty); |
23907 | 53 |
val substT_cterm = Drule.cterm_rule substT; |
54 |
||
55792 | 55 |
val qe_bnds' = substT qe_bnds; |
56 |
val qe_nolb' = substT qe_nolb; |
|
57 |
val qe_noub' = substT qe_noub; |
|
58 |
val gs' = map substT gs; |
|
59 |
val gst' = substT gst; |
|
60 |
val atoms' = map substT_cterm atoms; |
|
61 |
val result = |
|
62 |
{qe_bnds = qe_bnds', qe_nolb = qe_nolb', |
|
63 |
qe_noub = qe_noub', gs = gs', gst = gst', |
|
64 |
atoms = atoms'}; |
|
65 |
in SOME result end; |
|
66 |
in |
|
67 |
(case try Thm.match (pat, tm) of |
|
68 |
NONE => NONE |
|
69 |
| SOME (instT, _) => h instT) |
|
23907 | 70 |
end; |
71 |
||
55792 | 72 |
fun match_struct (_, entry as ({atoms = atoms, ...}): entry) = |
23907 | 73 |
get_first (match_inst entry) atoms; |
74 |
in get_first match_struct (snd (get ctxt)) end; |
|
75 |
||
55792 | 76 |
|
23907 | 77 |
(* concrete syntax *) |
78 |
||
79 |
local |
|
55792 | 80 |
val qeN = "qe"; |
81 |
val gatherN = "gather"; |
|
82 |
val atomsN = "atoms" |
|
83 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
|
84 |
val any_keyword = keyword qeN || keyword gatherN || keyword atomsN; |
|
23907 | 85 |
|
61476 | 86 |
val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm); |
55792 | 87 |
val terms = thms >> map Drule.dest_term; |
23907 | 88 |
in |
89 |
||
55792 | 90 |
val _ = |
91 |
Theory.setup |
|
69597 | 92 |
(Attrib.setup \<^binding>\<open>langford\<close> |
55792 | 93 |
((keyword qeN |-- thms) -- |
94 |
(keyword gatherN |-- thms) -- |
|
95 |
(keyword atomsN |-- terms) >> (fn ((qes, gs), atoms) => |
|
96 |
if length qes = 3 andalso length gs > 1 then |
|
97 |
let |
|
98 |
val [q1, q2, q3] = qes; |
|
99 |
val gst :: gss = gs; |
|
100 |
val entry = |
|
101 |
{qe_bnds = q1, qe_nolb = q2, |
|
102 |
qe_noub = q3, gs = gss, gst = gst, atoms = atoms}; |
|
103 |
in add entry end |
|
104 |
else error "Need 3 theorems for qe and at least one for gs")) |
|
105 |
"Langford data"); |
|
106 |
end; |
|
107 |
||
108 |
val _ = |
|
109 |
Theory.setup |
|
69597 | 110 |
(Attrib.setup \<^binding>\<open>langfordsimp\<close> (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
|
111 |
|
23907 | 112 |
end; |