Alex Weisberger (Sep 20 2023 at 00:21): Alex Weisberger (Sep 20 2023 at 00:21):I'm working on some proofs of state machine simulation, and came across a surprising rule application failure. The actual lemma isn't so important here, but here it is for completeness:
lemma gen_sim:
fixes I :: "('e, 's) proc" and M :: "('e, 's) proc"
assumes "case (I e s, M e (af s)) of (Some i, Some m) ⇒ af i = m | _ ⇒ False"
shows "simulates af I M e s"
using assms
unfolding simulates_def
by simp
Note that the conclusion is: shows "simulates af I M e s".
The following rule application fails:
lemma
shows "simulates af (compose_local_actions am_i) (compose_local_actions am_m) e s"
apply(rule gen_sim)
Shouldn't the following unifications happen when applying this rule?
I --> (compose_local_actions am_i)
M --> (compose_local_actions am_m)
Instead, I get the dreaded: Failed to apply proof method⌂:.
Alex Weisberger (Sep 20 2023 at 00:34):It seems like this is because of the fixes definitions. The types of the (compose_local_actions ..) terms don't necessarily unify to the same type. The rule application works fine I remove fixes from the lemma.
Mathias Fleury (Sep 20 2023 at 05:00):If the fixes causes the issues, then it is a type problem and your type specification is too weak
Mathias Fleury (Sep 20 2023 at 05:01):I would try
supply [[unify_trace_failure]]
apply(rule gen_sim)
to get an error message
Last updated: Dec 21 2024 at 12:33 UTC