285 

   286 %%%TODO Update the contents.

   919 %%% TODO: This introduction is same as the introduction to the previous section.

   920 

  1164 section {* Derivation of the shape of lifted and raw theorems\label{sec:descending} *}

  1165 

  1166 text {*

  1167   In the previous sections we have assumed, that the user specifies

  1168   both the raw theorem and the statement of the quotient one.

  1169   This allows complete flexibility, as to which parts of the statement

  1170   are lifted to the quotient level and which are intact. In

  1171   other implementations of automatic quotients (for example Homeier's

  1172   package) only the raw theorem is given to the quotient package and

  1173   the package is able to guess the quotient one. In this

  1174   section we give examples where there are multiple possible valid lifted

  1175   theorems starting from a raw one. We also show a heuristic for

  1176   computing the quotient theorem from a raw one, and a mechanism for

  1177   guessing a raw theorem starting with a quotient one.

  1178 *}

  1179 

  1180 subsection {* Multiple lifted theorems *}

  1181 

  1182 text {*

  1183   There are multiple reasons why multiple valid lifted theorems can arize.

  1184   Below we describe three possible scenarios: multiple raw variable,

  1185   multiple quotients for the same raw type and multiple quotients.

  1186 

  1187   Given a raw theorem there are often several variables that include

  1188   a raw type. It this case, one can choose which of the variables to

  1189   lift. In certain cases this can lead to a number of valid theorem

  1190   statements, however type constraints may disallow certain combinations.

  1191   Lets see an example where multiple variables can have different types.

  1192   The Isabelle/HOL induction principle for two lists is:

  1193   \begin{isabelle}\ \ \ \ \ %%%

  1194   @{thm list_induct2'}

  1195   \end{isabelle}

  1196 

  1197   the conclusion is a predicate of the form @{text "P xs ys"}, where

  1198   the two variables are lists. When lifting such theorem to the quotient

  1199   type one can choose if one want to quotient @{text "xs"} or @{text "ys"}, or

  1200   both. All these give rise to valid quotiented theorems, however the

  1201   automatic mode (or other quotient packages) would derive only the version

  1202   with both being quotiented, namely:

  1203   \begin{isabelle}\ \ \ \ \ %%%

  1204   @{thm list_induct2'[quot_lifted]}

  1205   \end{isabelle}

  1206 

  1207   A second scenario, where multiple possible quotient theorems arise is

  1208   when a single raw type is used in two quotients. Consider three quotients

  1209   of the list type: finite sets, finite multisets and lists with distinct

  1210   elements. We have developed all three types with the help of the quotient

  1211   package. Given a theorem that talks about lists --- for example the regular

  1212   induction principle --- one can lift it to three possible theorems: the

  1213   induction principle for finite sets, induction principle for finite

  1214   multisets or the induction principle for distinct lists. Again given an

  1215   induction principle for two lists this gives rise to 15 possible valid

  1216   lifted theorems.

  1217 

  1218   In our developments using the quotient package we also encountered a

  1219   scenario where multiple valid theorem statements arise, but the raw

  1220   types are not identical. Consider the type of lambda terms, where the

  1221   variables are indexed with strings. Quotienting lambda terms by alpha

  1222   equivalence gives rise to a Nominal construction~\cite{Nominal}. However

  1223   at the same time the type of strings being a list of characters can

  1224   lift to theorems about finite sets of characters.

  1225 *}

  1226 

  1227 subsection {* Derivation of the shape of theorems *}

  1228 

  1229 text {*

  1230   To derive a the shape of a lifted or raw theorem the quotient package

  1231   first builds a type and term substitution.

  1232 

  1233   The list of type substitution is created by taking the pairs

  1234   @{text "(raw_type, quotient_type)"} for every user defined quotient.

  1235   The term substitutions are of two types: First for every user-defined

  1236   quotient constant, the pair @{text "(raw_term, quotient_constant)"}

  1237   is included in the substitution. Second, for every quotient relation

  1238   @{text "\<approx>"} the pair @{text "(\<approx>, =)"} with the equality being the

  1239   equality on the defined quotient type is included in the substitution.

  1240 

  1241   The derivation function next traverses the theorem statement expressed

  1242   as a term and replaces the types of all free variables and of all

  1243   lambda-abstractions using the type substitution. For every constant

  1244   is not matched by the term substitution and we perform the type substitution

  1245   on the type of the constant (this is necessary for quotienting theorems

  1246   with polymorphic constants) or the type of the substitution is matched

  1247   and the match is returned.

  1248 

  1249   The heuristic defined above is greedy and according to our experience

  1250   this is what the user wants. The procedure may in some cases produce

  1251   theorem statements that do not type-check. However verifying all

  1252   possible theorem statements is too costly in general.

  1253 *}

  1254 

  1255 subsection {* Interaction modes and derivation of the the shape of theorems *}

  1256 

  1257 text {*

  1258   In the quotient package we provide three interaction modes, that use

  1259   can the procedure procedure defined in the previous subsection.

  1260 

  1261   First, the completely manual mode which we implemented as the

  1262   Isabelle method @{text lifting}. In this mode the user first

  1263   proves the raw theorem. Then the lifted theorem can be proved

  1264   by the method lifting, that takes the reference to the raw theorem

  1265   (or theorem list) as an argument. Such completely manual mode is

  1266   necessary for theorems where the specification of the lifted theorem

  1267   from the raw one is not unique, which we discussed in the previous

  1268   subsection.

  1269 

  1270   Next, we provide a mode for automatically lifting a given

  1271   raw theorem. We implemented this mode as an isabelle attribute,

  1272   so given the raw theorem @{text thm}, the user can refer to the

  1273   theorem @{text "thm[quot_lifted]"}.

  1274 

  1275   Finally we provie a method for translating a given quotient

  1276   level theorem to a raw one. We implemented this as an Isabelle

  1277   method @{text descending}. The user starts with expressing a

  1278   quotient level theorem statement and applies this method.

  1279   The quotient package derives a raw level statement and assumes

  1280   it as a subgoal. Given that this subgoal is proved, the quotient

  1281   package can lift the raw theorem fulfilling the proof of the

  1282   original lifted theorem statement. 

  1283 *}

  1284