255 i : number of subgoal the tactic should be applied to |
255 i : number of subgoal the tactic should be applied to |
256 *****************************************************************************) |
256 *****************************************************************************) |
257 |
257 |
258 fun split_tac [] i = no_tac |
258 fun split_tac [] i = no_tac |
259 | split_tac splits i = |
259 | split_tac splits i = |
260 let fun const(thm) = let val _$(t as _$lhs)$_ = concl_of thm |
260 let fun const(thm) = |
261 val (Const(a,_),args) = strip_comb lhs |
261 (case concl_of thm of _$(t as _$lhs)$_ => |
262 in (a,(thm,fastype_of t,length args)) end |
262 (case strip_comb lhs of (Const(a,_),args) => |
|
263 (a,(thm,fastype_of t,length args)) |
|
264 | _ => error("Wrong format for split rule")) |
|
265 | _ => error("Wrong format for split rule")) |
263 val cmap = map const splits; |
266 val cmap = map const splits; |
264 fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st |
267 fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st |
265 fun lift_split_tac st = st |> |
268 fun lift_split_tac st = st |> |
266 let val (Ts,t,splits) = select cmap st i |
269 let val (Ts,t,splits) = select cmap st i |
267 in case splits of |
270 in case splits of |