metadata 554 KB
Newer Older
 Manuel Eberl committed Feb 10, 2020 1 2 [Arith_Prog_Rel_Primes] title = Arithmetic progressions and relative primes  Manuel Eberl committed Feb 10, 2020 3 author = José Manuel Rodríguez Caballero  nipkow committed May 12, 2020 4 topic = Mathematics/Number theory  Manuel Eberl committed Feb 10, 2020 5 6 date = 2020-02-01 notify = jose.manuel.rodriguez.caballero@ut.ee  Lawrence Paulson committed Mar 26, 2020 7 abstract =  Manuel Eberl committed Feb 10, 2020 8  This article provides a formalization of the solution obtained by the  Lawrence Paulson committed Mar 26, 2020 9  author of the Problem “ARITHMETIC PROGRESSIONS” from the  Manuel Eberl committed Feb 10, 2020 10 11 12 13 14 15  Putnam exam problems of 2002. The statement of the problem is as follows: For which integers n > 1 does the set of positive integers less than and relatively prime to n constitute an arithmetic progression?  Lawrence Paulson committed May 06, 2020 16 17 18 19 20 21 22 [Banach_Steinhaus] title = Banach-Steinhaus Theorem author = Dominique Unruh , Jose Manuel Rodriguez Caballero topic = Mathematics/Analysis date = 2020-05-02 notify = jose.manuel.rodriguez.caballero@ut.ee, unruh@ut.ee abstract =  Lawrence Paulson committed May 11, 2020 23 24 25  We formalize in Isabelle/HOL a result due to S. Banach and H. Steinhaus known as the Banach-Steinhaus theorem or Uniform boundedness principle: a  Lawrence Paulson committed May 06, 2020 26 27  pointwise-bounded family of continuous linear operators from a Banach space to a normed space is uniformly bounded. Our approach is an  Lawrence Paulson committed May 06, 2020 28  adaptation to Isabelle/HOL of a proof due to A. Sokal.  Lawrence Paulson committed May 06, 2020 29   Manuel Eberl committed Jan 17, 2020 30 31 32 33 34 35 [Complex_Geometry] title = Complex Geometry author = Filip Marić , Danijela Simić topic = Mathematics/Geometry date = 2019-12-16 notify = danijela@matf.bg.ac.rs, filip@matf.bg.ac.rs, boutry@unistra.fr  Lawrence Paulson committed Jan 20, 2020 36 abstract =  Manuel Eberl committed Jan 17, 2020 37 38 39 40 41 42 43 44 45 46 47 48 49 50  A formalization of geometry of complex numbers is presented. Fundamental objects that are investigated are the complex plane extended by a single infinite point, its objects (points, lines and circles), and groups of transformations that act on them (e.g., inversions and Möbius transformations). Most objects are defined algebraically, but correspondence with classical geometric definitions is shown. [Poincare_Disc] title = Poincaré Disc Model author = Danijela Simić , Filip Marić , Pierre Boutry topic = Mathematics/Geometry date = 2019-12-16 notify = danijela@matf.bg.ac.rs, filip@matf.bg.ac.rs, boutry@unistra.fr  Lawrence Paulson committed Jan 20, 2020 51 abstract =  Manuel Eberl committed Jan 17, 2020 52 53 54  We describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the extended complex plane (one dimensional complex projectives  Manuel Eberl committed Jan 17, 2020 55  space ℂP1), formalized in the AFP entry “Complex Geometry”.  Manuel Eberl committed Jan 17, 2020 56 57 58 59 60 61 62  Points, lines, congruence of pairs of points, betweenness of triples of points, circles, and isometries are defined within the model. It is shown that the model satisfies all Tarski's axioms except the Euclid's axiom. It is shown that it satisfies its negation and the limiting parallels axiom (which proves it to be a model of hyperbolic geometry).  nipkow committed Sep 11, 2019 63 64 65 66 67 68 [Fourier] title = Fourier Series author = Lawrence C Paulson topic = Mathematics/Analysis date = 2019-09-06 notify = lp15@cam.ac.uk  Lawrence Paulson committed Oct 08, 2019 69 abstract =  nipkow committed Sep 11, 2019 70 71 72 73 74 75  This development formalises the square integrable functions over the reals and the basics of Fourier series. It culminates with a proof that every well-behaved periodic function can be approximated by a Fourier series. The material is ported from HOL Light: https://github.com/jrh13/hol-light/blob/master/100/fourier.ml  Gerwin Klein committed Nov 21, 2018 76 77 78 [Generic_Deriving] title = Deriving generic class instances for datatypes author = Jonas Rädle , Lars Hupel  nipkow committed May 12, 2020 79 topic = Computer science/Data structures  Gerwin Klein committed Nov 21, 2018 80 81 82 83 84 85 86 87 88 89 90 91 92 93 date = 2018-11-06 notify = jonas.raedle@gmail.com abstract =

We provide a framework for automatically deriving instances for generic type classes. Our approach is inspired by Haskell's generic-deriving package and Scala's shapeless library. In addition to generating the code for type class functions, we also attempt to automatically prove type class laws for these instances. As of now, however, some manual proofs are still required for recursive datatypes.

Note: There are already articles in the AFP that provide automatic instantiation for a number of classes. Concretely, Deriving allows the automatic instantiation of comparators, linear orders, equality, and hashing. Show instantiates a Haskell-style show class.

