theory Congruence
imports
Main
"HOL-Library.FuncSet"
begin
section ‹Objects›
subsection ‹Structure with Carrier Set.›
record 'a partial_object =
carrier :: "'a set"
lemma funcset_carrier:
"⟦ f ∈ carrier X → carrier Y; x ∈ carrier X ⟧ ⟹ f x ∈ carrier Y"
by (fact funcset_mem)
lemma funcset_carrier':
"⟦ f ∈ carrier A → carrier A; x ∈ carrier A ⟧ ⟹ f x ∈ carrier A"
by (fact funcset_mem)
subsection ‹Structure with Carrier and Equivalence Relation ‹eq››
record 'a eq_object = "'a partial_object" +
eq :: "'a ⇒ 'a ⇒ bool" (infixl ".=ı" 50)
definition
elem :: "_ ⇒ 'a ⇒ 'a set ⇒ bool" (infixl ".∈ı" 50)
where "x .∈⇘S⇙ A ⟷ (∃y ∈ A. x .=⇘S⇙ y)"
definition
set_eq :: "_ ⇒ 'a set ⇒ 'a set ⇒ bool" (infixl "{.=}ı" 50)
where "A {.=}⇘S⇙ B ⟷ ((∀x ∈ A. x .∈⇘S⇙ B) ∧ (∀x ∈ B. x .∈⇘S⇙ A))"
definition
eq_class_of :: "_ ⇒ 'a ⇒ 'a set" ("class'_ofı")
where "class_of⇘S⇙ x = {y ∈ carrier S. x .=⇘S⇙ y}"
definition
eq_classes :: "_ ⇒ ('a set) set" ("classesı")
where "classes⇘S⇙ = {class_of⇘S⇙ x | x. x ∈ carrier S}"
definition
eq_closure_of :: "_ ⇒ 'a set ⇒ 'a set" ("closure'_ofı")
where "closure_of⇘S⇙ A = {y ∈ carrier S. y .∈⇘S⇙ A}"
definition
eq_is_closed :: "_ ⇒ 'a set ⇒ bool" ("is'_closedı")
where "is_closed⇘S⇙ A ⟷ A ⊆ carrier S ∧ closure_of⇘S⇙ A = A"
abbreviation
not_eq :: "_ ⇒ 'a ⇒ 'a ⇒ bool" (infixl ".≠ı" 50)
where "x .≠⇘S⇙ y ≡ ¬(x .=⇘S⇙ y)"
abbreviation
not_elem :: "_ ⇒ 'a ⇒ 'a set ⇒ bool" (infixl ".∉ı" 50)
where "x .∉⇘S⇙ A ≡ ¬(x .∈⇘S⇙ A)"
abbreviation
set_not_eq :: "_ ⇒ 'a set ⇒ 'a set ⇒ bool" (infixl "{.≠}ı" 50)
where "A {.≠}⇘S⇙ B ≡ ¬(A {.=}⇘S⇙ B)"
locale equivalence =
fixes S (structure)
assumes refl [simp, intro]: "x ∈ carrier S ⟹ x .= x"
and sym [sym]: "⟦ x .= y; x ∈ carrier S; y ∈ carrier S ⟧ ⟹ y .= x"
and trans [trans]:
"⟦ x .= y; y .= z; x ∈ carrier S; y ∈ carrier S; z ∈ carrier S ⟧ ⟹ x .= z"
lemma equivalenceI:
fixes P :: "'a ⇒ 'a ⇒ bool" and E :: "'a set"
assumes refl: "⋀x. ⟦ x ∈ E ⟧ ⟹ P x x"
and sym: "⋀x y. ⟦ x ∈ E; y ∈ E ⟧ ⟹ P x y ⟹ P y x"
and trans: "⋀x y z. ⟦ x ∈ E; y ∈ E; z ∈ E ⟧ ⟹ P x y ⟹ P y z ⟹ P x z"
shows "equivalence ⦇ carrier = E, eq = P ⦈"
unfolding equivalence_def using assms
by (metis eq_object.select_convs(1) partial_object.select_convs(1))
locale partition =
fixes A :: "'a set" and B :: "('a set) set"
assumes unique_class: "⋀a. a ∈ A ⟹ ∃!b ∈ B. a ∈ b"
and incl: "⋀b. b ∈ B ⟹ b ⊆ A"
lemma equivalence_subset:
assumes "equivalence L" "A ⊆ carrier L"
shows "equivalence (L⦇ carrier := A ⦈)"
proof -
interpret L: equivalence L
by (simp add: assms)
show ?thesis
by (unfold_locales, simp_all add: L.sym assms rev_subsetD, meson L.trans assms(2) contra_subsetD)
qed
lemma elemI:
fixes R (structure)
assumes "a' ∈ A" "a .= a'"
shows "a .∈ A"
unfolding elem_def using assms by auto
lemma (in equivalence) elem_exact:
assumes "a ∈ carrier S" "a ∈ A"
shows "a .∈ A"
unfolding elem_def using assms by auto
lemma elemE:
fixes S (structure)
assumes "a .∈ A"
and "⋀a'. ⟦a' ∈ A; a .= a'⟧ ⟹ P"
shows "P"
using assms unfolding elem_def by auto
lemma (in equivalence) elem_cong_l [trans]:
assumes "a ∈ carrier S" "a' ∈ carrier S" "A ⊆ carrier S"
and "a' .= a" "a .∈ A"
shows "a' .∈ A"
using assms by (meson elem_def trans subsetCE)
lemma (in equivalence) elem_subsetD:
assumes "A ⊆ B" "a .∈ A"
shows "a .∈ B"
using assms by (fast intro: elemI elim: elemE dest: subsetD)
lemma (in equivalence) mem_imp_elem [simp, intro]:
assumes "x ∈ carrier S"
shows "x ∈ A ⟹ x .∈ A"
using assms unfolding elem_def by blast
lemma set_eqI:
fixes R (structure)
assumes "⋀a. a ∈ A ⟹ a .∈ B"
and "⋀b. b ∈ B ⟹ b .∈ A"
shows "A {.=} B"
using assms unfolding set_eq_def by auto
lemma set_eqI2:
fixes R (structure)
assumes "⋀a. a ∈ A ⟹ ∃b ∈ B. a .= b"
and "⋀b. b ∈ B ⟹ ∃a ∈ A. b .= a"
shows "A {.=} B"
using assms by (simp add: set_eqI elem_def)
lemma set_eqD1:
fixes R (structure)
assumes "A {.=} A'" and "a ∈ A"
shows "∃a'∈A'. a .= a'"
using assms by (simp add: set_eq_def elem_def)
lemma set_eqD2:
fixes R (structure)
assumes "A {.=} A'" and "a' ∈ A'"
shows "∃a∈A. a' .= a"
using assms by (simp add: set_eq_def elem_def)
lemma set_eqE:
fixes R (structure)
assumes "A {.=} B"
and "⟦ ∀a ∈ A. a .∈ B; ∀b ∈ B. b .∈ A ⟧ ⟹ P"
shows "P"
using assms unfolding set_eq_def by blast
lemma set_eqE2:
fixes R (structure)
assumes "A {.=} B"
and "⟦ ∀a ∈ A. ∃b ∈ B. a .= b; ∀b ∈ B. ∃a ∈ A. b .= a ⟧ ⟹ P"
shows "P"
using assms unfolding set_eq_def by (simp add: elem_def)
lemma set_eqE':
fixes R (structure)
assumes "A {.=} B" "a ∈ A" "b ∈ B"
and "⋀a' b'. ⟦ a' ∈ A; b' ∈ B ⟧ ⟹ b .= a' ⟹ a .= b' ⟹ P"
shows "P"
using assms by (meson set_eqE2)
lemma (in equivalence) eq_elem_cong_r [trans]:
assumes "A ⊆ carrier S" "A' ⊆ carrier S" "A {.=} A'"
shows "⟦ a ∈ carrier S ⟧ ⟹ a .∈ A ⟹ a .∈ A'"
using assms by (meson elemE elem_cong_l set_eqE subset_eq)
lemma (in equivalence) set_eq_sym [sym]:
assumes "A ⊆ carrier S" "B ⊆ carrier S"
shows "A {.=} B ⟹ B {.=} A"
using assms unfolding set_eq_def elem_def by auto
lemma (in equivalence) equal_set_eq_trans [trans]:
"⟦ A = B; B {.=} C ⟧ ⟹ A {.=} C"
by simp
lemma (in equivalence) set_eq_equal_trans [trans]:
"⟦ A {.=} B; B = C ⟧ ⟹ A {.=} C"
by simp
lemma (in equivalence) set_eq_trans_aux:
assumes "A ⊆ carrier S" "B ⊆ carrier S" "C ⊆ carrier S"
and "A {.=} B" "B {.=} C"
shows "⋀a. a ∈ A ⟹ a .∈ C"
using assms by (simp add: eq_elem_cong_r subset_iff)
corollary (in equivalence) set_eq_trans [trans]:
assumes "A ⊆ carrier S" "B ⊆ carrier S" "C ⊆ carrier S"
and "A {.=} B" " B {.=} C"
shows "A {.=} C"
proof (intro set_eqI)
show "⋀a. a ∈ A ⟹ a .∈ C" using set_eq_trans_aux assms by blast
next
show "⋀b. b ∈ C ⟹ b .∈ A" using set_eq_trans_aux set_eq_sym assms by blast
qed
lemma (in equivalence) is_closedI:
assumes closed: "⋀x y. ⟦x .= y; x ∈ A; y ∈ carrier S⟧ ⟹ y ∈ A"
and S: "A ⊆ carrier S"
shows "is_closed A"
unfolding eq_is_closed_def eq_closure_of_def elem_def
using S
by (blast dest: closed sym)
lemma (in equivalence) closure_of_eq:
assumes "A ⊆ carrier S" "x ∈ closure_of A"
shows "⟦ x' ∈ carrier S; x .= x' ⟧ ⟹ x' ∈ closure_of A"
using assms elem_cong_l sym unfolding eq_closure_of_def by blast
lemma (in equivalence) is_closed_eq [dest]:
assumes "is_closed A" "x ∈ A"
shows "⟦ x .= x'; x' ∈ carrier S ⟧ ⟹ x' ∈ A"
using assms closure_of_eq [where A = A] unfolding eq_is_closed_def by simp
corollary (in equivalence) is_closed_eq_rev [dest]:
assumes "is_closed A" "x' ∈ A"
shows "⟦ x .= x'; x ∈ carrier S ⟧ ⟹ x ∈ A"
using sym is_closed_eq assms by (meson contra_subsetD eq_is_closed_def)
lemma closure_of_closed [simp, intro]:
fixes S (structure)
shows "closure_of A ⊆ carrier S"
unfolding eq_closure_of_def by auto
lemma closure_of_memI:
fixes S (structure)
assumes "a .∈ A" "a ∈ carrier S"
shows "a ∈ closure_of A"
by (simp add: assms eq_closure_of_def)
lemma closure_ofI2:
fixes S (structure)
assumes "a .= a'" and "a' ∈ A" and "a ∈ carrier S"
shows "a ∈ closure_of A"
by (meson assms closure_of_memI elem_def)
lemma closure_of_memE:
fixes S (structure)
assumes "a ∈ closure_of A"
and "⟦a ∈ carrier S; a .∈ A⟧ ⟹ P"
shows "P"
using eq_closure_of_def assms by fastforce
lemma closure_ofE2:
fixes S (structure)
assumes "a ∈ closure_of A"
and "⋀a'. ⟦a ∈ carrier S; a' ∈ A; a .= a'⟧ ⟹ P"
shows "P"
using assms by (meson closure_of_memE elemE)
lemma (in partition) equivalence_from_partition:
"equivalence ⦇ carrier = A, eq = (λx y. y ∈ (THE b. b ∈ B ∧ x ∈ b))⦈"
unfolding partition_def equivalence_def
proof (auto)
let ?f = "λx. THE b. b ∈ B ∧ x ∈ b"
show "⋀x. x ∈ A ⟹ x ∈ ?f x"
using unique_class by (metis (mono_tags, lifting) theI')
show "⋀x y. ⟦ x ∈ A; y ∈ A ⟧ ⟹ y ∈ ?f x ⟹ x ∈ ?f y"
using unique_class by (metis (mono_tags, lifting) the_equality)
show "⋀x y z. ⟦ x ∈ A; y ∈ A; z ∈ A ⟧ ⟹ y ∈ ?f x ⟹ z ∈ ?f y ⟹ z ∈ ?f x"
using unique_class by (metis (mono_tags, lifting) the_equality)
qed
lemma (in partition) partition_coverture: "⋃B = A"
by (meson Sup_le_iff UnionI unique_class incl subsetI subset_antisym)
lemma (in partition) disjoint_union:
assumes "b1 ∈ B" "b2 ∈ B"
and "b1 ∩ b2 ≠ {}"
shows "b1 = b2"
proof (rule ccontr)
assume "b1 ≠ b2"
obtain a where "a ∈ A" "a ∈ b1" "a ∈ b2"
using assms(2-3) incl by blast
thus False using unique_class ‹b1 ≠ b2› assms(1) assms(2) by blast
qed
lemma partitionI:
fixes A :: "'a set" and B :: "('a set) set"
assumes "⋃B = A"
and "⋀b1 b2. ⟦ b1 ∈ B; b2 ∈ B ⟧ ⟹ b1 ∩ b2 ≠ {} ⟹ b1 = b2"
shows "partition A B"
proof
show "⋀a. a ∈ A ⟹ ∃!b. b ∈ B ∧ a ∈ b"
proof (rule ccontr)
fix a assume "a ∈ A" "∄!b. b ∈ B ∧ a ∈ b"
then obtain b1 b2 where "b1 ∈ B" "a ∈ b1"
and "b2 ∈ B" "a ∈ b2" "b1 ≠ b2" using assms(1) by blast
thus False using assms(2) by blast
qed
next
show "⋀b. b ∈ B ⟹ b ⊆ A" using assms(1) by blast
qed
lemma (in partition) remove_elem:
assumes "b ∈ B"
shows "partition (A - b) (B - {b})"
proof
show "⋀a. a ∈ A - b ⟹ ∃!b'. b' ∈ B - {b} ∧ a ∈ b'"
using unique_class by fastforce
next
show "⋀b'. b' ∈ B - {b} ⟹ b' ⊆ A - b"
using assms unique_class incl partition_axioms partition_coverture by fastforce
qed
lemma disjoint_sum:
"⟦ finite B; finite A; partition A B⟧ ⟹ (∑b∈B. ∑a∈b. f a) = (∑a∈A. f a)"
proof (induct arbitrary: A set: finite)
case empty thus ?case using partition.unique_class by fastforce
next
case (insert b B')
have "(∑b∈(insert b B'). ∑a∈b. f a) = (∑a∈b. f a) + (∑b∈B'. ∑a∈b. f a)"
by (simp add: insert.hyps(1) insert.hyps(2))
also have "... = (∑a∈b. f a) + (∑a∈(A - b). f a)"
using partition.remove_elem[of A "insert b B'" b] insert.hyps insert.prems
by (metis Diff_insert_absorb finite_Diff insert_iff)
finally show "(∑b∈(insert b B'). ∑a∈b. f a) = (∑a∈A. f a)"
using partition.remove_elem[of A "insert b B'" b] insert.prems
by (metis add.commute insert_iff partition.incl sum.subset_diff)
qed
lemma (in partition) disjoint_sum:
assumes "finite A"
shows "(∑b∈B. ∑a∈b. f a) = (∑a∈A. f a)"
proof -
have "finite B"
by (simp add: assms finite_UnionD partition_coverture)
thus ?thesis using disjoint_sum assms partition_axioms by blast
qed
lemma (in equivalence) set_eq_insert_aux:
assumes "A ⊆ carrier S"
and "x ∈ carrier S" "x' ∈ carrier S" "x .= x'"
and "y ∈ insert x A"
shows "y .∈ insert x' A"
by (metis assms(1) assms(4) assms(5) contra_subsetD elemI elem_exact insert_iff)
corollary (in equivalence) set_eq_insert:
assumes "A ⊆ carrier S"
and "x ∈ carrier S" "x' ∈ carrier S" "x .= x'"
shows "insert x A {.=} insert x' A"
by (meson set_eqI assms set_eq_insert_aux sym equivalence_axioms)
lemma (in equivalence) set_eq_pairI:
assumes xx': "x .= x'"
and carr: "x ∈ carrier S" "x' ∈ carrier S" "y ∈ carrier S"
shows "{x, y} {.=} {x', y}"
using assms set_eq_insert by simp
lemma (in equivalence) closure_inclusion:
assumes "A ⊆ B"
shows "closure_of A ⊆ closure_of B"
unfolding eq_closure_of_def using assms elem_subsetD by auto
lemma (in equivalence) classes_small:
assumes "is_closed B"
and "A ⊆ B"
shows "closure_of A ⊆ B"
by (metis assms closure_inclusion eq_is_closed_def)
lemma (in equivalence) classes_eq:
assumes "A ⊆ carrier S"
shows "A {.=} closure_of A"
using assms by (blast intro: set_eqI elem_exact closure_of_memI elim: closure_of_memE)
lemma (in equivalence) complete_classes:
assumes "is_closed A"
shows "A = closure_of A"
using assms by (simp add: eq_is_closed_def)
lemma (in equivalence) closure_idem_weak:
"closure_of (closure_of A) {.=} closure_of A"
by (simp add: classes_eq set_eq_sym)
lemma (in equivalence) closure_idem_strong:
assumes "A ⊆ carrier S"
shows "closure_of (closure_of A) = closure_of A"
using assms closure_of_eq complete_classes is_closedI by auto
lemma (in equivalence) classes_consistent:
assumes "A ⊆ carrier S"
shows "is_closed (closure_of A)"
using closure_idem_strong by (simp add: assms eq_is_closed_def)
lemma (in equivalence) classes_coverture:
"⋃classes = carrier S"
proof
show "⋃classes ⊆ carrier S"
unfolding eq_classes_def eq_class_of_def by blast
next
show "carrier S ⊆ ⋃classes" unfolding eq_classes_def eq_class_of_def
proof
fix x assume "x ∈ carrier S"
hence "x ∈ {y ∈ carrier S. x .= y}" using refl by simp
thus "x ∈ ⋃{{y ∈ carrier S. x .= y} |x. x ∈ carrier S}" by blast
qed
qed
lemma (in equivalence) disjoint_union:
assumes "class1 ∈ classes" "class2 ∈ classes"
and "class1 ∩ class2 ≠ {}"
shows "class1 = class2"
proof -
obtain x y where x: "x ∈ carrier S" "class1 = class_of x"
and y: "y ∈ carrier S" "class2 = class_of y"
using assms(1-2) unfolding eq_classes_def by blast
obtain z where z: "z ∈ carrier S" "z ∈ class1 ∩ class2"
using assms classes_coverture by fastforce
hence "x .= z ∧ y .= z" using x y unfolding eq_class_of_def by blast
hence "x .= y" using x y z trans sym by meson
hence "class_of x = class_of y"
unfolding eq_class_of_def using local.sym trans x y by blast
thus ?thesis using x y by simp
qed
lemma (in equivalence) partition_from_equivalence:
"partition (carrier S) classes"
proof (intro partitionI)
show "⋃classes = carrier S" using classes_coverture by simp
next
show "⋀class1 class2. ⟦ class1 ∈ classes; class2 ∈ classes ⟧ ⟹
class1 ∩ class2 ≠ {} ⟹ class1 = class2"
using disjoint_union by simp
qed
lemma (in equivalence) disjoint_sum:
assumes "finite (carrier S)"
shows "(∑c∈classes. ∑x∈c. f x) = (∑x∈(carrier S). f x)"
proof -
have "finite classes"
unfolding eq_classes_def using assms by auto
thus ?thesis using disjoint_sum assms partition_from_equivalence by blast
qed
end