Re: [isabelle] Printing instantiations

Hi Steve,

> How come the 'default proof' can't try to instantiate 'F' to 'f' and 'x' to
> 'd'? I presume there are no rules declared in the current context of this
> proof and of your proof, so what exactly does '..' or 'by rule' actually
> apply here and in your proof?

The ".." proof indeed defaults to (rule exI) in the example.  But rule
does only perform one resolution step, hence you have to apply it twice.
 Here the proof is given by an apply scripts:

axiomatization f :: "real => real" and d :: real where
  ax1: "f d = 0"

lemma test1: "EX (F::real=>real) x. F x = 0"
apply (rule exI)
apply (rule exI)
apply (rule ax1)

In Isar the matter is a little bit difficult: we cannot write

from `EX x. ...` have `EX y x. ...`

since the "EX x. ..." fact would trigger existential elimination.  So we
must write it as backward proof:

lemma test2: "EX (F::real=>real) x. F x = 0"
proof -
  from ax1 have *: "EX x. f x = 0" by (rule exI)
  show ?thesis by (rule exI) (rule *)

This looks not so beautiful but in practice such chained existential
introduction would be accomplished e.g. by blast.

The details can be found in the tutorial, chapter "The rules of the game".

> But doesn't Isabelle support polymorphism? If so, types shouldn't need to be
> explicitly declared, right?

These are two different things: polymorphism vs. type inference.  Type
inference assigns most general types, which may be more general than
actually wanted.

Hope this helps,



PGP available:

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