Max Nowak (Mar 24 2021 at 01:42): Max Nowak (Mar 24 2021 at 01:42):I'm trying to do some proofs about my own inductive predicates. When I put my cursor over then show ?case, not all hyps are shown in the Output window below. Can I view them nonetheless somehow?
Lukas Stevens (Mar 24 2021 at 09:27):What exactly do you mean by hyps?
Lukas Stevens (Mar 24 2021 at 09:28):A code sample with an explanation of what you expected would be great.
Mathias Fleury (Mar 24 2021 at 10:09):Do you mean that in something like that:
lemma
fixes xs ys :: ‹'a list›
assumes ‹P xs›
shows ‹Q ys›
proof (induction ys)
case Nil
then show ?case sorry
next
case (Cons a ys)
then show ?case sorry
qed
you don't see the P xs? If so that is expected. Isabelle shows only the fact that are threaded.
Lukas Stevens (Mar 24 2021 at 17:19):To clarify, you need an explicit using assms before the proof (induction ys).
Last updated: Dec 21 2024 at 16:20 UTC