1 (* Title: HOL/Tools/transfer.ML |
|
2 Author: Brian Huffman, TU Muenchen |
|
3 Author: Ondrej Kuncar, TU Muenchen |
|
4 |
|
5 Generic theorem transfer method. |
|
6 *) |
|
7 |
|
8 signature TRANSFER = |
|
9 sig |
|
10 val bottom_rewr_conv: thm list -> conv |
|
11 val top_rewr_conv: thm list -> conv |
|
12 |
|
13 val prep_conv: conv |
|
14 val get_transfer_raw: Proof.context -> thm list |
|
15 val get_relator_eq_item_net: Proof.context -> thm Item_Net.T |
|
16 val get_relator_eq: Proof.context -> thm list |
|
17 val get_sym_relator_eq: Proof.context -> thm list |
|
18 val get_relator_eq_raw: Proof.context -> thm list |
|
19 val get_relator_domain: Proof.context -> thm list |
|
20 val get_compound_lhs: Proof.context -> (term * thm) Item_Net.T |
|
21 val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T |
|
22 val transfer_add: attribute |
|
23 val transfer_del: attribute |
|
24 val transfer_raw_add: thm -> Context.generic -> Context.generic |
|
25 val transfer_raw_del: thm -> Context.generic -> Context.generic |
|
26 val transferred_attribute: thm list -> attribute |
|
27 val untransferred_attribute: thm list -> attribute |
|
28 val prep_transfer_domain_thm: Proof.context -> thm -> thm |
|
29 val transfer_domain_add: attribute |
|
30 val transfer_domain_del: attribute |
|
31 val transfer_rule_of_term: Proof.context -> bool -> term -> thm |
|
32 val transfer_rule_of_lhs: Proof.context -> term -> thm |
|
33 val eq_tac: Proof.context -> int -> tactic |
|
34 val transfer_step_tac: Proof.context -> int -> tactic |
|
35 val transfer_tac: bool -> Proof.context -> int -> tactic |
|
36 val transfer_prover_tac: Proof.context -> int -> tactic |
|
37 val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic |
|
38 val setup: theory -> theory |
|
39 end |
|
40 |
|
41 structure Transfer : TRANSFER = |
|
42 struct |
|
43 |
|
44 (** Theory Data **) |
|
45 |
|
46 val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst); |
|
47 val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq |
|
48 o HOLogic.dest_Trueprop o Thm.concl_of); |
|
49 |
|
50 structure Data = Generic_Data |
|
51 ( |
|
52 type T = |
|
53 { transfer_raw : thm Item_Net.T, |
|
54 known_frees : (string * typ) list, |
|
55 compound_lhs : (term * thm) Item_Net.T, |
|
56 compound_rhs : (term * thm) Item_Net.T, |
|
57 relator_eq : thm Item_Net.T, |
|
58 relator_eq_raw : thm Item_Net.T, |
|
59 relator_domain : thm Item_Net.T } |
|
60 val empty = |
|
61 { transfer_raw = Thm.intro_rules, |
|
62 known_frees = [], |
|
63 compound_lhs = compound_xhs_empty_net, |
|
64 compound_rhs = compound_xhs_empty_net, |
|
65 relator_eq = rewr_rules, |
|
66 relator_eq_raw = Thm.full_rules, |
|
67 relator_domain = Thm.full_rules } |
|
68 val extend = I |
|
69 fun merge |
|
70 ( { transfer_raw = t1, known_frees = k1, |
|
71 compound_lhs = l1, |
|
72 compound_rhs = c1, relator_eq = r1, |
|
73 relator_eq_raw = rw1, relator_domain = rd1 }, |
|
74 { transfer_raw = t2, known_frees = k2, |
|
75 compound_lhs = l2, |
|
76 compound_rhs = c2, relator_eq = r2, |
|
77 relator_eq_raw = rw2, relator_domain = rd2 } ) = |
|
78 { transfer_raw = Item_Net.merge (t1, t2), |
|
79 known_frees = Library.merge (op =) (k1, k2), |
|
80 compound_lhs = Item_Net.merge (l1, l2), |
|
81 compound_rhs = Item_Net.merge (c1, c2), |
|
82 relator_eq = Item_Net.merge (r1, r2), |
|
83 relator_eq_raw = Item_Net.merge (rw1, rw2), |
|
84 relator_domain = Item_Net.merge (rd1, rd2) } |
|
85 ) |
|
86 |
|
87 fun get_transfer_raw ctxt = ctxt |
|
88 |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof) |
|
89 |
|
90 fun get_known_frees ctxt = ctxt |
|
91 |> (#known_frees o Data.get o Context.Proof) |
|
92 |
|
93 fun get_compound_lhs ctxt = ctxt |
|
94 |> (#compound_lhs o Data.get o Context.Proof) |
|
95 |
|
96 fun get_compound_rhs ctxt = ctxt |
|
97 |> (#compound_rhs o Data.get o Context.Proof) |
|
98 |
|
99 fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt |
|
100 |
|
101 fun get_relator_eq ctxt = ctxt |
|
102 |> (Item_Net.content o #relator_eq o Data.get o Context.Proof) |
|
103 |> map safe_mk_meta_eq |
|
104 |
|
105 fun get_sym_relator_eq ctxt = ctxt |
|
106 |> (Item_Net.content o #relator_eq o Data.get o Context.Proof) |
|
107 |> map (Thm.symmetric o safe_mk_meta_eq) |
|
108 |
|
109 fun get_relator_eq_raw ctxt = ctxt |
|
110 |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof) |
|
111 |
|
112 fun get_relator_domain ctxt = ctxt |
|
113 |> (Item_Net.content o #relator_domain o Data.get o Context.Proof) |
|
114 |
|
115 fun map_data f1 f2 f3 f4 f5 f6 f7 |
|
116 { transfer_raw, known_frees, compound_lhs, compound_rhs, |
|
117 relator_eq, relator_eq_raw, relator_domain } = |
|
118 { transfer_raw = f1 transfer_raw, |
|
119 known_frees = f2 known_frees, |
|
120 compound_lhs = f3 compound_lhs, |
|
121 compound_rhs = f4 compound_rhs, |
|
122 relator_eq = f5 relator_eq, |
|
123 relator_eq_raw = f6 relator_eq_raw, |
|
124 relator_domain = f7 relator_domain } |
|
125 |
|
126 fun map_transfer_raw f = map_data f I I I I I I |
|
127 fun map_known_frees f = map_data I f I I I I I |
|
128 fun map_compound_lhs f = map_data I I f I I I I |
|
129 fun map_compound_rhs f = map_data I I I f I I I |
|
130 fun map_relator_eq f = map_data I I I I f I I |
|
131 fun map_relator_eq_raw f = map_data I I I I I f I |
|
132 fun map_relator_domain f = map_data I I I I I I f |
|
133 |
|
134 fun add_transfer_thm thm = Data.map |
|
135 (map_transfer_raw (Item_Net.update thm) o |
|
136 map_compound_lhs |
|
137 (case HOLogic.dest_Trueprop (Thm.concl_of thm) of |
|
138 Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ => |
|
139 Item_Net.update (lhs, thm) |
|
140 | _ => I) o |
|
141 map_compound_rhs |
|
142 (case HOLogic.dest_Trueprop (Thm.concl_of thm) of |
|
143 Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) => |
|
144 Item_Net.update (rhs, thm) |
|
145 | _ => I) o |
|
146 map_known_frees (Term.add_frees (Thm.concl_of thm))) |
|
147 |
|
148 fun del_transfer_thm thm = Data.map |
|
149 (map_transfer_raw (Item_Net.remove thm) o |
|
150 map_compound_lhs |
|
151 (case HOLogic.dest_Trueprop (Thm.concl_of thm) of |
|
152 Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ => |
|
153 Item_Net.remove (lhs, thm) |
|
154 | _ => I) o |
|
155 map_compound_rhs |
|
156 (case HOLogic.dest_Trueprop (Thm.concl_of thm) of |
|
157 Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) => |
|
158 Item_Net.remove (rhs, thm) |
|
159 | _ => I)) |
|
160 |
|
161 fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt |
|
162 fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt |
|
163 |
|
164 (** Conversions **) |
|
165 |
|
166 fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context} |
|
167 fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context} |
|
168 |
|
169 fun transfer_rel_conv conv = |
|
170 Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv))) |
|
171 |
|
172 val Rel_rule = Thm.symmetric @{thm Rel_def} |
|
173 |
|
174 fun dest_funcT cT = |
|
175 (case Thm.dest_ctyp cT of [T, U] => (T, U) |
|
176 | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], [])) |
|
177 |
|
178 fun Rel_conv ct = |
|
179 let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct) |
|
180 val (cU, _) = dest_funcT cT' |
|
181 in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end |
|
182 |
|
183 (* Conversion to preprocess a transfer rule *) |
|
184 fun safe_Rel_conv ct = |
|
185 Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct |
|
186 |
|
187 fun prep_conv ct = ( |
|
188 Conv.implies_conv safe_Rel_conv prep_conv |
|
189 else_conv |
|
190 safe_Rel_conv |
|
191 else_conv |
|
192 Conv.all_conv) ct |
|
193 |
|
194 (** Replacing explicit equalities with is_equality premises **) |
|
195 |
|
196 fun mk_is_equality t = |
|
197 Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t |
|
198 |
|
199 val is_equality_lemma = |
|
200 @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))" |
|
201 by (unfold is_equality_def, rule, drule meta_spec, |
|
202 erule meta_mp, rule refl, simp)} |
|
203 |
|
204 fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm = |
|
205 let |
|
206 val thy = Thm.theory_of_thm thm |
|
207 val prop = Thm.prop_of thm |
|
208 val (t, mk_prop') = dest prop |
|
209 (* Only consider "op =" at non-base types *) |
|
210 fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) = |
|
211 (case T of Type (_, []) => false | _ => true) |
|
212 | is_eq _ = false |
|
213 val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I) |
|
214 val eq_consts = rev (add_eqs t []) |
|
215 val eqTs = map (snd o dest_Const) eq_consts |
|
216 val used = Term.add_free_names prop [] |
|
217 val names = map (K "") eqTs |> Name.variant_list used |
|
218 val frees = map Free (names ~~ eqTs) |
|
219 val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees |
|
220 val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t) |
|
221 val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1)) |
|
222 val cprop = Thm.cterm_of thy prop2 |
|
223 val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop |
|
224 fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm |
|
225 in |
|
226 forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2})) |
|
227 end |
|
228 handle TERM _ => thm |
|
229 |
|
230 fun abstract_equalities_transfer ctxt thm = |
|
231 let |
|
232 fun dest prop = |
|
233 let |
|
234 val prems = Logic.strip_imp_prems prop |
|
235 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) |
|
236 val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl) |
|
237 in |
|
238 (rel, fn rel' => |
|
239 Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y))) |
|
240 end |
|
241 val contracted_eq_thm = |
|
242 Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm |
|
243 handle CTERM _ => thm |
|
244 in |
|
245 gen_abstract_equalities ctxt dest contracted_eq_thm |
|
246 end |
|
247 |
|
248 fun abstract_equalities_relator_eq ctxt rel_eq_thm = |
|
249 gen_abstract_equalities ctxt (fn x => (x, I)) |
|
250 (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]}) |
|
251 |
|
252 fun abstract_equalities_domain ctxt thm = |
|
253 let |
|
254 fun dest prop = |
|
255 let |
|
256 val prems = Logic.strip_imp_prems prop |
|
257 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) |
|
258 val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl) |
|
259 in |
|
260 (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y))) |
|
261 end |
|
262 fun transfer_rel_conv conv = |
|
263 Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv))) |
|
264 val contracted_eq_thm = |
|
265 Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm |
|
266 in |
|
267 gen_abstract_equalities ctxt dest contracted_eq_thm |
|
268 end |
|
269 |
|
270 |
|
271 (** Replacing explicit Domainp predicates with Domainp assumptions **) |
|
272 |
|
273 fun mk_Domainp_assm (T, R) = |
|
274 HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R) |
|
275 |
|
276 val Domainp_lemma = |
|
277 @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))" |
|
278 by (rule, drule meta_spec, |
|
279 erule meta_mp, rule refl, simp)} |
|
280 |
|
281 fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t |
|
282 | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u |
|
283 | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t |
|
284 | fold_Domainp _ _ = I |
|
285 |
|
286 fun subst_terms tab t = |
|
287 let |
|
288 val t' = Termtab.lookup tab t |
|
289 in |
|
290 case t' of |
|
291 SOME t' => t' |
|
292 | NONE => |
|
293 (case t of |
|
294 u $ v => (subst_terms tab u) $ (subst_terms tab v) |
|
295 | Abs (a, T, t) => Abs (a, T, subst_terms tab t) |
|
296 | t => t) |
|
297 end |
|
298 |
|
299 fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm = |
|
300 let |
|
301 val thy = Thm.theory_of_thm thm |
|
302 val prop = Thm.prop_of thm |
|
303 val (t, mk_prop') = dest prop |
|
304 val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t []) |
|
305 val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms |
|
306 val used = Term.add_free_names t [] |
|
307 val rels = map (snd o dest_comb) Domainp_tms |
|
308 val rel_names = map (fst o fst o dest_Var) rels |
|
309 val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used |
|
310 val frees = map Free (names ~~ Domainp_Ts) |
|
311 val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees); |
|
312 val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t |
|
313 val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t')) |
|
314 val prop2 = Logic.list_rename_params (rev names) prop1 |
|
315 val cprop = Thm.cterm_of thy prop2 |
|
316 val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop |
|
317 fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm; |
|
318 in |
|
319 forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2})) |
|
320 end |
|
321 handle TERM _ => thm |
|
322 |
|
323 fun abstract_domains_transfer ctxt thm = |
|
324 let |
|
325 fun dest prop = |
|
326 let |
|
327 val prems = Logic.strip_imp_prems prop |
|
328 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) |
|
329 val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl) |
|
330 in |
|
331 (x, fn x' => |
|
332 Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y))) |
|
333 end |
|
334 in |
|
335 gen_abstract_domains ctxt dest thm |
|
336 end |
|
337 |
|
338 fun abstract_domains_relator_domain ctxt thm = |
|
339 let |
|
340 fun dest prop = |
|
341 let |
|
342 val prems = Logic.strip_imp_prems prop |
|
343 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) |
|
344 val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl) |
|
345 in |
|
346 (y, fn y' => |
|
347 Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x $ y'))) |
|
348 end |
|
349 in |
|
350 gen_abstract_domains ctxt dest thm |
|
351 end |
|
352 |
|
353 fun detect_transfer_rules thm = |
|
354 let |
|
355 fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of |
|
356 (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false |
|
357 | _ $ _ $ _ => true |
|
358 | _ => false |
|
359 fun safe_transfer_rule_conv ctm = |
|
360 if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm |
|
361 in |
|
362 Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm |
|
363 end |
|
364 |
|
365 (** Adding transfer domain rules **) |
|
366 |
|
367 fun prep_transfer_domain_thm ctxt thm = |
|
368 (abstract_equalities_domain ctxt o detect_transfer_rules) thm |
|
369 |
|
370 fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o |
|
371 prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt |
|
372 |
|
373 fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o |
|
374 prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt |
|
375 |
|
376 (** Transfer proof method **) |
|
377 |
|
378 val post_simps = |
|
379 @{thms transfer_forall_eq [symmetric] |
|
380 transfer_implies_eq [symmetric] transfer_bforall_unfold} |
|
381 |
|
382 fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) => |
|
383 let |
|
384 val keepers = keepers @ get_known_frees ctxt |
|
385 val vs = rev (Term.add_frees t []) |
|
386 val vs' = filter_out (member (op =) keepers) vs |
|
387 in |
|
388 Induct.arbitrary_tac ctxt 0 vs' i |
|
389 end) |
|
390 |
|
391 fun mk_relT (T, U) = T --> U --> HOLogic.boolT |
|
392 |
|
393 fun mk_Rel t = |
|
394 let val T = fastype_of t |
|
395 in Const (@{const_name Transfer.Rel}, T --> T) $ t end |
|
396 |
|
397 fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u = |
|
398 let |
|
399 val thy = Proof_Context.theory_of ctxt |
|
400 (* precondition: prj(T,U) must consist of only TFrees and type "fun" *) |
|
401 fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) = |
|
402 let |
|
403 val r1 = rel T1 U1 |
|
404 val r2 = rel T2 U2 |
|
405 val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U) |
|
406 in |
|
407 Const (@{const_name rel_fun}, rT) $ r1 $ r2 |
|
408 end |
|
409 | rel T U = |
|
410 let |
|
411 val (a, _) = dest_TFree (prj (T, U)) |
|
412 in |
|
413 Free (the (AList.lookup (op =) tab a), mk_relT (T, U)) |
|
414 end |
|
415 fun zip _ thms (Bound i) (Bound _) = (nth thms i, []) |
|
416 | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) = |
|
417 let |
|
418 val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt |
|
419 val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U) |
|
420 val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop) |
|
421 val thm0 = Thm.assume cprop |
|
422 val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u |
|
423 val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop)) |
|
424 val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1)) |
|
425 val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1)) |
|
426 val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2)) |
|
427 val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2] |
|
428 val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)] |
|
429 val rule = Drule.instantiate' tinsts insts @{thm Rel_abs} |
|
430 val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1)) |
|
431 in |
|
432 (thm2 COMP rule, hyps) |
|
433 end |
|
434 | zip ctxt thms (f $ t) (g $ u) = |
|
435 let |
|
436 val (thm1, hyps1) = zip ctxt thms f g |
|
437 val (thm2, hyps2) = zip ctxt thms t u |
|
438 in |
|
439 (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2) |
|
440 end |
|
441 | zip _ _ t u = |
|
442 let |
|
443 val T = fastype_of t |
|
444 val U = fastype_of u |
|
445 val prop = mk_Rel (rel T U) $ t $ u |
|
446 val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop) |
|
447 in |
|
448 (Thm.assume cprop, [cprop]) |
|
449 end |
|
450 val r = mk_Rel (rel (fastype_of t) (fastype_of u)) |
|
451 val goal = HOLogic.mk_Trueprop (r $ t $ u) |
|
452 val rename = Thm.trivial (cterm_of thy goal) |
|
453 val (thm, hyps) = zip ctxt [] t u |
|
454 in |
|
455 Drule.implies_intr_list hyps (thm RS rename) |
|
456 end |
|
457 |
|
458 (* create a lambda term of the same shape as the given term *) |
|
459 fun skeleton (is_atom : term -> bool) ctxt t = |
|
460 let |
|
461 fun dummy ctxt = |
|
462 let |
|
463 val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt |
|
464 in |
|
465 (Free (c, dummyT), ctxt) |
|
466 end |
|
467 fun go (Bound i) ctxt = (Bound i, ctxt) |
|
468 | go (Abs (x, _, t)) ctxt = |
|
469 let |
|
470 val (t', ctxt) = go t ctxt |
|
471 in |
|
472 (Abs (x, dummyT, t'), ctxt) |
|
473 end |
|
474 | go (tu as (t $ u)) ctxt = |
|
475 if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else |
|
476 let |
|
477 val (t', ctxt) = go t ctxt |
|
478 val (u', ctxt) = go u ctxt |
|
479 in |
|
480 (t' $ u', ctxt) |
|
481 end |
|
482 | go _ ctxt = dummy ctxt |
|
483 in |
|
484 go t ctxt |> fst |> Syntax.check_term ctxt |> |
|
485 map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type}))) |
|
486 end |
|
487 |
|
488 (** Monotonicity analysis **) |
|
489 |
|
490 (* TODO: Put extensible table in theory data *) |
|
491 val monotab = |
|
492 Symtab.make |
|
493 [(@{const_name transfer_implies}, [~1, 1]), |
|
494 (@{const_name transfer_forall}, [1])(*, |
|
495 (@{const_name implies}, [~1, 1]), |
|
496 (@{const_name All}, [1])*)] |
|
497 |
|
498 (* |
|
499 Function bool_insts determines the set of boolean-relation variables |
|
500 that can be instantiated to implies, rev_implies, or iff. |
|
501 |
|
502 Invariants: bool_insts p (t, u) requires that |
|
503 u :: _ => _ => ... => bool, and |
|
504 t is a skeleton of u |
|
505 *) |
|
506 fun bool_insts p (t, u) = |
|
507 let |
|
508 fun strip2 (t1 $ t2, u1 $ u2, tus) = |
|
509 strip2 (t1, u1, (t2, u2) :: tus) |
|
510 | strip2 x = x |
|
511 fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z) |
|
512 fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab |
|
513 | go Ts p (t, u) tab = |
|
514 let |
|
515 val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t))) |
|
516 val (_, tf, tus) = strip2 (t, u, []) |
|
517 val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE |
|
518 val tab1 = |
|
519 case ps_opt of |
|
520 SOME ps => |
|
521 let |
|
522 val ps' = map (fn x => p * x) (take (length tus) ps) |
|
523 in |
|
524 fold I (map2 (go Ts) ps' tus) tab |
|
525 end |
|
526 | NONE => tab |
|
527 val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))] |
|
528 in |
|
529 Symtab.join (K or3) (tab1, tab2) |
|
530 end |
|
531 val tab = go [] p (t, u) Symtab.empty |
|
532 fun f (a, (true, false, false)) = SOME (a, @{const implies}) |
|
533 | f (a, (false, true, false)) = SOME (a, @{const rev_implies}) |
|
534 | f (a, (true, true, _)) = SOME (a, HOLogic.eq_const HOLogic.boolT) |
|
535 | f _ = NONE |
|
536 in |
|
537 map_filter f (Symtab.dest tab) |
|
538 end |
|
539 |
|
540 fun retrieve_terms t net = map fst (Item_Net.retrieve net t) |
|
541 |
|
542 fun matches_list ctxt term = |
|
543 is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term)) |
|
544 |
|
545 fun transfer_rule_of_term ctxt equiv t : thm = |
|
546 let |
|
547 val compound_rhs = get_compound_rhs ctxt |
|
548 fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t |
|
549 val s = skeleton is_rhs ctxt t |
|
550 val frees = map fst (Term.add_frees s []) |
|
551 val tfrees = map fst (Term.add_tfrees s []) |
|
552 fun prep a = "R" ^ Library.unprefix "'" a |
|
553 val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt |
|
554 val tab = tfrees ~~ rnames |
|
555 fun prep a = the (AList.lookup (op =) tab a) |
|
556 val thm = transfer_rule_of_terms fst ctxt' tab s t |
|
557 val binsts = bool_insts (if equiv then 0 else 1) (s, t) |
|
558 val cbool = @{ctyp bool} |
|
559 val relT = @{typ "bool => bool => bool"} |
|
560 val idx = Thm.maxidx_of thm + 1 |
|
561 val thy = Proof_Context.theory_of ctxt |
|
562 fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool) |
|
563 fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t) |
|
564 in |
|
565 thm |
|
566 |> Thm.generalize (tfrees, rnames @ frees) idx |
|
567 |> Thm.instantiate (map tinst binsts, map inst binsts) |
|
568 end |
|
569 |
|
570 fun transfer_rule_of_lhs ctxt t : thm = |
|
571 let |
|
572 val compound_lhs = get_compound_lhs ctxt |
|
573 fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t |
|
574 val s = skeleton is_lhs ctxt t |
|
575 val frees = map fst (Term.add_frees s []) |
|
576 val tfrees = map fst (Term.add_tfrees s []) |
|
577 fun prep a = "R" ^ Library.unprefix "'" a |
|
578 val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt |
|
579 val tab = tfrees ~~ rnames |
|
580 fun prep a = the (AList.lookup (op =) tab a) |
|
581 val thm = transfer_rule_of_terms snd ctxt' tab t s |
|
582 val binsts = bool_insts 1 (s, t) |
|
583 val cbool = @{ctyp bool} |
|
584 val relT = @{typ "bool => bool => bool"} |
|
585 val idx = Thm.maxidx_of thm + 1 |
|
586 val thy = Proof_Context.theory_of ctxt |
|
587 fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool) |
|
588 fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t) |
|
589 in |
|
590 thm |
|
591 |> Thm.generalize (tfrees, rnames @ frees) idx |
|
592 |> Thm.instantiate (map tinst binsts, map inst binsts) |
|
593 end |
|
594 |
|
595 fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) |
|
596 THEN_ALL_NEW rtac @{thm is_equality_eq} |
|
597 |
|
598 fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt) |
|
599 |
|
600 fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt)) |
|
601 THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt))) |
|
602 |
|
603 fun transfer_tac equiv ctxt i = |
|
604 let |
|
605 val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} |
|
606 val start_rule = |
|
607 if equiv then @{thm transfer_start} else @{thm transfer_start'} |
|
608 val rules = get_transfer_raw ctxt |
|
609 val eq_rules = get_relator_eq_raw ctxt |
|
610 (* allow unsolved subgoals only for standard transfer method, not for transfer' *) |
|
611 val end_tac = if equiv then K all_tac else K no_tac |
|
612 val err_msg = "Transfer failed to convert goal to an object-logic formula" |
|
613 fun main_tac (t, i) = |
|
614 rtac start_rule i THEN |
|
615 (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t)) |
|
616 THEN_ALL_NEW |
|
617 (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)) |
|
618 ORELSE' end_tac)) (i + 1) |
|
619 handle TERM (_, ts) => raise TERM (err_msg, ts) |
|
620 in |
|
621 EVERY |
|
622 [rewrite_goal_tac ctxt pre_simps i THEN |
|
623 SUBGOAL main_tac i, |
|
624 (* FIXME: rewrite_goal_tac does unwanted eta-contraction *) |
|
625 rewrite_goal_tac ctxt post_simps i, |
|
626 Goal.norm_hhf_tac ctxt i] |
|
627 end |
|
628 |
|
629 fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) => |
|
630 let |
|
631 val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t |
|
632 val rule1 = transfer_rule_of_term ctxt false rhs |
|
633 val rules = get_transfer_raw ctxt |
|
634 val eq_rules = get_relator_eq_raw ctxt |
|
635 val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}]) |
|
636 in |
|
637 EVERY |
|
638 [CONVERSION prep_conv i, |
|
639 rtac @{thm transfer_prover_start} i, |
|
640 ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1)) |
|
641 THEN_ALL_NEW |
|
642 (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1), |
|
643 rtac @{thm refl} i] |
|
644 end) |
|
645 |
|
646 (** Transfer attribute **) |
|
647 |
|
648 fun transferred ctxt extra_rules thm = |
|
649 let |
|
650 val start_rule = @{thm transfer_start} |
|
651 val start_rule' = @{thm transfer_start'} |
|
652 val rules = extra_rules @ get_transfer_raw ctxt |
|
653 val eq_rules = get_relator_eq_raw ctxt |
|
654 val err_msg = "Transfer failed to convert goal to an object-logic formula" |
|
655 val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} |
|
656 val thm1 = Drule.forall_intr_vars thm |
|
657 val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) []) |
|
658 |> map (fn v as ((a, _), S) => (v, TFree (a, S))) |
|
659 val thm2 = thm1 |
|
660 |> Thm.certify_instantiate (instT, []) |
|
661 |> Raw_Simplifier.rewrite_rule ctxt pre_simps |
|
662 val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt |
|
663 val t = HOLogic.dest_Trueprop (Thm.concl_of thm2) |
|
664 val rule = transfer_rule_of_lhs ctxt' t |
|
665 val tac = |
|
666 resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN |
|
667 (rtac rule |
|
668 THEN_ALL_NEW |
|
669 (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) |
|
670 THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1 |
|
671 handle TERM (_, ts) => raise TERM (err_msg, ts) |
|
672 val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac) |
|
673 val tnames = map (fst o dest_TFree o snd) instT |
|
674 in |
|
675 thm3 |
|
676 |> Raw_Simplifier.rewrite_rule ctxt' post_simps |
|
677 |> Simplifier.norm_hhf ctxt' |
|
678 |> Drule.generalize (tnames, []) |
|
679 |> Drule.zero_var_indexes |
|
680 end |
|
681 (* |
|
682 handle THM _ => thm |
|
683 *) |
|
684 |
|
685 fun untransferred ctxt extra_rules thm = |
|
686 let |
|
687 val start_rule = @{thm untransfer_start} |
|
688 val rules = extra_rules @ get_transfer_raw ctxt |
|
689 val eq_rules = get_relator_eq_raw ctxt |
|
690 val err_msg = "Transfer failed to convert goal to an object-logic formula" |
|
691 val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} |
|
692 val thm1 = Drule.forall_intr_vars thm |
|
693 val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) []) |
|
694 |> map (fn v as ((a, _), S) => (v, TFree (a, S))) |
|
695 val thm2 = thm1 |
|
696 |> Thm.certify_instantiate (instT, []) |
|
697 |> Raw_Simplifier.rewrite_rule ctxt pre_simps |
|
698 val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt |
|
699 val t = HOLogic.dest_Trueprop (Thm.concl_of thm2) |
|
700 val rule = transfer_rule_of_term ctxt' true t |
|
701 val tac = |
|
702 rtac (thm2 RS start_rule) 1 THEN |
|
703 (rtac rule |
|
704 THEN_ALL_NEW |
|
705 (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) |
|
706 THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1 |
|
707 handle TERM (_, ts) => raise TERM (err_msg, ts) |
|
708 val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac) |
|
709 val tnames = map (fst o dest_TFree o snd) instT |
|
710 in |
|
711 thm3 |
|
712 |> Raw_Simplifier.rewrite_rule ctxt' post_simps |
|
713 |> Simplifier.norm_hhf ctxt' |
|
714 |> Drule.generalize (tnames, []) |
|
715 |> Drule.zero_var_indexes |
|
716 end |
|
717 |
|
718 (** Methods and attributes **) |
|
719 |
|
720 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => |
|
721 error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)) |
|
722 |
|
723 val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon) |
|
724 |-- Scan.repeat free) [] |
|
725 |
|
726 fun transfer_method equiv : (Proof.context -> Proof.method) context_parser = |
|
727 fixing >> (fn vs => fn ctxt => |
|
728 SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt)) |
|
729 |
|
730 val transfer_prover_method : (Proof.context -> Proof.method) context_parser = |
|
731 Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt)) |
|
732 |
|
733 (* Attribute for transfer rules *) |
|
734 |
|
735 fun prep_rule ctxt = |
|
736 abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv |
|
737 |
|
738 val transfer_add = |
|
739 Thm.declaration_attribute (fn thm => fn ctxt => |
|
740 (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt) |
|
741 |
|
742 val transfer_del = |
|
743 Thm.declaration_attribute (fn thm => fn ctxt => |
|
744 (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt) |
|
745 |
|
746 val transfer_attribute = |
|
747 Attrib.add_del transfer_add transfer_del |
|
748 |
|
749 (* Attributes for transfer domain rules *) |
|
750 |
|
751 val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm |
|
752 |
|
753 val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm |
|
754 |
|
755 val transfer_domain_attribute = |
|
756 Attrib.add_del transfer_domain_add transfer_domain_del |
|
757 |
|
758 (* Attributes for transferred rules *) |
|
759 |
|
760 fun transferred_attribute thms = Thm.rule_attribute |
|
761 (fn context => transferred (Context.proof_of context) thms) |
|
762 |
|
763 fun untransferred_attribute thms = Thm.rule_attribute |
|
764 (fn context => untransferred (Context.proof_of context) thms) |
|
765 |
|
766 val transferred_attribute_parser = |
|
767 Attrib.thms >> transferred_attribute |
|
768 |
|
769 val untransferred_attribute_parser = |
|
770 Attrib.thms >> untransferred_attribute |
|
771 |
|
772 (* Theory setup *) |
|
773 |
|
774 val relator_eq_setup = |
|
775 let |
|
776 val name = @{binding relator_eq} |
|
777 fun add_thm thm context = context |
|
778 |> Data.map (map_relator_eq (Item_Net.update thm)) |
|
779 |> Data.map (map_relator_eq_raw |
|
780 (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm))) |
|
781 fun del_thm thm context = context |
|
782 |> Data.map (map_relator_eq (Item_Net.remove thm)) |
|
783 |> Data.map (map_relator_eq_raw |
|
784 (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm))) |
|
785 val add = Thm.declaration_attribute add_thm |
|
786 val del = Thm.declaration_attribute del_thm |
|
787 val text = "declaration of relator equality rule (used by transfer method)" |
|
788 val content = Item_Net.content o #relator_eq o Data.get |
|
789 in |
|
790 Attrib.setup name (Attrib.add_del add del) text |
|
791 #> Global_Theory.add_thms_dynamic (name, content) |
|
792 end |
|
793 |
|
794 val relator_domain_setup = |
|
795 let |
|
796 val name = @{binding relator_domain} |
|
797 fun add_thm thm context = |
|
798 let |
|
799 val thm = abstract_domains_relator_domain (Context.proof_of context) thm |
|
800 in |
|
801 context |> Data.map (map_relator_domain (Item_Net.update thm)) |> add_transfer_domain_thm thm |
|
802 end |
|
803 fun del_thm thm context = |
|
804 let |
|
805 val thm = abstract_domains_relator_domain (Context.proof_of context) thm |
|
806 in |
|
807 context |> Data.map (map_relator_domain (Item_Net.remove thm)) |> del_transfer_domain_thm thm |
|
808 end |
|
809 val add = Thm.declaration_attribute add_thm |
|
810 val del = Thm.declaration_attribute del_thm |
|
811 val text = "declaration of relator domain rule (used by transfer method)" |
|
812 val content = Item_Net.content o #relator_domain o Data.get |
|
813 in |
|
814 Attrib.setup name (Attrib.add_del add del) text |
|
815 #> Global_Theory.add_thms_dynamic (name, content) |
|
816 end |
|
817 |
|
818 val setup = |
|
819 relator_eq_setup |
|
820 #> relator_domain_setup |
|
821 #> Attrib.setup @{binding transfer_rule} transfer_attribute |
|
822 "transfer rule for transfer method" |
|
823 #> Global_Theory.add_thms_dynamic |
|
824 (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get) |
|
825 #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute |
|
826 "transfer domain rule for transfer method" |
|
827 #> Attrib.setup @{binding transferred} transferred_attribute_parser |
|
828 "raw theorem transferred to abstract theorem using transfer rules" |
|
829 #> Attrib.setup @{binding untransferred} untransferred_attribute_parser |
|
830 "abstract theorem transferred to raw theorem using transfer rules" |
|
831 #> Global_Theory.add_thms_dynamic |
|
832 (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get) |
|
833 #> Method.setup @{binding transfer} (transfer_method true) |
|
834 "generic theorem transfer method" |
|
835 #> Method.setup @{binding transfer'} (transfer_method false) |
|
836 "generic theorem transfer method" |
|
837 #> Method.setup @{binding transfer_prover} transfer_prover_method |
|
838 "for proving transfer rules" |
|
839 |
|
840 end |
|