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⌂:.
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.
If the fixes causes the issues, then it is a type problem and your type specification is too weak
I would try
supply [[unify_trace_failure]] apply(rule gen_sim)
to get an error message
Last updated: Dec 07 2023 at 08:19 UTC