(* 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_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"

(* 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