Our approach works for arbitrary classes (with some Isabelle/HOL overhead for each class), but a smaller set of datatypes.

 kleing committed Jun 07, 2018 94 95 96 [Partial_Order_Reduction] title = Partial Order Reduction author = Julian Brunner  nipkow committed May 12, 2020 97 topic = Computer science/Automata and formal languages  kleing committed Jun 07, 2018 98 99 date = 2018-06-05 notify = brunnerj@in.tum.de  Lars Hupel committed Jun 15, 2018 100 abstract =  kleing committed Jun 07, 2018 101 102 103 104 105 106 107  This entry provides a formalization of the abstract theory of ample set partial order reduction. The formalization includes transition systems with actions, trace theory, as well as basics on finite, infinite, and lazy sequences. We also provide a basic framework for static analysis on concurrent systems with respect to the ample set condition.  kleing committed Mar 21, 2018 108 109 [CakeML] title = CakeML  Lars Hupel committed Jul 16, 2018 110 author = Lars Hupel , Yu Zhang <>  Lars Hupel committed Jan 08, 2019 111 contributors = Johannes Åman Pohjola <>  nipkow committed May 12, 2020 112 topic = Computer science/Programming languages/Language definitions  kleing committed Mar 21, 2018 113 114 date = 2018-03-12 notify = hupel@in.tum.de  Lars Hupel committed Jun 06, 2018 115 abstract =  kleing committed Mar 21, 2018 116 117 118 119 120 121 122  CakeML is a functional programming language with a proven-correct compiler and runtime system. This entry contains an unofficial version of the CakeML semantics that has been exported from the Lem specifications to Isabelle. Additionally, there are some hand-written theory files that adapt the exported code to Isabelle and port proofs from the HOL4 formalization, e.g. termination and equivalence proofs.  Lawrence Paulson committed Jul 11, 2019 123 124 125 [CakeML_Codegen] title = A Verified Code Generator from Isabelle/HOL to CakeML author = Lars Hupel  nipkow committed May 12, 2020 126 topic = Computer science/Programming languages/Compiling, Logic/Rewriting  Lawrence Paulson committed Jul 11, 2019 127 128 129 130 131 132 133 134 135 136 date = 2019-07-08 notify = lars@hupel.info abstract = This entry contains the formalization that accompanies my PhD thesis (see https://lars.hupel.info/research/codegen/). I develop a verified compilation toolchain from executable specifications in Isabelle/HOL to CakeML abstract syntax trees. This improves over the state-of-the-art in Isabelle by providing a trustworthy procedure for code generation.  gerwin.klein@data61.csiro.au committed Jul 18, 2018 137 138 139 [DiscretePricing] title = Pricing in discrete financial models author = Mnacho Echenim  nipkow committed May 12, 2020 140 topic = Mathematics/Probability theory, Mathematics/Games and economics  gerwin.klein@data61.csiro.au committed Jul 18, 2018 141 142 143 144 145 146 147 148 149 date = 2018-07-16 notify = mnacho.echenim@univ-grenoble-alpes.fr abstract = We have formalized the computation of fair prices for derivative products in discrete financial models. As an application, we derive a way to compute fair prices of derivative products in the Cox-Ross-Rubinstein model of a financial market, thus completing the work that was presented in this paper.  mechenim committed May 12, 2019 150 151 152 153 154 155 156 157 158 extra-history = Change history: [2019-05-12]: Renamed discr_mkt predicate to stk_strict_subs and got rid of predicate A for a more natural definition of the type discrete_market; renamed basic quantity processes for coherent notation; renamed value_process into val_process and closing_value_process to cls_val_process; relaxed hypothesis of lemma CRR_market_fair_price. Added functions to price some basic options. (revision 0b813a1a833f)
 kleing committed May 17, 2019 159   gerwin.klein@data61.csiro.au committed Jul 18, 2018 160   gerwin.klein@data61.csiro.au committed Jun 25, 2018 161 162 163 [Pell] title = Pell's Equation author = Manuel Eberl  nipkow committed May 12, 2020 164 topic = Mathematics/Number theory  gerwin.klein@data61.csiro.au committed Jun 25, 2018 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 date = 2018-06-23 notify = eberlm@in.tum.de abstract =

This article gives the basic theory of Pell's equation x2 = 1 + Dy2, where D ∈ ℕ is a parameter and x, y are integer variables.

The main result that is proven is the following: If D is not a perfect square, then there exists a fundamental solution (x0, y0) that is not the trivial solution (1, 0) and which generates all other solutions (x, y) in the sense that there exists some n ∈ ℕ such that |x| + |y| √D = (x0 + y0 √D)n. This also implies that the set of solutions is infinite, and it gives us an explicit and executable characterisation of all the solutions.

Based on this, simple executable algorithms for computing the fundamental solution and the infinite sequence of all non-negative solutions are also provided.

 nipkow committed Apr 29, 2018 197 198 199 [WebAssembly] title = WebAssembly author = Conrad Watt  nipkow committed May 12, 2020 200 topic = Computer science/Programming languages/Language definitions  nipkow committed Apr 29, 2018 201 202 date = 2018-04-29 notify = caw77@cam.ac.uk  Lawrence Paulson committed Apr 30, 2018 203 abstract =  nipkow committed Apr 29, 2018 204 205 206 207 208 209 210  This is a mechanised specification of the WebAssembly language, drawn mainly from the previously published paper formalisation of Haas et al. Also included is a full proof of soundness of the type system, together with a verified type checker and interpreter. We include only a partial procedure for the extraction of the type checker and interpreter here. For more details, please see our paper in CPP 2018.  nipkow committed Dec 18, 2017 211 212 [Knuth_Morris_Pratt] title = The string search algorithm by Knuth, Morris and Pratt  Manuel Eberl committed Feb 07, 2018 213 author = Fabian Hellauer , Peter Lammich  nipkow committed May 12, 2020 214 topic = Computer science/Algorithms  nipkow committed Dec 18, 2017 215 216 date = 2017-12-18 notify = hellauer@in.tum.de, lammich@in.tum.de  Lawrence Paulson committed Dec 22, 2017 217 abstract =  nipkow committed Dec 18, 2017 218  The Knuth-Morris-Pratt algorithm is often used to show that the  nipkow committed Dec 18, 2017 219 220 221  problem of finding a string s in a text t can be solved deterministically in O(|s| + |t|) time. We use the Isabelle  nipkow committed Dec 18, 2017 222 223 224 225 226  Refinement Framework to formulate and verify the algorithm. Via refinement, we apply some optimisations and finally use the Sepref tool to obtain executable code in Imperative/HOL.  gerwin.klein@data61.csiro.au committed Jul 15, 2017 227 228 229 [Minkowskis_Theorem] title = Minkowski's Theorem author = Manuel Eberl  nipkow committed May 12, 2020 230 topic = Mathematics/Geometry, Mathematics/Number theory  gerwin.klein@data61.csiro.au committed Jul 15, 2017 231 232 date = 2017-07-13 notify = eberlm@in.tum.de  Lawrence Paulson committed Sep 04, 2017 233 abstract =  gerwin.klein@data61.csiro.au committed Jul 15, 2017 234 235 236 237 238 239 240 241 242 243 244 245 246 247 

Minkowski's theorem relates a subset of ℝn, the Lebesgue measure, and the integer lattice ℤn: It states that any convex subset of ℝn with volume greater than 2n contains at least one lattice point from ℤn\{0}, i. e. a non-zero point with integer coefficients.

A related theorem which directly implies this is Blichfeldt's theorem, which states that any subset of ℝn with a volume greater than 1 contains two different points whose difference vector has integer components.

The entry contains a proof of both theorems.

 gerwin.klein@data61.csiro.au committed Jul 15, 2017 248 249 250 [Name_Carrying_Type_Inference] title = Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus author = Michael Rawson  nipkow committed May 12, 2020 251 topic = Computer science/Programming languages/Type systems  gerwin.klein@data61.csiro.au committed Jul 15, 2017 252 253 date = 2017-07-09 notify = mr644@cam.ac.uk, michaelrawson76@gmail.com  Lawrence Paulson committed Sep 04, 2017 254 abstract =  gerwin.klein@data61.csiro.au committed Jul 15, 2017 255 256 257 258 259 260 261 262 263 264 265  I formalise a Church-style simply-typed $$\lambda$$-calculus, extended with pairs, a unit value, and projection functions, and show some metatheory of the calculus, such as the subject reduction property. Particular attention is paid to the treatment of names in the calculus. A nominal style of binding is used, but I use a manual approach over Nominal Isabelle in order to extract an executable type inference algorithm. More information can be found in my undergraduate dissertation.  Rene Thiemann committed Jun 22, 2017 266 267 [Propositional_Proof_Systems] title = Propositional Proof Systems  Manuel Eberl committed Feb 07, 2018 268 author = Julius Michaelis , Tobias Nipkow  nipkow committed Apr 12, 2020 269 topic = Logic/Proof theory  Rene Thiemann committed Jun 22, 2017 270 271 date = 2017-06-21 notify = maintainafpppt@liftm.de  Lawrence Paulson committed Sep 04, 2017 272 abstract =  Rene Thiemann committed Jun 22, 2017 273 274 275 276 277 278 279  We formalize a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) and prove the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.  gerwin.klein@data61.csiro.au committed Jun 01, 2017 280 281 282 [Optics] title = Optics author = Simon Foster , Frank Zeyda  nipkow committed May 12, 2020 283 topic = Computer science/Functional programming, Mathematics/Algebra  gerwin.klein@data61.csiro.au committed Jun 01, 2017 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 date = 2017-05-25 notify = simon.foster@york.ac.uk abstract = Lenses provide an abstract interface for manipulating data types through spatially-separated views. They are defined abstractly in terms of two functions, get, the return a value from the source type, and put that updates the value. We mechanise the underlying theory of lenses, in terms of an algebraic hierarchy of lenses, including well-behaved and very well-behaved lenses, each lens class being characterised by a set of lens laws. We also mechanise a lens algebra in Isabelle that enables their composition and comparison, so as to allow construction of complex lenses. This is accompanied by a large library of algebraic laws. Moreover we also show how the lens classes can be applied by instantiating them with a number of Isabelle data types.  Simon Foster committed Mar 02, 2020 299 300 301 302 303 304 305 306 extra-history = Change history: [2020-03-02]: Added partial bijective and symmetric lenses. Improved alphabet command generating additional lenses and results. Several additional lens relations, including observational equivalence. Additional theorems throughout. Adaptations for Isabelle 2020.  Gerwin Klein committed Apr 13, 2020 307  (revision 44e2e5c)  gerwin.klein@data61.csiro.au committed Jun 01, 2017 308   Rene Thiemann committed May 11, 2017 309 310 [Game_Based_Crypto] title = Game-based cryptography in HOL  Andreas Lochbihler committed Jan 16, 2018 311 author = Andreas Lochbihler , S. Reza Sefidgar <>, Bhargav Bhatt  nipkow committed May 12, 2020 312 topic = Computer science/Security/Cryptography  Rene Thiemann committed May 11, 2017 313 date = 2017-05-05  Andreas Lochbihler committed Jan 16, 2018 314 notify = mail@andreas-lochbihler.de  315 abstract =  Rene Thiemann committed May 11, 2017 316 317 318 319 320 321 322 323 324 

