269 | _ => Seq.empty |
269 | _ => Seq.empty |
270 end |
270 end |
271 handle Subscript => Seq.empty |
271 handle Subscript => Seq.empty |
272 |
272 |
273 val supports_fresh_rule = thm "supports_fresh"; |
273 val supports_fresh_rule = thm "supports_fresh"; |
|
274 val fresh_def = thm "Nominal.fresh_def"; |
|
275 val fresh_prod = thm "Nominal.fresh_prod"; |
|
276 val fresh_unit = thm "Nominal.fresh_unit"; |
274 |
277 |
275 fun fresh_guess_tac tactical ss i st = |
278 fun fresh_guess_tac tactical ss i st = |
276 let |
279 let |
277 val goal = List.nth(cprems_of st, i-1) |
280 val goal = List.nth(cprems_of st, i-1) |
278 in |
281 in |
291 val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule; |
294 val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule; |
292 val _ $ (_ $ S $ _) = |
295 val _ $ (_ $ S $ _) = |
293 Logic.strip_assums_concl (hd (prems_of supports_fresh_rule')); |
296 Logic.strip_assums_concl (hd (prems_of supports_fresh_rule')); |
294 val supports_fresh_rule'' = Drule.cterm_instantiate |
297 val supports_fresh_rule'' = Drule.cterm_instantiate |
295 [(cert (head_of S), cert s')] supports_fresh_rule' |
298 [(cert (head_of S), cert s')] supports_fresh_rule' |
296 val fresh_def = thm "Nominal.fresh_def"; |
299 val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit] |
297 val fresh_prod = thm "Nominal.fresh_prod"; |
300 val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites.emptyI] |
298 val fresh_unit = thm "Nominal.fresh_unit"; |
301 (* FIXME sometimes these rewrite rules are already in the ss, *) |
299 val simps = [symmetric fresh_def,fresh_prod,fresh_unit] |
302 (* which produces a warning *) |
300 in |
303 in |
301 (tactical ("guessing of the right set that supports the goal", |
304 (tactical ("guessing of the right set that supports the goal", |
302 EVERY [compose_tac (false, supports_fresh_rule'', 3) i, |
305 EVERY [compose_tac (false, supports_fresh_rule'', 3) i, |
303 asm_full_simp_tac (ss addsimps simps) (i+2), |
306 asm_full_simp_tac ss1 (i+2), |
304 asm_full_simp_tac ss (i+1), |
307 asm_full_simp_tac ss2 (i+1), |
305 supports_tac tactical ss i])) st |
308 supports_tac tactical ss i])) st |
306 end |
309 end |
307 | _ => Seq.empty |
310 | _ => Seq.empty |
308 end |
311 end |
309 handle Subscript => Seq.empty |
312 handle Subscript => Seq.empty |