How do you print local variables and ?thesis in an Isabelle proof (debugging in Isabelle)?

Question

I sometimes find it hard to use Isabelle because I cannot have a "print command" like in normal programming.

For example, I want to see what ?thesis. The concrete semantics book says:

The unknown ?thesis is implicitly matched against any goal stated by lemma or show. Here is a typical example:

My silly sample FOL proof is:

lemma
  assumes "(∃ x. ∀ y. x ≤ y)"
  shows "(∀x. ∃ y. y ≤ x)"
proof (rule allI)
  show ?thesis

but I get the error:

proof (state)
goal (1 subgoal):
 1. ⋀x. ∃y. y ≤ x 
Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  ∀x. ∃y. y ≤ x

but I do know why.

I expected

?thesis === ⋀x. ∃y. y ≤ x

since my proof state is:

proof (state)
goal (1 subgoal):
 1. ⋀x. ∃y. y ≤ x

Why can't I print ?thesis?

It's really annoying to have to write the statement I'm trying to proof if it's obvious. Perhaps it's meant to be explicit but in the examples in chapter 5 they get away with using ?thesis in:

lemma fixes a b :: int assumes "b dvd (a+b)" shows "b dvd a" proof −
have "∃k′. a = b∗k′" if asm: "a+b = b∗k" for k proof
show "a = b∗(k − 1)" using asm by(simp add: algebra_simps) qed
then show ?thesis using assms by(auto simp add: dvd_def ) qed

but whenever I try to use ?thesis I always fail.

Why is it?

Note that this does work:

lemma
  assumes "(∃ x. ∀ y. x ≤ y)"
  shows "(∀x. ∃ y. y ≤ x)"
proof (rule allI)
  show "⋀x. ∃y. y ≤ x" proof -

but I thought ?thesis was there to avoid this.

---

Also, thm ?thesis didn't work either.

---

Another example is when I use:

let ?ys = take k1 xs

but I can't print ?ys value.

---

TODO:

why doesn't:

lemma "length(tl xs) = length xs - 1"
  thm (cases xs)

show anything? (same if your replaces cases with induction).

Answer 1

You can find ?theorem and others in the print context window:

As for why ?thesis doesn't work, by applying the introduction rule proof (rule allI) you are changing the goal, so it no longer matches ?thesis. The example in the book uses proof- which prevents Isabelle from applying any introduction rule.

Answer 2

It seems I asked a very similar question worth pointing to: What is the best way to search through general definitions, theorems, functions, etc for Isabelle?

But here is a list of thing's I've learned so far:

• thm: seems to work for definition, lemmas and functions. For definition do name_def for a definition with name name. For functions do thm f.simps for all definitions in the function. For a single one do thm f.simps(1) for the first one. For lemmas do thm lemma_name or thm impI or HOL.mp etc.
• term: for terms do term term_name e.g. in isar term ?thesis or term this
• print_theorems: if you place this after a definition or a function it shows all the theorems defined for those! It's amazing.
• print... I just noticed in jedit if you let the auto complete show you the rest for print it has a bunch of options! Probably useful!
• Search engine for Isabelle: https://search.isabelle.in.tum.de/
• You can use Query (TODO: improve this)
• TODO: how to find good way to display stuff about tactics.

I plan to update this as I learn all the ways to debug in Isabelle.