CODEWITHSUNDEEP
isabelletheorem-proving
Charlie Parker
Charlie Parker

Reputation: 5201

How does one insert values into unknowns in isabelle theorem prover?

I have the following subgoals:

proof (prove)
goal (2 subgoals):
 1. ⋀y. ∃x. P x ⟹ P (?x6 y)
 2. ⋀y. ∃x. P x ⟹ Q (?y8 y) ⟹ Q y

I want to conclude the proof or continue trying stuff but I don't know how to introduce things into the unknowns (schematic variables) i.e variables with ?.

How does one do that?

Upvotes: 2

Views: 304

Answers (2)

Peter Zeller
Peter Zeller

Reputation: 2276

The important parts are already explained by user9716869. I just wanted to add:

You current subgoal is probably not solvable if you don't have additional information available. If you need the x from ∃x. P x to instantiate the schematic variable ?x6 then you need to obtain the value of x before the schematic variable is created.

Schematic variables are instantiated automatically by matching. This works well if the schematic variable is not a function, so you can just continue to write your proof as if the correct value was already there. If you want to fix the value in an apply style proof (other cases are already given in the other answer), you could use subgoal_tac followed by assumption:

lemma "⋀y. ∃x. P x ⟹ ∃x::nat. P x"
  apply (rule exI)
 ― ‹⋀y. ∃x. P x ⟹ P (?x y)›
  apply (subgoal_tac "P 42", assumption)
 ― ‹⋀y. ∃x. P x ⟹ P 42›
  oops ― ‹Not possible to prove›

lemma "⋀y. ∃x. P x ⟹ ∃x::nat. P x"
  apply (erule exE)
 ― ‹⋀y x. P x ⟹ ∃x. P x›
  apply (rule exI)
 ― ‹⋀y x. P x ⟹ P (?x2 y x)›
  apply (subgoal_tac "P x", assumption)
 ― ‹⋀y x. P x ⟹ P x›
  by assumption

Upvotes: 1

user9716869 - supports Ukraine
user9716869 - supports Ukraine

Reputation: 1941

Firstly, it is necessary to understand how schematic variables appeared in your subgoals. Normally, unless you are using schematic_goal, schematic variables appear in the subgoals after some form of rule application, whether implicit or explicit.

  1. If the rule application was explicit (e.g. apply (rule conjunct1)), then a reasonably standard methodology for dealing with the problem that you described is to substitute the variables that you wish to 'try' directly into the rule, e.g. apply (rule conjunct1[of A]). In this case, there will be no schematic variables in your goals and, therefore, the problem implicitly disappears.
  2. If the rule application was implicit (e.g. via one of the tools for classical reasoning), then your options depend on whether the subgoals were generated in an apply script or within the body of an Isar proof. Nonetheless, before I proceed, I would like to mention that the proofs where you have to interact with subgoals generated after the application of any 'black-box' methods are not considered to be a very good style (at least, in my opinion). In the case of the former, there is nothing that you need to do to "try stuff". Once the variable that you wish to substitute (e.g. z) is defined, you can use show "∃x. P x ⟹ P (z y)" in the body of the Isar proof. Similarly, in an apply script, you can resolve with pre-substituted variables.

I demonstrate all these methods in the context of a simplified example below:

context
  fixes A B :: bool
  assumes AB: "A ∧ B"
begin

lemma A by (rule conjunct1[of _ B]) (rule AB)

lemma A 
  by (rule conjunct1) (rule AB)

lemma A 
proof(rule conjunct1)
  show "A ∧ B" by (rule AB)
qed

end

Upvotes: 2

Related Questions