105 func_one func_zero ring_simps) |
105 func_one func_zero ring_simps) |
106 apply (drule fun_cong) |
106 apply (drule fun_cong) |
107 apply simp |
107 apply simp |
108 done |
108 done |
109 |
109 |
110 class_interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"] |
110 interpretation set_semigroup_add!: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set" |
111 apply default |
111 apply default |
112 apply (unfold set_plus_def) |
112 apply (unfold set_plus_def) |
113 apply (force simp add: add_assoc) |
113 apply (force simp add: add_assoc) |
114 done |
114 done |
115 |
115 |
116 class_interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"] |
116 interpretation set_semigroup_mult!: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set" |
117 apply default |
117 apply default |
118 apply (unfold set_times_def) |
118 apply (unfold set_times_def) |
119 apply (force simp add: mult_assoc) |
119 apply (force simp add: mult_assoc) |
120 done |
120 done |
121 |
121 |
122 class_interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"] |
122 interpretation set_comm_monoid_add!: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set" |
123 apply default |
123 apply default |
124 apply (unfold set_plus_def) |
124 apply (unfold set_plus_def) |
125 apply (force simp add: add_ac) |
125 apply (force simp add: add_ac) |
126 apply force |
126 apply force |
127 done |
127 done |
128 |
128 |
129 class_interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"] |
129 interpretation set_comm_monoid_mult!: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set" |
130 apply default |
130 apply default |
131 apply (unfold set_times_def) |
131 apply (unfold set_times_def) |
132 apply (force simp add: mult_ac) |
132 apply (force simp add: mult_ac) |
133 apply force |
133 apply force |
134 done |
134 done |