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)


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,

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