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)
done

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 *)
qed

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,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de





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