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 Larry 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 |
54 The most widely used one, however, is |
54 implemented. The most widely used one, however, is Higher-Order Logic |
55 Higher-Order Logic (HOL). This logic consists of a small number of |
55 (HOL). This logic consists of a small number of axioms and inference rules |
56 axioms and inference |
56 over a simply-typed term-language. Safe reasoning in HOL is ensured by two |
57 rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted |
57 very restricted mechanisms for extending the logic: one is the definition of |
58 mechanisms for extending the logic: one is the definition of new constants |
58 new constants in terms of existing ones; the other is the introduction of |
59 in terms of existing ones; the other is the introduction of new types |
59 new types by identifying non-empty subsets in existing types. It is well |
60 by identifying non-empty subsets in existing types. It is well understood |
60 understood to use both mechanisms for dealing with quotient constructions in |
61 to use both mechanisms for dealing with quotient constructions in HOL (see for example |
61 HOL (see for example \cite{Homeier05,Paulson06}). For example the integers |
62 \cite{Paulson06}). |
62 in Isabelle/HOL are constructed by a quotient construction over the type |
63 For example the integers in Isabelle/HOL are constructed by a quotient construction over |
63 @{typ "nat \<times> nat"} and the equivalence relation |
64 the type @{typ "nat \<times> nat"} and the equivalence relation |
64 |
65 |
65 @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"} |
66 % I would avoid substraction for natural numbers. |
|
67 |
|
68 @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"} |
|
69 |
66 |
70 \noindent |
67 \noindent |
71 Similarly one can construct the type of finite sets by quotienting lists |
68 This produces the type @{typ int} and definitions for @{text "0::int"} and |
72 according to the equivalence relation |
69 @{text "1::int"} in terms of pairs of natural numbers can be given (namely |
73 |
70 @{text "(0, 0)"} and @{text "(1, 0)"}). Operations such as @{text "add::int |
74 @{text [display] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} |
71 \<Rightarrow> int \<Rightarrow> int"} can be defined in terms of operations on pairs of natural |
|
72 numbers. Similarly one can construct the type of finite sets by quotienting |
|
73 lists according to the equivalence relation |
|
74 |
|
75 @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} |
75 |
76 |
76 \noindent |
77 \noindent |
77 where @{text "\<in>"} stands for membership in a list. |
78 which means two lists are equivalent if every element in one list is also |
|
79 member in the other (@{text "\<in>"} stands here for membership in lists). |
78 |
80 |
79 The problem is that in order to start reasoning about, for example integers, |
81 The problem is that in order to start reasoning about, for example integers, |
80 definitions and theorems need to be transferred, or \emph{lifted}, |
82 definitions and theorems need to be transferred, or \emph{lifted}, |
81 from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}. |
83 from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}. |
82 This lifting usually requires a lot of tedious reasoning effort. |
84 This lifting usually requires a lot of tedious reasoning effort. |