441 fun IHinst tac rls = SUBGOAL (fn (Bi,i) => |
441 fun IHinst tac rls = SUBGOAL (fn (Bi,i) => |
442 let val bvs = bvars Bi [] |
442 let val bvs = bvars Bi [] |
443 val ihs = filter could_IH (Logic.strip_assums_hyp Bi) |
443 val ihs = filter could_IH (Logic.strip_assums_hyp Bi) |
444 val rnames = map (fn x=> |
444 val rnames = map (fn x=> |
445 let val (a,b) = get_bno [] 0 x |
445 let val (a,b) = get_bno [] 0 x |
446 in (List.nth(bvs,a),b) end) ihs |
446 in (nth bvs a, b) end) ihs |
447 fun try_IHs [] = no_tac |
447 fun try_IHs [] = no_tac |
448 | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs) |
448 | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (nth rls (y - 1)) i ORELSE (try_IHs xs) |
449 in try_IHs rnames end) |
449 in try_IHs rnames end) |
450 |
450 |
451 fun is_rigid_prog t = |
451 fun is_rigid_prog t = |
452 case (Logic.strip_assums_concl t) of |
452 case (Logic.strip_assums_concl t) of |
453 (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) => null (Term.add_vars a []) |
453 (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) => null (Term.add_vars a []) |