# Theory Congruence

Up to index of Isabelle/HOL/Free-Groups

theory Congruence
imports Main
`(*  Title:      HOL/Algebra/Congruence.thy    Author:     Clemens Ballarin, started 3 January 2008    Copyright:  Clemens Ballarin*)theory Congruenceimports Mainbeginsection {* 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_defusing assmsby fastlemma (in equivalence) elem_exact:  assumes "a ∈ carrier S" and "a ∈ A"  shows "a .∈ A"using assmsby (fast intro: elemI)lemma elemE:  fixes S (structure)  assumes "a .∈ A"    and "!!a'. [|a' ∈ A; a .= a'|] ==> P"  shows "P"using assmsunfolding elem_defby fastlemma (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 aapply (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 simpqedlemma (in equivalence) elem_subsetD:  assumes "A ⊆ B"    and aA: "a .∈ A"  shows "a .∈ B"using assmsby (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 blastlemma 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_defby (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 assmsunfolding set_eq_def elem_defby fastlemma set_eqD2:  fixes R (structure)  assumes AA': "A {.=} A'"    and "a' ∈ A'"  shows "∃a∈A. a' .= a"using assmsunfolding set_eq_def elem_defby fastlemma set_eqE:  fixes R (structure)  assumes AB: "A {.=} B"    and r: "[|∀a∈A. a .∈ B; ∀b∈B. b .∈ A|] ==> P"  shows "P"using ABunfolding set_eq_defby (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 ABunfolding set_eq_def elem_defby (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)qedlemma (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 congproof (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 simpqedlemma (in equivalence) set_eq_sym [sym]:  assumes "A {.=} B"    and "A ⊆ carrier S" "B ⊆ carrier S"  shows "B {.=} A"using assmsunfolding set_eq_def elem_defby 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 simplemma (in equivalence) set_eq_equal_trans [trans]:  assumes AB: "A {.=} B" and BC: "B = C"  shows "A {.=} C"  using AB BC by simplemma (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 simpnext  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 simpqed(* 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_defapply ruleapply ruleapply (case_tac "xa = x")using x apply fastapply (subgoal_tac "xa ∈ A") prefer 2 apply fastapply (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_defproof safe  have "x' ∈ {x', y}" by fast  with xx' show "∃b∈{x', y}. x .= b" by fastnext  have "y ∈ {x', y}" by fast  with carr show "∃b∈{x', y}. y .= b" by fastnext  have "x ∈ {x, y}" by fast  with xx'[symmetric] carr  show "∃a∈{x, y}. x' .= a" by fastnext  have "y ∈ {x, y}" by fast  with carr show "∃a∈{x, y}. y .= a" by fastqedlemma (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 simplemma (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_defby fastlemma closure_of_memI:  fixes S (structure)  assumes "a .∈ A"    and "a ∈ carrier S"  shows "a ∈ closure_of A"unfolding eq_closure_of_defusing assmsby fastlemma 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_defusing assmsby fastlemma 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)qedlemma 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 assmsapply (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 simpqed*)(*lemma (in equivalence) classes_small:  assumes "is_closed B"    and "A ⊆ B"  shows "closure_of A ⊆ B"using assmsby (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 assmsby (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 assmsby (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE)*)end`