(* Title: HOL/Algebra/Congruence.thy Author: Clemens Ballarin, started 3 January 2008 Copyright: Clemens Ballarin *) 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_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" (* 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) *) 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 end