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

[Brian Huffman]

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