In this AFP entry, we show how to specify game-based cryptographic security notions and formally prove secure several cryptographic constructions from the literature using the CryptHOL framework. Among others, we formalise the notions of a random oracle, a pseudo-random function, an unpredictable function, and of encryption schemes that are indistinguishable under chosen plaintext and/or ciphertext attacks. We prove the random-permutation/random-function switching lemma, security of the Elgamal and hashed Elgamal public-key encryption scheme and correctness and security of several constructions with pseudo-random  325  functions.  Rene Thiemann committed May 11, 2017 326 327 328 329 330 331 

Our proofs follow the game-hopping style advocated by Shoup and Bellare and Rogaway, from which most of the examples have been taken. We generalise some of their results such that they can be reused in other proofs. Thanks to CryptHOL's integration with Isabelle's parametricity infrastructure, many simple hops are easily justified using the theory of representation independence.

 Andreas Lochbihler committed Sep 28, 2018 332 333 334 335 336 extra-history = Change history: [2018-09-28]: added the CryptHOL tutorial for game-based cryptography (revision 489a395764ae)  Rene Thiemann committed May 11, 2017 337   Lawrence Paulson committed May 10, 2019 338 339 340 [Multi_Party_Computation] title = Multi-Party Computation author = David Aspinall , David Butler  nipkow committed May 12, 2020 341 topic = Computer science/Security  Lawrence Paulson committed May 10, 2019 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 date = 2019-05-09 notify = dbutler@turing.ac.uk abstract = We use CryptHOL to consider Multi-Party Computation (MPC) protocols. MPC was first considered by Yao in 1983 and recent advances in efficiency and an increased demand mean it is now deployed in the real world. Security is considered using the real/ideal world paradigm. We first define security in the semi-honest security setting where parties are assumed not to deviate from the protocol transcript. In this setting we prove multiple Oblivious Transfer (OT) protocols secure and then show security for the gates of the GMW protocol. We then define malicious security, this is a stronger notion of security where parties are assumed to be fully corrupted by an adversary. In this setting we again consider OT, as it is a fundamental building block of almost all MPC protocols.  Lawrence Paulson committed Oct 08, 2019 358 359 360 [Sigma_Commit_Crypto] title = Sigma Protocols and Commitment Schemes author = David Butler , Andreas Lochbihler  nipkow committed May 12, 2020 361 topic = Computer science/Security/Cryptography  Lawrence Paulson committed Oct 08, 2019 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 date = 2019-10-07 notify = dbutler@turing.ac.uk abstract = We use CryptHOL to formalise commitment schemes and Sigma-protocols. Both are widely used fundamental two party cryptographic primitives. Security for commitment schemes is considered using game-based definitions whereas the security of Sigma-protocols is considered using both the game-based and simulation-based security paradigms. In this work, we first define security for both primitives and then prove secure multiple case studies: the Schnorr, Chaum-Pedersen and Okamoto Sigma-protocols as well as a construction that allows for compound (AND and OR statements) Sigma-protocols and the Pedersen and Rivest commitment schemes. We also prove that commitment schemes can be constructed from Sigma-protocols. We formalise this proof at an abstract level, only assuming the existence of a Sigma-protocol; consequently, the instantiations of this result for the concrete Sigma-protocols we consider come for free.  Rene Thiemann committed May 11, 2017 380 381 [CryptHOL] title = CryptHOL  Andreas Lochbihler committed Jan 16, 2018 382 author = Andreas Lochbihler  nipkow committed May 12, 2020 383 topic = Computer science/Security/Cryptography, Computer science/Functional programming, Mathematics/Probability theory  Rene Thiemann committed May 11, 2017 384 date = 2017-05-05  Andreas Lochbihler committed Jan 16, 2018 385 notify = mail@andreas-lochbihler.de  386 abstract =  Rene Thiemann committed May 11, 2017 387 388 

