Extract explicit value from Isabelle proof

Question

How can I extract an explicit value for a schematic variable in Isabelle after using it in a proof? For example, in the following goal, I’m looking to extract a numerical value for ?solution, e.g. ?solution = 5:

schematic_goal test:
  assumes “x = 3” and “y = 2"
  shows “?solution = x + y”

The following proof works, but doesn’t provide a numerical value for ?solution. Isabelle seems content with ?solution = x + y without further simplification.

proof -
  show “x + y = x + y” using assms by auto
qed

I’ve also experimented with using existentials but didn’t seem to get anywhere with that either. Is this possible to achieve?

In the more general case, if I don’t know the exact form of the answer, how can I force a proof to provide a closed-form solution for an unknown target variable? (And is there an easy way to specify the “closed-form solution” requirement in Isabelle?)

Note that I’m not necessarily asking Isabelle to compute the answer, just enforcing that the proof won’t go through unless an explicit value is either provided or computed.

Answer 1

The value of ?solution in a schematic_goal-theorem depends on the proof.

schematic_goal test:
  assumes ‹x = 3› and ‹y = 2›
  shows ‹?solution = x + y›
  by simp

...leads to output:

theorem test:
 ?x = 3 ⟹ ?y = 2 ⟹ ?x + ?y = ?x + ?y 
goal instantiation:
    ?solution ↝ x + y

This tells us that ?solution is instantiated to x + y, which already suffices for the proof to go through. But the theorem is quite boring: The conclusion does not depend on the assumptions at all. For schematic_goal theorems, the proof matters. So the proof is where we have to look to understand the problem.

In Isabelle, the assumptions of the assumes-block are not automatically fed to the first proof method invocation. (A classic trap for beginning Isabelle users.) Thus, the proof state on which the simplifier is called is just 1. ?solution = x + y . Without knowledge about x and y, the instantiation of ?solution to x + y really is the best one can do!

The trick to add the knowledge on x and y to the proof is simple: Write using assms, where assms refers to the set of assumptions of the current theorem/lemma.

schematic_goal test:
  assumes ‹x = 3› and ‹y = 2›
  shows ‹?solution = x + y›
  using assms
  by simp

This proof with more knowledge indeed leads to a different instantiation of ?solution and a more specific theorem. The output reads:

theorem test:
 ?x = 3 ⟹ ?y = 2 ⟹ 5 = ?x + ?y 
goal instantiation:
    ?solution ↝ 5 

I guess this is what you've been looking for.