Email Gateway (Aug 22 2022 at 12:58): Email Gateway (Aug 22 2022 at 12:58):From: Diego Machado Dias <diegodias.m@gmail.com>
I am working with a theory where the application of certain rule fails when
placed in the middle of a larger proof, but if I declare a new theorem
containing exactly the problematic sub goal (where the application fails),
then Isabelle allows me to apply the rule I want in the proof of the new
theorem.
Originally, I suspected this was caused by some type mismatch, and I
enabled types in the output to investigate if the types match. They do. I
didn't find anything that makes the goal in the larger proof different from
its copied and pasted version used to create a new theorem.
Is there any way of extracting more information from Isabelle about the
reason that causes the application of a rule to fail?
Thanks,
Diego
Email Gateway (Aug 22 2022 at 12:58):From: Lars Hupel <hupel@in.tum.de>
Hi Diego,
Is there any way of extracting more information from Isabelle about the
reason that causes the application of a rule to fail?
try this:
using [[unify_trace_failure]]
apply (rule ...)
Then, you'll find the output like the following:
Clash: Scratch.P =/= Scratch.Q
Hope that helps.
Cheers
Lars
Email Gateway (Aug 22 2022 at 12:58):From: Diego Machado Dias <diegodias.m@gmail.com>
Hi Lars,
The clash information I get is this: "Lattices.sup_class.sup =/=
Set.insert".
It understood that it has to do with the usage of sets, but I will need to
find out
how this message can help me. Does this clash message ring a bell for you?
Thanks for you help!
Diego
Email Gateway (Aug 22 2022 at 12:58):From: Peter Lammich <lammich@in.tum.de>
Hi Diego,
it's quite obvious what happened here:
look at the theorem:
thm Law_Frame_Monotonic_Refinement
?c ⊑[?r] ?d ⟹ ?Y❙:?c ⊑[?r] ?Y❙:?d
it requires exactly (syntactically) the same ?Y on both sides. However,
contrary to your comment in the theory file, the actual subgoal looks
like:
({''oc''} ∪ {''ot''})❙:(❙r❙e❙l❙y ?rx3 ∙ ❙[true,true❙] [idrel]) ⊑[true]
{''oc'', ''ot''}❙:(❙r❙e❙l❙y true ∙ ❙[true,true❙] [idrel])
Note the subtle difference between {''oc''} ∪ {''ot''}
and {''oc'', ''ot''}.
The simp-call rewrites the {_}\<union>{_} to {_,_},
and then the rule works.
Hope this helps,
Peter
p.s.: Isabelle sees {a,b} as "insert a (insert b {})", while it
sees {a} \union {b} as "sup (insert a {}) (insert b {})". These are
semantically equal, but cannot be unified syntactically.
Last updated: Apr 26 2024 at 12:28 UTC