56 over a simply-typed term-language. Safe reasoning in HOL is ensured by two |
56 over a simply-typed term-language. Safe reasoning in HOL is ensured by two |
57 very restricted mechanisms for extending the logic: one is the definition of |
57 very restricted mechanisms for extending the logic: one is the definition of |
58 new constants in terms of existing ones; the other is the introduction of |
58 new constants in terms of existing ones; the other is the introduction of |
59 new types by identifying non-empty subsets in existing types. It is well |
59 new types by identifying non-empty subsets in existing types. It is well |
60 understood to use both mechanisms for dealing with quotient constructions in |
60 understood to use both mechanisms for dealing with quotient constructions in |
61 HOL (see for example \cite{Homeier05,Paulson06}). For example the integers |
61 HOL (see \cite{Homeier05,Paulson06}). For example the integers |
62 in Isabelle/HOL are constructed by a quotient construction over the type |
62 in Isabelle/HOL are constructed by a quotient construction over the type |
63 @{typ "nat \<times> nat"} and the equivalence relation |
63 @{typ "nat \<times> nat"} and the equivalence relation |
64 |
64 |
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"} |
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 |
66 |
67 \noindent |
67 \noindent |
68 This produces the type @{typ int} and definitions for @{text "0::int"} and |
68 This constructions yields the type @{typ int} and definitions for @{text |
69 @{text "1::int"} in terms of pairs of natural numbers can be given (namely |
69 "0::int"} and @{text "1::int"} in terms of pairs of natural numbers can be |
70 @{text "(0, 0)"} and @{text "(1, 0)"}). Operations such as @{text "add::int |
70 given (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations such as |
71 \<Rightarrow> int \<Rightarrow> int"} can be defined in terms of operations on pairs of natural |
71 @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in terms of operations on |
72 numbers. Similarly one can construct the type of finite sets by quotienting |
72 pairs of natural numbers (namely @{text "add\<^bsub>nat\<times>nat\<^esub> |
73 lists according to the equivalence relation |
73 (x\<^isub>1, y\<^isub>1) (x\<^isub>2, y\<^isub>2) \<equiv> (x\<^isub>1 + |
|
74 x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}). Similarly one can construct the |
|
75 type of finite sets by quotienting lists according to the equivalence |
|
76 relation |
74 |
77 |
75 @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} |
78 @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} |
76 |
79 |
77 \noindent |
80 \noindent |
78 which means two lists are equivalent if every element in one list is also |
81 which states that 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). |
82 member in the other (@{text "\<in>"} stands here for membership in lists). |
80 |
83 |
81 The problem is that in order to start reasoning about, for example integers, |
84 The problem is that in order to be able to reason about integers and |
82 definitions and theorems need to be transferred, or \emph{lifted}, |
85 finite sets, one needs to establish a reasoning infrastructure by |
83 from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}. |
86 transferring, or \emph{lifting}, definitions and theorems from the ``raw'' |
84 This lifting usually requires a lot of tedious reasoning effort. |
87 type @{typ "nat \<times> nat"} to the quotient type @{typ int} (similarly for |
85 The purpose of a \emph{quotient package} is to ease the lifting and automate |
88 @{text "\<alpha> list"} and finite sets of type @{text "\<alpha>"}). This lifting usually |
86 the reasoning involved as much as possible. Such a package is a central |
89 requires a \emph{lot} of tedious reasoning effort. The purpose of a \emph{quotient |
87 component of the new version of Nominal Isabelle where representations |
90 package} is to ease the lifting and automate the reasoning as much as |
88 of alpha-equated terms are constructed according to specifications given by |
91 possible. While for integers and finite sets teh tedious reasoning needs |
89 the user. |
92 to be done only once, Nominal Isabelle providing a reasoning infrastructure |
|
93 for binders and @{text "\<alpha>"}-equated terms it needs to be done over and over |
|
94 again. |
|
95 |
|
96 Such a package is a central component of the new version of |
|
97 Nominal Isabelle where representations of alpha-equated terms are |
|
98 constructed according to specifications given by the user. |
|
99 |
90 |
100 |
91 In the context of HOL, there have been several quotient packages (...). The |
101 In the context of HOL, there have been several quotient packages (...). The |
92 most notable is the one by Homeier (...) implemented in HOL4. However, what is |
102 most notable is the one by Homeier (...) implemented in HOL4. However, what is |
93 surprising, none of them can deal compositions of quotients, for example with |
103 surprising, none of them can deal compositions of quotients, for example with |
94 lifting theorems about @{text "concat"}: |
104 lifting theorems about @{text "concat"}: |