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