155 then @{thm (concl) fun_quotient[no_vars]} |
156 then @{thm (concl) fun_quotient[no_vars]} |
156 \end{lemma} |
157 \end{lemma} |
157 |
158 |
158 *} |
159 *} |
159 |
160 |
|
161 subsection {* Higher Order Logic *} |
|
162 |
|
163 text {* |
|
164 |
|
165 Types: |
|
166 \begin{eqnarray}\nonumber |
|
167 @{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber |
|
168 @{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)} |
|
169 \end{eqnarray} |
|
170 |
|
171 Terms: |
|
172 \begin{eqnarray}\nonumber |
|
173 @{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber |
|
174 @{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber |
|
175 @{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber |
|
176 @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber |
|
177 \end{eqnarray} |
|
178 |
|
179 *} |
|
180 |
160 section {* Constants *} |
181 section {* Constants *} |
161 |
182 |
162 (* Say more about containers? *) |
183 (* Say more about containers? *) |
163 |
184 |
164 text {* |
185 text {* |
171 This operation will also be used in translations of theorem statements |
192 This operation will also be used in translations of theorem statements |
172 and in the lifting procedure. |
193 and in the lifting procedure. |
173 |
194 |
174 The operation is additionally able to descend into types for which |
195 The operation is additionally able to descend into types for which |
175 maps are known. Such maps for most common types (list, pair, sum, |
196 maps are known. Such maps for most common types (list, pair, sum, |
176 option, \ldots) are described in Homeier, and our algorithm uses the |
197 option, \ldots) are described in Homeier, and we assume that @{text "map"} |
177 same kind of maps. Given the raw compound type and the quotient compound |
198 is the function that returns a map for a given type. Then REP/ABS is defined |
178 type the Rep/Abs algorithm does: |
199 as follows: |
179 |
200 |
180 \begin{itemize} |
201 \begin{itemize} |
181 \item For equal types or free type variables return identity. |
202 \item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"} |
182 |
203 \item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"} |
183 \item For function types recurse, change the Rep/Abs flag to |
204 \item @{text "ABS(\<sigma>, \<sigma>)"} = @{text "id"} |
184 the opposite one for the domain type and compose the |
205 \item @{text "REP(\<sigma>, \<sigma>)"} = @{text "id"} |
185 results with @{term "fun_map"}. |
206 \item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"} = @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"} |
186 |
207 \item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"} = @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"} |
187 \item For equal type constructors use the appropriate map function |
208 \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"} |
188 applied to the results for the arguments. |
209 \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"} |
189 |
210 \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"} |
190 \item For unequal type constructors, look in the quotients information |
211 \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"} |
191 for a quotient type that matches the type constructor, and instantiate |
|
192 the raw type |
|
193 appropriately getting back an instantiation environment. We apply |
|
194 the environment to the arguments and recurse composing it with the |
|
195 aggregate map function. |
|
196 \end{itemize} |
212 \end{itemize} |
197 |
213 |
198 The first three points above are identical to the algorithm present in |
214 Apart from the last 2 points the definition is same as the one implemented in |
199 in Homeier's HOL implementation, below is the definition of @{term fconcat} |
215 in Homeier's HOL package, below is the definition of @{term fconcat} |
200 that shows the last step: |
216 that shows the last points: |
201 |
217 |
202 @{thm fconcat_def[no_vars]} |
218 @{thm fconcat_def[no_vars]} |
203 |
219 |
204 The aggregate @{term Abs} function takes a finite set of finite sets |
220 The aggregate @{term Abs} function takes a finite set of finite sets |
205 and applies @{term "map rep_fset"} composed with @{term rep_fset} to |
221 and applies @{term "map rep_fset"} composed with @{term rep_fset} to |