CryptHOL provides a framework for formalising cryptographic arguments in Isabelle/HOL. It shallowly embeds a probabilistic functional  389  programming language in higher order logic. The language features  Rene Thiemann committed May 11, 2017 390 391  monadic sequencing, recursion, random sampling, failures and failure handling, and black-box access to oracles. Oracles are probabilistic  392  functions which maintain hidden state between different invocations.  Rene Thiemann committed May 11, 2017 393 394 395 396  All operators are defined in the new semantic domain of generative probabilistic values, a codatatype. We derive proof rules for the operators and establish a connection with the theory of relational parametricity. Thus, the resuting proofs are trustworthy and  397  comprehensible, and the framework is extensible and widely applicable.  Rene Thiemann committed May 11, 2017 398 399 400 401 402 

The framework is used in the accompanying AFP entry "Game-based Cryptography in HOL". There, we show-case our framework by formalizing different game-based proofs from the literature. This formalisation continues the work described in the author's ESOP 2016 paper.

 403   Lawrence Paulson committed Dec 19, 2018 404 405 [Constructive_Cryptography] title = Constructive Cryptography in HOL  nipkow committed Dec 20, 2018 406 author = Andreas Lochbihler , S. Reza Sefidgar<>  nipkow committed May 12, 2020 407 topic = Computer science/Security/Cryptography, Mathematics/Probability theory  Lawrence Paulson committed Dec 19, 2018 408 409 410 411 412 413 414 415 416 417 418 419 420 421 date = 2018-12-17 notify = mail@andreas-lochbihler.de, reza.sefidgar@inf.ethz.ch abstract = Inspired by Abstract Cryptography, we extend CryptHOL, a framework for formalizing game-based proofs, with an abstract model of Random Systems and provide proof rules about their composition and equality. This foundation facilitates the formalization of Constructive Cryptography proofs, where the security of a cryptographic scheme is realized as a special form of construction in which a complex random system is built from simpler ones. This is a first step towards a fully-featured compositional framework, similar to Universal Composability framework, that supports formalization of simulation-based proofs.  Rene Thiemann committed May 11, 2017 422 423 [Probabilistic_While] title = Probabilistic while loop  Andreas Lochbihler committed Jan 16, 2018 424 author = Andreas Lochbihler  nipkow committed May 12, 2020 425 topic = Computer science/Functional programming, Mathematics/Probability theory, Computer science/Algorithms  Rene Thiemann committed May 11, 2017 426 date = 2017-05-05  Andreas Lochbihler committed Jan 16, 2018 427 notify = mail@andreas-lochbihler.de  428 429 abstract = This AFP entry defines a probabilistic while operator based on  Rene Thiemann committed May 11, 2017 430 431 432 433 434  sub-probability mass functions and formalises zero-one laws and variant rules for probabilistic loop termination. As applications, we implement probabilistic algorithms for the Bernoulli, geometric and arbitrary uniform distributions that only use fair coin flips, and prove them correct and terminating with probability 1.  Andreas Lochbihler committed Feb 15, 2018 435 436 437 438 439 440 extra-history = Change history: [2018-02-02]: Added a proof that probabilistic conditioning can be implemented by repeated sampling. (revision 305867c4e911)
 Rene Thiemann committed May 11, 2017 441   Rene Thiemann committed May 11, 2017 442 443 [Monad_Normalisation] title = Monad normalisation  Andreas Lochbihler committed Jan 16, 2018 444 author = Joshua Schneider <>, Manuel Eberl , Andreas Lochbihler  nipkow committed May 12, 2020 445 topic = Tools, Computer science/Functional programming, Logic/Rewriting  Rene Thiemann committed May 11, 2017 446 date = 2017-05-05  Andreas Lochbihler committed Jan 16, 2018 447 notify = mail@andreas-lochbihler.de  448 abstract =  Rene Thiemann committed May 11, 2017 449  The usual monad laws can directly be used as rewrite rules for Isabelle’s  450  simplifier to normalise monadic HOL terms and decide equivalences.  Rene Thiemann committed May 11, 2017 451  In a commutative monad, however, the commutativity law is a  Rene Thiemann committed May 11, 2017 452 453  higher-order permutative rewrite rule that makes the simplifier loop. This AFP entry implements a simproc that normalises monadic  454  expressions in commutative monads using ordered rewriting. The  Rene Thiemann committed May 11, 2017 455  simproc can also permute computations across control operators like if  Rene Thiemann committed May 11, 2017 456  and case.  457   Rene Thiemann committed May 11, 2017 458 459 [Monomorphic_Monad] title = Effect polymorphism in higher-order logic  Andreas Lochbihler committed Jan 16, 2018 460 author = Andreas Lochbihler  nipkow committed May 12, 2020 461 topic = Computer science/Functional programming  Rene Thiemann committed May 11, 2017 462 date = 2017-05-05  Andreas Lochbihler committed Jan 16, 2018 463 notify = mail@andreas-lochbihler.de  464 abstract =  Rene Thiemann committed May 11, 2017 465 466 467 468 469 470 471 472 473  The notion of a monad cannot be expressed within higher-order logic (HOL) due to type system restrictions. We show that if a monad is used with values of only one type, this notion can be formalised in HOL. Based on this idea, we develop a library of effect specifications and implementations of monads and monad transformers. Hence, we can abstract over the concrete monad in HOL definitions and thus use the same definition for different (combinations of) effects. We illustrate the usefulness of effect polymorphism with a monadic interpreter for a simple language.  Andreas Lochbihler committed Feb 15, 2018 474 475 476 477 478 479 480 extra-history = Change history: [2018-02-15]: added further specifications and implementations of non-determinism; more examples (revision bc5399eea78e)
 Rene Thiemann committed May 11, 2017 481   Rene Thiemann committed Apr 20, 2017 482 483 484 485 486 487 [Constructor_Funs] title = Constructor Functions author = Lars Hupel topic = Tools date = 2017-04-19 notify = hupel@in.tum.de  Lawrence Paulson committed Apr 28, 2017 488 abstract =  Rene Thiemann committed Apr 20, 2017 489 490 491 492 493 494 495  Isabelle's code generator performs various adaptations for target languages. Among others, constructor applications have to be fully saturated. That means that for constructor calls occuring as arguments to higher-order functions, synthetic lambdas have to be inserted. This entry provides tooling to avoid this construction altogether by introducing constructor functions.  Rene Thiemann committed Apr 20, 2017 496 497 498 499 500 501 [Lazy_Case] title = Lazifying case constants author = Lars Hupel topic = Tools date = 2017-04-18 notify = hupel@in.tum.de  Lawrence Paulson committed Apr 28, 2017 502 abstract =  Rene Thiemann committed Apr 20, 2017 503 504 505 506 507 508 509 510 511 512 513 514 515  Isabelle's code generator performs various adaptations for target languages. Among others, case statements are printed as match expressions. Internally, this is a sophisticated procedure, because in HOL, case statements are represented as nested calls to the case combinators as generated by the datatype package. Furthermore, the procedure relies on laziness of match expressions in the target language, i.e., that branches guarded by patterns that fail to match are not evaluated. Similarly, if-then-else is printed to the corresponding construct in the target language. This entry provides tooling to replace these special cases in the code generator by ignoring these target language features, instead printing case expressions and if-then-else as functions.  516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 [Dict_Construction] title = Dictionary Construction author = Lars Hupel topic = Tools date = 2017-05-24 notify = hupel@in.tum.de abstract = Isabelle's code generator natively supports type classes. For targets that do not have language support for classes and instances, it performs the well-known dictionary translation, as described by Haftmann and Nipkow. This translation happens outside the logic, i.e., there is no guarantee that it is correct, besides the pen-and-paper proof. This work implements a certified dictionary translation that produces new class-free constants and derives equality theorems.  Lawrence Paulson committed Jan 15, 2019 531 532 533 [Higher_Order_Terms] title = An Algebra for Higher-Order Terms author = Lars Hupel  Lars Hupel committed Jan 16, 2019 534 contributors = Yu Zhang <>  nipkow committed May 12, 2020 535 topic = Computer science/Programming languages/Lambda calculi  Lawrence Paulson committed Jan 15, 2019 536 537 538 539 540 541 542 543 date = 2019-01-15 notify = lars@hupel.info abstract = In this formalization, I introduce a higher-order term algebra, generalizing the notions of free variables, matching, and substitution. The need arose from the work on a verified compiler from Isabelle to CakeML. Terms can be thought of as  Lars Hupel committed Jan 15, 2019 544  consisting of a generic (free variables, constants, application) and  Lawrence Paulson committed Jan 15, 2019 545 546 547 548 549 550 551 552  a specific part. As example applications, this entry provides instantiations for de-Bruijn terms, terms with named variables, and Blanchette’s λ-free higher-order terms. Furthermore, I implement translation functions between de-Bruijn terms and named terms and prove their correctness.  kleing committed Apr 07, 2017 553 554 555 556 557 558 [Subresultants] title = Subresultants author = Sebastiaan Joosten , René Thiemann , Akihisa Yamada topic = Mathematics/Algebra date = 2017-04-06 notify = rene.thiemann@uibk.ac.at  Lawrence Paulson committed Apr 28, 2017 559 abstract =  kleing committed Apr 07, 2017 560 561 562 563 564  We formalize the theory of subresultants and the subresultant polynomial remainder sequence as described by Brown and Traub. As a result, we obtain efficient certified algorithms for computing the resultant and the greatest common divisor of polynomials.  gerwin.klein@data61.csiro.au committed Mar 16, 2017 565 566 567 [Comparison_Sort_Lower_Bound] title = Lower bound on comparison-based sorting algorithms author = Manuel Eberl  nipkow committed May 12, 2020 568 topic = Computer science/Algorithms  gerwin.klein@data61.csiro.au committed Mar 16, 2017 569 570 date = 2017-03-15 notify = eberlm@in.tum.de  Lawrence Paulson committed Apr 28, 2017 571 abstract =  gerwin.klein@data61.csiro.au committed Mar 16, 2017 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 

