# Theory Group_On_With

```(*  Title:      HOL/Types_To_Sets/Examples/Group_On_With.thy
Author:     Fabian Immler, TU München
*)
theory Group_On_With
imports
Prerequisites
"../Types_To_Sets"
begin

subsection ‹∗‹on› carrier set ∗‹with› explicit group operations›

fixes S::"'a set" and pls::"'a⇒'a⇒'a"
assumes add_assoc: "a ∈ S ⟹ b ∈ S ⟹ c ∈ S ⟹ pls (pls a b) c = pls a (pls b c)"
assumes add_mem: "a ∈ S ⟹ b ∈ S ⟹ pls a b ∈ S"

assumes add_commute: "a ∈ S ⟹ b ∈ S ⟹ pls a b = pls b a"

fixes z
assumes add_zero: "a ∈ S ⟹ pls z a = a"
assumes zero_mem: "z ∈ S"
begin

lemma carrier_ne: "S ≠ {}" using zero_mem by auto

end

definition "sum_with pls z f S =
(if ∃C. f ` S ⊆ C ∧ comm_monoid_add_on_with C pls z then
Finite_Set.fold (pls o f) z S else z)"

lemma sum_with_empty[simp]: "sum_with pls z f {} = z"
by (auto simp: sum_with_def)

lemma sum_with_cases[case_names comm zero]:
"P (sum_with pls z f S)"
if "⋀C. f ` S ⊆ C ⟹ comm_monoid_add_on_with C pls z ⟹ P (Finite_Set.fold (pls o f) z S)"
"(⋀C. comm_monoid_add_on_with C pls z ⟹ (∃s∈S. f s ∉ C)) ⟹ P z"
using that
by (auto simp: sum_with_def)

lemma sum_with_infinite: "infinite A ⟹ sum_with pls z g A = z"
by (induction rule: sum_with_cases) auto

context begin

private abbreviation "pls' ≡ λx y. pls (if x ∈ S then x else z) (if y ∈ S then y else z)"

lemma fold_pls'_mem: "Finite_Set.fold (pls' ∘ g) z A ∈ S"
if "g ` A ⊆ S"
proof cases
assume A: "finite A"
interpret comp_fun_commute "pls' o g"
using that
by unfold_locales auto
from fold_graph_fold[OF A] have "fold_graph (pls' ∘ g) z A (Finite_Set.fold (pls' ∘ g) z A)" .
from fold_graph_closed_lemma[OF this, of S "pls' ∘ g"]
show ?thesis
by auto

lemma fold_pls'_eq: "Finite_Set.fold (pls' ∘ g) z A = Finite_Set.fold (pls ∘ g) z A"
if "g ` A ⊆ S"
by (intro fold_closed_eq[where B=S]) auto

