diff --git a/thys/Blue_Eyes/Blue_Eyes.thy b/thys/Blue_Eyes/Blue_Eyes.thy new file mode 100644 --- /dev/null +++ b/thys/Blue_Eyes/Blue_Eyes.thy @@ -0,0 +1,424 @@ +(*<*) +theory Blue_Eyes + imports Main +begin +(*>*) + +section \Introduction\ + +text \The original problem statement @{cite xkcd} explains the puzzle well: + +\begin{quotation} +A group of people with assorted eye colors live on an island. +They are all perfect logicians -- if a conclusion can be logically deduced, +they will do it instantly. +No one knows the color of their eyes. +Every night at midnight, a ferry stops at the island. +Any islanders who have figured out the color of their own eyes then leave the island, and the rest stay. +Everyone can see everyone else at all times +and keeps a count of the number of people they see with each eye color (excluding themselves), +but they cannot otherwise communicate. +Everyone on the island knows all the rules in this paragraph. + +On this island there are 100 blue-eyed people, +100 brown-eyed people, +and the Guru (she happens to have green eyes). +So any given blue-eyed person can see 100 people with brown eyes and 99 people with blue eyes (and one with green), +but that does not tell him his own eye color; +as far as he knows the totals could be 101 brown and 99 blue. +Or 100 brown, 99 blue, and he could have red eyes. + +The Guru is allowed to speak once (let's say at noon), +on one day in all their endless years on the island. +Standing before the islanders, she says the following: + +``I can see someone who has blue eyes.'' + +Who leaves the island, and on what night? +\end{quotation} + +It might seem weird that the Guru's declaration gives anyone any new information. +For an informal discussion, see \cite[Section~1.1]{fagin1995}.\ + +section \Modeling the world \label{sec:world}\ + +text \We begin by fixing two type variables: @{typ "'color"} and @{typ "'person"}. +The puzzle doesn't specify how many eye colors are possible, but four are mentioned. +Crucially, we must assume they are distinct. We specify the existence of colors other +than blue and brown, even though we don't mention them later, because when blue and brown +are the only possible colors, the puzzle has a different solution — the brown-eyed logicians +may leave one day after the blue-eyed ones. + +We refrain from specifying the exact population of the island, choosing to only assume +it is finite and denote a specific person as the Guru. + +We could also model the Guru as an outside entity instead of a participant. This doesn't change +the answer and results in a slightly simpler proof, but is less faithful to the problem statement.\ + +context + fixes blue brown green red :: 'color + assumes colors_distinct: "distinct [blue, brown, green, red]" + + fixes guru :: 'person + assumes "finite (UNIV :: 'person set)" +begin + +text \It's slightly tricky to formalize the behavior of perfect logicians. +The representation we use is centered around the type of a @{emph \world\}, +which describes the entire state of the environment. In our case, it's a function +@{typ "'person => 'color"} that assigns an eye color to everyone.@{footnote \We would introduce +a type synonym, but at the time of writing Isabelle doesn't support including type variables fixed +by a locale in a type synonym.\} + +The only condition known to everyone and not dependent on the observer is Guru's declaration:\ + +definition valid :: "('person \ 'color) \ bool" where + "valid w \ (\p. p \ guru \ w p = blue)" + +text \We then define the function @{term "possible n p w w'"}, which returns @{term True} +if on day \n\ the potential world \w'\ is plausible from the perspective of person \p\, +based on the observations they made in the actual world \w\. + +Then, @{term "leaves n p w"} is @{term True} if \p\ is able to unambiguously deduce +the color of their own eyes, i.e. if it is the same in all possible worlds. Note that if \p\ actually +left many moons ago, this function still returns @{term True}.\ + +fun leaves :: "nat \ 'person \ ('person \ 'color) \ bool" + and possible :: "nat \ 'person \ ('person \ 'color) \ ('person \ 'color) \ bool" + where + "leaves n p w = (\w'. possible n p w w' \ w' p = w p)" | + "possible n p w w' \ valid w \ valid w' + \ (\p' \ p. w p' = w' p') + \ (\n' < n. \p'. leaves n' p' w = leaves n' p' w')" + +text \Naturally, the act of someone leaving can be observed by others, thus the two definitions +are mutually recursive. As such, we need to instruct the simplifier to not unfold these definitions endlessly.\ +declare possible.simps[simp del] leaves.simps[simp del] + +text \A world is possible if + \<^enum> The Guru's declaration holds. + \<^enum> The eye color of everyone but the observer matches. + \<^enum> The same people left on each of the previous days. + +Moreover, we require that the actual world \w\ is \valid\, so that the relation is symmetric:\ + +lemma possible_sym: "possible n p w w' = possible n p w' w" + by (auto simp: possible.simps) + +text \In fact, \possible n p\ is an equivalence relation:\ + +lemma possible_refl: "valid w \ possible n p w w" + by (auto simp: possible.simps) + +lemma possible_trans: "possible n p w1 w2 \ possible n p w2 w3 \ possible n p w1 w3" + by (auto simp: possible.simps) + +section \Eye colors other than blue\ + +text \Since there is no way to distinguish between the colors other than blue, +only the blue-eyed people will ever leave. To formalize this notion, we define +a function that takes a world and replaces the eye color of a specified person. +The original color is specified too, so that the transformation composes nicely +with the recursive hypothetical worlds of @{const possible}.\ + +definition try_swap :: "'person \ 'color \ 'color \ ('person \ 'color) \ ('person \ 'color)" where + "try_swap p c\<^sub>1 c\<^sub>2 w x = (if c\<^sub>1 = blue \ c\<^sub>2 = blue \ x \ p then w x else Fun.swap c\<^sub>1 c\<^sub>2 id (w x))" + +lemma try_swap_valid[simp]: "valid (try_swap p c\<^sub>1 c\<^sub>2 w) = valid w" + by (auto simp add: try_swap_def valid_def swap_def) + +lemma try_swap_eq[simp]: "try_swap p c\<^sub>1 c\<^sub>2 w x = try_swap p c\<^sub>1 c\<^sub>2 w' x \ w x = w' x" + by (auto simp add: try_swap_def swap_def) + +lemma try_swap_inv[simp]: "try_swap p c\<^sub>1 c\<^sub>2 (try_swap p c\<^sub>1 c\<^sub>2 w) = w" + by (rule ext) (auto simp add: try_swap_def swap_def) + +lemma leaves_try_swap[simp]: + assumes "valid w" + shows "leaves n p (try_swap p' c\<^sub>1 c\<^sub>2 w) = leaves n p w" + using assms +proof (induction n arbitrary: p w rule: less_induct) + case (less n) + have "leaves n p w" if "leaves n p (try_swap p' c\<^sub>1 c\<^sub>2 w)" for w + proof (unfold leaves.simps; rule+) + fix w' + assume "possible n p w w'" + then have "possible n p (try_swap p' c\<^sub>1 c\<^sub>2 w) (try_swap p' c\<^sub>1 c\<^sub>2 w')" + by (fastforce simp: possible.simps less.IH) + with `leaves n p (try_swap p' c\<^sub>1 c\<^sub>2 w)` have "try_swap p' c\<^sub>1 c\<^sub>2 w' p = try_swap p' c\<^sub>1 c\<^sub>2 w p" + unfolding leaves.simps + by simp + thus "w' p = w p" by simp + qed + + with try_swap_inv show ?case by auto +qed + +text \This lets us prove that only blue-eyed people will ever leave the island.\ + +proposition only_blue_eyes_leave: + assumes "leaves n p w" and "valid w" + shows "w p = blue" +proof (rule ccontr) + assume "w p \ blue" + then obtain c where c: "w p \ c" "c \ blue" + using colors_distinct + by (metis distinct_length_2_or_more) + + let ?w' = "try_swap p (w p) c w" + have "possible n p w ?w'" + using `valid w` apply (simp add: possible.simps) + by (auto simp: try_swap_def) + moreover have "?w' p \ w p" + using c `w p \ blue` by (auto simp: try_swap_def) + ultimately have "\ leaves n p w" + by (auto simp: leaves.simps) + with assms show False by simp +qed + +section "The blue-eyed logicians" + +text \We will now consider the behavior of the logicians with blue eyes. First, +some simple lemmas. Reasoning about set cardinalities often requires considering infinite +sets separately. Usefully, all sets of people are finite by assumption.\ + +lemma people_finite[simp]: "finite (S::'person set)" +proof (rule finite_subset) + show "S \ UNIV" by auto + show "finite (UNIV::'person set)" by fact +qed + +text \Secondly, we prove a destruction rule for @{const possible}. It is strictly weaker than +the definition, but thanks to the simpler form, it's easier to guide the automation with it.\ +lemma possibleD_colors: + assumes "possible n p w w'" and "p' \ p" + shows "w' p' = w p'" + using assms unfolding possible.simps by simp + +text \A central concept in the reasoning is the set of blue-eyed people someone can see.\ +definition blues_seen :: "('person \ 'color) \ 'person \ 'person set" where + "blues_seen w p = {p'. w p' = blue} - {p}" + +lemma blues_seen_others: + assumes "w p' = blue" and "p \ p'" + shows "w p = blue \ card (blues_seen w p) = card (blues_seen w p')" + and "w p \ blue \ card (blues_seen w p) = Suc (card (blues_seen w p'))" +proof - + assume "w p = blue" + then have "blues_seen w p' = blues_seen w p \ {p} - {p'}" + by (auto simp add: blues_seen_def) + moreover have "p \ blues_seen w p" + unfolding blues_seen_def by auto + moreover have "p' \ blues_seen w p \ {p}" + unfolding blues_seen_def using `p \ p'` `w p' = blue` by auto + ultimately show "card (blues_seen w p) = card (blues_seen w p')" + by simp +next + assume "w p \ blue" + then have "blues_seen w p' = blues_seen w p - {p'}" + by (auto simp add: blues_seen_def) + moreover have "p' \ blues_seen w p" + unfolding blues_seen_def using `p \ p'` `w p' = blue` by auto + ultimately show "card (blues_seen w p) = Suc (card (blues_seen w p'))" + by (simp only: card_Suc_Diff1 people_finite) +qed + +lemma blues_seen_same[simp]: + assumes "possible n p w w'" + shows "blues_seen w' p = blues_seen w p" + using assms + by (auto simp: blues_seen_def possible.simps) + +lemma possible_blues_seen: + assumes "possible n p w w'" + assumes "w p' = blue" and "p \ p'" + shows "w' p = blue \ card (blues_seen w p) = card (blues_seen w' p')" + and "w' p \ blue \ card (blues_seen w p) = Suc (card (blues_seen w' p'))" + using possibleD_colors[OF `possible n p w w'`] and blues_seen_others assms + by (auto simp flip: blues_seen_same) + +text \Finally, the crux of the solution. We proceed by strong induction.\ + +lemma blue_leaves: + assumes "w p = blue" and "valid w" + and guru: "w guru \ blue" + shows "leaves n p w \ n \ card (blues_seen w p)" + using assms +proof (induction n arbitrary: p w rule: less_induct) + case (less n) + show ?case + proof + \ \First, we show that day \n\ is sufficient to deduce that the eyes are blue.\ + assume "n \ card (blues_seen w p)" + have "w' p = blue" if "possible n p w w'" for w' + proof (cases "card (blues_seen w' p)") + case 0 + moreover from `possible n p w w'` have "valid w'" + by (simp add: possible.simps) + ultimately show "w' p = blue" + unfolding valid_def blues_seen_def by auto + next + case (Suc k) + \ \We consider the behavior of somebody else, who also has blue eyes.\ + then have "blues_seen w' p \ {}" + by auto + then obtain p' where "w' p' = blue" and "p \ p'" + unfolding blues_seen_def by auto + then have "w p' = blue" + using possibleD_colors[OF `possible n p w w'`] by simp + + have "p \ guru" + using `w p = blue` and `w guru \ blue` by auto + hence "w' guru \ blue" + using `w guru \ blue` and possibleD_colors[OF `possible n p w w'`] by simp + + have "valid w'" + using `possible n p w w'` unfolding possible.simps by simp + + show "w' p = blue" + proof (rule ccontr) + assume "w' p \ blue" + \ \If our eyes weren't blue, then \p'\ would see one blue-eyed person less than us.\ + with possible_blues_seen[OF `possible n p w w'` `w p' = blue` `p \ p'`] + have *: "card (blues_seen w p) = Suc (card (blues_seen w' p'))" + by simp + \ \By induction, they would've left on day \k = blues_seen w' p'\.\ + let ?k = "card (blues_seen w' p')" + have "?k < n" + using `n \ card (blues_seen w p)` and * by simp + hence "leaves ?k p' w'" + using `valid w'` `w' p' = blue` `w' guru \ blue` + by (intro less.IH[THEN iffD2]; auto) + \ \However, we know that actually, \p'\ didn't leave that day yet.\ + moreover have "\ leaves ?k p' w" + proof + assume "leaves ?k p' w" + then have "?k \ card (blues_seen w p')" + using `?k < n` `w p' = blue` `valid w` `w guru \ blue` + by (intro less.IH[THEN iffD1]; auto) + + have "card (blues_seen w p) = card (blues_seen w p')" + by (intro blues_seen_others; fact) + with * have "?k < card (blues_seen w p')" + by simp + with `?k \ card (blues_seen w p')` show False by simp + qed + moreover have "leaves ?k p' w' = leaves ?k p' w" + using `possible n p w w'` `?k < n` + unfolding possible.simps by simp + ultimately show False by simp + qed + qed + thus "leaves n p w" + unfolding leaves.simps using `w p = blue` by simp + next + \ \Then, we show that it's not possible to deduce the eye color any earlier.\ + { + assume "n < card (blues_seen w p)" + \ \Consider a hypothetical world where \p\ has brown eyes instead. We will prove that this + world is \possible\.\ + let ?w' = "w(p := brown)" + have "?w' guru \ blue" + using `w guru \ blue` `w p = blue` + by auto + have "valid ?w'" + proof - + from `n < card (blues_seen w p)` have "card (blues_seen w p) \ 0" by auto + hence "blues_seen w p \ {}" + by auto + then obtain p' where "p' \ blues_seen w p" + by auto + hence "p \ p'" and "w p' = blue" + by (auto simp: blues_seen_def) + hence "?w' p' = blue" by auto + with `?w' guru \ blue` show "valid ?w'" + unfolding valid_def by auto + qed + moreover have "leaves n' p' w = leaves n' p' ?w'" if "n' < n" for n' p' + proof - + have not_leavesI: "\leaves n' p' w'" + if "valid w'" "w' guru \ blue" and P: "w' p' = blue \ n' < card (blues_seen w' p')" for w' + proof (cases "w' p' = blue") + case True + then have "leaves n' p' w' \ n' \ card (blues_seen w' p')" + using less.IH `n' < n` `valid w'` `w' guru \ blue` + by simp + with P[OF `w' p' = blue`] show "\leaves n' p' w'" by simp + next + case False + then show "\ leaves n' p' w'" + using only_blue_eyes_leave `valid w'` by auto + qed + + have "\leaves n' p' w" + proof (intro not_leavesI) + assume "w p' = blue" + with `w p = blue` have "card (blues_seen w p) = card (blues_seen w p')" + apply (cases "p = p'", simp) + by (intro blues_seen_others; auto) + with `n' < n` and `n < card (blues_seen w p)` show "n' < card (blues_seen w p')" + by simp + qed fact+ + + moreover have "\ leaves n' p' ?w'" + proof (intro not_leavesI) + assume "?w' p' = blue" + with colors_distinct have "p \ p'" and "?w' p \ blue" by auto + hence "card (blues_seen ?w' p) = Suc (card (blues_seen ?w' p'))" + using `?w' p' = blue` + by (intro blues_seen_others; auto) + moreover have "blues_seen w p = blues_seen ?w' p" + unfolding blues_seen_def by auto + ultimately show "n' < card (blues_seen ?w' p')" + using `n' < n` and `n < card (blues_seen w p)` + by auto + qed fact+ + + ultimately show "leaves n' p' w = leaves n' p' ?w'" by simp + qed + ultimately have "possible n p w ?w'" + using `valid w` + by (auto simp: possible.simps) + moreover have "?w' p \ blue" + using colors_distinct by auto + ultimately have "\ leaves n p w" + unfolding leaves.simps + using `w p = blue` by blast + } + then show "leaves n p w \ n \ card (blues_seen w p)" + by fastforce + qed +qed + +text \This can be combined into a theorem that describes the behavior of the logicians based +on the objective count of blue-eyed people, and not the count by a specific person. The xkcd +puzzle is the instance where \n = 99\.\ + +theorem blue_eyes: + assumes "card {p. w p = blue} = Suc n" and "valid w" and "w guru \ blue" + shows "leaves k p w \ w p = blue \ k \ n" +proof (cases "w p = blue") + case True + with assms have "card (blues_seen w p) = n" + unfolding blues_seen_def by simp + then show ?thesis + using `w p = blue` `valid w` `w guru \ blue` blue_leaves + by simp +next + case False + then show ?thesis + using only_blue_eyes_leave `valid w` by auto +qed + +end + +(*<*) +end +(*>*) + +section \Future work\ + +text \After completing this formalization, I have been made aware of epistemic logic. +The @{emph \possible worlds\} model in \cref{sec:world} turns out to be quite similar +to the usual semantics of this logic. It might be interesting to solve this puzzle within +the axiom system of epistemic logic, without explicit reasoning about possible worlds.\ \ No newline at end of file diff --git a/thys/Blue_Eyes/ROOT b/thys/Blue_Eyes/ROOT new file mode 100644 --- /dev/null +++ b/thys/Blue_Eyes/ROOT @@ -0,0 +1,9 @@ +chapter AFP + +session Blue_Eyes (AFP) = HOL + + options [timeout = 300] + theories + Blue_Eyes + document_files + "root.tex" + "root.bib" diff --git a/thys/Blue_Eyes/document/root.bib b/thys/Blue_Eyes/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Blue_Eyes/document/root.bib @@ -0,0 +1,15 @@ +@online{xkcd, + author = {Randall Munroe}, + title = {Blue Eyes --- A Logic Puzzle}, + url = {https://xkcd.com/blue_eyes.html}, + urldate = {2021-01-26} +} + +@book{fagin1995, + title = {Reasoning About Knowledge}, + language = {eng}, + publisher = {MIT Press}, + year = {1995}, + isbn = {0262061627}, + author = {Fagin, R. and Halpern, J.Y. and Moses, Y. and Vardi, M.Y.} +} \ No newline at end of file diff --git a/thys/Blue_Eyes/document/root.tex b/thys/Blue_Eyes/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Blue_Eyes/document/root.tex @@ -0,0 +1,68 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} +\usepackage[T1]{fontenc} +\usepackage[margin=2.5cm]{geometry} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap]{stmaryrd} + %for \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% this should be the last package used, but isn't, because cleveref complains when it is +\usepackage{pdfsetup} +\usepackage{cleveref} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + + +\begin{document} + +\title{Solution to the xkcd Blue Eyes puzzle} +\author{Jakub Kądziołka} +\maketitle + +\begin{abstract} + In a puzzle published by Randall Munroe~\cite{xkcd}, perfect logicians forbidden + from communicating are stranded on an island, and may only leave once they + have figured out their own eye color. We present a method of modeling the + behavior of perfect logicians and formalize a solution of the puzzle. +\end{abstract} + +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +\bibliographystyle{plainurl} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,576 +1,577 @@ 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 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 BNF_CC BNF_Operations Banach_Steinhaus Bell_Numbers_Spivey 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 CYK 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 CofGroups Coinductive Coinductive_Languages Collections Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties CSP_RefTK DFS_Framework DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC 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 Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of Hello_World HereditarilyFinite Hermite Hidden_Markov_Models Higher_Order_Terms Hoare_Time HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interval_Arithmetic_Word32 Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaGeoCoq 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 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 Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option 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 Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem 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_Of_Medians_Selection Menger Mersenne_Primes MiniML Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security 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 PCF PLM POPLmark-deBruijn PSemigroupsConvolution 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 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 Projective_Geometry Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem QHLProver QR_Decomposition Quantales 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 Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regular-Sets Regular_Algebras Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sort_Encodings Source_Coding_Theorem 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 SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God UPF UPF_Firewall UTP Universal_Turing_Machine UpDown_Scheme Valuation VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval Word_Lib WorkerWrapper XML ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL