Eine aufbereitete Darstellung der Quelle
Stufen
Anforderungen
|
Konzepte
|
Entwurf
|
Entwicklung
|
Qualitätssicherung
|
Lebenszyklus
|
Steuerung
Ziele
Untersuchung
mit Columbo
Integrität von
Datenbanken
Interaktion und
Portierbarkeit
Ergonomie der
Schnittstellen
Angebot
Produkte
Projekt
Beratung
Mittel
Analytik
Modellierung
Sprachen
Algebra
Logik
Hardware
Denken
Kreativität
Zusammenhänge
Gesellschaft
Wirtschaft
Branche
Firma
Benutzer
products
/
Sources
/
formale Sprachen
/
C
/
LibreOffice
/
icon-themes
/
elementary
/
cmd
/
32
/ (
LibreOffice
Version 25.8.3.2
©
) Datei vom 5.10.2025 mit Größe 1 kB
Bilddatei
Kruskal_Misc.thy
products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Kruskal/Kruskal_Misc.thy
section "Auxilliary Lemmas" theory Kruskal_Misc imports "Collections.Partial_Equivalence_Relation" "Automatic_Refinement.Misc" Refine_Imperative_HOL.Sepref begin lemma card2_get2: assumes "card x = 2" obtains a b where "x = {a, b}" "a \
b" proof - from assms have [simp,intro!]: "finite x" apply(rule_tac ccontr) by auto from assms obtain a where ax: "a \
x" by fastforce with assms have "card (x - {a}) = 1" by fastforce then obtain b where "x - {a} = {b}" "a \
b" by (metis Diff_cancel Diff_idemp card_1_singletonE insert_not_empty) with that ax show ?thesis by blast qed subsection "Lemmas on equivalence relations" lemma equiv_sym: "equiv V R \
(x,y)\
R \
(y,x)\
R" by (metis equiv_def symD) lemma equiv_trans: "equiv V R \
(x,y)\
R \
(y,z)\
R \
(x,z)\
R" by (metis equiv_def transD) lemma equiv_trans_sym: "\
equiv V R; (a,b)\
R; (c,b)\
R \
\
(a,c)\
R" "\
equiv V R; (a,b)\
R; (a,c)\
R \
\
(b,c)\
R" apply (metis equiv_sym equiv_trans)+ done lemma union_equiv: assumes "equiv V R" shows "equiv V (per_union R a b)" proof (rule equivI) have "R \
V \
V" and "refl_on V R" and "sym R" and "trans R" using \
equiv V R\
by (auto elim: equivE) show "per_union R a b \
V \
V" using \
R \
V \
V\
by (auto simp: per_union_def) show "refl_on V (per_union R a b)" using \
refl_on V R\
by (auto simp: per_union_def refl_on_def) show "sym (per_union R a b)" using \
sym R\
by (auto simp: per_union_def sym_def) show "trans (per_union R a b)" using \
trans R\
by (metis \
sym R\
part_equiv_def union_part_equivp) qed lemma equiv_mono: assumes "E' \
E" and "equiv E R1" shows "equiv E' (R1 \
E'\
E')" proof (rule equivI) show "Restr R1 E' \
E' \
E'" by simp next have "refl_on E R1" using \
equiv E R1\
by (auto elim: equivE) thus "refl_on E' (Restr R1 E')" by (metis (lifting) ext Field_square Refl_Restr UNIV_I assms(1) inf.absorb_iff2 refl_on_Int refl_on_def subsetI) next have "sym R1" using \
equiv E R1\
by (auto elim: equivE) thus "sym (Restr R1 E')" by (metis mem_Sigma_iff symI sym_Int) next have "trans R1" using \
equiv E R1\
by (auto elim: equivE) thus "trans (Restr R1 E')" using trans_Restr by fastforce qed lemma unify2EquivClasses_alt: assumes "R``{x} \
R``{y}" and inV: "y\
V" "x\
V" and "R\
V\
V" and eq: "equiv V R" and [simp]: "finite V" shows "Suc (card (quotient V (per_union R x y))) = card (quotient V R)" proof - from eq have Rtrancl: "R\<^sup>+ = R" by (auto elim: equivE) from \
equiv V R\
have sym: "sym R" unfolding equiv_def by auto let ?R' = "per_union R x y" \
\
the equivalence classes not contining x and y, stay unchanged when performing @{term per_union} \
have "\
z. z \
V \
z \
R `` {x} \
z \
R `` {y} \
per_union R x y `` {z} = R `` {z}" using sym by(auto simp: sym_def per_union_def) then have K: "(\
x \
(V-(R``{x})-(R``{y})). {?R'``{x}}) = (\
x \
(V-(R``{x})-(R``{y})). {R``{x}})" by auto have R_respect: "(\
x. {R `` {x}}) respects R" unfolding congruent_def using eq equiv_class_eq_iff by fastforce+ have R'_respect: "(\
xa. {?R' `` {xa}}) respects R" unfolding congruent_def per_union_def using eq equiv_class_eq_iff by force+ \
\
some facts about the equivalence class of x, before and after the @{term per_union} operation\
have xdrin: "(R``{x}) \
V" using assms(4) by auto have x1: "(\
x \
(R``{x}). {?R'``{x}}) = {?R'``{x}}" apply(rule UN_equiv_class) by fact+ have x2: "(\
x \
(R``{x}). {R``{x}}) = {R``{x}}" apply(rule UN_equiv_class) by fact+ \
\
some facts about the equivalence class of y, before and after the @{term per_union} operation\
have ydrin: "(R``{y}) \
V" using assms(4) by auto have y1: "(\
x \
(R``{y}). {?R'``{x}}) = {?R'``{y}}" apply(rule UN_equiv_class) by fact+ have y2: "(\
x \
(R``{y}). {R``{x}}) = {R``{y}}" apply(rule UN_equiv_class) by fact+ have z: "(y,x)\
?R'" unfolding per_union_def using sym sym_def using assms(2) assms(3) eq eq_equiv_class by fastforce have bla: "?R'``{y} = ?R'``{x}" apply(rule equiv_class_eq) apply(rule union_equiv) apply fact by fact let ?Vm = "(\
x \
(V-(R``{x})-(R``{y})). {R``{x}})" \
\
now consider the set of quotients wrt. the relation after the @{term per_union}\
have "quotient V ?R' = (\
x \
V. {?R'``{x}})" unfolding quotient_def by auto also \
\
decompose it into the quotients for elements equivalent to x, y in R, and the rest\
have "\
= (\
x \
(V-(R``{x})-(R``{y})). {?R'``{x}}) \
(\
x \
(R``{y}). {?R'``{x}}) \
(\
x \
(R``{x}). {?R'``{x}})" using xdrin ydrin by auto also \
\
for the elements equivalent to x and y in R the quotient is the quotient containing x and y respectively \
have "\
= (\
x \
(V-(R``{x})-(R``{y})). {?R'``{x}}) \
{?R'``{y}} \
{?R'``{x}}" using x1 y1 by auto also \
\
which is after uniting them, the same quotient \
have "\
= (\
x \
(V-(R``{x})-(R``{y})). {R``{x}}) \
{?R'``{y}}" using K bla by auto also have "\
= insert (?R'``{y}) ?Vm" by auto finally have leftside: "quotient V ?R' = insert (?R'``{y}) ?Vm" . have notin: "?R'``{y} \
?Vm" apply (auto simp: per_union_def) by (metis (no_types, lifting) Image_singleton_iff UnI1 assms(2) eq equiv_class_self local.sym symE) have o: "card (quotient V ?R') = Suc (card ?Vm)" unfolding leftside apply(rule card_insert_disjoint) using notin by auto \
\
now consider the set of quotients wrt. the relation before the @{term per_union}\
have "quotient V R = (\
x \
V. {R``{x}})" unfolding quotient_def by auto also \
\
decompose it into the quotients for elements equivalent to x, y in R, and the rest\
have "\
= (\
x \
(V-(R``{x})-(R``{y})). {R``{x}}) \
(\
x \
(R``{y}). {R``{x}}) \
(\
x \
(R``{x}). {R``{x}})" using xdrin ydrin by auto also \
\
for the elements equivalent to x and y in R the quotient is the quotient containing x and y respectively \
have "\
= (\
x \
(V-(R``{x})-(R``{y})). {R``{x}}) \
{R``{y}} \
{R``{x}}" using x2 y2 by auto also \
\
these are two distinct quotients \
have "\
= insert (R``{y}) (insert (R``{x}) ?Vm)" by auto finally have ii: "quotient V R = insert (R``{y}) (insert (R``{x}) ?Vm)" . have "R``{x} \
?Vm" using eq equiv_class_self by fastforce have "R``{y} \
?Vm" using eq equiv_class_self by fastforce with assms(1) have "R``{y} \
(insert (R``{x}) ?Vm)" by blast have "card (quotient V R) = Suc (card (insert (R``{x}) ?Vm))" apply(simp only: ii) apply(rule card_insert_disjoint) apply simp apply fact done also have "card (insert (R``{x}) ?Vm) = Suc (card ?Vm)" apply(rule card_insert_disjoint) apply simp apply fact done finally have a: "card (quotient V R) = Suc (Suc (card ?Vm))" by auto from a o show ?thesis by auto qed subsection "On the pigeon hole principle" lemma fixes f::"'c\
'd" and g ::"'c\
'd" assumes "finite A" and k: "\
a b. a\
A \
b\
A \
f a = f b \
g a = g b" shows coarser: "card (f ` A) \
card (g ` A)" using assms proof - let ?h = "\
d. THE x. {x} = g ` {x\
A. f x = d}" term image have z: "\
x. x\
A \
g ` {y\
A. f y = f x} = {g x} " unfolding image_def apply auto using k by blast have uz: "\
x. x\
A \
?h (f x) = g x" by (simp add: z) have "card (?h ` (f ` A)) \
card (f ` A)" apply(rule card_image_le) apply(rule finite_imageI) by fact moreover from uz have "?h ` (f ` A) = g ` A" by force ultimately show ?thesis by auto qed subsection "On sorting and \
max_node\
" definition edges_less_eq :: "('a \
'w::{linorder, ordered_comm_monoid_add} \
'a) \
('a \
'w \
'a) \
bool" where "edges_less_eq a b \
fst(snd a) \
fst(snd b)" definition "sort_edges \
quicksort_by_rel edges_less_eq []" definition "max_node l \
Max (insert 0 (fst`set l \
(snd o snd)`set l))" lemma max_node_impl[code]: "max_node l = fold (\
(u,_,w) x. max u (max w x)) l 0" proof - have "fold (\
(u,_,w) x. max u (max w x)) l a = Max (insert a (fst`set l \
(snd o snd)`set l))" for a apply (induction l arbitrary: a) apply (auto simp: ) subgoal for a b l aa apply (cases l) by (auto simp: ac_simps) done thus ?thesis unfolding max_node_def by auto qed definition "is_linorder_rel R \
(\
x y. R x y \
R y x) \
(\
x y z. R x y \
R y z \
R x z)" lemma edges_less_eq_linorder: "is_linorder_rel edges_less_eq" unfolding edges_less_eq_def is_linorder_rel_def by (metis linear order_trans) lemma sort_edges_correct: "sorted_wrt edges_less_eq (quicksort_by_rel edges_less_eq [] l)" by (metis (no_types, opaque_lifting) edges_less_eq_linorder is_linorder_rel_def sorted_wrt_quicksort_by_rel) lemma distinct_mset_eq:"distinct a \
mset a = mset b \
distinct b" by (metis card_distinct distinct_card set_mset_mset size_mset) lemma quicksort_by_rel_distinct: "distinct l \
distinct (quicksort_by_rel edges_less_eq [] l)" by (auto intro: distinct_mset_eq) subsection "On @{term list_rel}" lemma map_in_list_rel_conv: shows "(l, l') \
\
br \
I\
list_rel \
((\
x\
set l. I x) \
l'=map \
l)" proof (induction l arbitrary: l') case (Cons a l l') then show ?case apply(cases l') by (auto simp add: in_br_conv) qed simp lemma list_relD: "(x, y) \
\
br a I\
list_rel \
y = map a x" by(auto simp: map_in_list_rel_conv) lemma list_relD2: "(x, y) \
\
br a I\
list_rel \
y = map a x \
(\
x\
set x. I x)" by(auto simp: map_in_list_rel_conv) lemma list_set_rel_append: "(x,s)\
br a I \
(xs,S)\
\
br a I\
list_set_rel \
s\
S \
(xs@[x],insert s S)\
\
br a I\
list_set_rel" unfolding list_set_rel_def apply(intro relcompI[where b="map a (xs @ [x])"]) apply (auto simp: in_br_conv) apply parametricity by (auto dest: list_relD simp add: in_br_conv) subsection "Auxiliary lemmas for Sepref" lemma pure_fold: "(\
a c. \