lemma sum_with_mem: "sum_with pls z g A ∈ S" if "g ` A ⊆ S"
proof -
interpret comp_fun_commute "pls' o g"
by unfold_locales auto
have "∃C. g ` A ⊆ C ∧ comm_monoid_add_on_with C pls z"
then show ?thesis
using fold_pls'_mem[OF that]
by (simp add: sum_with_def fold_pls'_eq that)
qed

lemma sum_with_insert:
"sum_with pls z g (insert x A) = pls (g x) (sum_with pls z g A)"
if g_into: "g x ∈ S" "g ` A ⊆ S"
and A: "finite A" and x: "x ∉ A"
proof -
interpret comp_fun_commute "pls' o g"
by unfold_locales auto
have "Finite_Set.fold (pls ∘ g) z (insert x A) = Finite_Set.fold (pls' ∘ g) z (insert x A)"
using g_into
by (subst fold_pls'_eq) auto
also have "… = pls' (g x) (Finite_Set.fold (pls' ∘ g) z A)"
unfolding fold_insert[OF A x]
by (auto simp: o_def)
also have "… = pls (g x) (Finite_Set.fold (pls' ∘ g) z A)"
proof -
from fold_graph_fold[OF A] have "fold_graph (pls' ∘ g) z A (Finite_Set.fold (pls' ∘ g) z A)" .
have "Finite_Set.fold (pls' ∘ g) z A ∈ S"
by auto
then show ?thesis
using g_into by auto
qed
also have "Finite_Set.fold (pls' ∘ g) z A = Finite_Set.fold (pls ∘ g) z A"
using g_into
by (subst fold_pls'_eq) auto
finally
have "Finite_Set.fold (pls ∘ g) z (insert x A) = pls (g x) (Finite_Set.fold (pls ∘ g) z A)" .
moreover
have "∃C. g ` insert x A ⊆ C ∧ comm_monoid_add_on_with C pls z"
"∃C. g ` A ⊆ C ∧ comm_monoid_add_on_with C pls z"
using that (1,2) comm_monoid_add_on_with_axioms by auto
ultimately show ?thesis
qed

end

end

fixes mns um
assumes ab_left_minus: "a ∈ S ⟹ pls (um a) a = z"
assumes ab_diff_conv_add_uminus: "a ∈ S ⟹ b ∈ S ⟹ mns a b = pls a (um b)"
assumes uminus_mem: "a ∈ S ⟹ um a ∈ S"

subsection ‹obvious instances (by type class constraints)›

(∀a∈S. ∀b∈S. ∀c∈S. pls (pls a b) c = pls a (pls b c)) ∧ (∀a∈S. ∀b∈S. pls a b ∈ S)"

"ab_semigroup_add_on_with S pls ⟷ semigroup_add_on_with S pls ∧ (∀a∈S. ∀b∈S. pls a b = pls b a)"

"comm_monoid_add_on_with S pls z ⟷ ab_semigroup_add_on_with S pls ∧ (∀a∈S. pls z a = a) ∧ z ∈ S"

"ab_group_add_on_with S pls z mns um ⟷ comm_monoid_add_on_with S pls z ∧
(∀a∈S. pls (um a) a = z) ∧ (∀a∈S. ∀b∈S. mns a b = pls a (um b)) ∧ (∀a∈S. um a ∈ S)"

lemma sum_with: "sum f S = sum_with (+) 0 f S"
proof (induction rule: sum_with_cases)
case (comm C)
then show ?case
unfolding sum.eq_fold
by simp
next
case zero
show ?case by simp
qed

subsection ‹transfer rules›

includes lifting_syntax
assumes [transfer_rule]: "bi_unique A"
shows "(rel_set A ===> (A ===> A ===> A) ===> (=)) semigroup_add_on_with semigroup_add_on_with"
by transfer_prover

lemma Domainp_applyI:
includes lifting_syntax
shows "(A ===> B) f g ⟹ A x y ⟹ Domainp B (f x)"
by (auto simp: rel_fun_def)

lemma Domainp_apply2I:
includes lifting_syntax
shows "(A ===> B ===> C) f g ⟹ A x y ⟹ B x' y' ⟹ Domainp C (f x x')"
by (force simp: rel_fun_def)

includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows "((A ===> A ===> A) ===> (=)) (semigroup_add_on_with (Collect (Domainp A))) class.semigroup_add"
proof (intro rel_funI)
fix x y assume xy[transfer_rule]: "(A ===> A ===> A) x y"
by transfer (auto intro!: Domainp_apply2I[OF xy])
qed

includes lifting_syntax
assumes [transfer_rule]: "bi_unique A"
shows
"(rel_set A ===> (A ===> A ===> A) ===> (=)) ab_semigroup_add_on_with ab_semigroup_add_on_with"

includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows
"((A ===> A ===> A) ===> (=)) (ab_semigroup_add_on_with (Collect (Domainp A))) class.ab_semigroup_add"
by transfer_prover

includes lifting_syntax
assumes [transfer_rule]: "bi_unique A"
shows
"(rel_set A ===> (A ===> A ===> A) ===> A ===> (=)) comm_monoid_add_on_with comm_monoid_add_on_with"
by transfer_prover

includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows
"((A ===> A ===> A) ===> A ===> (=))
proof (intro rel_funI)
fix p p' z z'
assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'"
apply transfer
using ‹A z z'›
by auto
qed

includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows "((A ===> A ===> A) ===> A  ===> (A ===> A ===> A) ===> (A ===> A)===> (=))
proof (intro rel_funI)
fix p p' z z' m m' um um'
assume [transfer_rule]:
"(A ===> A ===> A) p p'" "A z z'" "(A ===> A ===> A) m m'"
and um[transfer_rule]: "(A ===> A) um um'"
show "ab_group_add_on_with (Collect (Domainp A)) p z m um = class.ab_group_add p' z' m' um'"
by transfer (use um in ‹auto simp: rel_fun_def›)
qed

includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows
"(rel_set A ===> (A ===> A ===> A) ===> A  ===> (A ===> A ===> A) ===> (A ===> A)===> (=))
by transfer_prover

includes lifting_syntax
assumes ex_comm: "∃C. f ` S ⊆ C ∧ comm_monoid_add_on_with C pls zero"
assumes transfers: "(A ===> A ===> A) pls pls'" "A zero zero'" "Domainp (rel_set B) S"
and in_dom: "⋀x. x ∈ S ⟹ Domainp A (f x)"
obtains C where "comm_monoid_add_on_with C pls zero" "f ` S ⊆ C" "Domainp (rel_set A) C"
proof -
from ex_comm obtain C0 where C0: "f ` S ⊆ C0" and comm: "comm_monoid_add_on_with C0 pls zero"
by auto
define C where "C = C0 ∩ Collect (Domainp A)"
using comm Domainp_apply2I[OF ‹(A ===> A ===> A) pls pls'›] ‹A zero zero'›
moreover have "f ` S ⊆ C" using C0
by (auto simp: C_def in_dom)
moreover have "Domainp (rel_set A) C" by (auto simp: C_def Domainp_set)
ultimately show ?thesis ..
qed

lemma sum_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A" "bi_unique B"
shows "((A ===> A ===> A) ===> A ===> (B ===> A) ===> rel_set B ===> A)
sum_with sum_with"
proof (safe intro!: rel_funI)
fix pls pls' zero zero' f g S T
assume transfer_pls[transfer_rule]: "(A ===> A ===> A) pls pls'"
and transfer_zero[transfer_rule]: "A zero zero'"
assume transfer_g[transfer_rule]: "(B ===> A) f g"
and transfer_T[transfer_rule]: "rel_set B S T"
show "A (sum_with pls zero f S) (sum_with pls' zero' g T)"
proof cases
assume ex_comm: "∃C. f ` S ⊆ C ∧ comm_monoid_add_on_with C pls zero"
have Domains: "Domainp (rel_set B) S" "(⋀x. x ∈ S ⟹ Domainp A (f x))"
using transfer_T transfer_g
by auto (meson Domainp_applyI rel_set_def)
from ex_comm_monoid_add_around_imageE[OF ex_comm transfer_pls transfer_zero Domains]
obtain C where comm: "comm_monoid_add_on_with C pls zero"
and C: "f ` S ⊆ C"
and "Domainp (rel_set A) C"
by auto
then obtain C' where [transfer_rule]: "rel_set A C C'" by auto
interpret comm: comm_monoid_add_on_with C pls zero by fact
have C': "g ` T ⊆ C'"
by transfer (rule C)
have comm': "comm_monoid_add_on_with C' pls' zero'"
by transfer (rule comm)
then interpret comm': comm_monoid_add_on_with C' pls' zero' .
from C' comm' have ex_comm': "∃C. g ` T ⊆ C ∧ comm_monoid_add_on_with C pls' zero'" by auto
show ?thesis
using transfer_T C C'
proof (induction S arbitrary: T rule: infinite_finite_induct)
case (infinite S)
note [transfer_rule] = infinite.prems
from infinite.hyps have "infinite T" by transfer
then show ?case by (simp add: sum_with_def infinite.hyps ‹A zero zero'›)
next
case [transfer_rule]: empty
have "T = {}" by transfer rule
then show ?case by (simp add: sum_with_def ‹A zero zero'›)
next
case (insert x F)
note [transfer_rule] = insert.prems(1)
have [simp]: "finite T"
obtain y where [transfer_rule]: "B x y" and y: "y ∈ T"
by (meson insert.prems insertI1 rel_setD1)
define T' where "T' = T - {y}"
have T_def: "T = insert y T'"
by (auto simp: T'_def y)
define sF where "sF = sum_with pls zero f F"
define sT where "sT = sum_with pls' zero' g T'"
have [simp]: "y ∉ T'" "finite T'"
by (auto simp: y T'_def)
have "rel_set B (insert x F - {x}) T'"
unfolding T'_def
by transfer_prover
then have transfer_T'[transfer_rule]: "rel_set B F T'"
using insert.hyps
by simp
from insert.prems have "f ` F ⊆ C" "g ` T' ⊆ C'"
by (auto simp: T'_def)
from insert.IH[OF transfer_T' this] have [transfer_rule]: "A sF sT" by (auto simp: sF_def sT_def o_def)
have rew: "(sum_with pls zero f (insert x F)) = pls (f x) (sum_with pls zero f F)"
apply (subst comm.sum_with_insert)
subgoal using insert.prems by auto
subgoal using insert.prems by auto
subgoal by fact
subgoal by fact
subgoal by auto
done
have rew': "(sum_with pls' zero' g (insert y T')) = pls' (g y) (sum_with pls' zero' g T')"
apply (subst comm'.sum_with_insert)
subgoal
apply transfer
using insert.prems by auto
subgoal
apply transfer
using insert.prems by auto
subgoal by fact
subgoal by fact
subgoal by auto
done
have "A (sum_with pls zero f (insert x F)) (sum_with pls' zero' g (insert y T'))"
unfolding sT_def[symmetric] sF_def[symmetric] rew rew'
by transfer_prover
then show ?case
qed
next
assume *: "∄C. f ` S ⊆ C ∧ comm_monoid_add_on_with C pls zero"
then have **: "∄C'. g ` T ⊆ C' ∧ comm_monoid_add_on_with C' pls' zero'"
by transfer simp
show ?thesis
by (simp add: sum_with_def * ** ‹A zero zero'›)
qed
qed

subsection ‹Rewrite rules to make ‹ab_group_add› operations explicit›

subsection ‹Locale defining ‹ab_group_add›-Operations in a local type›

locale local_typedef_ab_group_add_on_with = local_typedef S s +
for S ::"'b set" and s::"'s itself"
begin

lemma mem_minus_lt: "x ∈ S ⟹ y ∈ S ⟹ mns x y ∈ S"
by auto

context includes lifting_syntax begin

definition plus_S::"'s ⇒ 's ⇒ 's" where "plus_S = (rep ---> rep ---> Abs) pls"
definition minus_S::"'s ⇒ 's ⇒ 's" where "minus_S = (rep ---> rep ---> Abs) mns"
definition uminus_S::"'s ⇒ 's" where "uminus_S = (rep ---> Abs) um"
definition zero_S::"'s" where "zero_S = Abs z"

lemma plus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) pls plus_S"
unfolding plus_S_def
by (auto simp: cr_S_def add_mem intro!: rel_funI)

lemma minus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) mns minus_S"
unfolding minus_S_def
by (auto simp: cr_S_def mem_minus_lt intro!: rel_funI)

lemma uminus_S_transfer[transfer_rule]: "(cr_S ===> cr_S) um uminus_S"
unfolding uminus_S_def
by (auto simp: cr_S_def uminus_mem intro!: rel_funI)

lemma zero_S_transfer[transfer_rule]: "cr_S z zero_S"
unfolding zero_S_def
by (auto simp: cr_S_def zero_mem intro!: rel_funI)

end

sublocale type: ab_group_add plus_S "zero_S::'s" minus_S uminus_S
apply unfold_locales
subgoal by transfer (rule ab_left_minus)
done

context includes lifting_syntax begin

lemma sum_transfer[transfer_rule]:
"((A===>cr_S) ===> rel_set A ===> cr_S) (sum_with pls z) type.sum"
if [transfer_rule]: "bi_unique A"
proof (safe intro!: rel_funI)
fix f g I J
assume fg[transfer_rule]: "(A ===> cr_S) f g" and rel_set: "rel_set A I J"
show "cr_S (sum_with pls z f I) (type.sum g J)"
using rel_set
proof (induction I arbitrary: J rule: infinite_finite_induct)
case (infinite I)
note [transfer_rule] = infinite.prems
from infinite.hyps have "infinite J" by transfer
with infinite.hyps show ?case
next
case [transfer_rule]: empty
have "J = {}" by transfer rule
then show ?case by (simp add: zero_S_transfer)
next
case (insert x F)
note [transfer_rule] = insert.prems
have [simp]: "finite J"
obtain y where [transfer_rule]: "A x y" and y: "y ∈ J"
by (meson insert.prems insertI1 rel_setD1)
define J' where "J' = J - {y}"
have T_def: "J = insert y J'"
by (auto simp: J'_def y)
define sF where "sF = sum_with pls z f F"
define sT where "sT = type.sum g J'"
have [simp]: "y ∉ J'" "finite J'"
by (auto simp: y J'_def)
have "rel_set A (insert x F - {x}) J'"
unfolding J'_def
by transfer_prover
then have "rel_set A F J'"
using insert.hyps
by simp
from insert.IH[OF this] have [transfer_rule]: "cr_S sF sT" by (auto simp: sF_def sT_def)
have f_S: "f x ∈ S" "f ` F ⊆ S"
using ‹A x y› fg insert.prems
by (auto simp: rel_fun_def cr_S_def rel_set_def)
have "cr_S (pls (f x) sF) (plus_S (g y) sT)" by transfer_prover
then have "cr_S (sum_with pls z f (insert x F)) (type.sum g (insert y J'))"
by (simp add: sum_with_insert insert.hyps type.sum.insert_remove sF_def[symmetric]
sT_def[symmetric] f_S)
then show ?case
qed
qed

end

end

context includes lifting_syntax assumes ltd: "∃(Rep::'s ⇒ 'a) (Abs::'a ⇒ 's). type_definition Rep Abs S" begin

interpretation local_typedef_ab_group_add_on_with pls z mns um S "TYPE('s)" by unfold_locales fact

text‹Get theorem names:›

lemmas lt_sum_mono_neutral_cong_left = sum.mono_neutral_cong_left