Re: [isabelle] Equal on function objects



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.