|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Simplices.thy
Sprache: 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.30Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
|
|
|
|
|
