Re: [isabelle] Equal on function objects



Thanks for the help. Just curious, what if loc.ax1 is changed to:

"EX p. func1 p ~= func2 p / func3 p"

Can auto/blast intro: ext still be used to show that

"func1 ~= func2 / func3"?

In fact, why isn't ext defined with iff instead, i.e.:

lemma ext: "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) <==> (%x. f(x))=(%x. g(x))"

Thanks again.

John

On Mon, Feb 22, 2010 at 9:30 AM, Andreas Lochbihler
<andreas.lochbihler at kit.edu> wrote:
> Hi John,
>
>> lemma (in loc) lem1: "ALL p. func2 p = func1 p * func3 p"
>>  using ax1 ax2
>>  by (metis divide_le_eq divide_less_eq order_eq_refl order_less_irrefl
>> xt1(11))
>>
>> lemma (in loc) lem2:
>>  assumes "loc"
>>  shows "func2 = (%s. func1 s * func3 s)"
>>  using lem1
>>  by auto
>>
>> Does anyone know why having lem1 as a fact is insufficient to complete
>> the proof?
>
> You must tell auto explicitly to use function extensionality. Both
>
> by(auto intro: ext)
>
> and
>
> by(auto simp: expand_fun_eq)
>
> work for your example lemma. expand_fun_eq is more aggressive because it
> also works on the assumptions.
>
> Best regards,
> Andreas
>
> --
> Karlsruher Institut für Technologie
> IPD Snelting
>
> Andreas Lochbihler
> wissenschaftlicher Mitarbeiter
> Adenauerring 20a, Gebäude 50.41, Raum 023
> 76131 Karlsruhe
>
> Telefon: +49 721 608-8352
> Fax: +49 721 608-8457
> E-Mail: andreas.lochbihler at kit.edu
> http://pp.info.uni-karlsruhe.de
> KIT - Universität des Landes Baden-Württemberg und nationales
> Großforschungszentrum in der Helmholtz-Gemeinschaft
>





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