218 |
218 |
219 (*read instantiations with respect to subgoal i of proof state st*) |
219 (*read instantiations with respect to subgoal i of proof state st*) |
220 fun read_insts_in_state (st, i, sinsts, rule) = |
220 fun read_insts_in_state (st, i, sinsts, rule) = |
221 let val thy = Thm.theory_of_thm st |
221 let val thy = Thm.theory_of_thm st |
222 and params = params_of_state i st |
222 and params = params_of_state i st |
223 and rts = types_sorts rule and (types,sorts) = types_sorts st |
223 and rts = Drule.types_sorts rule and (types,sorts) = Drule.types_sorts st |
224 fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm) |
224 fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm) |
225 | types' ixn = types ixn; |
225 | types' ixn = types ixn; |
226 val used = Drule.add_used rule (Drule.add_used st []); |
226 val used = Drule.add_used rule (Drule.add_used st []); |
227 in read_insts thy rts (types',sorts) used sinsts end; |
227 in Drule.read_insts thy rts (types',sorts) used sinsts end; |
228 |
228 |
229 (*Lift and instantiate a rule wrt the given state and subgoal number *) |
229 (*Lift and instantiate a rule wrt the given state and subgoal number *) |
230 fun lift_inst_rule' (st, i, sinsts, rule) = |
230 fun lift_inst_rule' (st, i, sinsts, rule) = |
231 let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule) |
231 let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule) |
232 and {maxidx,...} = rep_thm st |
232 and {maxidx,...} = rep_thm st |
338 |
338 |
339 (*dresolve tactic applies a RULE to replace an assumption*) |
339 (*dresolve tactic applies a RULE to replace an assumption*) |
340 fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); |
340 fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); |
341 |
341 |
342 (*instantiate variables in the whole state*) |
342 (*instantiate variables in the whole state*) |
343 val instantiate_tac = PRIMITIVE o read_instantiate; |
343 val instantiate_tac = PRIMITIVE o Drule.read_instantiate; |
344 |
344 |
345 val instantiate_tac' = PRIMITIVE o Drule.read_instantiate'; |
345 val instantiate_tac' = PRIMITIVE o Drule.read_instantiate'; |
346 |
346 |
347 (*Deletion of an assumption*) |
347 (*Deletion of an assumption*) |
348 fun thin_tac s = eres_inst_tac [("V",s)] thin_rl; |
348 fun thin_tac s = eres_inst_tac [("V",s)] thin_rl; |