
diff -r 41701fce8ac7 -r f1e387195a56 src/HOL/Library/Function_Algebras.thy
--- a/src/HOL/Library/Function_Algebras.thy	Tue Feb 21 16:42:57 2012 +0100
+++ b/src/HOL/Library/Function_Algebras.thy	Tue Feb 21 16:48:10 2012 +0100
@@ -13,9 +13,7 @@
 instantiation "fun" :: (type, plus) plus
 begin
 
-definition
-  "f + g = (\<lambda>x. f x + g x)"
-
+definition "f + g = (\<lambda>x. f x + g x)"
 instance ..
 
 end
@@ -23,9 +21,7 @@
 instantiation "fun" :: (type, zero) zero
 begin
 
-definition
-  "0 = (\<lambda>x. 0)"
-
+definition "0 = (\<lambda>x. 0)"
 instance ..
 
 end
@@ -33,9 +29,7 @@
 instantiation "fun" :: (type, times) times
 begin
 
-definition
-  "f * g = (\<lambda>x. f x * g x)"
-
+definition "f * g = (\<lambda>x. f x * g x)"
 instance ..
 
 end
@@ -43,9 +37,7 @@
 instantiation "fun" :: (type, one) one
 begin
 
-definition
-  "1 = (\<lambda>x. 1)"
-
+definition "1 = (\<lambda>x. 1)"
 instance ..
 
 end
@@ -53,69 +45,70 @@
 
 text {* Additive structures *}
 
-instance "fun" :: (type, semigroup_add) semigroup_add proof
-qed (simp add: plus_fun_def add.assoc)
+instance "fun" :: (type, semigroup_add) semigroup_add
+  by default (simp add: plus_fun_def add.assoc)
 
-instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
-qed (simp_all add: plus_fun_def fun_eq_iff)
+instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
+  by default (simp_all add: plus_fun_def fun_eq_iff)
 
-instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
-qed (simp add: plus_fun_def add.commute)
+instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
+  by default (simp add: plus_fun_def add.commute)
 
-instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
-qed simp
+instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
+  by default simp
 
-instance "fun" :: (type, monoid_add) monoid_add proof
-qed (simp_all add: plus_fun_def zero_fun_def)
+instance "fun" :: (type, monoid_add) monoid_add
+  by default (simp_all add: plus_fun_def zero_fun_def)
 
-instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
-qed simp
+instance "fun" :: (type, comm_monoid_add) comm_monoid_add
+  by default simp
 
 instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
 
-instance "fun" :: (type, group_add) group_add proof
-qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
+instance "fun" :: (type, group_add) group_add
+  by default
+    (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
 
-instance "fun" :: (type, ab_group_add) ab_group_add proof
-qed (simp_all add: diff_minus)
+instance "fun" :: (type, ab_group_add) ab_group_add
+  by default (simp_all add: diff_minus)
 
 
 text {* Multiplicative structures *}
 
-instance "fun" :: (type, semigroup_mult) semigroup_mult proof
-qed (simp add: times_fun_def mult.assoc)
+instance "fun" :: (type, semigroup_mult) semigroup_mult
+  by default (simp add: times_fun_def mult.assoc)
 
-instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
-qed (simp add: times_fun_def mult.commute)
+instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
+  by default (simp add: times_fun_def mult.commute)
 
-instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
-qed (simp add: times_fun_def)
+instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
+  by default (simp add: times_fun_def)
 
-instance "fun" :: (type, monoid_mult) monoid_mult proof
-qed (simp_all add: times_fun_def one_fun_def)
+instance "fun" :: (type, monoid_mult) monoid_mult
+  by default (simp_all add: times_fun_def one_fun_def)
 
-instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
-qed simp
+instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
+  by default simp
 
 
 text {* Misc *}
 
 instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
 
-instance "fun" :: (type, mult_zero) mult_zero proof
-qed (simp_all add: zero_fun_def times_fun_def)
+instance "fun" :: (type, mult_zero) mult_zero
+  by default (simp_all add: zero_fun_def times_fun_def)
 
-instance "fun" :: (type, zero_neq_one) zero_neq_one proof
-qed (simp add: zero_fun_def one_fun_def fun_eq_iff)
+instance "fun" :: (type, zero_neq_one) zero_neq_one
+  by default (simp add: zero_fun_def one_fun_def fun_eq_iff)
 
 
 text {* Ring structures *}
 
-instance "fun" :: (type, semiring) semiring proof
-qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
+instance "fun" :: (type, semiring) semiring
+  by default (simp_all add: plus_fun_def times_fun_def algebra_simps)
 
-instance "fun" :: (type, comm_semiring) comm_semiring proof
-qed (simp add: plus_fun_def times_fun_def algebra_simps)
+instance "fun" :: (type, comm_semiring) comm_semiring
+  by default (simp add: plus_fun_def times_fun_def algebra_simps)
 
 instance "fun" :: (type, semiring_0) semiring_0 ..
 
@@ -127,8 +120,7 @@
 
 instance "fun" :: (type, semiring_1) semiring_1 ..
 
-lemma of_nat_fun:
-  shows "of_nat n = (\<lambda>x::'a. of_nat n)"
+lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
 proof -
   have comp: "comp = (\<lambda>f g x. f (g x))"
     by (rule ext)+ simp
@@ -147,7 +139,8 @@
 
 instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
 
-instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
+instance "fun" :: (type, semiring_char_0) semiring_char_0
+proof
   from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
     by (rule inj_fun)
   then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
@@ -168,23 +161,24 @@
 
 text {* Ordereded structures *}
 
-instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
-qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
+instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
+  by default (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
 
 instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
 
-instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
-qed (simp add: plus_fun_def le_fun_def)
+instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
+  by default (simp add: plus_fun_def le_fun_def)
 
 instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
 
 instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
 
-instance "fun" :: (type, ordered_semiring) ordered_semiring proof
-qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
+instance "fun" :: (type, ordered_semiring) ordered_semiring
+  by default
+    (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
 
-instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
-qed (fact mult_left_mono)
+instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
+  by default (fact mult_left_mono)
 
 instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
 