This article contains a formal proof of the well-known fact that number of comparisons that a comparison-based sorting algorithm needs to perform to sort a list of length n is at least log2 (n!) in the worst case, i. e. Ω(n log n).

For this purpose, a shallow embedding for comparison-based sorting algorithms is defined: a sorting algorithm is a recursive datatype containing either a HOL function or a query of a comparison oracle with a continuation containing the remaining computation. This makes it possible to force the algorithm to use only comparisons and to track the number of comparisons made.

[Quick_Sort_Cost] title = The number of comparisons in QuickSort author = Manuel Eberl  nipkow committed May 12, 2020 588 topic = Computer science/Algorithms  gerwin.klein@data61.csiro.au committed Mar 16, 2017 589 590 date = 2017-03-15 notify = eberlm@in.tum.de  Lawrence Paulson committed Apr 28, 2017 591 abstract =  gerwin.klein@data61.csiro.au committed Mar 16, 2017 592 593 594 595 596 597 598 599 600 601 

We give a formal proof of the well-known results about the number of comparisons performed by two variants of QuickSort: first, the expected number of comparisons of randomised QuickSort (i. e. QuickSort with random pivot choice) is 2 (n+1) Hn - 4 n, which is asymptotically equivalent to 2 n ln n; second, the number of comparisons performed by the classic non-randomised QuickSort has the same distribution in the average case as the randomised one.

 nipkow committed Apr 04, 2017 602 603 604 [Random_BSTs] title = Expected Shape of Random Binary Search Trees author = Manuel Eberl  nipkow committed May 12, 2020 605 topic = Computer science/Data structures  nipkow committed Apr 04, 2017 606 607 date = 2017-04-04 notify = eberlm@in.tum.de  Lawrence Paulson committed Apr 28, 2017 608 abstract =  nipkow committed Apr 04, 2017 609 610 611 612 613 614 615 616 617 618 

This entry contains proofs for the textbook results about the distributions of the height and internal path length of random binary search trees (BSTs), i. e. BSTs that are formed by taking an empty BST and inserting elements from a fixed set in random order.

In particular, we prove a logarithmic upper bound on the expected height and the Θ(n log n) closed-form solution for the expected internal path length in terms of the harmonic numbers. We also show how the internal path length relates to the average-case cost of a lookup in a BST.

 Lawrence Paulson committed Oct 19, 2018 619 620 621 [Randomised_BSTs] title = Randomised Binary Search Trees author = Manuel Eberl  nipkow committed May 12, 2020 622 topic = Computer science/Data structures  Lawrence Paulson committed Oct 19, 2018 623 624 625 626 627 628 629 630 631 632 633 date = 2018-10-19 notify = eberlm@in.tum.de abstract =

This work is a formalisation of the Randomised Binary Search Trees introduced by Martínez and Roura, including definitions and correctness proofs.

