1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "Quotient" |
3 imports "Quotient" |
4 "LaTeXsugar" |
4 "LaTeXsugar" |
5 begin |
5 begin |
6 |
6 |
7 notation (latex output) |
7 notation (latex output) |
|
8 rel_conj ("_ OOO _" [53, 53] 52) |
|
9 and |
|
10 fun_map ("_ ---> _" [51, 51] 50) |
|
11 and |
8 fun_rel ("_ ===> _" [51, 51] 50) |
12 fun_rel ("_ ===> _" [51, 51] 50) |
9 |
13 |
|
14 ML {* |
|
15 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; |
|
16 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
|
17 let |
|
18 val concl = |
|
19 Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t) |
|
20 in |
|
21 case concl of (_ $ l $ r) => proj (l, r) |
|
22 | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl) |
|
23 end); |
|
24 *} |
|
25 setup {* |
|
26 Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #> |
|
27 Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #> |
|
28 Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2)) |
|
29 *} |
10 (*>*) |
30 (*>*) |
11 |
31 |
12 section {* Introduction *} |
32 section {* Introduction *} |
13 |
33 |
14 text {* |
34 text {* |
24 in terms of existing ones; the other is the introduction of new types |
44 in terms of existing ones; the other is the introduction of new types |
25 by identifying non-empty subsets in existing types. It is well understood |
45 by identifying non-empty subsets in existing types. It is well understood |
26 to use both mechanism for dealing with quotient constructions in HOL (cite Larry). |
46 to use both mechanism for dealing with quotient constructions in HOL (cite Larry). |
27 For example the integers in Isabelle/HOL are constructed by a quotient construction over |
47 For example the integers in Isabelle/HOL are constructed by a quotient construction over |
28 the type @{typ "nat \<times> nat"} and the equivalence relation |
48 the type @{typ "nat \<times> nat"} and the equivalence relation |
|
49 |
|
50 % I would avoid substraction for natural numbers. |
29 |
51 |
30 @{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"} |
52 @{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"} |
31 |
53 |
32 \noindent |
54 \noindent |
33 Similarly one can construct the type of finite sets by quotienting lists |
55 Similarly one can construct the type of finite sets by quotienting lists |
51 In the context of HOL, there have been several quotient packages (...). The |
73 In the context of HOL, there have been several quotient packages (...). The |
52 most notable is the one by Homeier (...) implemented in HOL4. However, what is |
74 most notable is the one by Homeier (...) implemented in HOL4. However, what is |
53 surprising, none of them can deal compositions of quotients, for example with |
75 surprising, none of them can deal compositions of quotients, for example with |
54 lifting theorems about @{text "concat"}: |
76 lifting theorems about @{text "concat"}: |
55 |
77 |
56 @{text [display] "concat definition"} |
78 @{thm concat.simps(1)}\\ |
57 |
79 @{thm concat.simps(2)[no_vars]} |
|
80 |
58 \noindent |
81 \noindent |
59 One would like to lift this definition to the operation |
82 One would like to lift this definition to the operation |
60 |
83 |
61 @{text [display] "union definition"} |
84 @{text [display] "union definition"} |
62 |
85 |
82 composition. |
105 composition. |
83 |
106 |
84 \item We allow lifting only some occurrences of quotiented |
107 \item We allow lifting only some occurrences of quotiented |
85 types. Rsp/Prs extended. (used in nominal) |
108 types. Rsp/Prs extended. (used in nominal) |
86 |
109 |
87 \item We regularize more thanks to new lemmas. (inductions in |
|
88 nominal). |
|
89 |
|
90 \item The quotient package is very modular. Definitions can be added |
110 \item The quotient package is very modular. Definitions can be added |
91 separately, rsp and prs can be proved separately and theorems can |
111 separately, rsp and prs can be proved separately and theorems can |
92 be lifted on a need basis. (useful with type-classes). |
112 be lifted on a need basis. (useful with type-classes). |
93 |
113 |
94 \item Can be used both manually (attribute, separate tactics, |
114 \item Can be used both manually (attribute, separate tactics, |
95 rsp/prs databases) and programatically (automated definition of |
115 rsp/prs databases) and programatically (automated definition of |
96 lifted constants, the rsp proof obligations and theorem statement |
116 lifted constants, the rsp proof obligations and theorem statement |
97 translation according to given quotients). |
117 translation according to given quotients). |
99 \end{itemize} |
119 \end{itemize} |
100 *} |
120 *} |
101 |
121 |
102 section {* Quotient Type*} |
122 section {* Quotient Type*} |
103 |
123 |
104 text {* |
124 |
105 Defintion of quotient, |
125 |
106 |
126 text {* |
107 Equivalence, |
127 In this section we present the definitions of a quotient that follow |
108 |
128 those by Homeier, the proofs can be found there. |
109 Relation map and function map |
129 |
|
130 \begin{definition}[Quotient] |
|
131 A relation $R$ with an abstraction function $Abs$ |
|
132 and a representation function $Rep$ is a \emph{quotient} |
|
133 if and only if: |
|
134 |
|
135 \begin{enumerate} |
|
136 \item @{thm (rhs1) Quotient_def[of "R", no_vars]} |
|
137 \item @{thm (rhs2) Quotient_def[of "R", no_vars]} |
|
138 \item @{thm (rhs3) Quotient_def[of "R", no_vars]} |
|
139 \end{enumerate} |
|
140 |
|
141 \end{definition} |
|
142 |
|
143 \begin{definition}[Relation map and function map] |
|
144 @{thm fun_rel_def[no_vars]}\\ |
|
145 @{thm fun_map_def[no_vars]} |
|
146 \end{definition} |
|
147 |
|
148 The main theorems for building higher order quotients is: |
|
149 \begin{lemma}[Function Quotient] |
|
150 If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]} |
|
151 then @{thm (concl) fun_quotient[no_vars]} |
|
152 \end{lemma} |
|
153 |
110 *} |
154 *} |
111 |
155 |
112 section {* Constants *} |
156 section {* Constants *} |
113 |
157 |
114 text {* |
158 (* Describe what containers are? *) |
115 Rep and Abs, Rsp and Prs |
159 |
|
160 text {* |
|
161 \begin{definition}[Composition of Relations] |
|
162 @{abbrev "rel_conj R1 R2"} |
|
163 \end{definition} |
|
164 |
|
165 The first operation that we describe is the generation of |
|
166 aggregate Abs or Rep function for two given compound types. |
|
167 This operation will be used for the constant defnitions |
|
168 and for the translation of theorems statements. It relies on |
|
169 knowing map functions and relation functions for container types. |
|
170 It follows the following algorithm: |
|
171 |
|
172 \begin{itemize} |
|
173 \item For equal types or free type variables return identity. |
|
174 |
|
175 \item For function types recurse, change the Rep/Abs flag to |
|
176 the opposite one for the domain type and compose the |
|
177 results with @{term "fun_map"}. |
|
178 |
|
179 \item For equal type constructors use the appropriate map function |
|
180 applied to the results for the arguments. |
|
181 |
|
182 \item For unequal type constructors are unequal, we look in the |
|
183 quotients information for a raw type quotient type pair that |
|
184 matches the given types. We apply the environment to the arguments |
|
185 and recurse composing it with the aggregate map function. |
|
186 \end{itemize} |
|
187 |
|
188 |
|
189 |
|
190 Rsp and Prs |
116 *} |
191 *} |
117 |
192 |
118 section {* Lifting Theorems *} |
193 section {* Lifting Theorems *} |
119 |
194 |
120 text {* TBD *} |
195 text {* TBD *} |