Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Congruence.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Algebra/Congruence.thy
    Author:     Clemens Ballarin, started 3 January 2008
    with thanks to Paulo Emílio de Vilhena
*)

theory Congruence
  imports
    Main
    "HOL-Library.FuncSet"
begin

section \<open>Objects\<close>

subsection \<open>Structure with Carrier Set.\<close>

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 \<open>Structure with Carrier and Equivalence Relation \<open>eq\<close>\<close>

record 'a eq_object = "'a partial_object" +
  eq :: "'a \ 'a \ bool" (infixl ".=\" 50)

definition
  elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50)
  where "x .\\<^bsub>S\<^esub> A \ (\y \ A. x .=\<^bsub>S\<^esub> y)"

definition
  set_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.=}\" 50)
  where "A {.=}\<^bsub>S\<^esub> B \ ((\x \ A. x .\\<^bsub>S\<^esub> B) \ (\x \ B. x .\\<^bsub>S\<^esub> A))"

definition
  eq_class_of :: "_ \ 'a \ 'a set" ("class'_of\")
  where "class_of\<^bsub>S\<^esub> x = {y \ carrier S. x .=\<^bsub>S\<^esub> y}"

definition
  eq_classes :: "_ \ ('a set) set" ("classes\")
  where "classes\<^bsub>S\<^esub> = {class_of\<^bsub>S\<^esub> x | x. x \ carrier S}"

definition
  eq_closure_of :: "_ \ 'a set \ 'a set" ("closure'_of\")
  where "closure_of\<^bsub>S\<^esub> A = {y \ carrier S. y .\\<^bsub>S\<^esub> A}"

definition
  eq_is_closed :: "_ \ 'a set \ bool" ("is'_closed\")
  where "is_closed\<^bsub>S\<^esub> A \ A \ carrier S \ closure_of\<^bsub>S\<^esub> A = A"

abbreviation
  not_eq :: "_ \ 'a \ 'a \ bool" (infixl ".\\" 50)
  where "x .\\<^bsub>S\<^esub> y \ \(x .=\<^bsub>S\<^esub> y)"

abbreviation
  not_elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50)
  where "x .\\<^bsub>S\<^esub> A \ \(x .\\<^bsub>S\<^esub> A)"

abbreviation
  set_not_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.\}\" 50)
  where "A {.\}\<^bsub>S\<^esub> B \ \(A {.=}\<^bsub>S\<^esub> 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 equivalenceI:
  fixes P :: "'a \ 'a \ bool" and E :: "'a set"
  assumes refl: "\x. \ x \ E \ \ P x x"
    and    sym: "\x y. \ x \ E; y \ E \ \ P x y \ P y x"
    and  trans: "\x y z. \ x \ E; y \ E; z \ E \ \ P x y \ P y z \ P x z"
  shows "equivalence \ carrier = E, eq = P \"
  unfolding equivalence_def using assms
  by (metis eq_object.select_convs(1) partial_object.select_convs(1))

locale partition =
  fixes A :: "'a set" and B :: "('a set) set"
  assumes unique_class: "\a. a \ A \ \!b \ B. a \ b"
    and incl: "\b. b \ B \ b \ A"

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

(* Lemmas by Stephan Hohe *)

lemma elemI:
  fixes R (structure)
  assumes "a' \ A" "a .= a'"
  shows "a .\ A"
  unfolding elem_def using assms by auto

lemma (in equivalence) elem_exact:
  assumes "a \ carrier S" "a \ A"
  shows "a .\ A"
  unfolding elem_def using assms by auto

lemma elemE:
  fixes S (structure)
  assumes "a .\ A"
    and "\a'. \a' \ A; a .= a'\ \ P"
  shows "P"
  using assms unfolding elem_def by auto

lemma (in equivalence) elem_cong_l [trans]:
  assumes "a \ carrier S" "a' \ carrier S" "A \ carrier S"
    and "a' .= a" "a .\ A"
  shows "a' .\ A"
  using assms by (meson elem_def trans subsetCE)

lemma (in equivalence) elem_subsetD:
  assumes "A \ B" "a .\ A"
  shows "a .\ B"
  using assms by (fast intro: elemI elim: elemE dest: subsetD)

lemma (in equivalence) mem_imp_elem [simp, intro]:
  assumes "x \ carrier S"
  shows "x \ A \ x .\ A"
  using assms unfolding elem_def by blast

lemma set_eqI:
  fixes R (structure)
  assumes "\a. a \ A \ a .\ B"
    and   "\b. b \ B \ b .\ A"
  shows "A {.=} B"
  using assms unfolding set_eq_def by auto

lemma set_eqI2:
  fixes R (structure)
  assumes "\a. a \ A \ \b \ B. a .= b"
    and   "\b. b \ B \ \a \ A. b .= a"
  shows "A {.=} B"
  using assms by (simp add: set_eqI elem_def)

lemma set_eqD1:
  fixes R (structure)
  assumes "A {.=} A'" and "a \ A"
  shows "\a'\A'. a .= a'"
  using assms by (simp add: set_eq_def elem_def)

lemma set_eqD2:
  fixes R (structure)
  assumes "A {.=} A'" and "a' \ A'"
  shows "\a\A. a' .= a"
  using assms by (simp add: set_eq_def elem_def)

lemma set_eqE:
  fixes R (structure)
  assumes "A {.=} B"
    and "\ \a \ A. a .\ B; \b \ B. b .\ A \ \ P"
  shows "P"
  using assms unfolding set_eq_def by blast

lemma set_eqE2:
  fixes R (structure)
  assumes "A {.=} B"
    and "\ \a \ A. \b \ B. a .= b; \b \ B. \a \ A. b .= a \ \ P"
  shows "P"
  using assms unfolding set_eq_def by (simp add: elem_def)

lemma set_eqE':
  fixes R (structure)
  assumes "A {.=} B" "a \ A" "b \ B"
    and "\a' b'. \ a' \ A; b' \ B \ \ b .= a' \ a .= b' \ P"
  shows "P"
  using assms by (meson set_eqE2)

lemma (in equivalence) eq_elem_cong_r [trans]:
  assumes "A \ carrier S" "A' \ carrier S" "A {.=} A'"
  shows "\ a \ carrier S \ \ a .\ A \ a .\ A'"
  using assms by (meson elemE elem_cong_l set_eqE subset_eq)

lemma (in equivalence) set_eq_sym [sym]:
  assumes "A \ carrier S" "B \ carrier S"
  shows "A {.=} B \ B {.=} A"
  using assms unfolding set_eq_def elem_def by auto

lemma (in equivalence) equal_set_eq_trans [trans]:
  "\ A = B; B {.=} C \ \ A {.=} C"
  by simp

lemma (in equivalence) set_eq_equal_trans [trans]:
  "\ A {.=} B; B = C \ \ A {.=} C"
  by simp

lemma (in equivalence) set_eq_trans_aux:
  assumes "A \ carrier S" "B \ carrier S" "C \ carrier S"
    and "A {.=} B" "B {.=} C"
  shows "\a. a \ A \ a .\ C"
  using assms by (simp add: eq_elem_cong_r subset_iff)

corollary (in equivalence) set_eq_trans [trans]:
  assumes "A \ carrier S" "B \ carrier S" "C \ carrier S"
    and "A {.=} B" " B {.=} C"
  shows "A {.=} C"
proof (intro set_eqI)
  show "\a. a \ A \ a .\ C" using set_eq_trans_aux assms by blast
next
  show "\b. b \ C \ b .\ A" using set_eq_trans_aux set_eq_sym assms by blast
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:
  assumes "A \ carrier S" "x \ closure_of A"
  shows "\ x' \ carrier S; x .= x' \ \ x' \ closure_of A"
  using assms elem_cong_l sym unfolding eq_closure_of_def by blast

lemma (in equivalence) is_closed_eq [dest]:
  assumes "is_closed A" "x \ A"
  shows "\ x .= x'; x' \ carrier S \ \ x' \ A"
  using assms closure_of_eq [where A = A] unfolding eq_is_closed_def by simp

corollary (in equivalence) is_closed_eq_rev [dest]:
  assumes "is_closed A" "x' \ A"
  shows "\ x .= x'; x \ carrier S \ \ x \ A"
  using sym is_closed_eq assms by (meson contra_subsetD eq_is_closed_def)

lemma closure_of_closed [simp, intro]:
  fixes S (structure)
  shows "closure_of A \ carrier S"
  unfolding eq_closure_of_def by auto

lemma closure_of_memI:
  fixes S (structure)
  assumes "a .\ A" "a \ carrier S"
  shows "a \ closure_of A"
  by (simp add: assms eq_closure_of_def)

lemma closure_ofI2:
  fixes S (structure)
  assumes "a .= a'" and "a' \ A" and "a \ carrier S"
  shows "a \ closure_of A"
  by (meson assms closure_of_memI elem_def)

lemma closure_of_memE:
  fixes S (structure)
  assumes "a \ closure_of A"
    and "\a \ carrier S; a .\ A\ \ P"
  shows "P"
  using eq_closure_of_def assms by fastforce

lemma closure_ofE2:
  fixes S (structure)
  assumes "a \ closure_of A"
    and "\a'. \a \ carrier S; a' \ A; a .= a'\ \ P"
  shows "P"
  using assms by (meson closure_of_memE elemE)

lemma (in partition) equivalence_from_partition: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  "equivalence \ carrier = A, eq = (\x y. y \ (THE b. b \ B \ x \ b))\"
    unfolding partition_def equivalence_def
proof (auto)
  let ?f = "\x. THE b. b \ B \ x \ b"
  show "\x. x \ A \ x \ ?f x"
    using unique_class by (metis (mono_tags, lifting) theI')
  show "\x y. \ x \ A; y \ A \ \ y \ ?f x \ x \ ?f y"
    using unique_class by (metis (mono_tags, lifting) the_equality)
  show "\x y z. \ x \ A; y \ A; z \ A \ \ y \ ?f x \ z \ ?f y \ z \ ?f x"
    using unique_class by (metis (mono_tags, lifting) the_equality)
qed

lemma (in partition) partition_coverture: "\B = A" \<^marker>\contributor \Paulo Emílio de Vilhena\\
  by (meson Sup_le_iff UnionI unique_class incl subsetI subset_antisym)

lemma (in partition) disjoint_union: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "b1 \ B" "b2 \ B"
    and "b1 \ b2 \ {}"
  shows "b1 = b2"
proof (rule ccontr)
  assume "b1 \ b2"
  obtain a where "a \ A" "a \ b1" "a \ b2"
    using assms(2-3) incl by blast
  thus False using unique_class \<open>b1 \<noteq> b2\<close> assms(1) assms(2) by blast
qed

lemma partitionI: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  fixes A :: "'a set" and B :: "('a set) set"
  assumes "\B = A"
    and "\b1 b2. \ b1 \ B; b2 \ B \ \ b1 \ b2 \ {} \ b1 = b2"
  shows "partition A B"
proof
  show "\a. a \ A \ \!b. b \ B \ a \ b"
  proof (rule ccontr)
    fix a assume "a \ A" "\!b. b \ B \ a \ b"
    then obtain b1 b2 where "b1 \ B" "a \ b1"
                        and "b2 \ B" "a \ b2" "b1 \ b2" using assms(1) by blast
    thus False using assms(2) by blast
  qed
next
  show "\b. b \ B \ b \ A" using assms(1) by blast
qed

lemma (in partition) remove_elem: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "b \ B"
  shows "partition (A - b) (B - {b})"
proof
  show "\a. a \ A - b \ \!b'. b' \ B - {b} \ a \ b'"
    using unique_class by fastforce
next
  show "\b'. b' \ B - {b} \ b' \ A - b"
    using assms unique_class incl partition_axioms partition_coverture by fastforce
qed

lemma disjoint_sum: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  "\ finite B; finite A; partition A B\ \ (\b\B. \a\b. f a) = (\a\A. f a)"
proof (induct arbitrary: A set: finite)
  case empty thus ?case using partition.unique_class by fastforce
next
  case (insert b B')
  have "(\b\(insert b B'). \a\b. f a) = (\a\b. f a) + (\b\B'. \a\b. f a)"
    by (simp add: insert.hyps(1) insert.hyps(2))
  also have "... = (\a\b. f a) + (\a\(A - b). f a)"
    using partition.remove_elem[of A "insert b B'" b] insert.hyps insert.prems
    by (metis Diff_insert_absorb finite_Diff insert_iff)
  finally show "(\b\(insert b B'). \a\b. f a) = (\a\A. f a)"
    using partition.remove_elem[of A "insert b B'" b] insert.prems
    by (metis add.commute insert_iff partition.incl sum.subset_diff)
qed

lemma (in partition) disjoint_sum: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "finite A"
  shows "(\b\B. \a\b. f a) = (\a\A. f a)"
proof -
  have "finite B"
    by (simp add: assms finite_UnionD partition_coverture)
  thus ?thesis using disjoint_sum assms partition_axioms by blast
qed

lemma (in equivalence) set_eq_insert_aux: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "A \ carrier S"
    and "x \ carrier S" "x' \ carrier S" "x .= x'"
    and "y \ insert x A"
  shows "y .\ insert x' A"
  by (metis assms(1) assms(4) assms(5) contra_subsetD elemI elem_exact insert_iff)

corollary (in equivalence) set_eq_insert: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "A \ carrier S"
    and "x \ carrier S" "x' \ carrier S" "x .= x'"
  shows "insert x A {.=} insert x' A"
  by (meson set_eqI assms set_eq_insert_aux sym equivalence_axioms)

lemma (in equivalence) set_eq_pairI: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes xx': "x .= x'"
    and carr: "x \ carrier S" "x' \ carrier S" "y \ carrier S"
  shows "{x, y} {.=} {x', y}"
  using assms set_eq_insert by simp

lemma (in equivalence) closure_inclusion:
  assumes "A \ B"
  shows "closure_of A \ closure_of B"
  unfolding eq_closure_of_def using assms elem_subsetD by auto

lemma (in equivalence) classes_small:
  assumes "is_closed B"
    and "A \ B"
  shows "closure_of A \ B"
  by (metis assms closure_inclusion eq_is_closed_def)

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 "is_closed A"
  shows "A = closure_of A"
  using assms by (simp add: eq_is_closed_def)

lemma (in equivalence) closure_idem_weak:
  "closure_of (closure_of A) {.=} closure_of A"
  by (simp add: classes_eq set_eq_sym)

lemma (in equivalence) closure_idem_strong:
  assumes "A \ carrier S"
  shows "closure_of (closure_of A) = closure_of A"
  using assms closure_of_eq complete_classes is_closedI by auto

lemma (in equivalence) classes_consistent:
  assumes "A \ carrier S"
  shows "is_closed (closure_of A)"
  using closure_idem_strong by (simp add: assms eq_is_closed_def)

lemma (in equivalence) classes_coverture:
  "\classes = carrier S"
proof
  show "\classes \ carrier S"
    unfolding eq_classes_def eq_class_of_def by blast
next
  show "carrier S \ \classes" unfolding eq_classes_def eq_class_of_def
  proof
    fix x assume "x \ carrier S"
    hence "x \ {y \ carrier S. x .= y}" using refl by simp
    thus "x \ \{{y \ carrier S. x .= y} |x. x \ carrier S}" by blast
  qed
qed

lemma (in equivalence) disjoint_union:
  assumes "class1 \ classes" "class2 \ classes"
    and "class1 \ class2 \ {}"
    shows "class1 = class2"
proof -
  obtain x y where x: "x \ carrier S" "class1 = class_of x"
               and y: "y \ carrier S" "class2 = class_of y"
    using assms(1-2) unfolding eq_classes_def by blast
  obtain z   where z: "z \ carrier S" "z \ class1 \ class2"
    using assms classes_coverture by fastforce
  hence "x .= z \ y .= z" using x y unfolding eq_class_of_def by blast
  hence "x .= y" using x y z trans sym by meson
  hence "class_of x = class_of y"
    unfolding eq_class_of_def using local.sym trans x y by blast
  thus ?thesis using x y by simp
qed

lemma (in equivalence) partition_from_equivalence:
  "partition (carrier S) classes"
proof (intro partitionI)
  show "\classes = carrier S" using classes_coverture by simp
next
  show "\class1 class2. \ class1 \ classes; class2 \ classes \ \
                          class1 \<inter> class2 \<noteq> {} \<Longrightarrow> class1 = class2"
    using disjoint_union by simp
qed

lemma (in equivalence) disjoint_sum:
  assumes "finite (carrier S)"
  shows "(\c\classes. \x\c. f x) = (\x\(carrier S). f x)"
proof -
  have "finite classes"
    unfolding eq_classes_def using assms by auto
  thus ?thesis using disjoint_sum assms partition_from_equivalence by blast
qed

end

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.