52406
|
1 |
(* Title: HOL/Tools/reflection.ML
|
51726
|
2 |
Author: Amine Chaieb, TU Muenchen
|
|
3 |
|
52406
|
4 |
A trial for automatical reflection with user-space declarations.
|
51726
|
5 |
*)
|
|
6 |
|
52406
|
7 |
signature REFLECTION =
|
51726
|
8 |
sig
|
52406
|
9 |
val reflect: Proof.context -> thm list -> thm list -> conv
|
|
10 |
val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
|
|
11 |
val reflect_with_eval: Proof.context -> thm list -> thm list -> conv -> conv
|
|
12 |
val reflection_with_eval_tac: Proof.context -> thm list -> thm list -> conv -> term option -> int -> tactic
|
|
13 |
val get_default: Proof.context -> { reification_eqs: thm list, correctness_thms: thm list }
|
|
14 |
val add_reification_eq: attribute
|
|
15 |
val del_reification_eq: attribute
|
|
16 |
val add_correctness_thm: attribute
|
|
17 |
val del_correctness_thm: attribute
|
|
18 |
val default_reify_tac: Proof.context -> thm list -> term option -> int -> tactic
|
|
19 |
val default_reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
|
51726
|
20 |
end;
|
|
21 |
|
52406
|
22 |
structure Reflection : REFLECTION =
|
51726
|
23 |
struct
|
|
24 |
|
52406
|
25 |
fun subst_correctness corr_thms ct =
|
|
26 |
Conv.rewrs_conv (map (Thm.symmetric o mk_eq) corr_thms) ct
|
|
27 |
handle CTERM _ => error "No suitable correctness theorem found";
|
51726
|
28 |
|
52406
|
29 |
fun reflect ctxt corr_thms eqs =
|
|
30 |
(Reification.conv ctxt eqs) then_conv (subst_correctness corr_thms)
|
51726
|
31 |
|
52406
|
32 |
fun reflection_tac ctxt corr_thms eqs =
|
|
33 |
Reification.lift_conv ctxt (reflect ctxt corr_thms eqs);
|
52275
|
34 |
|
52406
|
35 |
fun first_arg_conv conv =
|
51726
|
36 |
let
|
52406
|
37 |
fun conv' ct =
|
|
38 |
if can Thm.dest_comb (fst (Thm.dest_comb ct))
|
|
39 |
then Conv.combination_conv conv' Conv.all_conv ct
|
|
40 |
else Conv.combination_conv Conv.all_conv conv ct;
|
|
41 |
in conv' end;
|
|
42 |
|
|
43 |
fun reflect_with_eval ctxt corr_thms eqs conv =
|
|
44 |
(reflect ctxt corr_thms eqs) then_conv (first_arg_conv conv) then_conv (Reification.dereify ctxt eqs);
|
|
45 |
|
|
46 |
fun reflection_with_eval_tac ctxt corr_thms eqs conv =
|
|
47 |
Reification.lift_conv ctxt (reflect_with_eval ctxt corr_thms eqs conv);
|
52288
|
48 |
|
52406
|
49 |
structure Data = Generic_Data
|
|
50 |
(
|
|
51 |
type T = thm list * thm list;
|
|
52 |
val empty = ([], []);
|
|
53 |
val extend = I;
|
|
54 |
fun merge ((ths1, rths1), (ths2, rths2)) =
|
|
55 |
(Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
|
|
56 |
);
|
|
57 |
|
|
58 |
fun get_default ctxt =
|
|
59 |
let
|
|
60 |
val (reification_eqs, correctness_thms) = Data.get (Context.Proof ctxt);
|
|
61 |
in { reification_eqs = reification_eqs, correctness_thms = correctness_thms } end;
|
52288
|
62 |
|
52406
|
63 |
val add_reification_eq = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
|
|
64 |
val del_reification_eq = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
|
|
65 |
val add_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
|
|
66 |
val del_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
|
52288
|
67 |
|
53171
|
68 |
val _ = Theory.setup
|
52406
|
69 |
(Attrib.setup @{binding reify}
|
53171
|
70 |
(Attrib.add_del add_reification_eq del_reification_eq)
|
|
71 |
"declare reification equations" #>
|
|
72 |
Attrib.setup @{binding reflection}
|
|
73 |
(Attrib.add_del add_correctness_thm del_correctness_thm)
|
|
74 |
"declare reflection correctness theorems");
|
51726
|
75 |
|
52406
|
76 |
fun default_reify_tac ctxt user_eqs =
|
52288
|
77 |
let
|
52406
|
78 |
val { reification_eqs = default_eqs, correctness_thms = _ } =
|
|
79 |
get_default ctxt;
|
|
80 |
val eqs = fold Thm.add_thm user_eqs default_eqs;
|
|
81 |
in Reification.tac ctxt eqs end;
|
52288
|
82 |
|
52406
|
83 |
fun default_reflection_tac ctxt user_thms user_eqs =
|
52288
|
84 |
let
|
52406
|
85 |
val { reification_eqs = default_eqs, correctness_thms = default_thms } =
|
|
86 |
get_default ctxt;
|
|
87 |
val corr_thms = fold Thm.add_thm user_thms default_thms;
|
|
88 |
val eqs = fold Thm.add_thm user_eqs default_eqs;
|
|
89 |
in reflection_tac ctxt corr_thms eqs end;
|
51726
|
90 |
|
52276
|
91 |
end;
|