Re: [isabelle] Eliminating two quantifiers in structural proof



On Sun, 16 Sep 2012, Alfio Martini wrote:

I am not sure if this is what you what, but in Isar is fairly natural to do
such proofs. I use it to teach natural deduction to students.
Here goes three proofs of this conjecture:

theorem th11a:
  assumes prem: "∀x. ∀y. P x y"
  shows "P a b"
    proof -
      from prem have "∀y. P a y" by (rule spec)
      thus "P a b" by (rule spec)
    qed

theorem th11b:
  assumes prem: "∀x. ∀y. P x y"
  shows "P a b"
    proof -
      from prem have "∀y. P a y" by (rule allE)
      thus "P a b" by (rule allE)
    qed

theorem th11c:
  assumes prem: "∀x. ∀y. P x y"
  shows "P a b"
    proof -
      from prem have "∀y. P a y" by (rule spec[where x =a])
      from this show  "P a b" by (rule spec[where x=b])
    qed

I assume you hardly have to use the qualifieres (e(limination), d(estruction)) when working in Isar. I use this style only when I am playing with linear scripts.

This is an important observation. The "erule" and "drule" rule application forms are never required in structure proof. Instead you indicate the forward deduction explicitly via the 'then' language element, and then just use a normal "rule" step, which is often not spelled out but left implicit.

Roughly speaking a tactic script with "apply (erule r)" corresponds to an Isar proof text fragment "then show proof (rule r)", and "apply (drule r)" corresponds to "then have proof (rule r)".

Note that the abbreviations "thus == then show" and "hence == then have" are merely historical accidents. They require fewer bytes in memory, but more typing by the user and more explanations to newcomers. The reason is that the chaining or not chaining for elementary 'show' and 'have' elements are often changed during the proof development. And there are further combinators like 'also' and 'moreover' that can be combined with 'have' or 'show', and other goal elements like 'obtain' that can participate in the chaining of facts in the same manner.

So there is a large combinatorial space of

  (then | from | with | ... | also | finally | moreover | ultimately)
    (have | show | obtain | interpret ...)

which is better spelled out as such explicitly, without the somewhat pointless shortcuts 'hence' and 'thus' getting in the way.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.