7 |
7 |
8 header {* Product Operator *} |
8 header {* Product Operator *} |
9 |
9 |
10 theory FiniteProduct = Group: |
10 theory FiniteProduct = Group: |
11 |
11 |
12 (* Instantiation of LC from Finite_Set.thy is not possible, |
12 text {* Instantiation of @{text LC} from theory @{text Finite_Set} is not |
13 because here we have explicit typing rules like x : carrier G. |
13 possible, because here we have explicit typing rules like @{text "x |
14 We introduce an explicit argument for the domain D *) |
14 : carrier G"}. We introduce an explicit argument for the domain |
|
15 @{text D}. *} |
15 |
16 |
16 consts |
17 consts |
17 foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set" |
18 foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set" |
18 |
19 |
19 inductive "foldSetD D f e" |
20 inductive "foldSetD D f e" |
279 by (simp add: foldD_Un_Int |
280 by (simp add: foldD_Un_Int |
280 left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff) |
281 left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff) |
281 |
282 |
282 subsection {* Products over Finite Sets *} |
283 subsection {* Products over Finite Sets *} |
283 |
284 |
284 constdefs |
285 constdefs (structure G) |
285 finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" |
286 finprod :: "[_, 'a => 'b, 'a set] => 'b" |
286 "finprod G f A == if finite A |
287 "finprod G f A == if finite A |
287 then foldD (carrier G) (mult G o f) (one G) A |
288 then foldD (carrier G) (mult G o f) \<one> A |
288 else arbitrary" |
289 else arbitrary" |
289 |
290 |
290 (* TODO: nice syntax for the summation operator inside the locale |
291 syntax |
291 like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *) |
292 "_finprod" :: "index => idt => 'a set => 'b => 'b" |
|
293 ("\<Otimes>__:_. _" [1000, 0, 51, 10] 10) |
|
294 syntax (xsymbols) |
|
295 "_finprod" :: "index => idt => 'a set => 'b => 'b" |
|
296 ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10) |
|
297 syntax (HTML output) |
|
298 "_finprod" :: "index => idt => 'a set => 'b => 'b" |
|
299 ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10) |
|
300 translations |
|
301 "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A" -- {* Beware of argument permutation! *} |
292 |
302 |
293 ML_setup {* |
303 ML_setup {* |
294 simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; |
304 simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; |
295 *} |
305 *} |
296 |
306 |
322 apply fast |
332 apply fast |
323 apply (auto simp add: finprod_def) |
333 apply (auto simp add: finprod_def) |
324 done |
334 done |
325 |
335 |
326 lemma (in comm_monoid) finprod_one [simp]: |
336 lemma (in comm_monoid) finprod_one [simp]: |
327 "finite A ==> finprod G (%i. \<one>) A = \<one>" |
337 "finite A ==> (\<Otimes>i:A. \<one>) = \<one>" |
328 proof (induct set: Finites) |
338 proof (induct set: Finites) |
329 case empty show ?case by simp |
339 case empty show ?case by simp |
330 next |
340 next |
331 case (insert A a) |
341 case (insert A a) |
332 have "(%i. \<one>) \<in> A -> carrier G" by auto |
342 have "(%i. \<one>) \<in> A -> carrier G" by auto |