1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Arbitrary_Comm_Monoid 8imports Main 9begin 10 11text \<open> 12 We define operations "arbitrary_add" and "arbitrary_zero" 13 to represent an arbitrary commutative monoid. 14\<close> 15 16definition 17 arbitrary_add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 18 (infixl "+\<^sub>?" 65) 19where 20 "arbitrary_add a b \<equiv> fst (SOME (f, z). comm_monoid f z) a b" 21 22definition 23 arbitrary_zero :: "'a" 24 ("0\<^sub>?") 25where 26 "arbitrary_zero \<equiv> snd (SOME (f, z). comm_monoid f z)" 27 28text \<open> 29 For every type, there exists some function @{term f} and 30 identity @{term e} on that type forming a monoid. 31\<close> 32lemma comm_monoid_exists: 33 "\<exists>f e. comm_monoid f e" 34proof cases 35 assume two_elements: "\<exists>(a :: 'a) b. a \<noteq> b" 36 37 obtain x e where diff: "x \<noteq> (e :: 'a)" 38 by (atomize_elim, clarsimp simp: two_elements) 39 40 define f where "f \<equiv> \<lambda>a b. (if a = e then b else (if b = e then a else x))" 41 42 have "\<forall>a b. f a b = f b a" 43 by (simp add: f_def) 44 moreover have "\<forall>a b c. f (f a b) c = f a (f b c)" 45 by (simp add: diff f_def) 46 moreover have "\<forall>b. f e b = b" 47 by (simp add: diff f_def) 48 ultimately show ?thesis 49 by (metis comm_monoid_def abel_semigroup_def semigroup_def 50 abel_semigroup_axioms_def comm_monoid_axioms_def) 51next 52 assume single_element: "\<not> (\<exists>(a :: 'a) b. a \<noteq> b)" 53 thus ?thesis 54 by (metis (full_types) comm_monoid_def abel_semigroup_def 55 semigroup_def abel_semigroup_axioms_def comm_monoid_axioms_def) 56qed 57 58text \<open> 59 These operations form a commutative monoid. 60\<close> 61interpretation comm_monoid arbitrary_add arbitrary_zero 62 unfolding arbitrary_add_def [abs_def] arbitrary_zero_def 63 by (rule someI2_ex, auto simp: comm_monoid_exists) 64 65locale idem_comm_monoid = comm_monoid + 66 assumes comm_idem: "a \<^bold>* a = a" 67 68locale canc_comm_monoid = comm_monoid + 69 assumes canc: "a \<^bold>* b = a \<^bold>* c \<Longrightarrow> b = c" 70 71lemma idem_comm_monoid_not_canc: 72 "((x :: 'a) \<noteq> e) \<Longrightarrow> idem_comm_monoid f (e :: 'a :: times) \<Longrightarrow> \<not> canc_comm_monoid f e" 73 apply (clarsimp simp: idem_comm_monoid_def canc_comm_monoid_def canc_comm_monoid_axioms_def 74 idem_comm_monoid_axioms_def) 75 apply (rule_tac x="x" in exI) 76 apply (rule_tac x="x" in exI) 77 apply (rule_tac x="e" in exI) 78 apply (erule_tac x=x in allE, clarsimp) 79 apply (clarsimp simp: comm_monoid_def comm_monoid_axioms_def abel_semigroup_def 80 abel_semigroup_axioms_def semigroup_def) 81 by metis 82 83lemma idem_comm_monoid_exists: 84 "\<exists>f e. idem_comm_monoid f e" 85 apply (cases "\<exists>(x :: 'a) e. x \<noteq> e") 86 apply (clarsimp) 87 apply (rule_tac x="\<lambda>a b. (if a = b then a else (if a = e then b else (if b = e then a else x)))" 88 in exI) 89 apply (rule_tac x=e in exI) 90 apply (intro_locales) 91 apply (clarsimp simp: semigroup_def) 92 apply (clarsimp simp: abel_semigroup_axioms_def) 93 apply (clarsimp simp: comm_monoid_axioms_def) 94 apply (clarsimp simp: idem_comm_monoid_axioms_def) 95 apply (clarsimp) 96 apply (rule_tac x="\<lambda>x. undefined" in exI) 97 apply (rule_tac x="undefined" in exI) 98 apply (intro_locales) 99 apply (clarsimp simp: semigroup_def) 100 apply (clarsimp simp: abel_semigroup_axioms_def) 101 apply (clarsimp simp: comm_monoid_axioms_def) 102 apply (clarsimp simp: idem_comm_monoid_axioms_def) 103 done 104 105end