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 ".=\<index>" 50)
definition
elem :: "_ => 'a => 'a set => bool" (infixl ".∈\<index>" 50)
where "x .∈⇘S⇙ A <-> (∃y ∈ A. x .=⇘S⇙ y)"
definition
set_eq :: "_ => 'a set => 'a set => bool" (infixl "{.=}\<index>" 50)
where "A {.=}⇘S⇙ B <-> ((∀x ∈ A. x .∈⇘S⇙ B) ∧ (∀x ∈ B. x .∈⇘S⇙ A))"
definition
eq_class_of :: "_ => 'a => 'a set" ("class'_of\<index>")
where "class_of⇘S⇙ x = {y ∈ carrier S. x .=⇘S⇙ y}"
definition
eq_closure_of :: "_ => 'a set => 'a set" ("closure'_of\<index>")
where "closure_of⇘S⇙ A = {y ∈ carrier S. y .∈⇘S⇙ A}"
definition
eq_is_closed :: "_ => 'a set => bool" ("is'_closed\<index>")
where "is_closed⇘S⇙ A <-> A ⊆ carrier S ∧ closure_of⇘S⇙ A = A"
abbreviation
not_eq :: "_ => 'a => 'a => bool" (infixl ".≠\<index>" 50)
where "x .≠⇘S⇙ y == ~(x .=⇘S⇙ y)"
abbreviation
not_elem :: "_ => 'a => 'a set => bool" (infixl ".∉\<index>" 50)
where "x .∉⇘S⇙ A == ~(x .∈⇘S⇙ A)"
abbreviation
set_not_eq :: "_ => 'a set => 'a set => bool" (infixl "{.≠}\<index>" 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