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

Tobias Nipkow nipkow at in.tum.de
Wed Nov 11 21:39:07 CET 2009

Hi Brian,

When I defined HOL and put in "ext", "eq_reflection" did not exist and
hence I could not derive "ext". Now we can. But this relies on
"eq_reflection", which is admissible, but I only added it to make the
simplifier work better and don't want to rely on it if it can be helped.

But thanks for pointing it out.


Brian Huffman schrieb:
> 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
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list