Like randomised treaps, they are a probabilistic data structure that behaves exactly as if elements were inserted into a non-balancing BST in random order. However, unlike treaps, they only use discrete probability distributions, but their use of randomness is more complicated.

 Gerwin Klein committed Jan 13, 2017 634 635 636 [E_Transcendental] title = The Transcendence of e author = Manuel Eberl  nipkow committed May 12, 2020 637 topic = Mathematics/Analysis, Mathematics/Number theory  Gerwin Klein committed Jan 13, 2017 638 639 date = 2017-01-12 notify = eberlm@in.tum.de  Lawrence Paulson committed Jan 18, 2017 640 abstract =  Gerwin Klein committed Jan 13, 2017 641 642 643 644 645 646 

This work contains a proof that Euler's number e is transcendental. The proof follows the standard approach of assuming that e is algebraic and then using a specific integer polynomial to derive two inconsistent bounds, leading to a contradiction.

This kind of approach can be found in many different sources; this formalisation mostly follows a PlanetMath article by Roger Lipsett.

 Lawrence Paulson committed Oct 02, 2018 647 648 649 [Pi_Transcendental] title = The Transcendence of π author = Manuel Eberl  nipkow committed May 12, 2020 650 topic = Mathematics/Number theory  Lawrence Paulson committed Oct 02, 2018 651 652 653 654 655 656 657 658 659 660 date = 2018-09-28 notify = eberlm@in.tum.de abstract =

This entry shows the transcendence of π based on the classic proof using the fundamental theorem of symmetric polynomials first given by von Lindemann in 1882, but the formalisation mostly follows the version by Niven. The proof reuses much of the machinery developed in the AFP entry on the transcendence of e.

 gerwin.klein@nicta.com.au committed Jul 05, 2016 661 662 [DFS_Framework] title = A Framework for Verifying Depth-First Search Algorithms  Manuel Eberl committed Feb 07, 2018 663 author = Peter Lammich , René Neumann  gerwin.klein@nicta.com.au committed Jul 05, 2016 664 665 notify = lammich@in.tum.de date = 2016-07-05  nipkow committed May 12, 2020 666 topic = Computer science/Algorithms/Graph  Lawrence Paulson committed Oct 26, 2016 667 abstract =  Lars Hupel committed Oct 18, 2016 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 

This entry presents a framework for the modular verification of DFS-based algorithms, which is described in our [CPP-2015] paper. It provides a generic DFS algorithm framework, that can be parameterized with user-defined actions on certain events (e.g. discovery of new node). It comes with an extensible library of invariants, which can be used to derive invariants of a specific parameterization. Using refinement techniques, efficient implementations of the algorithms can easily be derived. Here, the framework comes with templates for a recursive and a tail-recursive implementation, and also with several templates for implementing the data structures required by the DFS algorithm. Finally, this entry contains a set of re-usable DFS-based algorithms, which illustrate the application of the framework.

