CODEWITHSUNDEEP
isabelle
Gergely
Gergely

Reputation: 7525

Recognising that a subgoal is proved

I would like to understand the state machine of the Isar Virtual Machine.

Page 48 of Markus Wenzel's doctoral thesis gives a good overview but does not detail its messages in the Output panel. It might well be a later addendum to the system.

I have a simple Isar proof:

theory Propositional
imports Main
begin

lemma nj2: assumes p: P and q: Q shows "P ∧ (Q ∧ P)"
proof - 
  from q p have qp: "Q ∧ P" by (rule conjI)
  from p qp show "P ∧ (Q ∧ P)" by (rule conjI)
qed

after the second by (rule conjI) the Output panel says

show (P::bool) /\ (Q::bool) /\ P 
Successful attempt to solve goal by exported rule:
  (P::bool) /\ (Q::bool) /\ P 
proof (state): depth 0

this:
  (P::bool) /\ (Q::bool) /\ P

goal:
No subgoals!
variables:
  P, Q :: bool

so it explicitly recognizes the solution of the goal. However, at the first by (rule conjI) it says

have qp: (Q::bool) /\ (P::bool) 
proof (state): depth 0

this:
  (Q::bool) /\ (P::bool)

goal (1 subgoal):
 1. P /\ Q /\ P
variables:
  P, Q :: bool

I see no sign that the subgoal has been proved. Or, the fact that the have statement is the same as in the this register should remind me that it is proved?

Upvotes: 0

Views: 133

Answers (1)

Mathieu
Mathieu

Reputation: 746

Well, the subgoals in the output panel correspond to the subgoals of the context. In this case, the context is the one of the complete lemma, beginning with proof -. In this context, there is only one subgoal, which is the lemma to be proved.

When you state your intermediate property with have, the system doesn't verify anything with respect to the goals, and once it's proved, it just gives you access to this property (through the names this and qp) because you have proved it with by (rule conjI) and the fact that there is no error means that it is proved.

On the other hand, when you state a property with show, the system verifies that this property with the eventual assumptions you've made (with assume) actually corresponds to one of the subgoals, and fails otherwise.

When it arrives to the qed command, it finally verifies that all the subgoals of the context have been proved.

Another way to write this proof is like this (I didn't checked it worked, but it should...) :

theory Propositional
imports Main
begin

lemma nj2: assumes p: P and q: Q shows "P ∧ (Q ∧ P)"
proof (rule conjI)
  from p show P by assumption
next
  from q p show "Q ∧ P" by (rule conjI)
qed

In this case, proof (rule conjI) creates 2 subgoals P and Q ∧ P and the Output panel should confirm this.

Upvotes: 2

Related Questions