Theory Congruence

theory Congruence
imports Main
(*  Title:      HOL/Algebra/Congruence.thy
Author: Clemens Ballarin, started 3 January 2008
Copyright: Clemens Ballarin
*)


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_ofS x = {y ∈ carrier S. x .=S y}"

definition
eq_closure_of :: "_ => 'a set => 'a set" ("closure'_of\<index>")
where "closure_ofS A = {y ∈ carrier S. y .∈S A}"

definition
eq_is_closed :: "_ => 'a set => bool" ("is'_closed\<index>")
where "is_closedS A <-> A ⊆ carrier S ∧ closure_ofS 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"

(* Lemmas by Stephan Hohe *)

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

(* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *)
(* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *)

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

(* FIXME: generalise for insert *)

(*
lemma (in equivalence) set_eq_insert:
assumes x: "x .= x'"
and carr: "x ∈ carrier S" "x' ∈ carrier S" "A ⊆ carrier S"
shows "insert x A {.=} insert x' A"
unfolding set_eq_def elem_def
apply rule
apply rule
apply (case_tac "xa = x")
using x apply fast
apply (subgoal_tac "xa ∈ A") prefer 2 apply fast
apply (rule_tac x=xa in bexI)
using carr apply (rule_tac refl) apply auto [1]
apply safe
*)


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

(*
lemma (in equivalence) classes_consistent:
assumes Acarr: "A ⊆ carrier S"
shows "is_closed (closure_of A)"
apply (blast intro: elemI elim elemE)
using assms
apply (intro is_closedI closure_of_memI, simp)
apply (elim elemE closure_of_memE)
proof -
fix x a' a''
assume carr: "x ∈ carrier S" "a' ∈ carrier S"
assume a''A: "a'' ∈ A"
with Acarr have "a'' ∈ carrier S" by fast
note [simp] = carr this Acarr

assume "x .= a'"
also assume "a' .= a''"
also from a''A
have "a'' .∈ A" by (simp add: elem_exact)
finally show "x .∈ A" by simp
qed
*)

(*
lemma (in equivalence) classes_small:
assumes "is_closed B"
and "A ⊆ B"
shows "closure_of A ⊆ B"
using assms
by (blast dest: is_closedD2 elem_subsetD elim: closure_of_memE)

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 c: "is_closed A"
shows "A = closure_of A"
using assms
by (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE)
*)


end