Stream: Beginner Questions

Topic: Show inductive hyps in state

view this post on Zulip 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?

view this post on Zulip Lukas Stevens (Mar 24 2021 at 09:27):

What exactly do you mean by hyps?

view this post on Zulip Lukas Stevens (Mar 24 2021 at 09:28):

A code sample with an explanation of what you expected would be great.

view this post on Zulip 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.

view this post on Zulip Lukas Stevens (Mar 24 2021 at 17:19):

To clarify, you need an explicit using assms before the proof (induction ys).

Last updated: Nov 13 2025 at 04:27 UTC