[isabelle-dev] Isabelle/HOL axiom ext is redundant

Brian Huffman brianh at cs.pdx.edu
Wed Nov 11 18:46:01 CET 2009

```Hello all,

This morning I was looking at the following comment from HOL.thy:

ext:            "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
-- {*Extensionality is built into the meta-logic, and this rule expresses
a related property.  It is an eta-expanded version of the traditional
rule, and similar to the ABS rule of HOL*}

Then I was wondering exactly how this axiom was related to the
"extensionality built into the meta-logic". After looking into it, I
discovered that I could actually prove the "ext" axiom as a theorem. I
would suggest that we add lemma "meta_ext" to Pure.thy, and then put a
proof of rule "ext" in HOL.thy.

- Brian

lemma meta_ext:
fixes f g :: "'a::{} => 'b::{}"
shows "(!!x. f x == g x) ==> (%x. f x) == (%x. g x)"
by (tactic {*
let
val a = @{cterm "!!x. f x == g x"};
val t = @{cterm "t::'a"};
val thm1 = Thm.forall_elim t (Thm.assume a);
val thm2 = Thm.abstract_rule "x" t thm1;
val thm3 = Thm.implies_intr a thm2;
in
rtac thm3 1
end
*})

lemma ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
apply (rule meta_eq_to_obj_eq)
apply (rule meta_ext)
apply (rule eq_reflection)
apply (erule meta_spec)
done

```