CODEWITHSUNDEEP
isabelle
thor
thor

Reputation: 22460

Is there a way to name and refer to a assumption in Isabelle apply-scripts?

Is there any way in Isabelle (2021) to refer to assumptions in the old apply style proofs?

In particular, I am interested in using the assumptions as facts in the OF operator so that I can do (hypothetically):

apply(rule R[OF assm1  assm4])

, where assm1 and assm4 should refer to the 1st and 4th assumptions in the current proof state.

Often times, I can arrange assumptions of the current sugboal so that R[OF assm1 assm4] is the same as the subgoal. But then, I can't finish the proof because I don't know how to refer to assm1 assm4 etc. It seems that only global theorem names are allowed with OF.

I even tried to use the subgoal_tac method on the assumptions, but it does not seem to have an option of giving names to the fact.

In the end, I have to use an automatic script such as simp, which is somewhat opaque for something so obvious. By the way, this is for learning purposes. I tried setting up simp_trace, but still couldn't replicate the effect without using simp.

Moreover,

If there is no way to refer to assumptions, is this a limitation of the tactics or a fundamental limitation of natural deduction? (i.e. Is the rewriting style of R[OF assm1 assm4] not compatible with natural deduction?)

Upvotes: 0

Views: 236

Answers (1)

Mathias Fleury
Mathias Fleury

Reputation: 2261

The whole point is Isar is that you can name assumptions...

The first low-level solution is to use drule (or frule to keep the assumptions).

Here is an example:

lemma
  assumes ‹⋀x y. P x ⟹ Q y ⟹ R z› ‹P x› ‹Q y›
  shows ‹R z›
  using assms(2-) apply -
  apply (drule assms(1))
  apply assumption
  apply assumption
  done

Look at Chapter 5 for details on the destruction/elimination/intro rules.

The second solution is subgoal:

lemma
  assumes ‹⋀x y. P x ⟹ Q y ⟹ R z› ‹P x› ‹Q y›
  shows ‹R z›
  using assms(2-) apply -
  subgoal premises p
    by (rule assms(1)[OF p])
  done

but this creates hard-to-read proofs if you have very deep nesting.

The third and best solution is to use Isar proofs…

Here is a version that completely avoids using names:

lemma
  assumes ‹⋀x y. P x ⟹ Q y ⟹ R z› ‹P x› ‹Q y›
  shows ‹R z›
  using assms apply -
  apply (elim meta_allE[of _ x])
  apply (elim meta_allE[of _ y])
  apply (drule cut_rl)
   apply assumption  
  apply (drule cut_rl)
   apply assumption  
  apply assumption
  done

You can see how ugly this is and why you should avoid that.

Upvotes: 3

Related Questions