48 |
48 |
49 section {* Introduction *} |
49 section {* Introduction *} |
50 |
50 |
51 text {* |
51 text {* |
52 \noindent |
52 \noindent |
53 One might think quotients have been studied to death, but in the context of |
53 One might think quotients have been studied to death, but in the |
54 theorem provers many questions concerning them are far from settled. In |
54 context of theorem provers a number questions concerning them are |
55 this paper we address the question of how to establish a convenient reasoning |
55 far from settled. In this paper we address the question of how to |
56 infrastructure |
56 establish a convenient reasoning infrastructure for quotient |
57 for quotient constructions in the Isabelle/HOL |
57 constructions in the Isabelle/HOL theorem prover. Higher-Order Logic |
58 theorem prover. Higher-Order Logic (HOL) consists |
58 (HOL) consists of a small number of axioms and inference rules over |
59 of a small number of axioms and inference rules over a simply-typed |
59 a simply-typed term-language. Safe reasoning in HOL is ensured by |
60 term-language. Safe reasoning in HOL is ensured by two very restricted |
60 two very restricted mechanisms for extending the logic: one is the |
61 mechanisms for extending the logic: one is the definition of new constants |
61 definition of new constants in terms of existing ones; the other is |
62 in terms of existing ones; the other is the introduction of new types by |
62 the introduction of new types by identifying non-empty subsets in |
63 identifying non-empty subsets in existing types. Previous work has shown how |
63 existing types. Previous work has shown how to use both mechanisms |
64 to use both mechanisms for dealing with quotient constructions in HOL (see |
64 for dealing with quotient constructions in HOL (see |
65 \cite{Homeier05,Paulson06}). For example the integers in Isabelle/HOL are |
65 \cite{Homeier05,Paulson06}). For example the integers in |
66 constructed by a quotient construction over the type @{typ "nat \<times> nat"} and |
66 Isabelle/HOL are constructed by a quotient construction over the |
67 the equivalence relation |
67 type @{typ "nat \<times> nat"} and the equivalence relation |
68 |
68 |
69 |
69 |
70 \begin{isabelle}\ \ \ \ \ %%% |
70 \begin{isabelle}\ \ \ \ \ %%% |
71 @{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}\hfill\numbered{natpairequiv} |
71 @{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}\hfill\numbered{natpairequiv} |
72 \end{isabelle} |
72 \end{isabelle} |
81 \begin{isabelle}\ \ \ \ \ %%% |
81 \begin{isabelle}\ \ \ \ \ %%% |
82 @{text "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2, m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"} |
82 @{text "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2, m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"} |
83 \end{isabelle} |
83 \end{isabelle} |
84 |
84 |
85 \noindent |
85 \noindent |
86 Similarly one can construct the type of |
86 Similarly one can construct the type of finite sets, written @{term |
87 finite sets, written @{term "\<alpha> fset"}, |
87 "\<alpha> fset"}, by quotienting the type @{text "\<alpha> list"} according to the |
88 by quotienting the type @{text "\<alpha> list"} according to the equivalence relation |
88 equivalence relation |
89 |
89 |
90 \begin{isabelle}\ \ \ \ \ %%% |
90 \begin{isabelle}\ \ \ \ \ %%% |
91 @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv} |
91 @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv} |
92 \end{isabelle} |
92 \end{isabelle} |
93 |
93 |
94 \noindent |
94 \noindent |
95 which states that two lists are equivalent if every element in one list is |
95 which states that two lists are equivalent if every element in one |
96 also member in the other. The empty finite set, written @{term "{||}"}, can |
96 list is also member in the other, and vice versa. The empty finite |
97 then be defined as the empty list and the union of two finite sets, written |
97 set, written @{term "{||}"}, can then be defined as the empty list |
98 @{text "\<union>"}, as list append. |
98 and the union of two finite sets, written @{text "\<union>"}, as list |
|
99 append. |
99 |
100 |
100 Quotients are important in a variety of areas, but they are really ubiquitous in |
101 Quotients are important in a variety of areas, but they are really ubiquitous in |
101 the area of reasoning about programming language calculi. A simple example |
102 the area of reasoning about programming language calculi. A simple example |
102 is the lambda-calculus, whose raw terms are defined as |
103 is the lambda-calculus, whose raw, or un-quotient, terms are defined as |
103 |
104 |
104 \begin{isabelle}\ \ \ \ \ %%% |
105 \begin{isabelle}\ \ \ \ \ %%% |
105 @{text "t ::= x | t t | \<lambda>x.t"}%\hfill\numbered{lambda} |
106 @{text "t ::= x | t t | \<lambda>x.t"}%\hfill\numbered{lambda} |
106 \end{isabelle} |
107 \end{isabelle} |
107 |
108 |
108 \noindent |
109 \noindent |
109 The problem with this definition arises, for instance, when one attempts to |
110 The problem with this definition arises from the need to reason |
110 prove formally the substitution lemma \cite{Barendregt81} by induction |
111 modulo $\alpha$-equivalence, for instance, when one attempts to |
111 over the structure of terms. This can be fiendishly complicated (see |
112 prove formally the substitution lemma \cite{Barendregt81} by |
112 \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof |
113 induction over the structure of terms. This can be fiendishly |
113 about raw lambda-terms). In contrast, if we reason about |
114 complicated (see \cite[Pages 94--104]{CurryFeys58} for some |
114 $\alpha$-equated lambda-terms, that means terms quotient according to |
115 ``rough'' sketches of a proof about raw lambda-terms). In contrast, |
115 $\alpha$-equivalence, then the reasoning infrastructure provided, |
116 if we reason about $\alpha$-equated lambda-terms, that means terms |
116 for example, by Nominal Isabelle %%\cite{UrbanKaliszyk11} |
117 quotient according to $\alpha$-equivalence, then the reasoning |
117 makes the formal |
118 infrastructure provided, for example, by Nominal Isabelle |
118 proof of the substitution lemma almost trivial. |
119 \cite{UrbanKaliszyk11} makes the formal proof of the substitution |
|
120 lemma almost trivial. The fundamental reason is that in case of |
|
121 $\alpha$-equated terms, equality coincides with $\alpha$-equivalence and |
|
122 we can use for reasoning HOL's built-in notion of ``replacing equals by equals''. |
119 |
123 |
120 {\bf MAYBE AN EAMPLE FOR PARTIAL QUOTIENTS?} |
124 {\bf MAYBE AN EAMPLE FOR PARTIAL QUOTIENTS?} |
121 |
125 |
122 |
126 |
123 The difficulty is that in order to be able to reason about integers, finite |
127 The difficulty is that in order to be able to reason about integers, finite |