1767 |
1767 |
1768 \noindent where \isa{t} is the type constructor, \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} are distinct |
1768 \noindent where \isa{t} is the type constructor, \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} are distinct |
1769 type variables free in the local theory and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, |
1769 type variables free in the local theory and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, |
1770 \ldots, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{22}{\isachardoublequote}}} is a subsequence of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \ldots, |
1770 \ldots, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{22}{\isachardoublequote}}} is a subsequence of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \ldots, |
1771 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}. |
1771 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}. |
|
1772 |
|
1773 \end{description}% |
|
1774 \end{isamarkuptext}% |
|
1775 \isamarkuptrue% |
|
1776 % |
|
1777 \isamarkupsection{Transfer package% |
|
1778 } |
|
1779 \isamarkuptrue% |
|
1780 % |
|
1781 \begin{isamarkuptext}% |
|
1782 \begin{matharray}{rcl} |
|
1783 \indexdef{HOL}{method}{transfer}\hypertarget{method.HOL.transfer}{\hyperlink{method.HOL.transfer}{\mbox{\isa{transfer}}}} & : & \isa{method} \\ |
|
1784 \indexdef{HOL}{method}{transfer'}\hypertarget{method.HOL.transfer'}{\hyperlink{method.HOL.transfer'}{\mbox{\isa{transfer{\isaliteral{27}{\isacharprime}}}}}} & : & \isa{method} \\ |
|
1785 \indexdef{HOL}{method}{transfer\_prover}\hypertarget{method.HOL.transfer-prover}{\hyperlink{method.HOL.transfer-prover}{\mbox{\isa{transfer{\isaliteral{5F}{\isacharunderscore}}prover}}}} & : & \isa{method} \\ |
|
1786 \indexdef{HOL}{attribute}{transfer\_rule}\hypertarget{attribute.HOL.transfer-rule}{\hyperlink{attribute.HOL.transfer-rule}{\mbox{\isa{transfer{\isaliteral{5F}{\isacharunderscore}}rule}}}} & : & \isa{attribute} \\ |
|
1787 \indexdef{HOL}{attribute}{relator\_eq}\hypertarget{attribute.HOL.relator-eq}{\hyperlink{attribute.HOL.relator-eq}{\mbox{\isa{relator{\isaliteral{5F}{\isacharunderscore}}eq}}}} & : & \isa{attribute} \\ |
|
1788 \end{matharray} |
|
1789 |
|
1790 \begin{description} |
|
1791 |
|
1792 \item \hyperlink{method.HOL.transfer}{\mbox{\isa{transfer}}} method replaces the current subgoal |
|
1793 with a logically equivalent one that uses different types and |
|
1794 constants. The replacement of types and constants is guided by the |
|
1795 database of transfer rules. Goals are generalized over all free |
|
1796 variables by default; this is necessary for variables whose types |
|
1797 change, but can be overridden for specific variables with e.g. |
|
1798 \isa{{\isaliteral{22}{\isachardoublequote}}transfer\ fixing{\isaliteral{3A}{\isacharcolon}}\ x\ y\ z{\isaliteral{22}{\isachardoublequote}}}. |
|
1799 |
|
1800 \item \hyperlink{method.HOL.transfer'}{\mbox{\isa{transfer{\isaliteral{27}{\isacharprime}}}}} is a variant of \hyperlink{method.HOL.transfer}{\mbox{\isa{transfer}}} that allows replacing a subgoal with one that is |
|
1801 logically stronger (rather than equivalent). For example, a |
|
1802 subgoal involving equality on a quotient type could be replaced |
|
1803 with a subgoal involving equality (instead of the corresponding |
|
1804 equivalence relation) on the underlying raw type. |
|
1805 |
|
1806 \item \hyperlink{method.HOL.transfer-prover}{\mbox{\isa{transfer{\isaliteral{5F}{\isacharunderscore}}prover}}} method assists with proving |
|
1807 a transfer rule for a new constant, provided the constant is |
|
1808 defined in terms of other constants that already have transfer |
|
1809 rules. It should be applied after unfolding the constant |
|
1810 definitions. |
|
1811 |
|
1812 \item \hyperlink{attribute.HOL.transfer-rule}{\mbox{\isa{transfer{\isaliteral{5F}{\isacharunderscore}}rule}}} attribute maintains a |
|
1813 collection of transfer rules, which relate constants at two |
|
1814 different types. Typical transfer rules may relate different type |
|
1815 instances of the same polymorphic constant, or they may relate an |
|
1816 operation on a raw type to a corresponding operation on an |
|
1817 abstract type (quotient or subtype). For example: |
|
1818 |
|
1819 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ list{\isaliteral{5F}{\isacharunderscore}}all{\isadigit{2}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ list{\isaliteral{5F}{\isacharunderscore}}all{\isadigit{2}}\ B{\isaliteral{29}{\isacharparenright}}\ map\ map{\isaliteral{22}{\isachardoublequote}}}\\ |
|
1820 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}cr{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ cr{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ cr{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}u{\isaliteral{2C}{\isacharcomma}}v{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2B}{\isacharplus}}u{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{2B}{\isacharplus}}v{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ plus{\isaliteral{22}{\isachardoublequote}}} |
|
1821 |
|
1822 Lemmas involving predicates on relations can also be registered |
|
1823 using the same attribute. For example: |
|
1824 |
|
1825 \isa{{\isaliteral{22}{\isachardoublequote}}bi{\isaliteral{5F}{\isacharunderscore}}unique\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}list{\isaliteral{5F}{\isacharunderscore}}all{\isadigit{2}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ op\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}\ distinct\ distinct{\isaliteral{22}{\isachardoublequote}}}\\ |
|
1826 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}bi{\isaliteral{5F}{\isacharunderscore}}unique\ A{\isaliteral{3B}{\isacharsemicolon}}\ bi{\isaliteral{5F}{\isacharunderscore}}unique\ B{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ bi{\isaliteral{5F}{\isacharunderscore}}unique\ {\isaliteral{28}{\isacharparenleft}}prod{\isaliteral{5F}{\isacharunderscore}}rel\ A\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} |
|
1827 |
|
1828 \item \hyperlink{attribute.HOL.relator-eq}{\mbox{\isa{relator{\isaliteral{5F}{\isacharunderscore}}eq}}} attribute collects identity laws |
|
1829 for relators of various type constructors, e.g. \isa{{\isaliteral{22}{\isachardoublequote}}list{\isaliteral{5F}{\isacharunderscore}}all{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}op\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}op\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. The \hyperlink{method.HOL.transfer}{\mbox{\isa{transfer}}} method uses these |
|
1830 lemmas to infer transfer rules for non-polymorphic constants on |
|
1831 the fly. |
1772 |
1832 |
1773 \end{description}% |
1833 \end{description}% |
1774 \end{isamarkuptext}% |
1834 \end{isamarkuptext}% |
1775 \isamarkuptrue% |
1835 \isamarkuptrue% |
1776 % |
1836 % |