## Isabelle: A Generic Theorem ProverAs a generic theorem prover, Isabelle supports a variety of logics. Distinctive features include Isabelle's representation of logics within a meta-logic and the use of higher-order unification to combine inference rules. Isabelle can be applied to reasoning in pure mathematics or verification of computer systems. This volume constitutes the Isabelle documentation. It begins by outlining theoretical aspects and then demonstrates the use in practice. Virtually all Isabelle functions are described, with advice on correct usage and numerous examples. Isabelle's built-in logics are also described in detail. There is a comprehensive bebliography and index. The book addresses prospective users of Isabelle as well as researchers in logic and automated reasoning. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

1 Foundations | 3 |

12 Formalizing logical rules in Isabelle | 7 |

13 Proof construction in Isabelle | 11 |

14 Lifting a rule into a context | 15 |

15 Backward proof by resolution | 17 |

16 Variations on resolution | 21 |

2 Getting Started with Isabelle | 25 |

22 Backward proof | 30 |

14 The Classical Reasoner | 171 |

142 Simulating sequents by natural deduction | 172 |

143 Extra rules for the sequent calculus | 173 |

144 Classical rule sets | 174 |

145 The classical tactics | 176 |

146 Setting up the classical reasoner | 178 |

Isabelles ObjectLogics | 179 |

15 Basic Concepts | 181 |

23 Quantifier reasoning | 34 |

3 Advanced Methods | 41 |

32 Defining theories | 46 |

the natural numbers | 52 |

35 A Prolog interpreter | 58 |

The Isabelle Reference Manual | 63 |

4 Basic Use of Isabelle | 65 |

42 Ending a session | 66 |

45 Displaying exceptions as error messages | 68 |

The Subgoal Module | 71 |

52 Shortcuts for applying tactics | 74 |

53 Executing batch proofs | 76 |

54 Managing multiple proofs | 77 |

55 Debugging and inspecting | 78 |

6 Tactics | 81 |

62 Other basic tactics | 83 |

63 Obscure tactics | 85 |

64 Managing lots of rules | 87 |

65 Programming tools for proof strategies | 89 |

66 Sequences | 90 |

7 Tacticals | 93 |

72 Control and search tacticals | 95 |

73 Tacticals for subgoal numbering | 98 |

8 Theorems and Forward Proof | 101 |

82 Primitive metalevel inference rules | 105 |

83 Derived rules for goaldirected proof | 109 |

9 Theories Terms and Types | 113 |

92 Loading a new theory | 115 |

93 Reloading modified theories | 116 |

94 Basic operations on theories | 118 |

95 Terms | 119 |

96 Variable binding | 120 |

97 Certified terms | 121 |

98 Types | 122 |

10 Defining Logics | 125 |

103 Mixfix declarations | 131 |

some minimal logics | 136 |

11 Syntax Transformations | 139 |

112 Transforming parse trees to ASTs | 140 |

113 Transforming ASTs to terms | 142 |

Syntactic rewriting | 144 |

116 Translation functions | 150 |

12 Substitution Tactics | 153 |

122 Substitution in the hypotheses | 154 |

123 Setting up hyp_subst_tac | 155 |

13 Simplification | 157 |

132 The simplification tactics | 160 |

133 Examples using the simplifier | 161 |

134 Permutative rewrite rules | 164 |

135 Setting up the simplifier | 166 |

151 Syntax definitions | 182 |

152 Proof procedures | 183 |

16 FirstOrder Logic | 185 |

162 Generic packages | 186 |

164 Classical proof procedures | 191 |

165 An intuitionistic example | 192 |

166 An example of intuitionistic negation | 193 |

167 A classical example | 195 |

168 Derived rules and the classical tactics | 196 |

17 ZermeloFraenkel Set Theory | 203 |

172 The syntax of set theory | 204 |

173 Binding operators | 206 |

17A The ZermeloFraenkel axioms | 208 |

175 From basic lemmas to function spaces | 211 |

176 Further developments | 219 |

177 Simplification rules | 228 |

178 The examples directory | 229 |

179 A proof about powersets | 230 |

1710 Monotonicity of the union operator | 232 |

1711 Lowlevel reasoning about functions | 233 |

18 HigherOrder Logic | 235 |

182 Rules of inference | 240 |

183 A formulation of set theory | 245 |

184 Generic packages and classical reasoning | 251 |

185 Types | 253 |

186 The examples directories | 259 |

Cantors Theorem | 260 |

19 FirstOrder Sequent Calculus | 263 |

192 Syntax and rules of inference | 265 |

193 Tactics for the cut rule | 267 |

194 Tactics for sequents | 268 |

195 Packaging sequent rules | 269 |

196 Proof procedures | 270 |

197 A simple example of classical reasoning | 271 |

198 A more complex proof | 272 |

20 Constructive Type Theory | 275 |

201 Syntax | 277 |

203 Rule lists | 281 |

204 Tactics for subgoal reordering | 284 |

206 Tactics for logical reasoning | 285 |

207 A theory of arithmetic | 286 |

type inference | 288 |

2010 An example of logical reasoning | 289 |

deriving a currying functional | 292 |

proving the Axiom of Choice | 293 |

A Syntax of Isabelle Theories | 297 |

301 | |

305 | |

### Other editions - View all

### Common terms and phrases

abbreviates abstraction appear applies argument arities assumption axioms basic bool bound called classical commands conclusion constants constructor constructs contains defined definitions derived rules elimination equality example expressed fails False Figure first-order formalized formula function given goal higher-order identifiers induction infix instantiate introduction intuitionistic logic Isabelle Isabelle's Left Level logic macro natural numbers operator pairs parameters parse performs Pow(A premises prems presents printing priority Proceedings productions proof prop prove quantifier reasoning recursion relation REPEAT replaces requires resolution resolve_tac result returns rewrite rules rules Sect sequence set theory simplifier solve sort specifies step string subgoal SUM X:A symbol syntax tactic takes term theorem theory thm list translations true unification unifiers Union unit unknowns variables yields