equal
deleted
inserted
replaced
44 |
44 |
45 text {* |
45 text {* |
46 \begin{flushright} |
46 \begin{flushright} |
47 {\em ``Not using a [quotient] package has its advantages: we do not have to\\ |
47 {\em ``Not using a [quotient] package has its advantages: we do not have to\\ |
48 collect all the theorems we shall ever want into one giant list;''}\\ |
48 collect all the theorems we shall ever want into one giant list;''}\\ |
49 Paulson \cite{Paulson06} |
49 Larry Paulson \cite{Paulson06} |
50 \end{flushright}\smallskip |
50 \end{flushright}\smallskip |
51 |
51 |
52 \noindent |
52 \noindent |
53 Isabelle is a generic theorem prover in which many logics can be implemented. |
53 Isabelle is a generic theorem prover in which many logics can be implemented. |
54 The most widely used one, however, is |
54 The most widely used one, however, is |
56 axioms and inference |
56 axioms and inference |
57 rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted |
57 rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted |
58 mechanisms for extending the logic: one is the definition of new constants |
58 mechanisms for extending the logic: one is the definition of new constants |
59 in terms of existing ones; the other is the introduction of new types |
59 in terms of existing ones; the other is the introduction of new types |
60 by identifying non-empty subsets in existing types. It is well understood |
60 by identifying non-empty subsets in existing types. It is well understood |
61 to use both mechanism for dealing with quotient constructions in HOL (cite Larry). |
61 to use both mechanisms for dealing with quotient constructions in HOL (see for example |
|
62 \cite{Paulson06}). |
62 For example the integers in Isabelle/HOL are constructed by a quotient construction over |
63 For example the integers in Isabelle/HOL are constructed by a quotient construction over |
63 the type @{typ "nat \<times> nat"} and the equivalence relation |
64 the type @{typ "nat \<times> nat"} and the equivalence relation |
64 |
65 |
65 % I would avoid substraction for natural numbers. |
66 % I would avoid substraction for natural numbers. |
66 |
67 |