Isabelle/HOL Sample Clauses

Isabelle/HOL. ‌ Isabelle/HOL [33] is a proof assistant for Higher-Order Logic (HOL). A proof assistant en- xxxxx a theory engineer to develop theories, consisting of definitions and laws, and prove the- orems about those theories. Isabelle/HOL consists of an ML-style functional programming language and a proof system to assert and prove properties of defined constructs. Functional programming concepts include functions, algebraic datatypes, and records. A simple function for squaring an integer can be defined in Isabelle like so: definition square :: int ⇒ int where square n = n ∗ n ⇒ This definition command creates a new constant called square, whose type is int int, that is a total function from integers to integers. The body of the function is declared by the equation below the type declaration follow where. Mechanical proofs can be entered as a sequence of commands (apply-style) or using the ISAR [41] structured proof language, which supports readable proofs. Isabelle proofs are con- structed by the application of tactics that can be used to variously decompose a proof goal into a collection of simpler ones, until all goals have been discharged. Proofs are correct by construc- tion with respect to a small core of axioms as part of the LCF architecture that ensures relative soundness of the system. This follows since theories only introduce constants through defini- tion, and not through the addition of further axioms, though the latter is possible (with suitable justification) if a more powerful logic than HOL is required. Nevertheless, if the definitional approach is followed, no inconsistencies can be introduced by user theories. Though a consis- tency proof for the HOL axioms is impossible (a` la Go¨del), they have been given a semantics in ZFC set theory [23] and therefore HOL is as consistent as one of the main foundations of mathematics. Along with elementary deduction tactics, like backward chaining, Isabelle has a large number of automated proof tactics. This includes the equational simplifier simp, the classical xxxxxxxx blast, and the combination tactic auto. Tactics can be augmented with additional rules by plac- ing them in appropriate theorem sets. For instance, the set simp contains simplification laws and intro contains introduction laws. Isabelle also includes a number of high-level proof tools [4] such as sledgehammer, a principled integration of third-party automated theorem provers, and nitpick, a counterexample generator. We believe this combinat...