288 | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs); |
288 | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs); |
289 |
289 |
290 fun finite_guess_tac tactical ss i st = |
290 fun finite_guess_tac tactical ss i st = |
291 let val goal = List.nth(cprems_of st, i-1) |
291 let val goal = List.nth(cprems_of st, i-1) |
292 in |
292 in |
293 case Logic.strip_assums_concl (term_of goal) of |
293 case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of |
294 _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) => |
294 _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) => |
295 let |
295 let |
296 val cert = Thm.cterm_of (Thm.theory_of_thm st); |
296 val cert = Thm.cterm_of (Thm.theory_of_thm st); |
297 val ps = Logic.strip_params (term_of goal); |
297 val ps = Logic.strip_params (term_of goal); |
298 val Ts = rev (map snd ps); |
298 val Ts = rev (map snd ps); |
299 val vs = collect_vars 0 x []; |
299 val vs = collect_vars 0 x []; |
300 val s = Library.foldr (fn (v, s) => |
300 val s = Library.foldr (fn (v, s) => |
301 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) |
301 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) |
302 (vs, HOLogic.unit); |
302 (vs, HOLogic.unit); |
303 val s' = list_abs (ps, |
303 val s' = list_abs (ps, |
304 Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s); |
304 Const ("Nominal.supp", fastype_of1 (Ts, s) --> |
|
305 snd (split_last (binder_types T)) --> HOLogic.boolT) $ s); |
305 val supports_rule' = Thm.lift_rule goal supports_rule; |
306 val supports_rule' = Thm.lift_rule goal supports_rule; |
306 val _ $ (_ $ S $ _) = |
307 val _ $ (_ $ S $ _) = |
307 Logic.strip_assums_concl (hd (prems_of supports_rule')); |
308 Logic.strip_assums_concl (hd (prems_of supports_rule')); |
308 val supports_rule'' = Drule.cterm_instantiate |
309 val supports_rule'' = Drule.cterm_instantiate |
309 [(cert (head_of S), cert s')] supports_rule' |
310 [(cert (head_of S), cert s')] supports_rule' |