theory Arbitrary_Comm_Monoid

lemma comm_monoid_exists:
      "\<exists>f e. comm_monoid f e" proof cases assume two_elements: "\<exists>(a :: 'a) b. a \<noteq> b" obtain x e where diff: "x \<noteq> (e :: 'a)" by (atomize_elim, clarsimp simp: two_elements) define f where "f \<equiv> \<lambda>a b. (if a = e then b else (if b = e then a else x))" have "\<forall>a b. f a b = f b a" by (simp add: f_def) moreover have "\<forall>a b c. f (f a b) c = f a (f b c)" by (simp add: diff f_def) moreover have "\<forall>b. f e b = b" by (simp add: diff f_def) ultimately show ?thesis by (metis comm_monoid_def abel_semigroup_def semigroup_def
          abel_semigroup_axioms_def comm_monoid_axioms_def) next assume single_element: "\<not> (\<exists>(a :: 'a) b. a \<noteq> b)" thus ?thesis by (metis (full_types) comm_monoid_def abel_semigroup_def
          semigroup_def abel_semigroup_axioms_def comm_monoid_axioms_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>f e. comm_monoid f e proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>f e. comm_monoid f e
 2. \<not> ?P \<Longrightarrow> \<exists>f e. comm_monoid f e proof (state)
this:
\<exists>a b. a \<noteq> b

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>f e. comm_monoid f e
 2. \<not> ?P \<Longrightarrow> \<exists>f e. comm_monoid f e proof (prove)
goal (1 subgoal):
 1. (\<And>x e. x \<noteq> e \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
x \<noteq> e

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>f e. comm_monoid f e
 2. \<not> ?P \<Longrightarrow> \<exists>f e. comm_monoid f e proof (state)
this:
f \<equiv> \<lambda>a b. if a = e then b else if b = e then a else x

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>f e. comm_monoid f e
 2. \<not> ?P \<Longrightarrow> \<exists>f e. comm_monoid f e proof (prove)
goal (1 subgoal):
 1. \<forall>a b. f a b = f b a proof (state)
this:
\<forall>a b. f a b = f b a

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>f e. comm_monoid f e
 2. \<not> ?P \<Longrightarrow> \<exists>f e. comm_monoid f e proof (state)
this:
\<forall>a b. f a b = f b a

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>f e. comm_monoid f e
 2. \<not> ?P \<Longrightarrow> \<exists>f e. comm_monoid f e proof (prove)
goal (1 subgoal):
 1. \<forall>a b c. f (f a b) c = f a (f b c) proof (state)
this:
\<forall>a b c. f (f a b) c = f a (f b c)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>f e. comm_monoid f e
 2. \<not> ?P \<Longrightarrow> \<exists>f e. comm_monoid f e proof (state)
this:
\<forall>a b c. f (f a b) c = f a (f b c)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>f e. comm_monoid f e
 2. \<not> ?P \<Longrightarrow> \<exists>f e. comm_monoid f e proof (prove)
goal (1 subgoal):
 1. \<forall>b. f e b = b proof (state)
this:
\<forall>b. f e b = b

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>f e. comm_monoid f e
 2. \<not> ?P \<Longrightarrow> \<exists>f e. comm_monoid f e proof (chain)
picking this:
\<forall>a b. f a b = f b a
\<forall>a b c. f (f a b) c = f a (f b c)
\<forall>b. f e b = b proof (prove)
using this:
\<forall>a b. f a b = f b a
\<forall>a b c. f (f a b) c = f a (f b c)
\<forall>b. f e b = b

goal (1 subgoal):
 1. \<exists>f e. comm_monoid f e proof (state)
this:
\<exists>f e. comm_monoid f e

goal (1 subgoal):
 1. \<nexists>a b. a \<noteq> b \<Longrightarrow> \<exists>f e. comm_monoid f e proof (state)
goal (1 subgoal):
 1. \<nexists>a b. a \<noteq> b \<Longrightarrow> \<exists>f e. comm_monoid f e proof (state)
this:
\<nexists>a b. a \<noteq> b

goal (1 subgoal):
 1. \<nexists>a b. a \<noteq> b \<Longrightarrow> \<exists>f e. comm_monoid f e proof (prove)
using this:
\<nexists>a b. a \<noteq> b

goal (1 subgoal):
 1. \<exists>f e. comm_monoid f e proof (state)
this:
\<exists>f e. comm_monoid f e

goal:
No subgoals!