diff --git a/thys/Prefix_Free_Code_Combinators/Examples.thy b/thys/Prefix_Free_Code_Combinators/Examples.thy new file mode 100644 --- /dev/null +++ b/thys/Prefix_Free_Code_Combinators/Examples.thy @@ -0,0 +1,59 @@ +section \Examples\label{sec:examples}\ + +theory Examples + imports Prefix_Free_Code_Combinators +begin + +text \The following introduces a few examples for encoders:\ + +notepad +begin \<^marker>\tag visible\ + define example1 where "example1 = N\<^sub>e \\<^sub>e N\<^sub>e" + + text \This is an encoder for a pair of natural numbers using exponential Golomb codes.\ + + text \Given a pair it is possible to estimate the number of bits necessary to + encode it using the @{term "bit_count"} lemmas.\ + + have "bit_count (example1 (0,1)) = 4" + by (simp add:example1_def dependent_bit_count exp_golomb_bit_count_exact) + + text \Note that a finite bit count automatically implies that the encoded element is in the domain + of the encoding function. This means usually it is possible to establish a bound on the size of + the datastructure and verify that the value is encodable simultaneously.\ + + hence "(0,1) \ dom example1" + by (intro bit_count_finite_imp_dom, simp) + + define example2 + where "example2 = [0..<42] \\<^sub>e Nb\<^sub>e 314" + + text \The second example illustrates the use of the combinator @{term "(\\<^sub>e)"}, which allows + encoding functions with a known finite encodable domain, here we assume the values are smaller + than @{term "314"} on the domain @{term "{..<42}"}.\ + + have "bit_count (example2 f) = 42*9" (is "?lhs = ?rhs") + if a:"f \ {0..<42} \\<^sub>E {0..<314}" for f + proof - + have "?lhs = (\x\[0..<42]. bit_count (Nb\<^sub>e 314 (f x)))" + using a by (simp add:example2_def fun_bit_count PiE_def) + also have "... = (\x\[0..<42]. ereal (floorlog 2 313))" + using a Pi_def PiE_def bounded_nat_bit_count + by (intro arg_cong[where f="sum_list"] map_cong, auto) + also have "... = ?rhs" + by (simp add: compute_floorlog sum_list_triv) + finally show ?thesis by simp + qed + + define example3 + where "example3 = N\<^sub>e \\<^sub>e (\n. [0..<42] \\<^sub>e Nb\<^sub>e n)" + + text \The third example is more complex and illustrates the use of dependent encoders, consider + a function with domain @{term "{..<(42::nat)}"} whose values are natural numbers in the interval + @{term "{.. + +end + +end \ No newline at end of file diff --git a/thys/Prefix_Free_Code_Combinators/Prefix_Free_Code_Combinators.thy b/thys/Prefix_Free_Code_Combinators/Prefix_Free_Code_Combinators.thy new file mode 100644 --- /dev/null +++ b/thys/Prefix_Free_Code_Combinators/Prefix_Free_Code_Combinators.thy @@ -0,0 +1,886 @@ +section \Introduction\label{sec:intro}\ + +theory Prefix_Free_Code_Combinators + imports + "HOL-Library.Extended_Real" + "HOL-Library.Float" + "HOL-Library.FuncSet" + "HOL-Library.List_Lexorder" + "HOL-Library.Log_Nat" + "HOL-Library.Sublist" +begin + +text \The encoders are represented as partial prefix-free functions. The advantage of +prefix free codes is that they can be easily combined by concatenation. The approach +of using prefix free codes (on the byte-level) for the representation of complex data +structures is common in many industry encoding libraries (cf. \cite{rfc8949}). + +The reason for representing encoders using partial functions, stems from some use-cases +where the objects to be encoded may be in a much smaller sets, as their type may suggest. +For example a natural number may be known to have a given range, or a function may be +encodable because it has a finite domain. + +Note: Prefix-free codes can also be automatically derived using Huffmans' algorithm, which was +formalized by Blanchette~\cite{Huffman-AFP}. This is especially useful if it is possible to transmit +a dictionary before the data. On the other hand these standard codes are useful, when the above is +impractical and/or the distribution of the input is unknown or expected to be close to the one's +implied by standard codes. + +The following section contains general definitions and results, followed by +Section~\ref{sec:dep_enc} to \ref{sec:float_enc} where encoders for primitive types +and combinators are defined. Each construct is accompanied by lemmas verifying that they +form prefix free codes as well as bounds on the bit count to encode the data. +Section~\ref{sec:examples} concludes with a few examples.\ + +section \Encodings\ + +fun opt_prefix where + "opt_prefix (Some x) (Some y) = prefix x y" | + "opt_prefix _ _ = False" + +definition "opt_comp x y = (opt_prefix x y \ opt_prefix y x)" + +fun opt_append :: "bool list option \ bool list option \ bool list option" + where + "opt_append (Some x) (Some y) = Some (x@y)" | + "opt_append _ _ = None" + +lemma opt_comp_sym: "opt_comp x y = opt_comp y x" + by (simp add:opt_comp_def, blast) + +lemma opt_comp_append: + assumes "opt_comp (opt_append x y) z" + shows "opt_comp x z" +proof - + obtain x' y' z' where a: "x = Some x'" "y = Some y'" "z = Some z'" + using assms + by (cases x, case_tac[!] y, case_tac[!] z, auto simp: opt_comp_def) + have "prefix (x'@y') z' \ prefix z' (x'@y')" + using a assms by (simp add:opt_comp_def) + hence "prefix x' z' \ prefix z' x'" + using prefix_same_cases append_prefixD by blast + thus ?thesis + using a by (simp add:opt_comp_def) +qed + +lemma opt_comp_append_2: + assumes "opt_comp x (opt_append y z)" + shows "opt_comp x y" + using opt_comp_append opt_comp_sym assms by blast + +lemma opt_comp_append_3: + assumes "opt_comp (opt_append x y) (opt_append x z)" + shows "opt_comp y z" + using assms + by (cases x, case_tac[!] y, case_tac[!] z, auto simp: opt_comp_def) + +type_synonym 'a encoding = "'a \ bool list" + +definition is_encoding :: "'a encoding \ bool" + where "is_encoding f = (\x y. opt_prefix (f x) (f y) \ x = y)" + +text \An encoding function is represented as partial functions into lists of booleans, where +each list element represents a bit. Such a function is defined to be an encoding, if it is +prefix-free on its domain. This is similar to the formalization by Hibon and +Paulson~\cite{Source_Coding_Theorem-AFP} except for the use of partial functions for the +practical reasons described in Section~\ref{sec:intro}.\ + +lemma is_encodingI: + assumes "\x x' y y'. e x = Some x' \ e y = Some y' \ + prefix x' y' \ x = y" + shows "is_encoding e" +proof - + have "opt_prefix (e x) (e y) \ x = y" for x y + using assms by (cases "e x", case_tac[!] "e y", auto) + thus ?thesis by (simp add:is_encoding_def) +qed + +lemma is_encodingI_2: + assumes "\x y . opt_comp (e x) (e y) \ x = y" + shows "is_encoding e" + using assms by (simp add:opt_comp_def is_encoding_def) + +lemma encoding_triv: "is_encoding Map.empty" + by (rule is_encodingI_2, simp add:opt_comp_def) + +lemma is_encodingD: + assumes "is_encoding e" + assumes "opt_comp (e x) (e y)" + shows "x = y" + using assms by (auto simp add:opt_comp_def is_encoding_def) + +lemma encoding_imp_inj: + assumes "is_encoding f" + shows "inj_on f (dom f)" + using assms + by (intro inj_onI, simp add:is_encoding_def, force) + +fun bit_count :: "bool list option \ ereal" where + "bit_count None = \" | + "bit_count (Some x) = ereal (length x)" + +lemma bit_count_finite_imp_dom: + "bit_count (f x) < \ \ x \ dom f" + by (cases "f x", auto) + +lemma bit_count_append: + "bit_count (opt_append x y) = bit_count x + bit_count y" + by (cases x, case_tac[!] "y", simp_all) + +section $$Dependent) Products\label{sec:dep_enc}\ + +definition encode_dependent_prod :: + "'a encoding \ ('a \ 'b encoding) \ ('a \ 'b) encoding" + (infixr "\\<^sub>e" 65) + where + "encode_dependent_prod e f x = + opt_append (e (fst x)) (f (fst x) (snd x))" + +lemma dependent_encoding: + assumes "is_encoding e1" + assumes "\x. x \ dom e1 \ is_encoding (e2 x)" + shows "is_encoding (e1 \\<^sub>e e2)" +proof (rule is_encodingI_2) + fix x y + assume a:"opt_comp ((e1 \\<^sub>e e2) x) ((e1 \\<^sub>e e2) y)" + have d:"opt_comp (e1 (fst x)) (e1 (fst y))" + using a unfolding encode_dependent_prod_def + by (metis opt_comp_append opt_comp_append_2) + hence b:"fst x = fst y" + using is_encodingD[OF assms(1)] by simp + hence "opt_comp (e2 (fst x) (snd x)) (e2 (fst x) (snd y))" + using a unfolding encode_dependent_prod_def by (metis opt_comp_append_3) + moreover have "fst x \ dom e1" using d b + by (cases "e1 (fst x)", simp_all add:opt_comp_def dom_def) + ultimately have c:"snd x = snd y" + using is_encodingD[OF assms(2)] by simp + show "x = y" + using b c by (simp add: prod_eq_iff) +qed + +lemma dependent_bit_count: + "bit_count ((e\<^sub>1 \\<^sub>e e\<^sub>2) (x\<^sub>1,x\<^sub>2)) = + bit_count (e\<^sub>1 x\<^sub>1) + bit_count (e\<^sub>2 x\<^sub>1 x\<^sub>2)" + by (simp add: encode_dependent_prod_def bit_count_append) + +lemma dependent_bit_count_2: + "bit_count ((e\<^sub>1 \\<^sub>e e\<^sub>2) x) = + bit_count (e\<^sub>1 (fst x)) + bit_count (e\<^sub>2 (fst x) (snd x))" + by (simp add: encode_dependent_prod_def bit_count_append) + +text \This abbreviation is for non-dependent products.\ + +abbreviation encode_prod :: + "'a encoding \ 'b encoding \ ('a \ 'b) encoding" + (infixr "\\<^sub>e" 65) + where + "encode_prod e1 e2 \ e1 \\<^sub>e (\_. e2)" + +section \Composition\ + +lemma encoding_compose: + assumes "is_encoding f" + assumes "inj_on g {x. p x}" + shows "is_encoding (\x. if p x then f (g x) else None)" + using assms by (simp add:comp_def is_encoding_def inj_onD) + +lemma encoding_compose_2: + assumes "is_encoding f" + assumes "inj g" + shows "is_encoding (\x. f (g x))" + using assms by (simp add:comp_def is_encoding_def inj_onD) + +section \Natural Numbers\ + +fun encode_bounded_nat :: "nat \ nat \ bool list" where + "encode_bounded_nat (Suc l) n = + (let r = n \ (2^l) in r#encode_bounded_nat l (n-of_bool r*2^l))" | + "encode_bounded_nat 0 _ = []" + +lemma encode_bounded_nat_prefix_free: + fixes u v l :: nat + assumes "u < 2^l" + assumes "v < 2^l" + assumes "prefix (encode_bounded_nat l u) (encode_bounded_nat l v)" + shows "u = v" + using assms +proof (induction l arbitrary: u v) + case 0 + then show ?case by simp +next + case (Suc l) + have "prefix (encode_bounded_nat l (u - of_bool (u \ 2^l)*2^l)) + (encode_bounded_nat l (v - of_bool (v \ 2^l)*2^l))" + and a:"(u \ 2^l) = (v \ 2^l)" + using Suc(4) by (simp_all add:Let_def) + moreover have "u - of_bool (u \ 2^l)*2^l < 2^l" + using Suc(2) by (cases "u < 2^l", auto simp add:of_bool_def) + moreover have "v - of_bool (v \ 2^l)*2^l < 2^l" + using Suc(3) by (cases "v < 2^l", auto simp add:of_bool_def) + ultimately have + "u - of_bool (u \ 2^l)*2^l = v - of_bool (v \ 2^l)*2^l" + by (intro Suc(1), simp_all) + thus "u = v" using a by simp +qed + +definition Nb\<^sub>e :: "nat \ nat encoding" + where "Nb\<^sub>e l n = ( + if n < l + then Some (encode_bounded_nat (floorlog 2 (l-1)) n) + else None)" + +text \@{term "Nb\<^sub>e l"} is encoding for natural numbers strictly smaller than + @{term "l"} using a fixed length encoding.\ + +lemma bounded_nat_bit_count: + "bit_count (Nb\<^sub>e l y) = (if y < l then floorlog 2 (l-1) else$$" +proof - + have a:"length (encode_bounded_nat h m) = h" for h m + by (induction h arbitrary: m, simp, simp add:Let_def) + show ?thesis + using a by (simp add:Nb\<^sub>e_def) +qed + +lemma bounded_nat_bit_count_2: + assumes "y < l" + shows "bit_count (Nb\<^sub>e l y) = floorlog 2 (l-1)" + using assms bounded_nat_bit_count by simp + +lemma "dom (Nb\<^sub>e l) = {..e_def dom_def lessThan_def) + +lemma bounded_nat_encoding: "is_encoding (Nb\<^sub>e l)" +proof - + have "x < l \ x < 2 ^ floorlog 2 (l-1)" for x :: nat + by (intro floorlog_leD floorlog_mono, auto) + thus ?thesis + using encode_bounded_nat_prefix_free + by (intro is_encodingI, simp add:Nb\<^sub>e_def split:if_splits, blast) +qed + +fun encode_unary_nat :: "nat \ bool list" where + "encode_unary_nat (Suc l) = False#(encode_unary_nat l)" | + "encode_unary_nat 0 = [True]" + +lemma encode_unary_nat_prefix_free: + fixes u v :: nat + assumes "prefix (encode_unary_nat u) (encode_unary_nat v)" + shows "u = v" + using assms +proof (induction u arbitrary: v) + case 0 + then show ?case by (cases v, simp_all) +next + case (Suc u) + then show ?case by (cases v, simp_all) +qed + +definition Nu\<^sub>e :: "nat encoding" + where "Nu\<^sub>e n = Some (encode_unary_nat n)" + +text \@{term "Nu\<^sub>e"} is encoding for natural numbers using unary encoding. It is +inefficient except for special cases, where the probability of large numbers decreases +exponentially with its magnitude.\ + +lemma unary_nat_bit_count: + "bit_count (Nu\<^sub>e n) = Suc n" + unfolding Nu\<^sub>e_def by (induction n, auto) + +lemma unary_encoding: "is_encoding Nu\<^sub>e" + using encode_unary_nat_prefix_free + by (intro is_encodingI, simp add:Nu\<^sub>e_def) + +text \Encoding for positive numbers using Elias-Gamma code.\ + +definition Ng\<^sub>e :: "nat encoding" where + "Ng\<^sub>e n = + (if n > 0 + then (Nu\<^sub>e \\<^sub>e (\r. Nb\<^sub>e (2^r))) + (let r = floorlog 2 n - 1 in (r, n - 2^r)) + else None)" + +text \@{term "Ng\<^sub>e"} is an encoding for positive numbers using Elias-Gamma encoding\cite{elias1975}.\ + +lemma elias_gamma_bit_count: + "bit_count (Ng\<^sub>e n) = (if n > 0 then 2 * \log 2 n\ + 1 else (\::ereal))" +proof (cases "n > 0") + case True + define r where "r = floorlog 2 n - Suc 0" + have "floorlog 2 n \ 0" + using True + by (simp add:floorlog_eq_zero_iff) + hence a:"floorlog 2 n > 0" by simp + + have "n < 2^(floorlog 2 n)" + using True floorlog_bounds by simp + also have "... = 2^(r+1)" + using a by (simp add:r_def) + finally have "n < 2^(r+1)" by simp + hence b:"n - 2^r < 2^r" by simp + have "floorlog 2 (2 ^ r - Suc 0) \ r" + by (rule floorlog_leI, auto) + moreover have "r \ floorlog 2 (2 ^ r - Suc 0)" + by (cases r, simp, auto intro: floorlog_geI) + ultimately have c:"floorlog 2 (2 ^ r - Suc 0) = r" + using order_antisym by blast + + have "bit_count (Ng\<^sub>e n) = bit_count (Nu\<^sub>e r) + + bit_count (Nb\<^sub>e (2 ^ r) (n - 2 ^ r))" + using True by (simp add:Ng\<^sub>e_def r_def[symmetric] dependent_bit_count) + also have "... = ereal (r + 1) + ereal (r)" + using b c + by (simp add: unary_nat_bit_count bounded_nat_bit_count) + also have "... = 2 * r + 1" by simp + also have "... = 2 * \log 2 n\ + 1" + using True by (simp add:floorlog_def r_def) + finally show ?thesis using True by simp +next + case False + then show ?thesis by (simp add:Ng\<^sub>e_def) +qed + +lemma elias_gamma_encoding: "is_encoding Ng\<^sub>e" +proof - + have a: "inj_on (\x. let r = floorlog 2 x - 1 in (r, x - 2 ^ r)) + {n. 0 < n}" + proof (rule inj_onI) + fix x y :: nat + assume "x \ {n. 0 < n}" + hence x_pos: "0 < x" by simp + assume "y \ {n. 0 < n}" + hence y_pos: "0 < y" by simp + define r where "r = floorlog 2 x - Suc 0" + assume b:"(let r = floorlog 2 x - 1 in (r, x - 2 ^ r)) = + (let r = floorlog 2 y - 1 in (r, y - 2 ^ r))" + hence c:"r = floorlog 2 y - Suc 0" + by (simp_all add:Let_def r_def) + have "x - 2^r = y - 2^r" using b + by (simp add:Let_def r_def[symmetric] c[symmetric] prod_eq_iff) + moreover have "x \ 2^r" + using r_def x_pos floorlog_bounds by simp + moreover have "y \ 2^r" + using c floorlog_bounds y_pos by simp + ultimately show "x = y" using eq_diff_iff by blast + qed + + have "is_encoding (\n. Ng\<^sub>e n)" + unfolding Ng\<^sub>e_def using a + by (intro encoding_compose[where f="Nu\<^sub>e \\<^sub>e (\r. Nb\<^sub>e (2^r))"] + dependent_encoding unary_encoding bounded_nat_encoding) auto + thus ?thesis by simp +qed + +definition N\<^sub>e :: "nat encoding" where "N\<^sub>e x = Ng\<^sub>e (x+1)" + +text \@{term "N\<^sub>e"} is an encoding for all natural numbers using exponential Golomb +encoding~\cite{teuhola1978}. Exponential Golomb codes are also used in video compression +applications~\cite{richardson2010}.\ + +lemma exp_golomb_encoding: "is_encoding N\<^sub>e" +proof - + have "is_encoding (\n. N\<^sub>e n)" + unfolding N\<^sub>e_def + by (intro encoding_compose_2[where g="(\n. n + 1)"] elias_gamma_encoding, auto) + thus ?thesis by simp +qed + +lemma exp_golomb_bit_count_exact: + "bit_count (N\<^sub>e n) = 2 * \log 2 (n+1)\ + 1" + by (simp add:N\<^sub>e_def elias_gamma_bit_count) + +lemma exp_golomb_bit_count: + "bit_count (N\<^sub>e n) \ (2 * log 2 (real n+1) + 1)" + by (simp add:exp_golomb_bit_count_exact add.commute) + +lemma exp_golomb_bit_count_est: + assumes "n \ m " + shows "bit_count (N\<^sub>e n) \ (2 * log 2 (real m+1) + 1)" +proof - + have "bit_count (N\<^sub>e n) \ (2 * log 2 (real n+1) + 1)" + using exp_golomb_bit_count by simp + also have "... \ (2 * log 2 (real m+1) + 1)" + using assms by simp + finally show ?thesis by simp +qed + +section \Integers\ + +definition I\<^sub>e :: "int encoding" where + "I\<^sub>e x = N\<^sub>e (nat (if x \0 then (-2 * x) else (2*x-1)))" + +text \@{term "I\<^sub>e"} is an encoding for integers using exponential Golomb codes by embedding +the integers into the natural numbers, specifically the positive numbers are embedded into +the odd-numbers and the negative numbers are embedded into the even numbers. The embedding +has the benefit, that the bit count for an integer only depends on its absolute value.\ + +lemma int_encoding: "is_encoding I\<^sub>e" +proof - + have "inj (\x. nat (if x \ 0 then - 2 * x else 2 * x - 1))" + by (rule inj_onI, auto simp add:eq_nat_nat_iff, presburger) + thus ?thesis + unfolding I\<^sub>e_def + by (intro exp_golomb_encoding encoding_compose_2[where f="N\<^sub>e"]) + auto +qed + +lemma int_bit_count: "bit_count (I\<^sub>e n) = 2 * \log 2 (2*\n\+1)\ +1" +proof - + have a:"m > 0 \ + \log (real 2) (real (2 * m))\ = \log (real 2) (real (2 * m + 1))\" + for m :: nat by (rule floor_log_eq_if, auto) + have "n > 0 \ + \log 2 (2 * real_of_int n)\ = \log 2 (2 * real_of_int n + 1)\" + using a[where m="nat n"] by (simp add:add.commute) + thus ?thesis + by (simp add:I\<^sub>e_def exp_golomb_bit_count_exact floorlog_def) +qed + +lemma int_bit_count_1: + assumes "abs n > 0" + shows "bit_count (I\<^sub>e n) = 2 * \log 2 \n\\ +3" +proof - + have a:"m > 0 \ + \log (real 2) (real (2 * m))\ = \log (real 2) (real (2 * m + 1))\" + for m :: nat by (rule floor_log_eq_if, auto) + have "n < 0 \ + \log 2 (-2 * real_of_int n)\ = \log 2 (1-2 * real_of_int n)\" + using a[where m="nat (-n)"] by (simp add:add.commute) + hence "bit_count (I\<^sub>e n) = 2 * \log 2 (2*real_of_int \n\)\ +1" + using assms + by (simp add:I\<^sub>e_def exp_golomb_bit_count_exact floorlog_def) + also have "... = 2 * \log 2 \n\\ + 3" + using assms by (subst log_mult, auto) + finally show ?thesis by simp +qed + +lemma int_bit_count_est_1: + assumes "\n\ \ r" + shows "bit_count (I\<^sub>e n) \ 2 * log 2 (r+1) +3" +proof (cases "abs n > 0") + case True + have "real_of_int \log 2 \real_of_int n\\ \ log 2 \real_of_int n\" + using of_int_floor_le by blast + also have "... \ log 2 (real_of_int r+1)" + using True assms by force + finally have + "real_of_int \log 2 \real_of_int n\\ \ log 2 (real_of_int r + 1)" + by simp + then show ?thesis + using True assms by (simp add:int_bit_count_1) +next + case False + have "r \ 0" using assms by simp + moreover have "n = 0" using False by simp + ultimately show ?thesis by (simp add:I\<^sub>e_def exp_golomb_bit_count_exact) +qed + +lemma int_bit_count_est: + assumes "\n\ \ r" + shows "bit_count (I\<^sub>e n) \ 2 * log 2 (2*r+1) +1" +proof - + have "bit_count (I\<^sub>e n) \ 2 * log 2 (2*\n\+1) +1" + by (simp add:int_bit_count) + also have "... \ 2 * log 2 (2* r + 1) + 1" + using assms by simp + finally show ?thesis by simp +qed + +section \Lists\ + +definition Lf\<^sub>e where + "Lf\<^sub>e e n xs = + (if length xs = n + then fold (\x y. opt_append y (e x)) xs (Some []) + else None)" + +text \@{term "Lf\<^sub>e e n"} is an encoding for lists of length @{term"n"}, +where the elements are encoding using the encoder @{term "e"}.\ + +lemma fixed_list_encoding: + assumes "is_encoding e" + shows "is_encoding (Lf\<^sub>e e n)" +proof (induction n) + case 0 + then show ?case + by (rule is_encodingI_2, simp_all add:Lf\<^sub>e_def opt_comp_def split:if_splits) +next + case (Suc n) + show ?case + proof (rule is_encodingI_2) + fix x y + assume a:"opt_comp (Lf\<^sub>e e (Suc n) x) (Lf\<^sub>e e (Suc n) y)" + have b:"length x = Suc n" using a + by (cases "length x = Suc n", simp_all add:Lf\<^sub>e_def opt_comp_def) + then obtain x1 x2 where x_def: "x = x1@[x2]" "length x1 = n" + by (metis length_append_singleton lessI nat.inject order.refl + take_all take_hd_drop) + have c:"length y = Suc n" using a + by (cases "length y = Suc n", simp_all add:Lf\<^sub>e_def opt_comp_def) + then obtain y1 y2 where y_def: "y = y1@[y2]" "length y1 = n" + by (metis length_append_singleton lessI nat.inject order.refl + take_all take_hd_drop) + have d: "opt_comp (opt_append (Lf\<^sub>e e n x1) (e x2)) + (opt_append (Lf\<^sub>e e n y1) (e y2)) " + using a b c by (simp add:Lf\<^sub>e_def x_def y_def) + hence "opt_comp (Lf\<^sub>e e n x1) (Lf\<^sub>e e n y1)" + using opt_comp_append opt_comp_append_2 by blast + hence e:"x1 = y1" + using is_encodingD[OF Suc] by blast + hence "opt_comp (e x2) (e y2)" + using opt_comp_append_3 d by simp + hence "x2 = y2" + using is_encodingD[OF assms] by blast + thus "x = y" using e x_def y_def by simp + qed +qed + +lemma fixed_list_bit_count: + "bit_count (Lf\<^sub>e e n xs) = + (if length xs = n then (\x \ xs. (bit_count (e x))) else \)" +proof (induction n arbitrary: xs) + case 0 + then show ?case by (simp add:Lf\<^sub>e_def) +next + case (Suc n) + show ?case + proof (cases "length xs = Suc n") + case True + then obtain x1 x2 where x_def: "xs = x1@[x2]" "length x1 = n" + by (metis length_append_singleton lessI nat.inject order.refl + take_all take_hd_drop) + have "bit_count (Lf\<^sub>e e n x1) = (\x\x1. bit_count (e x))" + using x_def(2) Suc by simp + then show ?thesis by (simp add:Lf\<^sub>e_def x_def bit_count_append) + next + case False + then show ?thesis by (simp add:Lf\<^sub>e_def) + qed +qed + +definition L\<^sub>e + where "L\<^sub>e e xs = (Nu\<^sub>e \\<^sub>e (\n. Lf\<^sub>e e n)) (length xs, xs)" + +text \@{term "L\<^sub>e e"} is an encoding for arbitrary length lists, where the elements are encoding using the +encoder @{term "e"}.\ + +lemma list_encoding: + assumes "is_encoding e" + shows "is_encoding (L\<^sub>e e)" +proof - + have "inj (\xs. (length xs, xs))" + by (simp add: inj_on_def) + + hence "is_encoding (\xs. L\<^sub>e e xs)" + using assms unfolding L\<^sub>e_def + by (intro encoding_compose_2[where g=" (\x. (length x, x))"] + dependent_encoding unary_encoding fixed_list_encoding) auto + thus ?thesis by simp +qed + +lemma sum_list_triv_ereal: + fixes a :: ereal + shows "sum_list (map (\_. a) xs) = length xs * a" + apply (cases a, simp add:sum_list_triv) + by (induction xs, simp, simp)+ + +lemma list_bit_count: + "bit_count (L\<^sub>e e xs) = (\x \ xs. bit_count (e x) + 1) + 1" +proof - + have "bit_count (L\<^sub>e e xs) = + ereal (1 + real (length xs)) + (\x\xs. bit_count (e x))" + by (simp add: L\<^sub>e_def dependent_bit_count fixed_list_bit_count unary_nat_bit_count) + also have "... = (\x\xs. bit_count (e x)) + (\x \ xs. 1) + 1" + by (simp add:ac_simps group_cancel.add1 sum_list_triv_ereal) + also have "... = (\x \ xs. bit_count (e x) + 1) + 1" + by (simp add:sum_list_addf) + finally show ?thesis by simp +qed + +section \Functions\ + +definition encode_fun :: "'a list \ 'b encoding \ ('a \ 'b) encoding" + (infixr "\\<^sub>e" 65) where + "encode_fun xs e f = + (if f \ extensional (set xs) + then (Lf\<^sub>e e (length xs) (map f xs)) + else None)" + +text \@{term "xs \\<^sub>e e"} is an encoding for functions whose domain is @{term "set xs"}, +where the values are encoding using the encoder @{term "e"}.\ + +lemma fun_encoding: + assumes "is_encoding e" + shows "is_encoding (xs \\<^sub>e e)" +proof - + have a:"inj_on (\x. map x xs) {x. x \ extensional (set xs)}" + by (rule inj_onI) (simp add: extensionalityI) + have "is_encoding (\x. (xs \\<^sub>e e) x)" + unfolding encode_fun_def + by (intro encoding_compose[where f="Lf\<^sub>e e (length xs)"] + fixed_list_encoding assms a) + thus ?thesis by simp +qed + +lemma fun_bit_count: + "bit_count ((xs \\<^sub>e e) f) = + (if f \ extensional (set xs) then (\x \ xs. bit_count (e (f x))) else \)" + by (simp add:encode_fun_def fixed_list_bit_count comp_def) + +lemma fun_bit_count_est: + assumes "f \ extensional (set xs)" + assumes "\x. x \ set xs \ bit_count (e (f x)) \ a" + shows "bit_count ((xs \\<^sub>e e) f) \ ereal (real (length xs)) * a" +proof - + have "bit_count ((xs \\<^sub>e e) f) = (\x \ xs. bit_count (e (f x)))" + using assms(1) by (simp add:fun_bit_count) + also have "... \ (\x \ xs. a)" + by (intro sum_list_mono assms(2), simp) + also have "... = ereal (real (length xs)) * a" + by (simp add:sum_list_triv_ereal) + finally show ?thesis by simp +qed + +section \Finite Sets\ + +definition S\<^sub>e :: "'a encoding \ 'a set encoding" where + "S\<^sub>e e S = + (if finite S \ S \ dom e + then (L\<^sub>e e (linorder.sorted_key_list_of_set (\) (the \ e) S)) + else None)" + +text \@{term "S\<^sub>e e"} is an encoding for finite sets whose elements are encoded using the + encoder @{term "e"}.\ + +lemma set_encoding: + assumes "is_encoding e" + shows "is_encoding (S\<^sub>e e)" +proof - + have a:"inj_on (the \ e) (dom e)" + using inj_on_def + by (intro comp_inj_on encoding_imp_inj assms, fastforce) + + interpret folding_insort_key "(\)" "(<)" "(dom e)" "(the \ e)" + using a by (unfold_locales) auto + have "is_encoding (\S. S\<^sub>e e S)" + unfolding S\<^sub>e_def using sorted_key_list_of_set_inject + by (intro encoding_compose[where f="L\<^sub>e e"] list_encoding assms(1) inj_onI, simp) + thus ?thesis by simp +qed + +lemma set_bit_count: + assumes "is_encoding e" + shows "bit_count (S\<^sub>e e S) = (if finite S then (\x \ S. bit_count (e x)+1)+1 else \)" +proof (cases "finite S") + case f:True + have "bit_count (S\<^sub>e e S) = (\x\S. bit_count (e x)+1)+1" + proof (cases "S \ dom e") + case True + + have a:"inj_on (the \ e) (dom e)" + using inj_on_def by (intro comp_inj_on encoding_imp_inj[OF assms], fastforce) + + interpret folding_insort_key "(\)" "(<)" "(dom e)" "(the \ e)" + using a by (unfold_locales) auto + + have b:"distinct (linorder.sorted_key_list_of_set (\) (the \ e) S)" + (is "distinct ?l") using distinct_sorted_key_list_of_set True + distinct_if_distinct_map by auto + + have "bit_count (S\<^sub>e e S) = (\x\?l. bit_count (e x) + 1) + 1" + using f True by (simp add:S\<^sub>e_def list_bit_count) + also have "... = (\x\S. bit_count (e x)+1)+1" + by (simp add: sum_list_distinct_conv_sum_set[OF b] + set_sorted_key_list_of_set[OF True f]) + finally show ?thesis by simp + next + case False + hence "\i\S. e i = None" by force + hence "\i\S. bit_count (e i) = \" by force + hence "(\x\S. bit_count (e x) + 1) = \" + by (simp add:sum_Pinfty f) + then show ?thesis using False by (simp add:S\<^sub>e_def) + qed + thus ?thesis using f by simp +next + case False + then show ?thesis by (simp add:S\<^sub>e_def) +qed + +lemma sum_triv_ereal: + fixes a :: ereal + assumes "finite S" + shows "(\_ \ S. a) = card S * a" +proof (cases a) + case (real r) + then show ?thesis by simp +next + case PInf + show ?thesis using assms PInf + by (induction S rule:finite_induct, auto) +next + case MInf + show ?thesis using assms MInf + by (induction S rule:finite_induct, auto) +qed + +lemma set_bit_count_est: + assumes "is_encoding f" + assumes "finite S" + assumes "card S \ m" + assumes "0 \ a" + assumes "\x. x \ S \ bit_count (f x) \ a" + shows "bit_count (S\<^sub>e f S) \ ereal (real m) * (a+1) + 1" +proof - + have "bit_count (S\<^sub>e f S) = (\x\S. bit_count (f x) + 1) + 1" + using assms by (simp add:set_bit_count) + also have "... \ (\x\S. a + 1) + 1" + using assms by (intro sum_mono add_mono) auto + also have "... = ereal (real (card S)) * (a + 1) + 1" + by (simp add:sum_triv_ereal[OF assms(2)]) + also have "... \ ereal (real m) * (a+1) + 1" + using assms(3,4) by (intro add_mono ereal_mult_right_mono) auto + finally show ?thesis by simp +qed + +section \Floating point numbers\label{sec:float_enc}\ +definition F\<^sub>e where "F\<^sub>e f = (I\<^sub>e \\<^sub>e I\<^sub>e) (mantissa f,exponent f)" + +lemma float_encoding: + "is_encoding F\<^sub>e" +proof - + have "inj (\x. (mantissa x, exponent x))" (is "inj ?g") + proof (rule injI) + fix x y + assume "(mantissa x, exponent x) = (mantissa y, exponent y)" + hence "real_of_float x = real_of_float y" + by (simp add:mantissa_exponent) + thus "x = y" + by (metis real_of_float_inverse) + qed + thus "is_encoding (\f. F\<^sub>e f)" + unfolding F\<^sub>e_def + by (intro encoding_compose_2[where g="?g"] + dependent_encoding int_encoding) auto +qed + +lemma suc_n_le_2_pow_n: + fixes n :: nat + shows "n + 1 \ 2 ^ n" + by (induction n, simp, simp) + +lemma float_bit_count_1: + "bit_count (F\<^sub>e f) \ 6 + 2 * (log 2 (\mantissa f\ + 1) + + log 2 (\exponent f\ + 1))" (is "?lhs \ ?rhs") +proof - + have "?lhs = bit_count (I\<^sub>e (mantissa f)) + + bit_count (I\<^sub>e (exponent f))" + by (simp add:F\<^sub>e_def dependent_bit_count) + also have "... \ + ereal (2 * log 2 (real_of_int (\mantissa f\ + 1)) + 3) + + ereal (2 * log 2 (real_of_int (\exponent f\ + 1)) + 3)" + by (intro int_bit_count_est_1 add_mono) auto + also have "... = ?rhs" + by simp + finally show ?thesis by simp +qed + +text \The following establishes an estimate for the bit count of a floating +point number in non-normalized representation:\ + +lemma float_bit_count_2: + fixes m :: int + fixes e :: int + defines "f \ float_of (m * 2 powr e)" + shows "bit_count (F\<^sub>e f) \ + 6 + 2 * (log 2 (\m\ + 2) + log 2 (\e\ + 1))" +proof - + have b:" (r + 1) * int i \ r * (2 ^ i - 1) + 1" + if b_assms: "r \ 1" for r :: int and i :: nat + proof (cases "i > 0") + case True + have "(r + 1) * int i = r * i + 2 * int ((i-1)+1) - i" + using True by (simp add:algebra_simps) + also have "... \ r * i + int (2^1) * int (2^(i-1)) - i" + using b_assms + by (intro add_mono diff_mono mult_mono of_nat_mono suc_n_le_2_pow_n) + simp_all + also have "... = r * i + 2^i - i" + using True + by (subst of_nat_mult[symmetric], subst power_add[symmetric]) + simp + also have "... = r *i + 1 * (2 ^ i - int i - 1) + 1" by simp + also have "... \ r *i + r * (2 ^ i - int i - 1) + 1" + using b_assms + by (intro add_mono mult_mono, simp_all) + also have "... = r * (2 ^ i - 1) + 1" + by (simp add:algebra_simps) + finally show ?thesis by simp + next + case False + hence "i = 0" by simp + then show ?thesis by simp + qed + + have a:"log 2 (\mantissa f\ + 1) + log 2 (\exponent f\ + 1) \ + log 2 (\m\+2) + log 2 (\e\+1)" + proof (cases "f=0") + case True then show ?thesis by simp + next + case False + moreover have "f = Float m e" + by (simp add:f_def Float.abs_eq) + ultimately obtain i :: nat + where m_def: "m = mantissa f * 2 ^ i" + and e_def: "e = exponent f - i" + using denormalize_shift by blast + + have mantissa_ge_1: "1 \ \mantissa f\" + using False mantissa_noteq_0 by fastforce + + have "(\mantissa f\ + 1) * (\exponent f\ + 1) = + (\mantissa f\ + 1) * (\e+i\+1)" + by (simp add:e_def) + also have "... \ (\mantissa f\ + 1) * ((\e\+\i\)+1)" + by (intro mult_mono add_mono, simp_all) + also have "... = (\mantissa f\ + 1) * ((\e\+1)+i)" + by simp + also have "... = (\mantissa f\ + 1) * (\e\+1) + (\mantissa f\+1)*i" + by (simp add:algebra_simps) + also have "... \ (\mantissa f\ + 1) * (\e\+1) + (\mantissa f\ * (2^i-1)+1)" + by (intro add_mono b mantissa_ge_1, simp) + also have "... = (\mantissa f\ + 1) * (\e\+1) + (\mantissa f\ * (2^i-1)+1)*(1)" + by simp + also have + "... \ (\mantissa f\ + 1) * (\e\+1) + (\mantissa f\* (2^i-1)+1)*(\e\+1)" + by (intro add_mono mult_left_mono, simp_all) + also have "... = ((\mantissa f\ + 1)+(\mantissa f\* (2^i-1)+1))*(\e\+1)" + by (simp add:algebra_simps) + also have "... = (\mantissa f\*2^i+2)*(\e\+1)" + by (simp add:algebra_simps) + also have "... = (\m\+2)*(\e\+1)" + by (simp add:m_def abs_mult) + finally have "(\mantissa f\ + 1) * (\exponent f\ + 1) \ (\m\+2)*(\e\+1)" + by simp + + hence "(\real_of_int (mantissa f)\ + 1) * (\of_int (exponent f)\ + 1) \ + (\of_int m\+2)*(\of_int e\+1)" + by (simp flip:of_int_abs) (metis (mono_tags, opaque_lifting) numeral_One + of_int_add of_int_le_iff of_int_mult of_int_numeral) + then show ?thesis by (simp add:log_mult[symmetric]) + qed + have "bit_count (F\<^sub>e f) \ + 6 + 2 * (log 2 (\mantissa f\ + 1) + log 2 (\exponent f\ + 1))" + using float_bit_count_1 by simp + also have "... \ 6 + 2 * (log 2 (\m\ + 2) + log 2 (\e\ + 1))" + using a by simp + finally show ?thesis by simp +qed + +lemma float_bit_count_zero: + "bit_count (F\<^sub>e (float_of 0)) = 2" + by (simp add:F\<^sub>e_def dependent_bit_count int_bit_count + zero_float.abs_eq[symmetric]) + + + +end \ No newline at end of file diff --git a/thys/Prefix_Free_Code_Combinators/ROOT b/thys/Prefix_Free_Code_Combinators/ROOT new file mode 100644 --- /dev/null +++ b/thys/Prefix_Free_Code_Combinators/ROOT @@ -0,0 +1,9 @@ +chapter AFP + +session Prefix_Free_Code_Combinators (AFP) = "HOL-Library" + + options [timeout = 300] + theories + Examples + document_files + "root.tex" + "root.bib" diff --git a/thys/Prefix_Free_Code_Combinators/document/root.bib b/thys/Prefix_Free_Code_Combinators/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Prefix_Free_Code_Combinators/document/root.bib @@ -0,0 +1,77 @@ +@article{teuhola1978, + title = {A compression method for clustered bit-vectors}, + journal = {Information Processing Letters}, + volume = {7}, + number = {6}, + pages = {308-311}, + year = {1978}, + issn = {0020-0190}, + _doi = {https://doi.org/10.1016/0020-0190(78)90024-8}, + _url = {https://www.sciencedirect.com/science/article/pii/0020019078900248}, + author = {Jukka Teuhola}, + keywords = {Encoding methods, bit-vector compression} +} + +@article{elias1975, + author={Elias, P.}, + journal={IEEE Transactions on Information Theory}, + title={Universal codeword sets and representations of the integers}, + year={1975}, + volume={21}, + number={2}, + pages={194-203}, + _doi={10.1109/TIT.1975.1055349} +} + +@misc{rfc8949, + series = {Request for Comments}, + number = 8949, + howpublished = {RFC 8949}, + publisher = {RFC Editor}, + doi = {10.17487/RFC8949}, + _url = {https://rfc-editor.org/rfc/rfc8949.txt}, + author = {Carsten Bormann and Paul E. Hoffman}, + title = {{Concise Binary Object Representation (CBOR)}}, + pagetotal = 66, + year = 2020, + month = dec, +} + + +@inbook{richardson2010, + author = {Richardson, Iain E.}, + publisher = {John Wiley \& Sons, Ltd}, + isbn = {9780470989418}, + title = {H.264 Transform and Coding}, + booktitle = {The H.264 Advanced Video Compression Standard}, + chapter = {7}, + pages = {179-221}, + _doi = {https://doi.org/10.1002/9780470989418.ch7}, + _url = {https://onlinelibrary.wiley.com/doi/abs/10.1002/9780470989418.ch7}, + eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1002/9780470989418.ch7}, + year = {2010}, + keywords = {H.264 transform and coding process development, binary coding - converting source video signal to H.264/AVC, transform and quantization - H.264 transforms, inverse transform - inverse quantization, luma and chrom transform processes, block scan orders - scanning blocks of transform coefficients, coded H.264 stream and coding methods}, + abstract = {Summary This chapter contains sections titled: Introduction Transform and quantization Block scan orders Coding Summary References} +} + +@article{Huffman-AFP, + author = {Jasmin Christian Blanchette}, + title = {The Textbook Proof of Huffman's Algorithm}, + journal = {Archive of Formal Proofs}, + month = oct, + year = 2008, + note = {\url{https://isa-afp.org/entries/Huffman.html}, + Formal proof development}, + ISSN = {2150-914x}, +} + +@article{Source_Coding_Theorem-AFP, + author = {Quentin Hibon and Lawrence C. Paulson}, + title = {Source Coding Theorem}, + journal = {Archive of Formal Proofs}, + month = oct, + year = 2016, + note = {\url{https://isa-afp.org/entries/Source_Coding_Theorem.html}, + Formal proof development}, + ISSN = {2150-914x}, +} \ No newline at end of file diff --git a/thys/Prefix_Free_Code_Combinators/document/root.tex b/thys/Prefix_Free_Code_Combinators/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Prefix_Free_Code_Combinators/document/root.tex @@ -0,0 +1,34 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} +\usepackage{amssymb} +\usepackage{pdfsetup} +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{A Combinator Library for Prefix-Free Codes} +\author{Emin Karayel} +\maketitle + +\abstract{This entry contains a set of binary encodings for primitive data types, such as +natural numbers, integers, floating-point numbers as well as combinators to construct +encodings for products, lists, sets or functions of/between such types. + +For natural numbers and integers, the entry contains various encodings, such as Elias-Gamma-Codes +and exponential Golomb Codes, which are efficient variable-length codes in use by current +compression formats. + +A use-case for this library is measuring the persisted size of a complex data structure without +having to hand-craft a dedicated encoding for it, independent of Isabelle's internal +representation.} + +\parindent 0pt\parskip 0.5ex + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,673 +1,674 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate +Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quasi_Borel_Spaces Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL