theory Congruence
imports Main
begin
section ‹Objects›
subsection ‹Structure with Carrier Set.›
record 'a partial_object =
carrier :: "'a set"
subsection ‹Structure with Carrier and Equivalence Relation @{text 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_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 elemI:
fixes R (structure)
assumes "a' ∈ A" and "a .= a'"
shows "a .∈ A"
unfolding elem_def
using assms
by fast
lemma (in equivalence) elem_exact:
assumes "a ∈ carrier S" and "a ∈ A"
shows "a .∈ A"
using assms
by (fast intro: elemI)
lemma elemE:
fixes S (structure)
assumes "a .∈ A"
and "⋀a'. ⟦a' ∈ A; a .= a'⟧ ⟹ P"
shows "P"
using assms
unfolding elem_def
by fast
lemma (in equivalence) elem_cong_l [trans]:
assumes cong: "a' .= a"
and a: "a .∈ A"
and carr: "a ∈ carrier S" "a' ∈ carrier S"
and Acarr: "A ⊆ carrier S"
shows "a' .∈ A"
using a
apply (elim elemE, intro elemI)
proof assumption
fix b
assume bA: "b ∈ A"
note [simp] = carr bA[THEN subsetD[OF Acarr]]
note cong
also assume "a .= b"
finally show "a' .= b" by simp
qed
lemma (in equivalence) elem_subsetD:
assumes "A ⊆ B"
and aA: "a .∈ A"
shows "a .∈ B"
using assms
by (fast intro: elemI elim: elemE dest: subsetD)
lemma (in equivalence) mem_imp_elem [simp, intro]:
"[| x ∈ A; x ∈ carrier S |] ==> x .∈ A"
unfolding elem_def by blast
lemma set_eqI:
fixes R (structure)
assumes ltr: "⋀a. a ∈ A ⟹ a .∈ B"
and rtl: "⋀b. b ∈ B ⟹ b .∈ A"
shows "A {.=} B"
unfolding set_eq_def
by (fast intro: ltr rtl)
lemma set_eqI2:
fixes R (structure)
assumes ltr: "⋀a b. a ∈ A ⟹ ∃b∈B. a .= b"
and rtl: "⋀b. b ∈ B ⟹ ∃a∈A. b .= a"
shows "A {.=} B"
by (intro set_eqI, unfold elem_def) (fast intro: ltr rtl)+
lemma set_eqD1:
fixes R (structure)
assumes AA': "A {.=} A'"
and "a ∈ A"
shows "∃a'∈A'. a .= a'"
using assms
unfolding set_eq_def elem_def
by fast
lemma set_eqD2:
fixes R (structure)
assumes AA': "A {.=} A'"
and "a' ∈ A'"
shows "∃a∈A. a' .= a"
using assms
unfolding set_eq_def elem_def
by fast
lemma set_eqE:
fixes R (structure)
assumes AB: "A {.=} B"
and r: "⟦∀a∈A. a .∈ B; ∀b∈B. b .∈ A⟧ ⟹ P"
shows "P"
using AB
unfolding set_eq_def
by (blast dest: r)
lemma set_eqE2:
fixes R (structure)
assumes AB: "A {.=} B"
and r: "⟦∀a∈A. (∃b∈B. a .= b); ∀b∈B. (∃a∈A. b .= a)⟧ ⟹ P"
shows "P"
using AB
unfolding set_eq_def elem_def
by (blast dest: r)
lemma set_eqE':
fixes R (structure)
assumes AB: "A {.=} B"
and aA: "a ∈ A" and bB: "b ∈ B"
and r: "⋀a' b'. ⟦a' ∈ A; b .= a'; b' ∈ B; a .= b'⟧ ⟹ P"
shows "P"
proof -
from AB aA
have "∃b'∈B. a .= b'" by (rule set_eqD1)
from this obtain b'
where b': "b' ∈ B" "a .= b'" by auto
from AB bB
have "∃a'∈A. b .= a'" by (rule set_eqD2)
from this obtain a'
where a': "a' ∈ A" "b .= a'" by auto
from a' b'
show "P" by (rule r)
qed
lemma (in equivalence) eq_elem_cong_r [trans]:
assumes a: "a .∈ A"
and cong: "A {.=} A'"
and carr: "a ∈ carrier S"
and Carr: "A ⊆ carrier S" "A' ⊆ carrier S"
shows "a .∈ A'"
using a cong
proof (elim elemE set_eqE)
fix b
assume bA: "b ∈ A"
and inA': "∀b∈A. b .∈ A'"
note [simp] = carr Carr Carr[THEN subsetD] bA
assume "a .= b"
also from bA inA'
have "b .∈ A'" by fast
finally
show "a .∈ A'" by simp
qed
lemma (in equivalence) set_eq_sym [sym]:
assumes "A {.=} B"
and "A ⊆ carrier S" "B ⊆ carrier S"
shows "B {.=} A"
using assms
unfolding set_eq_def elem_def
by fast
lemma (in equivalence) equal_set_eq_trans [trans]:
assumes AB: "A = B" and BC: "B {.=} C"
shows "A {.=} C"
using AB BC by simp
lemma (in equivalence) set_eq_equal_trans [trans]:
assumes AB: "A {.=} B" and BC: "B = C"
shows "A {.=} C"
using AB BC by simp
lemma (in equivalence) set_eq_trans [trans]:
assumes AB: "A {.=} B" and BC: "B {.=} C"
and carr: "A ⊆ carrier S" "B ⊆ carrier S" "C ⊆ carrier S"
shows "A {.=} C"
proof (intro set_eqI)
fix a
assume aA: "a ∈ A"
with carr have "a ∈ carrier S" by fast
note [simp] = carr this
from aA
have "a .∈ A" by (simp add: elem_exact)
also note AB
also note BC
finally
show "a .∈ C" by simp
next
fix c
assume cC: "c ∈ C"
with carr have "c ∈ carrier S" by fast
note [simp] = carr this
from cC
have "c .∈ C" by (simp add: elem_exact)
also note BC[symmetric]
also note AB[symmetric]
finally
show "c .∈ A" by simp
qed
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}"
unfolding set_eq_def elem_def
proof safe
have "x' ∈ {x', y}" by fast
with xx' show "∃b∈{x', y}. x .= b" by fast
next
have "y ∈ {x', y}" by fast
with carr show "∃b∈{x', y}. y .= b" by fast
next
have "x ∈ {x, y}" by fast
with xx'[symmetric] carr
show "∃a∈{x, y}. x' .= a" by fast
next
have "y ∈ {x, y}" by fast
with carr show "∃a∈{x, y}. y .= a" by fast
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:
"[| x .= x'; A ⊆ carrier S; x ∈ closure_of A; x ∈ carrier S; x' ∈ carrier S |] ==> x' ∈ closure_of A"
unfolding eq_closure_of_def elem_def
by (blast intro: trans sym)
lemma (in equivalence) is_closed_eq [dest]:
"[| x .= x'; x ∈ A; is_closed A; x ∈ carrier S; x' ∈ carrier S |] ==> x' ∈ A"
unfolding eq_is_closed_def
using closure_of_eq [where A = A]
by simp
lemma (in equivalence) is_closed_eq_rev [dest]:
"[| x .= x'; x' ∈ A; is_closed A; x ∈ carrier S; x' ∈ carrier S |] ==> x ∈ A"
by (drule sym) (simp_all add: is_closed_eq)
lemma closure_of_closed [simp, intro]:
fixes S (structure)
shows "closure_of A ⊆ carrier S"
unfolding eq_closure_of_def
by fast
lemma closure_of_memI:
fixes S (structure)
assumes "a .∈ A"
and "a ∈ carrier S"
shows "a ∈ closure_of A"
unfolding eq_closure_of_def
using assms
by fast
lemma closure_ofI2:
fixes S (structure)
assumes "a .= a'"
and "a' ∈ A"
and "a ∈ carrier S"
shows "a ∈ closure_of A"
unfolding eq_closure_of_def elem_def
using assms
by fast
lemma closure_of_memE:
fixes S (structure)
assumes p: "a ∈ closure_of A"
and r: "⟦a ∈ carrier S; a .∈ A⟧ ⟹ P"
shows "P"
proof -
from p
have acarr: "a ∈ carrier S"
and "a .∈ A"
by (simp add: eq_closure_of_def)+
thus "P" by (rule r)
qed
lemma closure_ofE2:
fixes S (structure)
assumes p: "a ∈ closure_of A"
and r: "⋀a'. ⟦a ∈ carrier S; a' ∈ A; a .= a'⟧ ⟹ P"
shows "P"
proof -
from p have acarr: "a ∈ carrier S" by (simp add: eq_closure_of_def)
from p have "∃a'∈A. a .= a'" by (simp add: eq_closure_of_def elem_def)
from this obtain a'
where "a' ∈ A" and "a .= a'" by auto
from acarr and this
show "P" by (rule r)
qed
end