What are the semantics of assume for Isabelle/Isar?

4
votes

I found a surprising behaviour (for me) when using Isar. I try to use assume and sometimes Isar complains it cannot resolve pending goals, for example my most typical example is having a an assumption and not being able to assume it:

lemma 
  assumes "A"
  shows "A"
proof -
  assume "A"
  from this show "A" by (simp)
qed

though the following does work:

lemma 
  shows "A⟹A"
proof -
  assume "A"
  from this show "A" by simp
qed

which is not terribly surprising.

But the next one is surprising to me that it works given that my first example failed:

lemma 
  assumes "A"
  shows "A"
proof -
  have "A" by (simp add: assms)
  from this show "A" by (simp)
qed

why is the first one different from the second one?

Error msg:

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (A) ⟹ A
1
isabelletheorem-provingisar

1 Answers

4
votes

You can find an answer in "Chapter 6: Proofs" of the document Isar-ref. Ideally, you wish to read through the introduction to the chapter, as well as sections 6.1 and 6.2 to fully resolve your concerns. Below, I present the most relevant passages:

The logical proof context consists of fixed variables and assumptions.

...

Similarly, introducing some assumption χ has two effects. On the one hand, a local theorem is created that may be used as a fact in subsequent proof steps. On the other hand, any result χ ⊢ φ exported from the context becomes conditional wrt. the assumption: ⊢ χ ==> φ. Thus, solving an enclosing goal using such a result would basically introduce a new subgoal stemming from the assumption. How this situation is handled depends on the version of assumption command used: while assume insists on solving the subgoal by unification with some premise of the goal, presume leaves the subgoal unchanged in order to be proved later by the user.

Let us look at your first example:

lemma 
  assumes "A"
  shows "A"
proof -
  assume "A"
  from this show "A" by (simp)
qed

There is only one subgoal with no premises: A. Given that there are no premises, 'unification with premises' is inapplicable.

In the second example,

lemma 
  shows "A⟹A"
proof -
  assume "A"
  from this show "A" by simp
qed

the subgoal is A⟹A with the premise A. Thus, you can use assume: unification can be performed.

Lastly,

lemma 
  assumes "A"
  shows "A"
proof -
  have "A" by (simp add: assms)
  from this show "A" by (simp)
qed

is different from the previous cases, because you do not introduce any assumptions. Therefore, you can use show to discharge the subgoal. It should be noted that from this show "A" by (simp) is identical to from assms show "A" by simp or, better yet, from this show "A".:

lemma 
  assumes "A"
  shows "A"
proof -
  from assms show "A".
qed