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

[Tobias Nipkow]

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.

Tobias

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