[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
More information about the isabelle-dev
mailing list