28 fun merge _ |
28 fun merge _ |
29 ({intros = intros1, unfolds = unfolds1, |
29 ({intros = intros1, unfolds = unfolds1, |
30 refolds = refolds1, consts = consts1}, |
30 refolds = refolds1, consts = consts1}, |
31 {intros = intros2, unfolds = unfolds2, |
31 {intros = intros2, unfolds = unfolds2, |
32 refolds = refolds2, consts = consts2}) = |
32 refolds = refolds2, consts = consts2}) = |
33 {intros = Drule.merge_rules (intros1, intros2), |
33 {intros = Thm.merge_thms (intros1, intros2), |
34 unfolds = Drule.merge_rules (unfolds1, unfolds2), |
34 unfolds = Thm.merge_thms (unfolds1, unfolds2), |
35 refolds = Drule.merge_rules (refolds1, refolds2), |
35 refolds = Thm.merge_thms (refolds1, refolds2), |
36 consts = Library.merge (op =) (consts1, consts2)} : T; |
36 consts = Library.merge (op =) (consts1, consts2)} : T; |
37 ); |
37 ); |
38 |
|
39 val transfer_start = thm "transfer_start" |
|
40 |
38 |
41 fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t |
39 fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t |
42 | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts) |
40 | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts) |
43 | unstar_typ T = T |
41 | unstar_typ T = T |
44 |
42 |
46 let |
44 let |
47 fun unstar (Const(a,T) $ t) = if member (op =) consts a then (unstar t) |
45 fun unstar (Const(a,T) $ t) = if member (op =) consts a then (unstar t) |
48 else (Const(a,unstar_typ T) $ unstar t) |
46 else (Const(a,unstar_typ T) $ unstar t) |
49 | unstar (f $ t) = unstar f $ unstar t |
47 | unstar (f $ t) = unstar f $ unstar t |
50 | unstar (Const(a,T)) = Const(a,unstar_typ T) |
48 | unstar (Const(a,T)) = Const(a,unstar_typ T) |
51 | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) |
49 | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) |
52 | unstar t = t |
50 | unstar t = t |
53 in |
51 in |
54 unstar term |
52 unstar term |
55 end |
53 end |
56 |
54 |
65 val u = unstar_term consts t' |
63 val u = unstar_term consts t' |
66 val tac = |
64 val tac = |
67 rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN |
65 rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN |
68 ALLGOALS ObjectLogic.full_atomize_tac THEN |
66 ALLGOALS ObjectLogic.full_atomize_tac THEN |
69 match_tac [transitive_thm] 1 THEN |
67 match_tac [transitive_thm] 1 THEN |
70 resolve_tac [transfer_start] 1 THEN |
68 resolve_tac [@{thm transfer_start}] 1 THEN |
71 REPEAT_ALL_NEW (resolve_tac intros) 1 THEN |
69 REPEAT_ALL_NEW (resolve_tac intros) 1 THEN |
72 match_tac [reflexive_thm] 1 |
70 match_tac [reflexive_thm] 1 |
73 in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end |
71 in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end |
74 |
72 |
75 fun transfer_tac ctxt ths = |
73 fun transfer_tac ctxt ths = |
90 |
88 |
91 fun map_refolds f = TransferData.map |
89 fun map_refolds f = TransferData.map |
92 (fn {intros,unfolds,refolds,consts} => |
90 (fn {intros,unfolds,refolds,consts} => |
93 {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts}) |
91 {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts}) |
94 in |
92 in |
95 val intro_add = Thm.declaration_attribute (map_intros o Drule.add_rule); |
93 val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm); |
96 val intro_del = Thm.declaration_attribute (map_intros o Drule.del_rule); |
94 val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm); |
97 |
95 |
98 val unfold_add = Thm.declaration_attribute (map_unfolds o Drule.add_rule); |
96 val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm); |
99 val unfold_del = Thm.declaration_attribute (map_unfolds o Drule.del_rule); |
97 val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm); |
100 |
98 |
101 val refold_add = Thm.declaration_attribute (map_refolds o Drule.add_rule); |
99 val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm); |
102 val refold_del = Thm.declaration_attribute (map_refolds o Drule.del_rule); |
100 val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm); |
103 end |
101 end |
104 |
102 |
105 fun add_const c = Context.theory_map (TransferData.map |
103 fun add_const c = Context.theory_map (TransferData.map |
106 (fn {intros,unfolds,refolds,consts} => |
104 (fn {intros,unfolds,refolds,consts} => |
107 {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})) |
105 {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})) |