|
1 (* Title: HOL/Nonstandard_Analysis/transfer_principle.ML |
|
2 Author: Brian Huffman |
|
3 |
|
4 Transfer principle tactic for nonstandard analysis. |
|
5 *) |
|
6 |
|
7 signature TRANSFER_PRINCIPLE = |
|
8 sig |
|
9 val transfer_tac: Proof.context -> thm list -> int -> tactic |
|
10 val add_const: string -> theory -> theory |
|
11 end; |
|
12 |
|
13 structure Transfer_Principle: TRANSFER_PRINCIPLE = |
|
14 struct |
|
15 |
|
16 structure Data = Generic_Data |
|
17 ( |
|
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 = []}; |
|
25 val extend = I; |
|
26 fun merge |
|
27 ({intros = intros1, unfolds = unfolds1, |
|
28 refolds = refolds1, consts = consts1}, |
|
29 {intros = intros2, unfolds = unfolds2, |
|
30 refolds = refolds2, consts = consts2}) : T = |
|
31 {intros = Thm.merge_thms (intros1, intros2), |
|
32 unfolds = Thm.merge_thms (unfolds1, unfolds2), |
|
33 refolds = Thm.merge_thms (refolds1, refolds2), |
|
34 consts = Library.merge (op =) (consts1, consts2)}; |
|
35 ); |
|
36 |
|
37 fun unstar_typ (Type (@{type_name star}, [t])) = unstar_typ t |
|
38 | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts) |
|
39 | unstar_typ T = T |
|
40 |
|
41 fun unstar_term consts term = |
|
42 let |
|
43 fun unstar (Const(a,T) $ t) = if member (op =) consts a then (unstar t) |
|
44 else (Const(a,unstar_typ T) $ unstar t) |
|
45 | unstar (f $ t) = unstar f $ unstar t |
|
46 | unstar (Const(a,T)) = Const(a,unstar_typ T) |
|
47 | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) |
|
48 | unstar t = t |
|
49 in |
|
50 unstar term |
|
51 end |
|
52 |
|
53 local exception MATCH |
|
54 in |
|
55 fun transfer_star_tac ctxt = |
|
56 let |
|
57 fun thm_of (Const (@{const_name Ifun}, _) $ t $ u) = @{thm transfer_Ifun} OF [thm_of t, thm_of u] |
|
58 | thm_of (Const (@{const_name star_of}, _) $ _) = @{thm star_of_def} |
|
59 | thm_of (Const (@{const_name star_n}, _) $ _) = @{thm Pure.reflexive} |
|
60 | thm_of _ = raise MATCH; |
|
61 |
|
62 fun thm_of_goal (Const (@{const_name Pure.eq}, _) $ t $ (Const (@{const_name star_n}, _) $ _)) = |
|
63 thm_of t |
|
64 | thm_of_goal _ = raise MATCH; |
|
65 in |
|
66 SUBGOAL (fn (t, i) => |
|
67 resolve_tac ctxt [thm_of_goal (strip_all_body t |> Logic.strip_imp_concl)] i |
|
68 handle MATCH => no_tac) |
|
69 end; |
|
70 end; |
|
71 |
|
72 fun transfer_thm_of ctxt ths t = |
|
73 let |
|
74 val {intros,unfolds,refolds,consts} = Data.get (Context.Proof ctxt); |
|
75 val meta = Local_Defs.meta_rewrite_rule ctxt; |
|
76 val ths' = map meta ths; |
|
77 val unfolds' = map meta unfolds and refolds' = map meta refolds; |
|
78 val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of ctxt t)) |
|
79 val u = unstar_term consts t' |
|
80 val tac = |
|
81 rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN |
|
82 ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN |
|
83 match_tac ctxt [transitive_thm] 1 THEN |
|
84 resolve_tac ctxt [@{thm transfer_start}] 1 THEN |
|
85 REPEAT_ALL_NEW (resolve_tac ctxt intros ORELSE' transfer_star_tac ctxt) 1 THEN |
|
86 match_tac ctxt [reflexive_thm] 1 |
|
87 in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end; |
|
88 |
|
89 fun transfer_tac ctxt ths = SUBGOAL (fn (t, _) => (fn th => |
|
90 let |
|
91 val tr = transfer_thm_of ctxt ths t |
|
92 val (_$ l $ r) = Thm.concl_of tr; |
|
93 val trs = if l aconv r then [] else [tr]; |
|
94 in rewrite_goals_tac ctxt trs th end)); |
|
95 |
|
96 local |
|
97 |
|
98 fun map_intros f = Data.map |
|
99 (fn {intros,unfolds,refolds,consts} => |
|
100 {intros=f intros, unfolds=unfolds, refolds=refolds, consts=consts}) |
|
101 |
|
102 fun map_unfolds f = Data.map |
|
103 (fn {intros,unfolds,refolds,consts} => |
|
104 {intros=intros, unfolds=f unfolds, refolds=refolds, consts=consts}) |
|
105 |
|
106 fun map_refolds f = Data.map |
|
107 (fn {intros,unfolds,refolds,consts} => |
|
108 {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts}) |
|
109 in |
|
110 |
|
111 val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm); |
|
112 val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm); |
|
113 |
|
114 val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm); |
|
115 val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm); |
|
116 |
|
117 val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm); |
|
118 val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm); |
|
119 |
|
120 end |
|
121 |
|
122 fun add_const c = Context.theory_map (Data.map |
|
123 (fn {intros,unfolds,refolds,consts} => |
|
124 {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})) |
|
125 |
|
126 val _ = |
|
127 Theory.setup |
|
128 (Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del) |
|
129 "declaration of transfer introduction rule" #> |
|
130 Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del) |
|
131 "declaration of transfer unfolding rule" #> |
|
132 Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del) |
|
133 "declaration of transfer refolding rule") |
|
134 |
|
135 end; |