src/HOL/Library/Function_Algebras.thy
changeset 46575 f1e387195a56
parent 39302 d7728f65b353
child 48173 c6a5a4336edf
     1.1 --- a/src/HOL/Library/Function_Algebras.thy	Tue Feb 21 16:42:57 2012 +0100
     1.2 +++ b/src/HOL/Library/Function_Algebras.thy	Tue Feb 21 16:48:10 2012 +0100
     1.3 @@ -13,9 +13,7 @@
     1.4  instantiation "fun" :: (type, plus) plus
     1.5  begin
     1.6  
     1.7 -definition
     1.8 -  "f + g = (\<lambda>x. f x + g x)"
     1.9 -
    1.10 +definition "f + g = (\<lambda>x. f x + g x)"
    1.11  instance ..
    1.12  
    1.13  end
    1.14 @@ -23,9 +21,7 @@
    1.15  instantiation "fun" :: (type, zero) zero
    1.16  begin
    1.17  
    1.18 -definition
    1.19 -  "0 = (\<lambda>x. 0)"
    1.20 -
    1.21 +definition "0 = (\<lambda>x. 0)"
    1.22  instance ..
    1.23  
    1.24  end
    1.25 @@ -33,9 +29,7 @@
    1.26  instantiation "fun" :: (type, times) times
    1.27  begin
    1.28  
    1.29 -definition
    1.30 -  "f * g = (\<lambda>x. f x * g x)"
    1.31 -
    1.32 +definition "f * g = (\<lambda>x. f x * g x)"
    1.33  instance ..
    1.34  
    1.35  end
    1.36 @@ -43,9 +37,7 @@
    1.37  instantiation "fun" :: (type, one) one
    1.38  begin
    1.39  
    1.40 -definition
    1.41 -  "1 = (\<lambda>x. 1)"
    1.42 -
    1.43 +definition "1 = (\<lambda>x. 1)"
    1.44  instance ..
    1.45  
    1.46  end
    1.47 @@ -53,69 +45,70 @@
    1.48  
    1.49  text {* Additive structures *}
    1.50  
    1.51 -instance "fun" :: (type, semigroup_add) semigroup_add proof
    1.52 -qed (simp add: plus_fun_def add.assoc)
    1.53 +instance "fun" :: (type, semigroup_add) semigroup_add
    1.54 +  by default (simp add: plus_fun_def add.assoc)
    1.55  
    1.56 -instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
    1.57 -qed (simp_all add: plus_fun_def fun_eq_iff)
    1.58 +instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
    1.59 +  by default (simp_all add: plus_fun_def fun_eq_iff)
    1.60  
    1.61 -instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
    1.62 -qed (simp add: plus_fun_def add.commute)
    1.63 +instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
    1.64 +  by default (simp add: plus_fun_def add.commute)
    1.65  
    1.66 -instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
    1.67 -qed simp
    1.68 +instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
    1.69 +  by default simp
    1.70  
    1.71 -instance "fun" :: (type, monoid_add) monoid_add proof
    1.72 -qed (simp_all add: plus_fun_def zero_fun_def)
    1.73 +instance "fun" :: (type, monoid_add) monoid_add
    1.74 +  by default (simp_all add: plus_fun_def zero_fun_def)
    1.75  
    1.76 -instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
    1.77 -qed simp
    1.78 +instance "fun" :: (type, comm_monoid_add) comm_monoid_add
    1.79 +  by default simp
    1.80  
    1.81  instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
    1.82  
    1.83 -instance "fun" :: (type, group_add) group_add proof
    1.84 -qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
    1.85 +instance "fun" :: (type, group_add) group_add
    1.86 +  by default
    1.87 +    (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
    1.88  
    1.89 -instance "fun" :: (type, ab_group_add) ab_group_add proof
    1.90 -qed (simp_all add: diff_minus)
    1.91 +instance "fun" :: (type, ab_group_add) ab_group_add
    1.92 +  by default (simp_all add: diff_minus)
    1.93  
    1.94  
    1.95  text {* Multiplicative structures *}
    1.96  
    1.97 -instance "fun" :: (type, semigroup_mult) semigroup_mult proof
    1.98 -qed (simp add: times_fun_def mult.assoc)
    1.99 +instance "fun" :: (type, semigroup_mult) semigroup_mult
   1.100 +  by default (simp add: times_fun_def mult.assoc)
   1.101  
   1.102 -instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
   1.103 -qed (simp add: times_fun_def mult.commute)
   1.104 +instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
   1.105 +  by default (simp add: times_fun_def mult.commute)
   1.106  
   1.107 -instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
   1.108 -qed (simp add: times_fun_def)
   1.109 +instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
   1.110 +  by default (simp add: times_fun_def)
   1.111  
   1.112 -instance "fun" :: (type, monoid_mult) monoid_mult proof
   1.113 -qed (simp_all add: times_fun_def one_fun_def)
   1.114 +instance "fun" :: (type, monoid_mult) monoid_mult
   1.115 +  by default (simp_all add: times_fun_def one_fun_def)
   1.116  
   1.117 -instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
   1.118 -qed simp
   1.119 +instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
   1.120 +  by default simp
   1.121  
   1.122  
   1.123  text {* Misc *}
   1.124  
   1.125  instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
   1.126  
   1.127 -instance "fun" :: (type, mult_zero) mult_zero proof
   1.128 -qed (simp_all add: zero_fun_def times_fun_def)
   1.129 +instance "fun" :: (type, mult_zero) mult_zero
   1.130 +  by default (simp_all add: zero_fun_def times_fun_def)
   1.131  
   1.132 -instance "fun" :: (type, zero_neq_one) zero_neq_one proof
   1.133 -qed (simp add: zero_fun_def one_fun_def fun_eq_iff)
   1.134 +instance "fun" :: (type, zero_neq_one) zero_neq_one
   1.135 +  by default (simp add: zero_fun_def one_fun_def fun_eq_iff)
   1.136  
   1.137  
   1.138  text {* Ring structures *}
   1.139  
   1.140 -instance "fun" :: (type, semiring) semiring proof
   1.141 -qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
   1.142 +instance "fun" :: (type, semiring) semiring
   1.143 +  by default (simp_all add: plus_fun_def times_fun_def algebra_simps)
   1.144  
   1.145 -instance "fun" :: (type, comm_semiring) comm_semiring proof
   1.146 -qed (simp add: plus_fun_def times_fun_def algebra_simps)
   1.147 +instance "fun" :: (type, comm_semiring) comm_semiring
   1.148 +  by default (simp add: plus_fun_def times_fun_def algebra_simps)
   1.149  
   1.150  instance "fun" :: (type, semiring_0) semiring_0 ..
   1.151  
   1.152 @@ -127,8 +120,7 @@
   1.153  
   1.154  instance "fun" :: (type, semiring_1) semiring_1 ..
   1.155  
   1.156 -lemma of_nat_fun:
   1.157 -  shows "of_nat n = (\<lambda>x::'a. of_nat n)"
   1.158 +lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
   1.159  proof -
   1.160    have comp: "comp = (\<lambda>f g x. f (g x))"
   1.161      by (rule ext)+ simp
   1.162 @@ -147,7 +139,8 @@
   1.163  
   1.164  instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
   1.165  
   1.166 -instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
   1.167 +instance "fun" :: (type, semiring_char_0) semiring_char_0
   1.168 +proof
   1.169    from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
   1.170      by (rule inj_fun)
   1.171    then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
   1.172 @@ -168,23 +161,24 @@
   1.173  
   1.174  text {* Ordereded structures *}
   1.175  
   1.176 -instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
   1.177 -qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
   1.178 +instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
   1.179 +  by default (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
   1.180  
   1.181  instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
   1.182  
   1.183 -instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
   1.184 -qed (simp add: plus_fun_def le_fun_def)
   1.185 +instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
   1.186 +  by default (simp add: plus_fun_def le_fun_def)
   1.187  
   1.188  instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
   1.189  
   1.190  instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
   1.191  
   1.192 -instance "fun" :: (type, ordered_semiring) ordered_semiring proof
   1.193 -qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
   1.194 +instance "fun" :: (type, ordered_semiring) ordered_semiring
   1.195 +  by default
   1.196 +    (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
   1.197  
   1.198 -instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
   1.199 -qed (fact mult_left_mono)
   1.200 +instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
   1.201 +  by default (fact mult_left_mono)
   1.202  
   1.203  instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
   1.204