# HG changeset patch
# User haftmann
# Date 1246980086 -7200
# Node ID c3844c4d0c2cad639d0cc682303fc98ce942b71e
# Parent  9787769764bb3a128543f676239c974419f21cd5
more accurate certificates for constant aliasses

diff -r 9787769764bb -r c3844c4d0c2c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jul 07 07:56:24 2009 +0200
+++ b/src/HOL/HOL.thy	Tue Jul 07 17:21:26 2009 +0200
@@ -1869,7 +1869,27 @@
 declare simp_thms(6) [code nbe]
 
 setup {*
-  Code.add_const_alias @{thm equals_eq}
+  Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
+*}
+
+lemma equals_alias_cert: "OFCLASS('a, eq_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> eq)" (is "?ofclass \<equiv> ?eq")
+proof
+  assume "PROP ?ofclass"
+  show "PROP ?eq"
+    by (tactic {* ALLGOALS (rtac (Drule.unconstrainTs @{thm equals_eq})) *}) 
+      (fact `PROP ?ofclass`)
+next
+  assume "PROP ?eq"
+  show "PROP ?ofclass" proof
+  qed (simp add: `PROP ?eq`)
+qed
+  
+setup {*
+  Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>eq \<Rightarrow> 'a \<Rightarrow> bool"})
+*}
+
+setup {*
+  Code.add_const_alias @{thm equals_alias_cert}
 *}
 
 hide (open) const eq