56 (HOL). This logic consists of a small number of axioms and inference rules |
56 (HOL). This logic consists of a small number of axioms and inference rules |
57 over a simply-typed term-language. Safe reasoning in HOL is ensured by two |
57 over a simply-typed term-language. Safe reasoning in HOL is ensured by two |
58 very restricted mechanisms for extending the logic: one is the definition of |
58 very restricted mechanisms for extending the logic: one is the definition of |
59 new constants in terms of existing ones; the other is the introduction of |
59 new constants in terms of existing ones; the other is the introduction of |
60 new types by identifying non-empty subsets in existing types. It is well |
60 new types by identifying non-empty subsets in existing types. It is well |
61 understood how to use both mechanisms for dealing with quotient |
61 understood how to use both mechanisms for dealing with many quotient |
62 constructions in HOL (see \cite{Homeier05,Paulson06}). For example the |
62 constructions in HOL (see \cite{Homeier05,Paulson06}). For example the |
63 integers in Isabelle/HOL are constructed by a quotient construction over the |
63 integers in Isabelle/HOL are constructed by a quotient construction over the |
64 type @{typ "nat \<times> nat"} and the equivalence relation |
64 type @{typ "nat \<times> nat"} and the equivalence relation |
65 |
65 |
66 @{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 @{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"} |
69 This constructions yields the new type @{typ int} and definitions for @{text |
69 This constructions yields the new type @{typ int} and definitions for @{text |
70 "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of |
70 "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of |
71 natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations |
71 natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations |
72 such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in |
72 such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in |
73 terms of operations on pairs of natural numbers (namely @{text |
73 terms of operations on pairs of natural numbers (namely @{text |
74 "add\<^bsub>nat\<times>nat\<^esub> (x\<^isub>1, y\<^isub>1) (x\<^isub>2, |
74 "add\<^bsub>nat\<times>nat\<^esub> (n\<^isub>1, m\<^isub>1) (n\<^isub>2, |
75 y\<^isub>2) \<equiv> (x\<^isub>1 + x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}). |
75 m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}). |
76 Similarly one can construct the type of finite sets by quotienting lists |
76 Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"}, |
77 according to the equivalence relation |
77 by quotienting @{text "\<alpha> list"} according to the equivalence relation |
78 |
78 |
79 @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} |
79 @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} |
80 |
80 |
81 \noindent |
81 \noindent |
82 which states that two lists are equivalent if every element in one list is also |
82 which states that two lists are equivalent if every element in one list is also |
88 calculi. A simple example is the lambda-calculus, whose ``raw'' terms are defined as |
88 calculi. A simple example is the lambda-calculus, whose ``raw'' terms are defined as |
89 |
89 |
90 @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"} |
90 @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"} |
91 |
91 |
92 \noindent |
92 \noindent |
93 The problem with this definition arises when one, for example, attempts to |
93 The problem with this definition arises when one attempts to |
94 prove formally the substitution lemma \cite{Barendregt81} by induction |
94 prove formally, for example, the substitution lemma \cite{Barendregt81} by induction |
95 ove the structure of terms. This can be fiendishly complicated (see |
95 over the structure of terms. This can be fiendishly complicated (see |
96 \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof |
96 \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof |
97 about ``raw'' lambda-terms). In contrast, if we reason about |
97 about ``raw'' lambda-terms). In contrast, if we reason about |
98 $\alpha$-equated lambda-terms, that means terms quotient according to |
98 $\alpha$-equated lambda-terms, that means terms quotient according to |
99 $\alpha$-equivalence, then the reasoning infrastructure provided by, |
99 $\alpha$-equivalence, then the reasoning infrastructure provided by, |
100 for example, Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal |
100 for example, Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal |
101 proof of the substitution lemma almost trivial. |
101 proof of the substitution lemma almost trivial. |
102 |
102 |
103 The difficulty is that in order to be able to reason about integers, finite |
103 The difficulty is that in order to be able to reason about integers, finite |
104 sets or $\alpha$-equated lambda-terms one needs to establish a reasoning |
104 sets or $\alpha$-equated lambda-terms one needs to establish a reasoning |
105 infrastructure by transferring, or \emph{lifting}, definitions and theorems |
105 infrastructure by transferring, or \emph{lifting}, definitions and theorems |
106 from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int} |
106 from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int} |
107 (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting |
107 (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting |
108 usually requires a \emph{lot} of tedious reasoning effort. |
108 usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}. |
|
109 It is feasible to to this work manually if one has only a few quotient |
|
110 constructions, but if they have to be done over and over again as in |
|
111 Nominal Isabelle, then manual reasoning is not an option. |
109 |
112 |
110 The purpose of a \emph{quotient package} is to ease the lifting and automate |
113 The purpose of a \emph{quotient package} is to ease the lifting and automate |
111 the reasoning as much as possible. In the context of HOL, there have been |
114 the reasoning as much as possible. In the context of HOL, there have been |
112 several quotient packages (...). The most notable is the one by Homeier |
115 a few quotient packages already \cite{harrison-thesis,Slotosch97}. The |
113 (...) implemented in HOL4. The fundamental construction the quotient |
116 most notable is the one by Homeier \cite{Homeier05} implemented in HOL4. |
114 package performs can be illustrated by the following picture: |
117 The fundamental construction these quotient packages perform can be |
|
118 illustrated by the following picture: |
115 |
119 |
116 \begin{center} |
120 \begin{center} |
117 \mbox{}\hspace{20mm}\begin{tikzpicture} |
121 \mbox{}\hspace{20mm}\begin{tikzpicture} |
118 %%\draw[step=2mm] (-4,-1) grid (4,1); |
122 %%\draw[step=2mm] (-4,-1) grid (4,1); |
119 |
123 |
139 \end{center} |
143 \end{center} |
140 |
144 |
141 \noindent |
145 \noindent |
142 The starting point is an existing type over which a user-given equivalence |
146 The starting point is an existing type over which a user-given equivalence |
143 relation is defined. With this input, the package introduces a new type, |
147 relation is defined. With this input, the package introduces a new type, |
144 which comes with two associated abstraction and representation functions, |
148 which comes with two associated abstraction and representation functions, written |
145 @{text Abs} and @{text Rep}, that relate elements in the existing and new |
149 @{text Abs} and @{text Rep}. They relate elements in the existing and new |
146 type. These two function represent an isomorphism between the non-empty |
150 type and can be uniquely identified by their type (which however we omit for |
147 subset and the new type. |
151 better readability). These two function represent an isomorphism between |
148 |
152 the non-empty subset and the new type. They are necessary making definitions |
149 The abstractions and representation functions are important for defining |
153 over the new type. For example @{text "0"} and @{text "1"} |
150 concepts involving the new type. For example @{text "0"} and @{text "1"} |
|
151 of type @{typ int} can be defined as |
154 of type @{typ int} can be defined as |
152 |
155 |
153 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
156 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
154 @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"} |
157 @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"} |
155 \end{isabelle} |
158 \end{isabelle} |
156 |
159 |
157 \noindent |
160 \noindent |
158 Slightly more complicated is the definition of @{text "add"} with type |
161 Slightly more complicated is the definition of @{text "add"} which has type |
159 @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition looks as follows |
162 @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows |
160 |
163 |
161 @{text [display, indent=10] "add x y \<equiv> Abs (add\<^bsub>nat\<times>nat\<^esub> (Rep x) (Rep y))"} |
164 @{text [display, indent=10] "add n m \<equiv> Abs (add\<^bsub>nat\<times>nat\<^esub> (Rep n) (Rep m))"} |
162 |
165 |
163 \noindent |
166 \noindent |
164 where we have to take first the representation of @{text x} and @{text y}, |
167 where we have to take first the representation of @{text n} and @{text m}, |
165 add them according to @{text "add\<^bsub>nat\<times>nat\<^esub>"} and then take the |
168 add them according to @{text "add\<^bsub>nat\<times>nat\<^esub>"} and then take the |
166 abstraction of the result. This is all straightforward and the existing |
169 abstraction of the result. This is all straightforward and the existing |
167 quotient packages can deal with such definitions. But what is surprising |
170 quotient packages can deal with such definitions. But what is surprising |
168 that none of them can deal with more complicated definitions involving |
171 that none of them can deal with more complicated definitions involving |
169 \emph{compositions} of quotients. Such compositions are needed for example |
172 \emph{compositions} of quotients. Such compositions are needed for example |
170 when quotienting finite lists (@{text "\<alpha> list"}) to yield finite sets |
173 in case of finite sets. There one would like to have a corresponding definition |
171 (@{text "\<alpha> fset"}). There one would like to have a corresponding definition |
174 for finite sets for the operator @{term "concat"} defined over lists. This |
172 for the operator @{term "concat"}, which flattens lists of lists as follows |
175 operator flattens lists of lists as follows |
173 |
176 |
174 @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]} |
177 @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]} |
175 |
178 |
176 \noindent |
179 \noindent |
177 We expect that the corresponding operator on finite sets, written @{term "fconcat"}, |
180 We expect that the corresponding operator on finite sets, written @{term "fconcat"}, |