[CPP-2015] Peter Lammich, René Neumann: A Framework for Verifying Depth-First Search Algorithms. CPP 2015: 137-146

 gerwin.klein@nicta.com.au committed Jul 05, 2016 684   Lawrence Paulson committed Jun 02, 2017 685 686 [Flow_Networks] title = Flow Networks and the Min-Cut-Max-Flow Theorem  Manuel Eberl committed Feb 07, 2018 687 author = Peter Lammich , S. Reza Sefidgar <>  nipkow committed May 12, 2020 688 topic = Mathematics/Graph theory  Lawrence Paulson committed Jun 02, 2017 689 690 691 692 693 date = 2017-06-01 notify = lammich@in.tum.de abstract = We present a formalization of flow networks and the Min-Cut-Max-Flow theorem. Our formal proof closely follows a standard textbook proof,  Lawrence Paulson committed Jun 02, 2017 694  and is accessible even without being an expert in Isabelle/HOL, the  Lawrence Paulson committed Jun 02, 2017 695 696  interactive theorem prover used for the formalization.  Lawrence Paulson committed Jun 02, 2017 697 698 [Prpu_Maxflow] title = Formalizing Push-Relabel Algorithms  Manuel Eberl committed Feb 07, 2018 699 author = Peter Lammich , S. Reza Sefidgar <>  nipkow committed May 12, 2020 700 topic = Computer science/Algorithms/Graph, Mathematics/Graph theory  Lawrence Paulson committed Jun 02, 2017 701 702 703 704 705 706 707 708 709 710 711 712 713 714 date = 2017-06-01 notify = lammich@in.tum.de abstract = We present a formalization of push-relabel algorithms for computing the maximum flow in a network. We start with Goldberg's et al.~generic push-relabel algorithm, for which we show correctness and the time complexity bound of O(V^2E). We then derive the relabel-to-front and FIFO implementation. Using stepwise refinement techniques, we derive an efficient verified implementation. Our formal proof of the abstract algorithms closely follows a standard textbook proof. It is accessible even without being an expert in Isabelle/HOL, the interactive theorem prover used for the formalization.  gerwin.klein@nicta.com.au committed Jul 01, 2016 715 716 717 718 719 720 [Buildings] title = Chamber Complexes, Coxeter Systems, and Buildings author = Jeremy Sylvestre notify = jeremy.sylvestre@ualberta.ca date = 2016-07-01 topic = Mathematics/Algebra, Mathematics/Geometry  Lawrence Paulson committed Oct 26, 2016 721 abstract =  Lars Hupel committed Oct 18, 2016 722 723 724 725 726 727 728 729 730 731  We provide a basic formal framework for the theory of chamber complexes and Coxeter systems, and for buildings as thick chamber complexes endowed with a system of apartments. Along the way, we develop some of the general theory of abstract simplicial complexes and of groups (relying on the group_add class for the basics), including free groups and group presentations, and their universal properties. The main results verified are that the deletion condition is both necessary and sufficient for a group with a set of generators of order two to be a Coxeter system, and that the apartments in a (thick) building are all uniformly Coxeter.  gerwin.klein@nicta.com.au committed Jul 01, 2016 732   gerwin.klein@nicta.com.au committed Jun 18, 2016 733 734 735 736 737 738 [Algebraic_VCs] title = Program Construction and Verification Components Based on Kleene Algebra author = Victor B. F. Gomes , Georg Struth notify = victor.gomes@cl.cam.ac.uk, g.struth@sheffield.ac.uk date = 2016-06-18 topic = Mathematics/Algebra  Lawrence Paulson committed Oct 26, 2016 739 abstract =  Lars Hupel committed Oct 18, 2016 740 741 742 743 744 745 746 747 748 749 750 751  Variants of Kleene algebra support program construction and verification by algebraic reasoning. This entry provides a verification component for Hoare logic based on Kleene algebra with tests, verification components for weakest preconditions and strongest postconditions based on Kleene algebra with domain and a component for step-wise refinement based on refinement Kleene algebra with tests. In addition to these components for the partial correctness of while programs, a verification component for total correctness based on divergence Kleene algebras and one for (partial correctness) of recursive programs based on domain quantales are provided. Finally we have integrated memory models for programs with pointers and a program trace semantics into the weakest precondition component.  gerwin.klein@nicta.com.au committed Jun 18, 2016 752   Lawrence Paulson committed Aug 06, 2019 753 754 755 [C2KA_DistributedSystems] title = Communicating Concurrent Kleene Algebra for Distributed Systems Specification author = Maxime Buyse , Jason Jaskolka  nipkow committed May 12, 2020 756 topic = Computer science/Automata and formal languages, Mathematics/Algebra  Lawrence Paulson committed Aug 06, 2019 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 date = 2019-08-06 notify = maxime.buyse@polytechnique.edu, jason.jaskolka@carleton.ca abstract = Communicating Concurrent Kleene Algebra (C²KA) is a mathematical framework for capturing the communicating and concurrent behaviour of agents in distributed systems. It extends Hoare et al.'s Concurrent Kleene Algebra (CKA) with communication actions through the notions of stimuli and shared environments. C²KA has applications in studying system-level properties of distributed systems such as safety, security, and reliability. In this work, we formalize results about C²KA and its application for distributed systems specification. We first formalize the stimulus structure and behaviour structure (CKA). Next, we combine them to formalize C²KA and its properties. Then, we formalize notions and properties related to the topology of distributed systems and the potential for communication via stimuli and via shared environments of agents, all within the algebraic setting of C²KA.  gerwin.klein@nicta.com.au committed May 24, 2016 775 776 777 778 779 780 [Card_Equiv_Relations] title = Cardinality of Equivalence Relations author = Lukas Bulwahn notify = lukas.bulwahn@gmail.com date = 2016-05-24 topic = Mathematics/Combinatorics  Lawrence Paulson committed Oct 26, 2016 781 abstract =  Lars Hupel committed Oct 18, 2016 782 783 784 785 786 787 788 789 790 791 792 793 794  This entry provides formulae for counting the number of equivalence relations and partial equivalence relations over a finite carrier set with given cardinality. To count the number of equivalence relations, we provide bijections between equivalence relations and set partitions, and then transfer the main results of the two AFP entries, Cardinality of Set Partitions and Spivey's Generalized Recurrence for Bell Numbers, to theorems on equivalence relations. To count the number of partial equivalence relations, we observe that counting partial equivalence relations over a set A is equivalent to counting all equivalence relations over all subsets of the set A. From this observation and the results on equivalence relations, we show that the cardinality of partial equivalence relations over a finite set of cardinality n is equal to the n+1-th Bell number.  gerwin.klein@nicta.com.au committed May 24, 2016 795   Lawrence Paulson committed Dec 30, 2016 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 [Twelvefold_Way] title = The Twelvefold Way author = Lukas Bulwahn topic = Mathematics/Combinatorics date = 2016-12-29 notify = lukas.bulwahn@gmail.com abstract = This entry provides all cardinality theorems of the Twelvefold Way. The Twelvefold Way systematically classifies twelve related combinatorial problems concerning two finite sets, which include counting permutations, combinations, multisets, set partitions and number partitions. This development builds upon the existing formal developments with cardinality theorems for those structures. It provides twelve bijections from the various structures to different equivalence classes on finite functions, and hence, proves cardinality formulae for these equivalence classes on finite functions.  Lawrence Paulson committed Oct 11, 2016 813 814 815 816 817 818 [Chord_Segments] title = Intersecting Chords Theorem author = Lukas Bulwahn notify = lukas.bulwahn@gmail.com date = 2016-10-11 topic = Mathematics/Geometry  Lawrence Paulson committed Oct 26, 2016 819 abstract =  Lars Hupel committed Oct 18, 2016 820 821 822 823 824 825 826 827 828  This entry provides a geometric proof of the intersecting chords theorem. The theorem states that when two chords intersect each other inside a circle, the products of their segments are equal. After a short review of existing proofs in the literature, I decided to use a proof approach that employs reasoning about lengths of line segments, the orthogonality of two lines and the Pythagoras Law. Hence, one can understand the formalized proof easily with the knowledge of a few general geometric facts that are commonly taught in high-school. This theorem is the 55th theorem of the Top 100 Theorems list.  Lawrence Paulson committed Oct 11, 2016 829   gerwin.klein@nicta.com.au committed Jun 26, 2016 830 831 832 833 834 [Category3] title = Category Theory with Adjunctions and Limits author = Eugene W. Stark notify = stark@cs.stonybrook.edu date = 2016-06-26  nipkow committed May 12, 2020 835 topic = Mathematics/Category theory  Lawrence Paulson committed Oct 26, 2016 836 abstract =  Lars Hupel committed Oct 18, 2016 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869  This article attempts to develop a usable framework for doing category theory in Isabelle/HOL. Our point of view, which to some extent differs from that of the previous AFP articles on the subject, is to try to explore how category theory can be done efficaciously within HOL, rather than trying to match exactly the way things are done using a traditional approach. To this end, we define the notion of category in an "object-free" style, in which a category is represented by a single partial composition operation on arrows. This way of defining categories provides some advantages in the context of HOL, including the ability to avoid the use of records and the possibility of defining functors and natural transformations simply as certain functions on arrows, rather than as composite objects. We define various constructions associated with the basic notions, including: dual category, product category, functor category, discrete category, free category, functor composition, and horizontal and vertical composite of natural transformations. A "set category" locale is defined that axiomatizes the notion "category of all sets at a type and all functions between them," and a fairly extensive set of properties of set categories is derived from the locale assumptions. The notion of a set category is used to prove the Yoneda Lemma in a general setting of a category equipped with a "hom embedding," which maps arrows of the category to the "universe" of the set category. We also give a treatment of adjunctions, defining adjunctions via left and right adjoint functors, natural bijections between hom-sets, and unit and counit natural transformations, and showing the equivalence of these definitions. We also develop the theory of limits, including representations of functors, diagrams and cones, and diagonal functors. We show that right adjoint functors preserve limits, and that limits can be constructed via products and equalizers. We characterize the conditions under which limits exist in a set category. We also examine the case of limits in a functor category, ultimately culminating in a proof that the Yoneda embedding preserves limits.  Eugene W. Stark committed May 29, 2018 870 871 872 873 874 extra-history = Change history: [2018-05-29]: Revised axioms for the category locale. Introduced notation for composition and "in hom". (revision 8318366d4575)
 Eugene W. Stark committed Feb 15, 2020 875 876 877 878  [2020-02-15]: Move ConcreteCategory.thy from Bicategory to Category3 and use it systematically. Make other minor improvements throughout. (revision a51840d36867)
 gerwin.klein@nicta.com.au committed Jun 26, 2016 879   nipkow committed May 05, 2017 880 881 882 [MonoidalCategory] title = Monoidal Categories author = Eugene W. Stark  nipkow committed May 12, 2020 883 topic = Mathematics/Category theory  nipkow committed May 05, 2017 884 885 date = 2017-05-04 notify = stark@cs.stonybrook.edu  886 abstract =  nipkow committed May 05, 2017 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903  Building on the formalization of basic category theory set out in the author's previous AFP article, the present article formalizes some basic aspects of the theory of monoidal categories. Among the notions defined here are monoidal category, monoidal functor, and equivalence of monoidal categories. The main theorems formalized are MacLane's coherence theorem and the constructions of the free monoidal category and free strict monoidal category generated by a given category. The coherence theorem is proved syntactically, using a structurally recursive approach to reduction of terms that might have some novel aspects. We also give proofs of some results given by Etingof et al, which may prove useful in a formal setting. In particular, we show that the left and right unitors need not be taken as given data in the definition of monoidal category, nor does the definition of monoidal functor need to take as given a specific isomorphism expressing the preservation of the unit object. Our definitions of monoidal category and monoidal functor are stated so as to take advantage of the economy afforded by these facts.  Eugene W. Stark committed May 29, 2018 904 905 906 907 908 909 910 911 extra-history = Change history: [2017-05-18]: Integrated material from MonoidalCategory/Category3Adapter into Category3/ and deleted adapter. (revision 015543cdd069)
