Re: [isabelle] Printing instantiations



On Fri, Jun 18, 2010 at 8:13 AM, Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de> wrote:

> Hi Steve,
>
> how automated proof tools actually accomplish the proof is somehow
> magic; if you want to specify single proof steps explicitly, restrict
> yourself to proper Isar proofs with methods rule, default etc., see also
> the tutorial on Isar.  For your example, this could read e.g.
>
> definition c :: real where
>  ax1: "c = 0"
>
> lemma test: "EX x::real. x = 0"
> proof -
>  from ax1 show "EX x::real. x = 0" ..
> qed
>

Thanks. Indeed. If I have something slightly less trivial:

consts
f :: "real => real"
d :: real

axioms
ax1: "f d = 0"

lemma test: "EX (F::real=>real) x. F x = 0"
proof -
 from ax1 show ?thesis
   ..

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?


>
> Note also that auto won't ever use ax1 in your proof: you need a type
> constraint on the existential x, otherwise ax1 is not sufficient.
>

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

Thanks again.
Steve


> 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.