update instance proofs to new style
Wed, 02 Jan 2008 01:20:18 +0100
changeset 25758 89c7c22e64b4
parent 25757 5957e3d72fec
child 25759 6326138c1bd7
update instance proofs to new style
--- a/src/HOLCF/Ffun.thy	Tue Jan 01 20:35:16 2008 +0100
+++ b/src/HOLCF/Ffun.thy	Wed Jan 02 01:20:18 2008 +0100
@@ -15,30 +15,29 @@
 subsection {* Full function space is a partial order *}
-instance "fun"  :: (type, sq_ord) sq_ord ..
+instantiation "fun"  :: (type, sq_ord) sq_ord
-defs (overloaded)
   less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  
-lemma refl_less_fun: "(f::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f"
-by (simp add: less_fun_def)
-lemma antisym_less_fun:
-  "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f1\<rbrakk> \<Longrightarrow> f1 = f2"
-by (simp add: less_fun_def expand_fun_eq antisym_less)
+instance ..
-lemma trans_less_fun:
-  "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f3\<rbrakk> \<Longrightarrow> f1 \<sqsubseteq> f3"
-apply (unfold less_fun_def)
-apply clarify
-apply (rule trans_less)
-apply (erule spec)
-apply (erule spec)
-instance "fun"  :: (type, po) po
-by intro_classes
-  (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+
+instance "fun" :: (type, po) po
+  fix f :: "'a \<Rightarrow> 'b"
+  show "f \<sqsubseteq> f"
+    by (simp add: less_fun_def)
+  fix f g :: "'a \<Rightarrow> 'b"
+  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
+    by (simp add: less_fun_def expand_fun_eq antisym_less)
+  fix f g h :: "'a \<Rightarrow> 'b"
+  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
+    unfolding less_fun_def by (fast elim: trans_less)
 text {* make the symbol @{text "<<"} accessible for type fun *}