[2018-05-29]: Modifications required due to 'Category3' changes. Introduced notation for "in hom". (revision 8318366d4575)
 Eugene W. Stark committed Feb 15, 2020 912 913 914  [2020-02-15]: Cosmetic improvements. (revision a51840d36867)
 nipkow committed May 05, 2017 915   gerwin.klein@nicta.com.au committed Jun 26, 2016 916 917 918 919 920 921 [Card_Multisets] title = Cardinality of Multisets author = Lukas Bulwahn notify = lukas.bulwahn@gmail.com date = 2016-06-26 topic = Mathematics/Combinatorics  Lawrence Paulson committed Oct 26, 2016 922 abstract =  Lars Hupel committed Oct 18, 2016 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 

This entry provides three lemmas to count the number of multisets of a given size and finite carrier set. The first lemma provides a cardinality formula assuming that the multiset's elements are chosen from the given carrier set. The latter two lemmas provide formulas assuming that the multiset's elements also cover the given carrier set, i.e., each element of the carrier set occurs in the multiset at least once.

The proof of the first lemma uses the argument of the recurrence relation for counting multisets. The proof of the second lemma is straightforward, and the proof of the third lemma is easily obtained using the first cardinality lemma. A challenge for the formalization is the derivation of the required induction rule, which is a special combination of the induction rules for finite sets and natural numbers. The induction rule is derived by defining a suitable inductive predicate and transforming the predicate's induction rule.

 gerwin.klein@nicta.com.au committed Jun 26, 2016 938   gerwin.klein@nicta.com.au committed May 24, 2016 939 940 941 942 943 [Posix-Lexing] title = POSIX Lexing with Derivatives of Regular Expressions author = Fahad Ausaf , Roy Dyckhoff , Christian Urban notify = christian.urban@kcl.ac.uk date = 2016-05-24  nipkow committed May 12, 2020 944 topic = Computer science/Automata and formal languages  Lawrence Paulson committed Oct 26, 2016 945 abstract =  Lars Hupel committed Oct 18, 2016 946 947 948 949 950 951 952 953 954 955 956  Brzozowski introduced the notion of derivatives for regular expressions. They can be used for a very simple regular expression matching algorithm. Sulzmann and Lu cleverly extended this algorithm in order to deal with POSIX matching, which is the underlying disambiguation strategy for regular expressions needed in lexers. In this entry we give our inductive definition of what a POSIX value is and show (i) that such a value is unique (for given regular expression and string being matched) and (ii) that Sulzmann and Lu's algorithm always generates such a value (provided that the regular expression matches the string). We also prove the correctness of an optimised version of the POSIX matching algorithm.  gerwin.klein@nicta.com.au committed May 24, 2016 957   Lawrence Paulson committed Apr 28, 2017 958 959 960 [LocalLexing] title = Local Lexing author = Steven Obua  nipkow committed May 12, 2020 961 topic = Computer science/Automata and formal languages  Lawrence Paulson committed Apr 28, 2017 962 963 964 965 966 967 968 969 970 971 972 973 974 date = 2017-04-28 notify = steven@recursivemind.com abstract = This formalisation accompanies the paper Local Lexing which introduces a novel parsing concept of the same name. The paper also gives a high-level algorithm for local lexing as an extension of Earley's algorithm. This formalisation proves the algorithm to be correct with respect to its local lexing semantics. As a special case, this formalisation thus also contains a proof of the correctness of Earley's algorithm. The paper contains a short outline of how this formalisation is organised.  gerwin.klein@nicta.com.au committed May 09, 2016 975 [MFMC_Countable]  Lawrence Paulson committed May 18, 2016 976 title = A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks  Lars Hupel committed Sep 27, 2018 977 author = Andreas Lochbihler  gerwin.klein@nicta.com.au committed May 09, 2016 978 date = 2016-05-09  nipkow committed May 12, 2020 979 topic = Mathematics/Graph theory  Lawrence Paulson committed Oct 26, 2016 980 abstract =  Lars Hupel committed May 10, 2016 981 982 983 984 985 986 987 988 989 990 991 992  This article formalises a proof of the maximum-flow minimal-cut theorem for networks with countably many edges. A network is a directed graph with non-negative real-valued edge labels and two dedicated vertices, the source and the sink. A flow in a network assigns non-negative real numbers to the edges such that for all vertices except for the source and the sink, the sum of values on incoming edges equals the sum of values on outgoing edges. A cut is a subset of the vertices which contains the source, but not the sink. Our theorem states that in every network, there is a flow and a cut such that the flow saturates all the edges going out of the cut and is zero on all the incoming edges. The proof is based on the paper The Max-Flow Min-Cut theorem for countable networks by  Andreas Lochbihler committed Sep 07, 2017 993  Aharoni et al. Additionally, we prove a characterisation of the  Lars Hupel committed May 10, 2016 994 995 996  lifting operation for relations on discrete probability distributions, which leads to a concise proof of its distributivity over relation composition.  Andreas Lochbihler committed Jan 16, 2018 997 notify = mail@andreas-lochbihler.de  Andreas Lochbihler committed Sep 07, 2017 998 999 1000 extra-history = Change history: [2017-09-06]: