Changes

Summary

1. merged
2. Some hyphens that should be en dashes
3. slightly refine WPO-definition - previous formalization of WPO deviated a bit to paper version (requiring less computation) - both versions are equivalent whenever order in parameter is strongly normalizing - however, this is no longer true for co-WPO, a variant of WPO with non strongly normalizing orders - consequence: change formalization so that it is more closely related to paper version, so that also results on coWPO can be proven
4. merged
5. no "open" of ML structures: it makes sources unmaintainable;
6. adapted to Isabelle/5db014c36f42;
7. adapted to Isabelle/f4cd6e3b5075;
8. adapted to Isabelle/5db014c36f42;
9. This file should have been removed in the previous commit.
10. Sync with my development repo. Main changes related to CartesianMonoidalCategory.
11. update timing;
12. eliminated pointless parallelism: approx. 1.3s as plain sequential ML;
13. tuned;
14. alternative version by Manuel Eberl, following the approach of Isabelle2022/src/HOL/Tools/sat.ML with one big hyp;
15. adapted to Isabelle/c274f52b11ff;
16. Backed out changeset a537fb4c92af
17. slightly faster thanks to Thm.shared_context from Isabelle/4f9117e6020d;
18. merged
19. moved lemma to FDS exercises
20. Fix proofs broken by previous commit.
21. Add congurence rule for bind_tm in Root_Balanced_Tree.Time_Monad The rule is necessary for the termination proof of some recursive functions over the time monad.
22. tuned;
23. tuned;
24. eliminated aliases: prefer existing Thm.elim_implies;
25. tuned;
26. more standard use of structure Unsynchronized;
27. tuned whitespace;
28. not unused!
29. Added running time analysis
30. some remarks on division
31. clarified scope of document
32. no subsection without section
33. merged
34. Deleted library material
35. adapted to Isabelle/b43ee37926a9;
36. merged
37. adapted to Isabelle/13cee8c2ed8d;
38. Add related entry for Combinatorial_Enumeration_Algorithms. Note: I followed APA style guide for the reference. https://apastyle.apa.org/style-grammar-guidelines/references/examples/published-dissertation-references Note: Ran sitegen.
39. small simplifications
40. shortened some parts of Huffman proof using Sledgehammer
41. added another simplification rule when alternatives are equal
42. added more simplification rules involving Zero
43. adapted to Isabelle/4a174bea55e2;
44. uodated map update syntax
45. Adjusted to changes in distribution.
46. more realistic timeout;
47. avoid hardwired documents; tuned whitespace;
48. merged
49. simplified a few proofs
50. added character sets to the extension directory of regular expressions
51. more syntax adjustments
52. more syntax update for map update syntax
53. more map update syntax updates
54. merged
55. updated to new map update syntax priorities
56. Some simplifications of proofs
57. Minor refinements
58. tiny simplifications
59. tidied another file
60. tidied a bit more
61. merged
62. More tidying
63. completed the addtion of Rec in the Extension directory
64. added another regular expression for Record
65. More tidying of the Ordinal entry
66. A massive tidying
67. Tiny bit more tidying
68. more robust: allow optional arguments in isabelle.Progress.echo;
69. More tidying
70. merged
71. Suppression of duplicate syntax for abs_summable_on, etc.
72. No more sorted_take, sorted_drop
73. Update entries MDP-Rewards and MDP-Algorithms
74. Migration of material from Jordan_Hoelder to HOL-Algebra
75. merged
76. Tidied up some messy proofs
77. Adjustments for the new infix status of has_sum
78. A tiny spelling correction
79. merged
80. A little more migration
81. Backed out changeset fa59c080cb3b
82. Backed out changeset 811f0b8d4f58
83. tuned metis call to avoid obscure feature
84. merged
85. Migration of material to the repository and necessary modifications
86. more map_of adaptions
87. adapted to new List.map_of
88. update Real_Time_Deque
89. Removal of a stray sledgehammer command
90. explicit range types in abstractions
91. somehow more clear terminology
92. merged
93. Some tidying and moving some material to the distribution
94. Deleted use of Euclidean_Division
95. Repaired session name
96. "Repaired boundary behaviour of mod+- for even modulus, Added locale module_spec for possible instantiation of Dilithium"
97. Update names to match thesis.
98. proper components base, following "isabelle components -I": downloaded components should be shared for all Isabelle versions;
99. proper symbolic handle on component resources (see Isabelle/3eb3de867786);
100. more realistic timeout, based on CPU time;
101. adapted to Isabelle/9a60c1759543;
102. more realistic timeout, based on CPU time;
103. fixed looping proofs
104. dropped reference to dead clone
105. removed dead clone
106. modernized
107. Modernized.
108. More instances.
109. Tuned whitespace.
110. Updated references.
111. More correct references.
112. Removed a bit of unnecessary material
113. merged
114. Shortened several messy proofs
115. Fix name clash in Frequency_Moments.
116. Fixed a name clash
117. Moving more material to the distribution
118. Moving some material to the main repository
119. adapted to db93f67a;
120. merged
121. generalized theory name: euclidean division denotes one particular division definition on integers
122. more efficient specification
123. merge from afp-2022
124. metadata for Suppes' theorem + sitegen
125. new entry: Suppes' Theorem
126. new entry HoareForDivergence
127. tuned css;
128. metadat for StrictOmegaCategories
129. new entry StrictOmegaCategories
130. tuned css;
131. cleanup accidental unused document files;
132. check ROOTs: add warning-only checks;
133. tuned;
134. add ROOT checks for document presence and unused files;
135. afp-submit visual improvements;
136. update bibtex example;
137. new doi
138. sitegen for AOT
139. merged
140. New entry AOT
141. New entry: Propositional_Logic_Class
142. sitegen for Cook_Levin
143. New entry Cook_Levin
144. Sorry — extra files for Boolos_Curious_Inference_Automated
145. Metadata for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Boolos_Curious_Inference_Automated
146. New entry Boolos_Curious_Inference_Automated
147. New entry: Synthetic_Completeness
148. New entry: Quantifier_Elimination_Hybrid
149. New entry Birkhoff_Finite_Distributive_Lattices
150. sitegen for Kneser_Cauchy_Davenport
151. metadata for Kneser_Cauchy_Davenport
152. new entry: Kneser_Cauchy_Davenport
153. sitegen for Turan
154. added metadata for Turans graph theorem
155. new entry: Turans Graph Theorem
156. new entry Multitape_To_Singletape_TM
157. removed static pages from rss feed;
158. Minor rerating of the abstract of Sauer_Shelah_Lemma
159. sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Sauer_Shelah_Lemma
160. New entry Sauer_Shelah_Lemma
161. sitegen for the aforementioned changes
162. adjustments to the abstract, requested by the author
163. CHERI-C_Memory_Model patch & metadata
164. New submission CHERI-C_Memory_Model
165. updated docs;
166. improve page layout slightly;
167. fixed broken abstract for PAPP_Impossibility
168. remove dead code
169. metadata and sitegen for PAPP_Impossibility
170. new entry PAPP_Impossibility
171. remove old .sitegen-ignore and mention AFP chapter in submission guidelines;
172. afp_check_roots: proper error message printing;
173. metadata and sitegen for Balog_Szemeredi_Gowers
174. new entry: Balog_Szemeredi_Gowers
175. tuned check names;
176. make check roots tool less dependent on AFP structure;
177. tuned;
178. web for Combinatorial_Enumeration_Algorithms
179. sitegen for Combinatorial_Enumeration_Algorithms
180. New entry Combinatorial_Enumeration_Algorithms
181. fix duplicate affiliations from author and notify;
182. add metadata check tool to sitegen;
183. update check tools: add formatting checks, new cmd options;
184. check for entries instead of session due to session nesting allowed in entries;
185. added unused thy check;
186. clarified check roots tool;
187. afp-submit: tuned logging;
188. afp-submit: encode new notify addresses properly;
189. afp-submit: correct build status on empty file;
190. afp-submit: remove padding on select;
191. re-format metadata;
192. afp-submit: update on correct status change;
193. afp-submit: clarified date format, tuned logging;
194. switch fonts to www prefixed isa-afp.org domain;
195. switch to www prefixed isa-afp.org domain;
196. clarified afp-submit error handling;
197. clarified afp-submit creation and message;
198. list submission system website;
199. afp-submit: clarified api urls;
200. Removal of more unused material
201. Small simplifications. Removed a needless assumption.
202. isabelle update -u cite;
203. more accurate root.bib, based on original \bibitem entries in root.tex 1a42ddd5dbbc;
204. Fixed the bib issues and supplied a root.bib based on the one in Types_Tableaus_and_Goedels_God (by the same author)
205. merged
206. Added the missing .bib file
207. proper bib context for formal citations, although there is no document;
208. back to unchecked \cite: entry lacks .bib file;
209. back to unchecked \cite: entry lacks .bib file;
210. back to unchecked \cite: there is entry lacks .bib file;
211. proper citation;
212. merged
213. added lemmas image_grounding_of_cls_grounding_of_cls and grounding_of_clss_grounding_of_clss[simp]
214. merged
215. isabelle update -u cite;
216. merged
217. consistent casing in \cite
218. ETTS: updated bibliography and citations
219. merged
220. more correct and complete citations;
221. unchecked \cite for unidentifiable citation;
222. proper @{cite} syntax;
223. isabelle update -u cite;
224. Updating Risk Free Lending Entry - Adding lemma for transfers in special case - Fixing grammar in abstract - Adding citation
225. added bibliography to ROOT;
226. CTR and ETTS: several amendments (fact names, printing, presentation)
227. Removed a reference to the (redundant) wf_restr
228. added bibliographies to ROOTs;
229. Changes for generalised lemmas
230. Changes for generalised lemmas
231. Generalised Lemmas
232. merged
233. adapted to Isabelle/c9e091867206
234. tuned;
235. tuned signature, following Isabelle/947510ce4e36;
236. adapted to Isabelle/25900fbea7ad; fewer clones of Isabelle sources;
237. adapted to Isabelle/b61ad889dffa
238. removed Restricted_Predicates.transp_on following the introduction of equivalent Relation.transp_on in HOL
239. merged
240. adapted to Isabelle/d33fc5228aae
241. fixed proof following Isabelle/66cae055ac7b
242. merge
243. adapted to Isabelle/c48fe2be847f
244. enable -no-pie for CakeML
245. fixed proofs and removed duplicates following Isabelle/e65a50f6c2de
246. tuned proofs to use asymI, asymD, asympI, and asympD
247. Fix failing continuous integration
248. fixed proof following Isabelle/8fff4e4d81cb
249. removed Restricted_Predicates.antisymp_on following the introduction of equivalent Relation.antisymp_on in HOL
250. added lemma imgu_range_vars_subset
251. Update headers and metadata.
252. Fix ROOT again
253. Fix ROOT
254. Use transfinite induction to prove Lindenbaum's lemma, removing the countable assumption.
255. Fixed proofs following Isabelle/a7d2a7a737b8
256. added lemmas mem_range_varsI and imgu_subst_domain_subset
257. weakened the definition of redundant_inference
258. removed Restricted_Predicates.irreflp_on following the introduction of equivalent Relation.irreflp_on in HOL
259. fixed Containers following introduction of irrefl_on
260. added lemmas ex_unify_if_unifiers_not_empty, ex_mgu_if_unifiers_not_empty, and imgu_range_vars_of_equations_vars_subset
261. name change
262. AFP and DBLP
263. merged
264. added lemmas subst_range_rename_subst_domain_subset and range_vars_rename_subst_domain_subset
265. added lemma subst_domain_rename_subst_domain_subset
266. added lemma image_the_Var_image_subst_renaming_eq
267. Added acknowledgements
268. Added code export to ROOT
269. Removed out of place code
270. tuned lemma subst_domain_restrict_subst_domain
271. added lemmas rename_subst_domain_range_Var_lhs[simp] and rename_subst_domain_range_Var_rhs[simp]
272. added attribute [simp] to lemma rename_subst_domain_Var_rhs
273. added lemmas inj_on_Var[simp] and rename_subst_domain_Var_lhs[simp]
274. merged
275. removed Restricted_Predicates.reflp_on following the introduction of equivalent Relation.reflp_on in HOL
276. removed Restricted_Predicates.total_on following the introduction of equivalent Relation.totalp_on in HOL
277. added lemmas grounding_of_subst_cls_renaming_ident[simp] and grounding_of_subst_clss_renaming_ident[simp]
278. added lemmas is_ground_cls_add_mset[simp], grounding_of_subst_cls_subset, and grounding_of_subst_clss_subset
279. Streamlined a proof
280. added lemmas
281. moved lemma around
282. redefined mgu as a definition
283. tuned naming
284. fixed proof
285. added definition restrict_subst_domain and associated lemmas
286. tuned (sub)subsection
287. added lemma member_image_the_Var_image_subst
288. added lemmas unify_subst_domain_range_vars_disjoint
289. added lemma unify_range_vars
290. added lemma unify_subst_domain
291. added definition rename_subst_domain_range and related lemmas
292. merged
293. added lemmas vars_term_subst_apply_term and vars_term_subst_apply_term_subset
294. Fixed the ROOT file, so that the theory of cardinals is loaded
295. added lemma ex_mgu_if_subst_apply_term_eq_subst_apply_term
296. added lemmas unify_append_prefix_same, unify_Cons_same, unify_same, and mgu_same
297. added lemma decompose_same_Fun[simp]
298. added lemma zip_option_same[simp]
299. added definition rename_subst_domain and lemma renaming_cancels_rename_subst_domain
300. removed simp annotation from subst_apply_term_eq_subst_apply_term_if_mgu
301. used rho for renamming
302. tuned assumptions
303. added lemma subst_apply_term_eq_subst_apply_term_if_mgu
304. added lemmas inv_renaming_sound and ex_inverse_of_renaming
305. added lemma subst_apply_term_ident
306. added lemmas subst_range_Var and range_vars_Var and moved stuff around
307. added lemma subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs and tuned naming
308. tuned naming
309. added lemma mgu_range_vars
310. added lemma subst_compose_apply_eq_apply_lhs_if
311. added lemmas is_Var_mgu_if_not_in_equations, ball_is_Var_mgu, and inj_on_mgu
312. RealTimeDeque: replace `reverseN` with `take_rev
313. replaced Open_Induction.Restricted_Predicates.total_on by equivalent HOL.Relation.totap_on
314. merge from afp-2022
315. add missing thy files in Sturm_Tarski + repair
316. afp-submit: style page, improve elements;
317. afp-submit: added repository updates;
318. afp-submit: added download and faster file handling;
319. add submission pages to web ui;
320. afp-submit: add submission and build status with adapter to existing system;
321. add user-facing exception handling to web app;
322. clarified submission handling;
323. afp-submit: added submission read-only and list views;
324. add afp-submit web app;
325. add web app facilities;
326. RealTimeDeque: Separate implementation and auxiliary functions
327. Backed out changeset 3a67df508397 The finite simproc is no longer active by default
328. adapted to new simproc finite
329. clarified signature, following Isabelle/f362975e8ba1;
330. more direct Proof_Context.init_global;
331. proper naming conventions for Isabelle/ML;
332. Updated citation
333. merge from afp-2022
334. Isabelle2022: new release download links
335. Added tag Isabelle2022 for changeset 548e384c0445
336. Removal of some old junk
337. Deleted unused material
338. nothing
339. Instantiation of the order solver for ⊑ and ⊏ (no real effect though)
340. proof simplifications
341. merged
342. Simplified the proofs a bit
343. merged
344. replaced fmember.rep_eq by fmember_iff_member_fset
345. merge from afp-2021-1
346. adapted to Isabelle/457f1cba78fb
347. merged
348. added lemmas generalizes_lit_refl[simp] and generalizes_lit_trans; added simp annotation to generalizes_refl
349. extracted proof cases from lifting_lemma to distinct lemmas
350. tuned proof due to new simp rules
351. corresponding lemma was removed from distribution