Jan van Brügge (Mar 10 2022 at 13:23): Jan van Brügge (Mar 10 2022 at 13:23):Is there a tactic that works like resolve_tac, but only does the unification and not solve the goal yet? The rule I want to resolve with has variables in the assumptions that are not part of the conclusion and I want to instantiate them with id. To do that I would first need to fix all variables that are used in the goal (i.e. do unification). If I don't do this I end up with a goal like prems ==> bij (?f3 <all forall bound variables>) which isabelle refuses to unify with id if i try to apply bij_id
Dmitriy Traytel (Mar 10 2022 at 14:20):If bij_id is not applicable to this goal, then the type of ?f3 must not unify with ?'a => ?'a.
Mathias Fleury (Mar 10 2022 at 14:21):To some extend using supply [[unify_trace_failure]] gives an error message that helps finding out why goals do not unify
Jan van Brügge (Mar 10 2022 at 14:24):I am not sure why, but replacing TRYALL (resolve_tac ctxt @{thms bij_id} ORELSE' assume_tac ctxt) with REPEAT_DETERM (resolve_tac ctxt @{thms bij_id} 1 ORELSE assume_tac ctxt 1) works? Wat?
Dmitriy Traytel (Mar 10 2022 at 14:29):TRYALL starts with the last subgoal, whereas REPEAT_DETERM with the first. Since you have schematic variables in your goals, the order can matter.
Jan van Brügge (Mar 10 2022 at 14:31):Ah, yes there were two kinds of goals that were still schematic and the bij goal just happend to be the one that failed. Adding more theorems to the resolve tac to cover the other kinds, makes it work with TRYALL too.
Notification Bot (Mar 10 2022 at 14:31):Jan van Brügge has marked this topic as resolved.
Last updated: Dec 21 2024 at 12:33 UTC