79 predicate or set @{text R} that is consistent with given rules: |
79 predicate or set @{text R} that is consistent with given rules: |
80 every element of @{text R} can be seen as arising by applying a rule |
80 every element of @{text R} can be seen as arising by applying a rule |
81 to elements of @{text R}. An important example is using |
81 to elements of @{text R}. An important example is using |
82 bisimulation relations to formalise equivalence of processes and |
82 bisimulation relations to formalise equivalence of processes and |
83 infinite data structures. |
83 infinite data structures. |
84 |
84 |
85 Both inductive and coinductive definitions are based on the |
85 Both inductive and coinductive definitions are based on the |
86 Knaster-Tarski fixed-point theorem for complete lattices. The |
86 Knaster-Tarski fixed-point theorem for complete lattices. The |
87 collection of introduction rules given by the user determines a |
87 collection of introduction rules given by the user determines a |
88 functor on subsets of set-theoretic relations. The required |
88 functor on subsets of set-theoretic relations. The required |
89 monotonicity of the recursion scheme is proven as a prerequisite to |
89 monotonicity of the recursion scheme is proven as a prerequisite to |
1336 'is' @{syntax term}; |
1338 'is' @{syntax term}; |
1337 "} |
1339 "} |
1338 |
1340 |
1339 \begin{description} |
1341 \begin{description} |
1340 |
1342 |
1341 \item @{command (HOL) "setup_lifting"} Sets up the Lifting package to work with |
1343 \item @{command (HOL) "setup_lifting"} Sets up the Lifting package |
1342 a user-defined type. The user must provide either a quotient |
1344 to work with a user-defined type. The user must provide either a |
1343 theorem @{text "Quotient R Abs Rep T"} or a type_definition theorem |
1345 quotient theorem @{text "Quotient R Abs Rep T"} or a |
1344 @{text "type_definition Rep Abs A"}. |
1346 type_definition theorem @{text "type_definition Rep Abs A"}. The |
1345 The package configures |
1347 package configures transfer rules for equality and quantifiers on |
1346 transfer rules for equality and quantifiers on the type, and sets |
1348 the type, and sets up the @{command_def (HOL) "lift_definition"} |
1347 up the @{command_def (HOL) "lift_definition"} command to work with the type. |
1349 command to work with the type. In the case of a quotient theorem, |
1348 In the case of a quotient theorem, |
1350 an optional theorem @{text "reflp R"} can be provided as a second |
1349 an optional theorem @{text "reflp R"} can be provided as a second argument. |
1351 argument. This allows the package to generate stronger transfer |
1350 This allows the package to generate stronger transfer rules. |
1352 rules. |
1351 |
1353 |
1352 @{command (HOL) "setup_lifting"} is called automatically if a quotient type |
1354 @{command (HOL) "setup_lifting"} is called automatically if a |
1353 is defined by the command @{command (HOL) "quotient_type"} from the Quotient package. |
1355 quotient type is defined by the command @{command (HOL) |
1354 |
1356 "quotient_type"} from the Quotient package. |
1355 If @{command (HOL) "setup_lifting"} is called with a type_definition theorem, |
1357 |
1356 the abstract type implicitly defined by the theorem is declared as an abstract type in |
1358 If @{command (HOL) "setup_lifting"} is called with a |
1357 the code generator. This allows @{command (HOL) "lift_definition"} to register |
1359 type_definition theorem, the abstract type implicitly defined by |
1358 (generated) code certificate theorems as abstract code equations in the code generator. |
1360 the theorem is declared as an abstract type in the code |
1359 The option @{text "no_abs_code"} of the command @{command (HOL) "setup_lifting"} |
1361 generator. This allows @{command (HOL) "lift_definition"} to |
1360 can turn off that behavior and causes that code certificate theorems generated |
1362 register (generated) code certificate theorems as abstract code |
1361 by @{command (HOL) "lift_definition"} are not registred as abstract code equations. |
1363 equations in the code generator. The option @{text "no_abs_code"} |
1362 |
1364 of the command @{command (HOL) "setup_lifting"} can turn off that |
1363 \item @{command (HOL) "lift_definition"} @{text "f :: \<tau> is t"} |
1365 behavior and causes that code certificate theorems generated by |
1364 Defines a new function @{text f} with an abstract type @{text \<tau>} in |
1366 @{command (HOL) "lift_definition"} are not registred as abstract |
1365 terms of a corresponding operation @{text t} on a representation type. |
1367 code equations. |
1366 The term @{text t} doesn't have to be necessarily a constant but it can |
1368 |
1367 be any term. |
1369 \item @{command (HOL) "lift_definition"} @{text "f :: \<tau> is t"} |
|
1370 Defines a new function @{text f} with an abstract type @{text \<tau>} |
|
1371 in terms of a corresponding operation @{text t} on a |
|
1372 representation type. The term @{text t} doesn't have to be |
|
1373 necessarily a constant but it can be any term. |
1368 |
1374 |
1369 Users must discharge a respectfulness proof obligation when each |
1375 Users must discharge a respectfulness proof obligation when each |
1370 constant is defined. For a type copy, i.e. a typedef with @{text UNIV}, |
1376 constant is defined. For a type copy, i.e. a typedef with @{text |
1371 the proof is discharged automatically. The obligation is |
1377 UNIV}, the proof is discharged automatically. The obligation is |
1372 presented in a user-friendly, readable form. A respectfulness |
1378 presented in a user-friendly, readable form. A respectfulness |
1373 theorem in the standard format @{text f.rsp} and a transfer rule @{text f.tranfer} |
1379 theorem in the standard format @{text f.rsp} and a transfer rule |
1374 for the Transfer package are generated by the package. |
1380 @{text f.tranfer} for the Transfer package are generated by the |
|
1381 package. |
1375 |
1382 |
1376 Integration with code_abstype: For typedefs (e.g. subtypes |
1383 Integration with code_abstype: For typedefs (e.g. subtypes |
1377 corresponding to a datatype invariant, such as dlist), |
1384 corresponding to a datatype invariant, such as dlist), @{command |
1378 @{command (HOL) "lift_definition"} |
1385 (HOL) "lift_definition"} generates a code certificate theorem |
1379 generates a code certificate theorem @{text f.rep_eq} and sets up |
1386 @{text f.rep_eq} and sets up code generation for each constant. |
1380 code generation for each constant. |
|
1381 |
1387 |
1382 \item @{command (HOL) "print_quotmaps"} prints stored quotient map |
1388 \item @{command (HOL) "print_quotmaps"} prints stored quotient map |
1383 theorems. |
1389 theorems. |
1384 |
1390 |
1385 \item @{command (HOL) "print_quotients"} prints stored quotient theorems. |
1391 \item @{command (HOL) "print_quotients"} prints stored quotient |
1386 |
1392 theorems. |
1387 \item @{attribute (HOL) quot_map} registers a quotient map theorem. For examples see |
1393 |
1388 @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy files. |
1394 \item @{attribute (HOL) quot_map} registers a quotient map |
1389 |
1395 theorem. For examples see @{file |
1390 \item @{attribute (HOL) invariant_commute} registers a theorem which shows a relationship |
1396 "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy |
1391 between the constant @{text Lifting.invariant} (used for internal encoding of proper subtypes) |
1397 files. |
1392 and a relator. |
1398 |
1393 Such theorems allows the package to hide @{text Lifting.invariant} from a user |
1399 \item @{attribute (HOL) invariant_commute} registers a theorem which |
1394 in a user-readable form of a respectfulness theorem. For examples see |
1400 shows a relationship between the constant @{text |
1395 @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy files. |
1401 Lifting.invariant} (used for internal encoding of proper subtypes) |
1396 |
1402 and a relator. Such theorems allows the package to hide @{text |
1397 |
1403 Lifting.invariant} from a user in a user-readable form of a |
1398 \end{description} |
1404 respectfulness theorem. For examples see @{file |
1399 |
1405 "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy |
1400 *} |
1406 files. |
|
1407 |
|
1408 \end{description} |
|
1409 *} |
|
1410 |
1401 |
1411 |
1402 section {* Quotient types *} |
1412 section {* Quotient types *} |
1403 |
1413 |
1404 text {* |
1414 text {* |
1405 \begin{matharray}{rcl} |
1415 \begin{matharray}{rcl} |
1887 |
1897 |
1888 \item[@{text locale}] specifies how to process conjectures in |
1898 \item[@{text locale}] specifies how to process conjectures in |
1889 a locale context, i.e., they can be interpreted or expanded. |
1899 a locale context, i.e., they can be interpreted or expanded. |
1890 The option is a whitespace-separated list of the two words |
1900 The option is a whitespace-separated list of the two words |
1891 @{text interpret} and @{text expand}. The list determines the |
1901 @{text interpret} and @{text expand}. The list determines the |
1892 order they are employed. The default setting is to first use |
1902 order they are employed. The default setting is to first use |
1893 interpretations and then test the expanded conjecture. |
1903 interpretations and then test the expanded conjecture. |
1894 The option is only provided as attribute declaration, but not |
1904 The option is only provided as attribute declaration, but not |
1895 as parameter to the command. |
1905 as parameter to the command. |
1896 |
1906 |
1897 \item[@{text timeout}] sets the time limit in seconds. |
1907 \item[@{text timeout}] sets the time limit in seconds. |
1898 |
1908 |
1899 \item[@{text default_type}] sets the type(s) generally used to |
1909 \item[@{text default_type}] sets the type(s) generally used to |
1900 instantiate type variables. |
1910 instantiate type variables. |
2285 |
2295 |
2286 \item @{command (HOL) "code_reflect"} without a ``@{text "file"}'' |
2296 \item @{command (HOL) "code_reflect"} without a ``@{text "file"}'' |
2287 argument compiles code into the system runtime environment and |
2297 argument compiles code into the system runtime environment and |
2288 modifies the code generator setup that future invocations of system |
2298 modifies the code generator setup that future invocations of system |
2289 runtime code generation referring to one of the ``@{text |
2299 runtime code generation referring to one of the ``@{text |
2290 "datatypes"}'' or ``@{text "functions"}'' entities use these precompiled |
2300 "datatypes"}'' or ``@{text "functions"}'' entities use these |
2291 entities. With a ``@{text "file"}'' argument, the corresponding code |
2301 precompiled entities. With a ``@{text "file"}'' argument, the |
2292 is generated into that specified file without modifying the code |
2302 corresponding code is generated into that specified file without |
2293 generator setup. |
2303 modifying the code generator setup. |
2294 |
2304 |
2295 \item @{command (HOL) "code_pred"} creates code equations for a predicate |
2305 \item @{command (HOL) "code_pred"} creates code equations for a |
2296 given a set of introduction rules. Optional mode annotations determine |
2306 predicate given a set of introduction rules. Optional mode |
2297 which arguments are supposed to be input or output. If alternative |
2307 annotations determine which arguments are supposed to be input or |
2298 introduction rules are declared, one must prove a corresponding elimination |
2308 output. If alternative introduction rules are declared, one must |
2299 rule. |
2309 prove a corresponding elimination rule. |
2300 |
2310 |
2301 \end{description} |
2311 \end{description} |
2302 *} |
2312 *} |
2303 |
2313 |
2304 |
2314 |