diff --git a/metadata/entries/Distributed_Distinct_Elements.toml b/metadata/entries/Distributed_Distinct_Elements.toml
--- a/metadata/entries/Distributed_Distinct_Elements.toml
+++ b/metadata/entries/Distributed_Distinct_Elements.toml
@@ -1,28 +1,28 @@
title = "Distributed Distinct Elements"
date = 2023-04-03
topics = [
"Computer science/Algorithms/Distributed",
"Computer science/Algorithms/Approximation",
"Computer science/Algorithms/Randomized",
]
abstract = "This entry formalizes a randomized cardinality estimation data structure with asymptotically optimal space usage. It is inspired by the streaming algorithm presented by Błasiok in 2018. His work closed the gap between the best-known lower bound and upper bound after a long line of research started by Flajolet and Martin in 1984 and was to first to apply expander graphs (in addition to hash families) to the problem. The formalized algorithm has two improvements compared to the algorithm by Błasiok. It supports operation in parallel mode, and it relies on a simpler pseudo-random construction avoiding the use of code based extractors."
license = "bsd"
note = ""
[authors]
[authors.karayel]
email = "karayel_email"
[contributors]
[notify]
karayel = "karayel_email"
[history]
[extra]
[related]
-dois = []
+dois = ["10.4230/LIPIcs.APPROX/RANDOM.2023.35","10.48550/arXiv.2307.00985"]
pubs = []
diff --git a/metadata/entries/Finite_Fields.toml b/metadata/entries/Finite_Fields.toml
--- a/metadata/entries/Finite_Fields.toml
+++ b/metadata/entries/Finite_Fields.toml
@@ -1,37 +1,40 @@
title = "Finite Fields"
date = 2022-06-08
topics = [
"Mathematics/Algebra",
]
abstract = """
This entry formalizes the classification of the finite fields (also
called Galois fields): For each prime power $p^n$ there exists exactly
one (up to isomorphisms) finite field of that size and there are no
other finite fields. The derivation includes a formalization of the
-characteristic of rings, the Frobenius endomorphism, formal
-differentiation for polynomials in HOL-Algebra and Gauss' formula
-for the number of monic irreducible polynomials over finite fields: \\[
+characteristic of rings, the Frobenius endomorphism, formal differentiation
+for polynomials in HOL-Algebra, Rabin's test for the irreducibility of
+polynomials and Gauss' formula for the number of monic irreducible
+polynomials over finite fields: \\[
\\frac{1}{n} \\sum_{d | n} \\mu(d) p^{n/d} \\textrm{.} \\] The proofs are
-based on the books from Ireland
-and Rosen, as well as, Lidl and
+and Rosen, Rabin, as
+well as, Lidl and
Niederreiter."""
license = "bsd"
note = ""
[authors]
[authors.karayel]
homepage = "karayel_homepage"
[contributors]
[notify]
karayel = "karayel_email"
[history]
+2024-01-17 = "Added Rabin's test for the irreducibility of polynomials in finite fields."
+2024-01-18 = "Added exectuable algorithms for the construction of (and calculations in) finite fields."
[extra]
[related]
diff --git a/thys/Automatic_Refinement/Lib/Misc.thy b/thys/Automatic_Refinement/Lib/Misc.thy
--- a/thys/Automatic_Refinement/Lib/Misc.thy
+++ b/thys/Automatic_Refinement/Lib/Misc.thy
@@ -1,4507 +1,4495 @@
(* Title: Miscellaneous Definitions and Lemmas
Author: Peter Lammich
Maintainer: Peter Lammich
Thomas Tuerk
*)
(*
CHANGELOG:
2010-05-09: Removed AC, AI locales, they are superseeded by concepts
from OrderedGroups
2010-09-22: Merges with ext/Aux
2017-06-12: Added a bunch of lemmas from various other projects
*)
section \Miscellaneous Definitions and Lemmas\
theory Misc
imports Main
"HOL-Library.Multiset"
"HOL-ex.Quicksort"
"HOL-Library.Option_ord"
"HOL-Library.Infinite_Set"
"HOL-Eisbach.Eisbach"
begin
text_raw \\label{thy:Misc}\
subsection \Isabelle Distribution Move Proposals\
subsubsection \Pure\
lemma TERMI: "TERM x" unfolding Pure.term_def .
subsubsection \HOL\
(* Stronger disjunction elimination rules. *)
lemma disjE1: "\ P \ Q; P \ R; \\P;Q\ \ R \ \ R"
by metis
lemma disjE2: "\ P \ Q; \P; \Q\ \ R; Q \ R \ \ R"
by blast
lemma imp_mp_iff[simp]:
"a \ (a \ b) \ a \ b"
"(a \ b) \ a \ a \ b" (* is Inductive.imp_conj_iff, but not in simpset by default *)
by blast+
lemma atomize_Trueprop_eq[atomize]: "(Trueprop x \ Trueprop y) \ Trueprop (x=y)"
apply rule
apply (rule)
apply (erule equal_elim_rule1)
apply assumption
apply (erule equal_elim_rule2)
apply assumption
apply simp
done
subsubsection \Set\
lemma inter_compl_diff_conv[simp]: "A \ -B = A - B" by auto
lemma pair_set_inverse[simp]: "{(a,b). P a b}\ = {(b,a). P a b}"
by auto
lemma card_doubleton_eq_2_iff[simp]: "card {a,b} = 2 \ a\b" by auto
subsubsection \List\
(* TODO: Move, analogous to List.length_greater_0_conv *)
thm List.length_greater_0_conv
lemma length_ge_1_conv[iff]: "Suc 0 \ length l \ l\[]"
by (cases l) auto
\ \Obtains a list from the pointwise characterization of its elements\
lemma obtain_list_from_elements:
assumes A: "\ili. P li i)"
obtains l where
"length l = n"
"\il. length l=n \ (\iii l!j"
by (simp add: sorted_iff_nth_mono)
also from nth_eq_iff_index_eq[OF D] B have "l!i \ l!j"
by auto
finally show ?thesis .
qed
lemma distinct_sorted_strict_mono_iff:
assumes "distinct l" "sorted l"
assumes "i il!j \ i\j"
by (metis assms distinct_sorted_strict_mono_iff leD le_less_linear)
(* List.thy has:
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!]
We could, analogously, declare rules for "map _ _ = _@_" as dest!,
or use elim!, or declare the _conv-rule as simp
*)
lemma map_eq_appendE:
assumes "map f ls = fl@fl'"
obtains l l' where "ls=l@l'" and "map f l=fl" and "map f l' = fl'"
using assms
proof (induction fl arbitrary: ls thesis)
case (Cons x xs)
then obtain l ls' where [simp]: "ls = l#ls'" "f l = x" by force
with Cons.prems(2) have "map f ls' = xs @ fl'" by simp
from Cons.IH[OF _ this] obtain ll ll' where "ls' = ll @ ll'" "map f ll = xs" "map f ll' = fl'" .
with Cons.prems(1)[of "l#ll" ll'] show thesis by simp
qed simp
lemma map_eq_append_conv: "map f ls = fl@fl' \ (\l l'. ls = l@l' \ map f l = fl \ map f l' = fl')"
by (auto elim!: map_eq_appendE)
lemmas append_eq_mapE = map_eq_appendE[OF sym]
lemma append_eq_map_conv: "fl@fl' = map f ls \ (\l l'. ls = l@l' \ map f l = fl \ map f l' = fl')"
by (auto elim!: append_eq_mapE)
lemma distinct_mapI: "distinct (map f l) \ distinct l"
by (induct l) auto
lemma map_distinct_upd_conv:
"\i \ (map f l)[i := x] = map (f(l!i := x)) l"
\ \Updating a mapped distinct list is equal to updating the
mapping function\
by (auto simp: nth_eq_iff_index_eq intro: nth_equalityI)
lemma zip_inj: "\length a = length b; length a' = length b'; zip a b = zip a' b'\ \ a=a' \ b=b'"
proof (induct a b arbitrary: a' b' rule: list_induct2)
case Nil
then show ?case by (cases a'; cases b'; auto)
next
case (Cons x xs y ys)
then show ?case by (cases a'; cases b'; auto)
qed
lemma zip_eq_zip_same_len[simp]:
"\ length a = length b; length a' = length b' \ \
zip a b = zip a' b' \ a=a' \ b=b'"
by (auto dest: zip_inj)
lemma upt_merge[simp]: "i\j \ j\k \ [i.. (ys \ [] \ butlast ys = xs \ last ys = x)"
by auto
(* Case distinction how two elements of a list can be related to each other *)
lemma list_match_lel_lel:
assumes "c1 @ qs # c2 = c1' @ qs' # c2'"
obtains
(left) c21' where "c1 = c1' @ qs' # c21'" "c2' = c21' @ qs # c2"
| (center) "c1' = c1" "qs' = qs" "c2' = c2"
| (right) c21 where "c1' = c1 @ qs # c21" "c2 = c21 @ qs' # c2'"
using assms
apply (clarsimp simp: append_eq_append_conv2)
subgoal for us by (cases us) auto
done
lemma xy_in_set_cases[consumes 2, case_names EQ XY YX]:
assumes A: "x\set l" "y\set l"
and C:
"!!l1 l2. \ x=y; l=l1@y#l2 \ \ P"
"!!l1 l2 l3. \ x\y; l=l1@x#l2@y#l3 \ \ P"
"!!l1 l2 l3. \ x\y; l=l1@y#l2@x#l3 \ \ P"
shows P
proof (cases "x=y")
case True with A(1) obtain l1 l2 where "l=l1@y#l2" by (blast dest: split_list)
with C(1) True show ?thesis by blast
next
case False
from A(1) obtain l1 l2 where S1: "l=l1@x#l2" by (blast dest: split_list)
from A(2) obtain l1' l2' where S2: "l=l1'@y#l2'" by (blast dest: split_list)
from S1 S2 have M: "l1@x#l2 = l1'@y#l2'" by simp
thus P proof (cases rule: list_match_lel_lel[consumes 1, case_names 1 2 3])
case (1 c) with S1 have "l=l1'@y#c@x#l2" by simp
with C(3) False show ?thesis by blast
next
case 2 with False have False by blast
thus ?thesis ..
next
case (3 c) with S1 have "l=l1@x#c@y#l2'" by simp
with C(2) False show ?thesis by blast
qed
qed
lemma list_e_eq_lel[simp]:
"[e] = l1@e'#l2 \ l1=[] \ e'=e \ l2=[]"
"l1@e'#l2 = [e] \ l1=[] \ e'=e \ l2=[]"
apply (cases l1, auto) []
apply (cases l1, auto) []
done
lemma list_ee_eq_leel[simp]:
"([e1,e2] = l1@e1'#e2'#l2) \ (l1=[] \ e1=e1' \ e2=e2' \ l2=[])"
"(l1@e1'#e2'#l2 = [e1,e2]) \ (l1=[] \ e1=e1' \ e2=e2' \ l2=[])"
apply (cases l1, auto) []
apply (cases l1, auto) []
done
subsubsection \Transitive Closure\
text \A point-free induction rule for elements reachable from an initial set\
lemma rtrancl_reachable_induct[consumes 0, case_names base step]:
assumes I0: "I \ INV"
assumes IS: "E``INV \ INV"
shows "E\<^sup>*``I \ INV"
by (metis I0 IS Image_closed_trancl Image_mono subset_refl)
lemma acyclic_empty[simp, intro!]: "acyclic {}" by (unfold acyclic_def) auto
lemma acyclic_union:
"acyclic (A\B) \ acyclic A"
"acyclic (A\B) \ acyclic B"
by (metis Un_upper1 Un_upper2 acyclic_subset)+
text \Here we provide a collection of miscellaneous definitions and helper lemmas\
subsection "Miscellaneous (1)"
text \This stuff is used in this theory itself, and thus occurs in first place or is simply not sorted into any other section of this theory.\
lemma IdD: "(a,b)\Id \ a=b" by simp
text \Conversion Tag\
definition [simp]: "CNV x y \ x=y"
lemma CNV_I: "CNV x x" by simp
lemma CNV_eqD: "CNV x y \ x=y" by simp
lemma CNV_meqD: "CNV x y \ x\y" by simp
(* TODO: Move. Shouldn't this be detected by simproc? *)
lemma ex_b_b_and_simp[simp]: "(\b. b \ Q b) \ Q True" by auto
lemma ex_b_not_b_and_simp[simp]: "(\b. \b \ Q b) \ Q False" by auto
method repeat_all_new methods m = m;(repeat_all_new \m\)?
subsubsection "AC-operators"
text \Locale to declare AC-laws as simplification rules\
locale Assoc =
fixes f
assumes assoc[simp]: "f (f x y) z = f x (f y z)"
locale AC = Assoc +
assumes commute[simp]: "f x y = f y x"
lemma (in AC) left_commute[simp]: "f x (f y z) = f y (f x z)"
by (simp only: assoc[symmetric]) simp
lemmas (in AC) AC_simps = commute assoc left_commute
text \Locale to define functions from surjective, unique relations\
locale su_rel_fun =
fixes F and f
assumes unique: "\(A,B)\F; (A,B')\F\ \ B=B'"
assumes surjective: "\!!B. (A,B)\F \ P\ \ P"
assumes f_def: "f A == THE B. (A,B)\F"
lemma (in su_rel_fun) repr1: "(A,f A)\F" proof (unfold f_def)
obtain B where "(A,B)\F" by (rule surjective)
with theI[where P="\B. (A,B)\F", OF this] show "(A, THE x. (A, x) \ F) \ F" by (blast intro: unique)
qed
lemma (in su_rel_fun) repr2: "(A,B)\F \ B=f A" using repr1
by (blast intro: unique)
lemma (in su_rel_fun) repr: "(f A = B) = ((A,B)\F)" using repr1 repr2
by (blast)
\ \Contract quantification over two variables to pair\
lemma Ex_prod_contract: "(\a b. P a b) \ (\z. P (fst z) (snd z))"
by auto
lemma All_prod_contract: "(\a b. P a b) \ (\z. P (fst z) (snd z))"
by auto
lemma nat_geq_1_eq_neqz: "x\1 \ x\(0::nat)"
by auto
lemma nat_in_between_eq:
"(a b\Suc a) \ b = Suc a"
"(a\b \ b b = a"
by auto
lemma Suc_n_minus_m_eq: "\ n\m; m>1 \ \ Suc (n - m) = n - (m - 1)"
by simp
lemma Suc_to_right: "Suc n = m \ n = m - Suc 0" by simp
lemma Suc_diff[simp]: "\n m. n\m \ m\1 \ Suc (n - m) = n - (m - 1)"
by simp
lemma if_not_swap[simp]: "(if \c then a else b) = (if c then b else a)" by auto
lemma all_to_meta: "Trueprop (\a. P a) \ (\a. P a)"
apply rule
by auto
lemma imp_to_meta: "Trueprop (P\Q) \ (P\Q)"
apply rule
by auto
(* for some reason, there is no such rule in HOL *)
lemma iffI2: "\P \ Q; \ P \ \ Q\ \ P \ Q"
by metis
lemma iffExI:
"\ \x. P x \ Q x; \x. Q x \ P x \ \ (\x. P x) \ (\x. Q x)"
by metis
lemma bex2I[intro?]: "\ (a,b)\S; (a,b)\S \ P a b \ \ \a b. (a,b)\S \ P a b"
by blast
(* TODO: Move lemma to HOL! *)
lemma cnv_conj_to_meta: "(P \ Q \ PROP X) \ (\P;Q\ \ PROP X)"
by (rule BNF_Fixpoint_Base.conj_imp_eq_imp_imp)
subsection \Sets\
lemma remove_subset: "x\