Re: [isabelle] Eliminating two quantifiers in structural proof



On Sun, 16 Sep 2012, Alfio Martini wrote:

Forgot this one:

theorem th11d:
  "∀x. ∀y. P x y ==> P a b"
    proof -
      assume  "∀x. ∀y. P x y"
      from this have "∀y. P a y" by (rule spec[where x =a])
      from this show  "P a b" by (rule spec[where x=b])
    qed

Yet more examples on this thread, using native natural deduction statements in Isabelle/Pure, without any auxiliary HOL connectives getting in the way:

lemma
  assumes "⋀x y. P x y"
  shows "P a b"
proof -
  from `P a b` show ?thesis .
qed

Using the Pure quantifier in the assumption, you get arbitrary instances of the proposition for free, using unification behind the scenes. The backquote notation is a "literal fact reference", stating an instance of something you have already visibly in the proof context.


Here is the same, without the initial goal statement getting between you and the understanding of natural deduction reasoning in a local context:

notepad
begin

  assume "⋀x y. P x y"

  note `P a b`

  have "P a b" by fact
end

So you build up a context with some general fact, and then project instances from it. The backquote and "by fact" form are operationally equalivalent, but the latter works via a local result with nested goal state. Both forms have there uses in practical applications.


	Makarius


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