|
1 signature TRANSFER_TAC = |
|
2 sig |
|
3 val transfer_tac: thm list -> int -> tactic |
|
4 val setup: (theory -> theory) list |
|
5 end; |
|
6 |
|
7 structure Transfer: TRANSFER_TAC = |
|
8 struct |
|
9 |
|
10 (* TODO: make this list extensible *) |
|
11 val star_consts = |
|
12 [ "StarType.star_of", "StarType.Ifun" |
|
13 , "StarType.unstar", "StarType.Iset" ] |
|
14 |
|
15 structure TransferData = TheoryDataFun |
|
16 (struct |
|
17 val name = "HOL/transfer"; |
|
18 type T = { |
|
19 intros: thm list, |
|
20 unfolds: thm list, |
|
21 refolds: thm list, |
|
22 consts: string list |
|
23 }; |
|
24 val empty = {intros = [], unfolds = [], refolds = [], consts = star_consts}; |
|
25 val copy = I; |
|
26 val extend = I; |
|
27 fun merge _ |
|
28 ({intros = intros1, unfolds = unfolds1, |
|
29 refolds = refolds1, consts = consts1}, |
|
30 {intros = intros2, unfolds = unfolds2, |
|
31 refolds = refolds2, consts = consts2}) = |
|
32 {intros = Drule.merge_rules (intros1, intros2), |
|
33 unfolds = Drule.merge_rules (unfolds1, unfolds2), |
|
34 refolds = Drule.merge_rules (refolds1, refolds2), |
|
35 consts = merge_lists consts1 consts2}; |
|
36 fun print _ _ = (); |
|
37 end); |
|
38 |
|
39 val transfer_start = thm "transfer_start" |
|
40 |
|
41 fun unstar_typ (Type ("StarType.star",[t])) = unstar_typ t |
|
42 | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts) |
|
43 | unstar_typ T = T |
|
44 |
|
45 fun unstar_term consts term = |
|
46 let |
|
47 fun delete a = exists (fn x => x = a) consts |
|
48 fun unstar (Const(a,T) $ t) = if (delete a) then (unstar t) |
|
49 else (Const(a,unstar_typ T) $ unstar t) |
|
50 | unstar (f $ t) = unstar f $ unstar t |
|
51 | unstar (Const(a,T)) = Const(a,unstar_typ T) |
|
52 | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) |
|
53 | unstar t = t |
|
54 in |
|
55 unstar term |
|
56 end |
|
57 |
|
58 val atomizers = map thm ["atomize_all", "atomize_imp", "atomize_eq"] |
|
59 |
|
60 fun transfer_thm_of thy ths t = |
|
61 let |
|
62 val {intros,unfolds,refolds,consts} = TransferData.get thy |
|
63 val (_$_$t') = concl_of (Tactic.rewrite true unfolds (cterm_of thy t)) |
|
64 val u = unstar_term consts t' |
|
65 val ct = cterm_of thy (Logic.mk_equals (t,u)) |
|
66 val tacs = |
|
67 [ rewrite_goals_tac atomizers |
|
68 , match_tac [transitive_thm] 1 |
|
69 , resolve_tac [transfer_start] 1 |
|
70 , REPEAT_ALL_NEW (resolve_tac intros) 1 |
|
71 , match_tac [reflexive_thm] 1 ] |
|
72 in |
|
73 prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs) |
|
74 end |
|
75 |
|
76 fun transfer_tac ths = |
|
77 SUBGOAL (fn (t,i) => |
|
78 (fn th => |
|
79 let val thy = theory_of_thm th |
|
80 val tr = transfer_thm_of thy ths t |
|
81 in rewrite_goals_tac [tr] th |
|
82 end |
|
83 ) |
|
84 ) |
|
85 |
|
86 local |
|
87 fun map_intros f = TransferData.map |
|
88 (fn {intros,unfolds,refolds,consts} => |
|
89 {intros=f intros, unfolds=unfolds, refolds=refolds, consts=consts}) |
|
90 |
|
91 fun map_unfolds f = TransferData.map |
|
92 (fn {intros,unfolds,refolds,consts} => |
|
93 {intros=intros, unfolds=f unfolds, refolds=refolds, consts=consts}) |
|
94 |
|
95 fun map_refolds f = TransferData.map |
|
96 (fn {intros,unfolds,refolds,consts} => |
|
97 {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts}) |
|
98 |
|
99 fun map_consts f = TransferData.map |
|
100 (fn {intros,unfolds,refolds,consts} => |
|
101 {intros=intros, unfolds=unfolds, refolds=refolds, consts=f consts}) |
|
102 in |
|
103 fun intro_add_global (thy, thm) = (map_intros (Drule.add_rule thm) thy, thm); |
|
104 fun intro_del_global (thy, thm) = (map_intros (Drule.del_rule thm) thy, thm); |
|
105 |
|
106 fun unfold_add_global (thy, thm) = (map_unfolds (Drule.add_rule thm) thy, thm); |
|
107 fun unfold_del_global (thy, thm) = (map_unfolds (Drule.del_rule thm) thy, thm); |
|
108 |
|
109 fun refold_add_global (thy, thm) = (map_refolds (Drule.add_rule thm) thy, thm); |
|
110 fun refold_del_global (thy, thm) = (map_refolds (Drule.del_rule thm) thy, thm); |
|
111 end |
|
112 |
|
113 local |
|
114 val undef_local = |
|
115 Attrib.add_del_args |
|
116 Attrib.undef_local_attribute |
|
117 Attrib.undef_local_attribute; |
|
118 in |
|
119 val intro_attr = |
|
120 (Attrib.add_del_args intro_add_global intro_del_global, undef_local); |
|
121 val unfold_attr = |
|
122 (Attrib.add_del_args unfold_add_global unfold_del_global, undef_local); |
|
123 val refold_attr = |
|
124 (Attrib.add_del_args refold_add_global refold_del_global, undef_local); |
|
125 end |
|
126 |
|
127 val transfer_method = Method.SIMPLE_METHOD' HEADGOAL o transfer_tac; |
|
128 |
|
129 val setup = |
|
130 [ TransferData.init |
|
131 , Attrib.add_attributes |
|
132 [ ("transfer_intro", intro_attr, "transfer introduction rule") |
|
133 , ("transfer_unfold", unfold_attr, "transfer unfolding rule") |
|
134 , ("transfer_refold", refold_attr, "transfer refolding rule") |
|
135 ] |
|
136 , Method.add_method |
|
137 ("transfer", Method.thms_args transfer_method, "transfer principle") |
|
138 ]; |
|
139 |
|
140 end; |