# HG changeset patch
# User huffman
# Date 1199233218 -3600
# Node ID 89c7c22e64b443f79712506bb453b9dadc088be7
# Parent  5957e3d72fecdd92659093ee132b0aa3bfbf3e11
update instance proofs to new style

diff -r 5957e3d72fec -r 89c7c22e64b4 src/HOLCF/Ffun.thy
--- 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
+begin
 
-defs (overloaded)
+definition
   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 ..
+end
 
-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)
-done
-
-instance "fun"  :: (type, po) po
-by intro_classes
-  (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+
+instance "fun" :: (type, po) po
+proof
+  fix f :: "'a \<Rightarrow> 'b"
+  show "f \<sqsubseteq> f"
+    by (simp add: less_fun_def)
+next
+  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)
+next
+  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)
+qed
 
 text {* make the symbol @{text "<<"} accessible for type fun *}