23 structure Def: DEF = |
23 structure Def: DEF = |
24 struct |
24 struct |
25 |
25 |
26 (* context data *) |
26 (* context data *) |
27 |
27 |
28 type def = {lhs: term, mk_eq: morphism -> thm}; |
28 type def = {lhs: term, eq: thm}; |
29 |
29 |
30 val eq_def : def * def -> bool = op aconv o apply2 #lhs; |
30 val eq_def : def * def -> bool = op aconv o apply2 #lhs; |
31 |
31 |
32 fun transform_def phi ({lhs, mk_eq}: def) = |
32 fun transform_def phi ({lhs, eq}: def) = |
33 {lhs = Morphism.term phi lhs, mk_eq = Morphism.transform phi mk_eq}; |
33 {lhs = Morphism.term phi lhs, eq = Morphism.thm phi eq}; |
34 |
34 |
35 structure Data = Generic_Data |
35 structure Data = Generic_Data |
36 ( |
36 ( |
37 type T = def Item_Net.T; |
37 type T = def Item_Net.T; |
38 val empty : T = Item_Net.init eq_def (single o #lhs); |
38 val empty : T = Item_Net.init eq_def (single o #lhs); |
39 val merge = Item_Net.merge; |
39 val merge = Item_Net.merge; |
40 ); |
40 ); |
41 |
41 |
42 fun declare_def lhs eq lthy = |
42 fun declare_def lhs eq lthy = |
43 let |
43 let val def0: def = {lhs = lhs, eq = Thm.trim_context eq} in |
44 val eq0 = Thm.trim_context eq; |
|
45 val def: def = {lhs = lhs, mk_eq = fn phi => Morphism.thm phi eq0}; |
|
46 in |
|
47 lthy |> Local_Theory.declaration {syntax = false, pervasive = true} |
44 lthy |> Local_Theory.declaration {syntax = false, pervasive = true} |
48 (fn phi => fn context => |
45 (fn phi => fn context => |
49 let val psi = Morphism.set_trim_context'' context phi |
46 let val psi = Morphism.set_trim_context'' context phi |
50 in (Data.map o Item_Net.update) (transform_def psi def) context end) |
47 in (Data.map o Item_Net.update) (transform_def psi def0) context end) |
51 end; |
48 end; |
52 |
49 |
53 fun get_def ctxt ct = |
50 fun get_def ctxt ct = |
54 let |
51 let |
55 val thy = Proof_Context.theory_of ctxt; |
52 val thy = Proof_Context.theory_of ctxt; |
56 val data = Data.get (Context.Proof ctxt); |
53 val data = Data.get (Context.Proof ctxt); |
57 val t = Thm.term_of ct; |
54 val t = Thm.term_of ct; |
58 fun match_def {lhs, mk_eq} = |
55 fun match_def {lhs, eq} = |
59 if Pattern.matches thy (lhs, t) then |
56 if Pattern.matches thy (lhs, t) then |
60 let |
57 let val inst = Thm.match (Thm.cterm_of ctxt lhs, ct) |
61 val inst = Thm.match (Thm.cterm_of ctxt lhs, ct); |
58 in SOME (Thm.instantiate inst (Thm.transfer thy eq)) end |
62 val eq = |
|
63 Morphism.form mk_eq |
|
64 |> Thm.transfer thy |
|
65 |> Thm.instantiate inst; |
|
66 in SOME eq end |
|
67 else NONE; |
59 else NONE; |
68 in Item_Net.retrieve_matching data t |> get_first match_def end; |
60 in Item_Net.retrieve_matching data t |> get_first match_def end; |
69 |
61 |
70 |
62 |
71 (* simproc setup *) |
63 (* simproc setup *) |