Changes

Summary

1. merge from afp-2022
2. re-generate site;
3. tuned for smaller diffs;
4. New topic for Gray_Codes
5. More Gray_Codes
6. More Gray_Codes
7. New entry Gray_Codes
8. metadata and sitegen for Executable_Randomized_Algorithms
9. New entry Executable_Randomized_Algorithms
10. new entry DCR-ExecutionEquivalence
11. Zeckendorf: metadata and sitegen
12. new entry Zeckendorf
13. Crypto_Standards: Fixed a spelling error
14. Crypto_Standards metadata & website
15. New entry Crypto_Standards
16. move TOML module to Isabelle (see Isabelle/be8aaaa4ac25);
17. added missing timeout;
18. reformat;
19. remove duplicate fields;
20. check TOML parse structure properly;
21. proper typed TOML layer;
22. tuned imports;
23. Updated links
24. Added citations
25. Added citations
26. Added citations
27. Added refs
28. Added DOIs
29. Added DOIs
30. Added DOIs
31. Added DOI
32. Added DOI
33. added DOI
34. Median_Method: Add a tight version of the median bound, suggested by Yong Kiam Tan.
35. parse proper toml syntax;
36. Syntax for symmetric set difference, plus tidying
37. Update
38. Update
39. Add
40. Update
41. Update
42. merged
43. Three_Squares: time limit increase; and now sym_diff is declared in main HOL
44. moved Subterm_and_Context into First_Order_Terms, merged context of Term_Aux into Term
45. replace scala.sys.process with proper Bash.Process;
46. renamed "flatten" to "unindex"
47. Resolved some operator clashes
48. merged
49. simplified some proofs
50. Modifications for moving from f ` S <= T to f:S->T
51. Updated for new HOL-CSP
52. merge
53. updated ROOT.
54. Registers: Fixed nonterminating subproof
55. Collected changes to Complex_Bounded_Operators AFP entry: Complex_Vector_Spaces.thy ========================= New lemmas: clinear_scaleR[simp], abs_summable_on_scaleC_left[intro], abs_summable_on_scaleC_right[intro], ccspan_superset', ccspan_closure[simp], ccspan_finite, ccspan_UNIV[simp], infsum_in_closed_csubspaceI, closed_csubspace_space_as_set[simp], SUP_ccspan Renamed lemma: bounded_clinear_eq_on -> bounded_clinear_eq_on_closure Changed typeclass: basis_enum (has additional constant "canonical_basis_length") Renamed definition: Abs_clinear_space -> Abs_ccsubspace Complex_Inner_Product.thy ========================= New lemmas: mem_ortho_ccspanI, basis_projections_reconstruct_has_sum, basis_projections_reconstruct, basis_projections_reconstruct_summable, parseval_identity_has_sum, parseval_identity_summable, parseval_identity, canonical_basis_is_onb[simp] Complex_Bounded_Linear_Functions.thy ==================================== New definition: invertible_cblinfun (operator has with left inverse) New lemmas: not_not_singleton_cblinfun_zero, cblinfun_norm_approx_witness', summable_on_cblinfun_apply, summable_on_cblinfun_apply_left, abs_summable_on_cblinfun_apply_left, infsum_cblinfun_apply_left, has_sum_cblinfun_apply_left, bounded_clinear_cblinfun_compose_left, bounded_clinear_cblinfun_compose_right, clinear_cblinfun_compose_left, clinear_cblinfun_compose_right, additive_cblinfun_compose_left[simp], additive_cblinfun_compose_right[simp], isCont_cblinfun_compose_left, isCont_cblinfun_compose_right, cspan_compose_closed, cspan_adj_closed, unitaryI, norm_isometry_compose', unitary_nonzero[simp], isometry_inj, unitary_adj_inv, isometry_cinner_both_sides, isometry_image_is_ortho_set, cblinfun_apply_in_image', cblinfun_image_ccspan_leqI, cblinfun_same_on_image, lift_cblinfun_comp, cblinfun_image_def2, unitary_image_onb, sandwich_arg_compose, sandwich_compose, inj_sandwich_isometry, sandwich_isometry_id, is_Proj_id[simp], norm_is_Proj_nonzero, Proj_compose_cancelI, space_as_setI_via_Proj, unitary_image_ortho_compl, Proj_on_image[simp], kernel_apply_self, leq_kernel_iff, cblinfun_image_kernel, cblinfun_image_kernel_unitary, kernel_cblinfun_compose, eigenspace_0[simp], kernel_isometry, cblinfun_image_eigenspace_isometry, cblinfun_image_eigenspace_unitary, kernel_member_iff, kernel_square[simp], cblinfun_inv_left, inv_cblinfun_invertible, cblinfun_inv_right, iso_cblinfun_unitary, invertible_cblinfun_isometry, summable_cblinfun_apply_invertible, infsum_cblinfun_apply_invertible, less_eq_scaled_id_norm, butterflies_sum_id_finite, butterfly_sum_left, butterfly_sum_right, cblinfun_extension_exists_restrict Changed lemmas: cblinfun_image_INF_eq_general, cblinfun_image_INF_eq (more general), positive_hermitianI (flipped sides of equality), rank1_compose_right, rank1_uminus, rank1_uminus_iff (more general type class) Removed lemma: dense_span_separating (use bounded_clinear_eq_on_closure instead) Removed bundles: blinfun_notation, no_blinfun_notation Complex_L2.thy ============== New lemmas: clinear_Rep_ell2[simp], Abs_ell2_inverse_finite[simp], norm_ell2_bound_trunc, bounded_clinear_Rep_ell2, trunc_ell2_singleton, trunc_ell2_insert, trunc_ell2_finite_sum, is_orthogonal_trunc_ell2, ell2_decompose_has_sum, ell2_decompose_infsum, ell2_decompose_summable, Rep_ell2_cblinfun_apply_sum, explicit_cblinfun_exists, explicit_cblinfun_exists_bounded, explicit_cblinfun_exists_finite_dim[simp], explicit_cblinfun_ket, Rep_ell2_explicit_cblinfun_ket[simp] Changed lemmas: cinner_ket (uses "of_bool" instead of "if") Changed definition: ket (uses "of_bool" instead of "if") New definition: explicit_cblinfun (define an operator by giving the entries of an infinite matrix) Cblinfun_Code: ============== New definition: butterfly_code New lemma: butterfly_code Renamed definition: cblinfun_apply_code -> cblinfun_apply_ell2 Renamed lemmas: - vec_of_ell2_timesScalarVec -> vec_of_ell2_scaleC - cinner_ell2_code' -> cinner_ell2_code - times_ell2_code' -> times_ell2_code - divide_ell2_code' -> divide_ell2_code - inverse_ell2_code' -> inverse_ell2_code - one_ell2_code' -> one_ell2_code - cblinfun_apply_code -> cblinfun_apply_ell2 - cblinfun_apply_code -> cblinfun_apply_ell2 Cblinfun_Matrix.thy =================== New lemmas: vec_of_basis_enum_carrier_vec, cblinfun_of_mat_invalid extra/Extra_General.thy ======================= New lemmas: not_not_singleton_zero, has_sumI_metric, limitin_pullback_topology, tendsto_coordinatewise, limitin_closure_of extra/Extra_Vector_Spaces.thy ============================= New lemmas: summable_on_bounded_linear, any_norm_exists, abs_summable_on_scaleR_left[intro], abs_summable_on_scaleR_right[intro], Changed lemma: enum_idx_bound (expressed using CARD, added [simp]) extra/Extra_Jordan_Normal_Form.thy ================================== New lemmas: map_map_vec_cols, map_vec_conjugate
56. Renamings of operators, and a major theorem on distributivity of Mprefix vs Sync. Renamings of some lemmata.
57. Updated metadata for several entries. - Updated categorization for derandomization libraries, based on the newly introduced CS/Alg./Randomized category. - Added related reference for Nils Cremer's Tree Enumeration - Removed obsolete comments in Expander Grapgs
58. metadata and sitegen for Directed_Sets
59. new entry: Directed_Sets
60. merge from AFP 2022
61. metadata and sitegen for Multirelations_Heterogeneous
62. new entry: Multirelations_Heterogeneous
63. adjust Schwartz_Zippel entry - Use Pi_pmf from HOL-Probability - Generalize theorem(s) in example
64. adjusted Simple_Clause_Learning from AFP 2022 to AFP devel
65. adjusted Given_Clause_Loops from AFP 2022 to AFP devel
66. adjusted CommCSL from AFP 2022 to AFP devel
67. adjusted DigitsInBase from AFP 2022 to AFP devel
68. adjusted Schwartz_Zippel from AFP 2022 to AFP devel
69. adjusted TsirelsonBound from AFP 2022 to AFP devel
70. adjusted Tree_Enumeration from AFP 2022 to AFP devel
71. adjusted efficient WPO from AFP 2022 to afp devel
72. merge from afp-2022
73. New entry Efficient_Weighted_Path_Order
74. add edit mode to afp-submit UI;
75. solved subtle problem with multiple entries and new authors;
76. better error logging;
77. added edit handler to submission app;
78. added frontend in devel mode;
79. tuned (mostly api path handling);
80. A real title in place of MLSS_Decision_Proc
81. MLSS_Decision_Proc sitegen
82. New entry MLSS_Decision_Proc
83. metadata and sitegen for TsirelsonBound
84. new entry: TsirelsonBound
85. New entry Tree_Enumeration
86. Three_Squares citegen
87. New entry Three_Squares
88. fixed some ACM/AMS categories
89. more files
90. New entry MHComputation
91. make index.json files line-by-line for smaller diffs;
92. cleanup;
93. added new entry DigitsInBase;
94. fixed broken LaTeX quotation marks in abstracts
95. recategorised some entries
96. new topic: Computer science/Algorithms/Randomized
97. sitegen for Schwartz_Zippel
98. new entry: Schwartz_Zippel
99. New entry: Simple_Clause_Learning
100. New entry HyperHoareLogic
101. New entry Distributed_Distinct_Elements
102. metadata for CommCSL + sitegen
103. new entry: CommCSL
104. New entry No_FTL_observers_Gen_Rel
105. added new files generated by sitegen
106. sitegen
107. metadata for Expander Graphs
108. new entry: Expander Graphs
109. tuned;
110. fix of toml-entries and rerun of sitegen: problem: links where in these quotes: ”...” and not in the standard ones "..."
111. sitegen (for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection)
112. metadata for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection
113. new entry: Two_Generated_Word_Monoids_Intersection
114. new entry: Binary_Code_Imprimitive
115. running sort on ROOTS
116. New entry Probability_Inequality_Completeness
117. Rensets metadata
118. New entry Rensets
119. more Edwards
120. New entry Edwards_Elliptic_Curves_Group
121. metadata and sitegen for CVP_Hardness
122. new entry: CVP_Hardness
123. rerun sitegen
124. revert proof compression experiment
125. metadata for ABY3_Protocols
126. new entry ABY3_Protocols
127. sitegen for Given_Clause_Loops
128. New entry Given_Clause_Loops
129. Adjustments for the simplified version of real_le_lsqrt
130. adapted to Isabelle/84a7a0029c82
131. merged
132. adapted to Isabelle/0252d635bfb2
133. merge
134. merge
135. Merge with developper version on LISN gut
136. merged
137. prefer @{attributes} antiquotation over Attrib.internal; adapted to Isabelle/bc42c074e58f;
138. tuned proofs;
139. Deleted a superfluous assumption. This proof is a horror
140. merged
141. fixed some bibliographic entries
142. merged
143. tuned
144. merged
145. merged
146. adapted to current Isabelle/ec1c0daa3fbd;
147. adapted to current Isabelle/ec1c0daa3fbd;
148. adapted to Isabelle/5edd5b12017d;
149. proper morphism context;
150. backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531;
151. proper morphism context;
152. adapted to Isabelle/5ab5add88922;
153. SMT-LIB interpretation of floating-point arithmetic
154. merged
155. SMT-LIB interpretation of floating-point arithmetic
156. IEEE model with a single NaN value
157. Minor
158. merging
159. updates for future formalizations
160. adapted to Isabelle/f78cdc6fe971;
161. adapted to Isabelle/f78cdc6fe971;
162. A slight beautification
163. adapted to 3f354d5bbf98;
164. Rounding modes renamed
165. merged
166. Add the rounding mode roundNearestTiesToAway.
167. Merge realtime deque renamings
168. simplify some measurements
169. rename Deque.Idle to Idles
170. Rename Big and Small cases
171. rename `Transforming` to `Rebal`
172. rename `Common.state` to `common_state`
173. rename Small.state to small_state
174. rename Big.state to big_state
175. backed out changeset 2ecb8f5e085f: obsolete thanks to Isabelle/21cdcd120a78;
176. more robust: make it work with Isabelle/a12c48fbf10f;
177. adapted to Isabelle/c4677a6aae2c;
178. adapted to Isabelle/c4677a6aae2c;