81 \isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}% |
81 \isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}% |
82 } |
82 } |
83 \isamarkuptrue% |
83 \isamarkuptrue% |
84 % |
84 % |
85 \begin{isamarkuptext}% |
85 \begin{isamarkuptext}% |
86 An \emph{inductive definition} specifies the least predicate |
86 \begin{matharray}{rcl} |
87 or set \isa{R} closed under given rules: applying a rule to |
87 \indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
88 elements of \isa{R} yields a result within \isa{R}. For |
88 \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
89 example, a structural operational semantics is an inductive |
89 \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
90 definition of an evaluation relation. |
90 \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
91 \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\ |
|
92 \end{matharray} |
|
93 |
|
94 An \emph{inductive definition} specifies the least predicate or set |
|
95 \isa{R} closed under given rules: applying a rule to elements of |
|
96 \isa{R} yields a result within \isa{R}. For example, a |
|
97 structural operational semantics is an inductive definition of an |
|
98 evaluation relation. |
91 |
99 |
92 Dually, a \emph{coinductive definition} specifies the greatest |
100 Dually, a \emph{coinductive definition} specifies the greatest |
93 predicate or set \isa{R} that is consistent with given rules: |
101 predicate or set \isa{R} that is consistent with given rules: |
94 every element of \isa{R} can be seen as arising by applying a rule |
102 every element of \isa{R} can be seen as arising by applying a rule |
95 to elements of \isa{R}. An important example is using |
103 to elements of \isa{R}. An important example is using |
107 defined relation: there must be a monotonicity theorem of the form |
115 defined relation: there must be a monotonicity theorem of the form |
108 \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ B{\isaliteral{22}{\isachardoublequote}}}, for each premise \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4D3E}{\isasymM}}\ R\ t{\isaliteral{22}{\isachardoublequote}}} in an |
116 \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ B{\isaliteral{22}{\isachardoublequote}}}, for each premise \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4D3E}{\isasymM}}\ R\ t{\isaliteral{22}{\isachardoublequote}}} in an |
109 introduction rule. The default rule declarations of Isabelle/HOL |
117 introduction rule. The default rule declarations of Isabelle/HOL |
110 already take care of most common situations. |
118 already take care of most common situations. |
111 |
119 |
112 \begin{matharray}{rcl} |
|
113 \indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
114 \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
115 \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
116 \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
117 \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\ |
|
118 \end{matharray} |
|
119 |
|
120 \begin{railoutput} |
120 \begin{railoutput} |
121 \rail@begin{10}{} |
121 \rail@begin{10}{} |
122 \rail@bar |
122 \rail@bar |
123 \rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[] |
123 \rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[] |
124 \rail@nextbar{1} |
124 \rail@nextbar{1} |
879 \isamarkupsubsection{Old-style recursive function definitions (TFL)% |
879 \isamarkupsubsection{Old-style recursive function definitions (TFL)% |
880 } |
880 } |
881 \isamarkuptrue% |
881 \isamarkuptrue% |
882 % |
882 % |
883 \begin{isamarkuptext}% |
883 \begin{isamarkuptext}% |
884 The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}} for defining recursive are mostly obsolete; \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} or \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} should be used instead. |
884 \begin{matharray}{rcl} |
885 |
|
886 \begin{matharray}{rcl} |
|
887 \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ |
885 \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ |
888 \indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef-tc}{\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ |
886 \indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef-tc}{\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ |
889 \end{matharray} |
887 \end{matharray} |
|
888 |
|
889 The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}} for defining recursive are mostly obsolete; \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} or \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} should be used instead. |
890 |
890 |
891 \begin{railoutput} |
891 \begin{railoutput} |
892 \rail@begin{5}{} |
892 \rail@begin{5}{} |
893 \rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[] |
893 \rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[] |
894 \rail@bar |
894 \rail@bar |
1485 \isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}% |
1485 \isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}% |
1486 } |
1486 } |
1487 \isamarkuptrue% |
1487 \isamarkuptrue% |
1488 % |
1488 % |
1489 \begin{isamarkuptext}% |
1489 \begin{isamarkuptext}% |
1490 A Gordon/HOL-style type definition is a certain axiom scheme |
1490 \begin{matharray}{rcl} |
1491 that identifies a new type with a subset of an existing type. More |
1491 \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ |
|
1492 \end{matharray} |
|
1493 |
|
1494 A Gordon/HOL-style type definition is a certain axiom scheme that |
|
1495 identifies a new type with a subset of an existing type. More |
1492 precisely, the new type is defined by exhibiting an existing type |
1496 precisely, the new type is defined by exhibiting an existing type |
1493 \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, a set \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ set{\isaliteral{22}{\isachardoublequote}}}, and a theorem that proves |
1497 \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, a set \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ set{\isaliteral{22}{\isachardoublequote}}}, and a theorem that proves |
1494 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequote}}}. Thus \isa{A} is a non-empty subset of \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, and the new type denotes this subset. New functions are |
1498 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequote}}}. Thus \isa{A} is a non-empty subset of \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, and the new type denotes this subset. New functions are |
1495 postulated that establish an isomorphism between the new type and |
1499 postulated that establish an isomorphism between the new type and |
1496 the subset. In general, the type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} may involve type |
1500 the subset. In general, the type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} may involve type |
1504 downwards-closed wrt.\ arbitrary non-empty subsets. Thus genuinely |
1508 downwards-closed wrt.\ arbitrary non-empty subsets. Thus genuinely |
1505 new types introduced by \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} stay within the range |
1509 new types introduced by \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} stay within the range |
1506 of HOL models by construction. Note that \indexref{}{command}{type\_synonym}\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}} from Isabelle/Pure merely introduces syntactic |
1510 of HOL models by construction. Note that \indexref{}{command}{type\_synonym}\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}} from Isabelle/Pure merely introduces syntactic |
1507 abbreviations, without any logical significance. |
1511 abbreviations, without any logical significance. |
1508 |
1512 |
1509 \begin{matharray}{rcl} |
|
1510 \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ |
|
1511 \end{matharray} |
|
1512 |
|
1513 \begin{railoutput} |
1513 \begin{railoutput} |
1514 \rail@begin{2}{} |
1514 \rail@begin{2}{} |
1515 \rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[] |
1515 \rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[] |
1516 \rail@bar |
1516 \rail@bar |
1517 \rail@nextbar{1} |
1517 \rail@nextbar{1} |
1766 \isamarkupsection{Quotient types% |
1766 \isamarkupsection{Quotient types% |
1767 } |
1767 } |
1768 \isamarkuptrue% |
1768 \isamarkuptrue% |
1769 % |
1769 % |
1770 \begin{isamarkuptext}% |
1770 \begin{isamarkuptext}% |
1771 The quotient package defines a new quotient type given a raw type |
1771 \begin{matharray}{rcl} |
1772 and a partial equivalence relation. |
|
1773 It also includes automation for transporting definitions and theorems. |
|
1774 It can automatically produce definitions and theorems on the quotient type, |
|
1775 given the corresponding constants and facts on the raw type. |
|
1776 |
|
1777 \begin{matharray}{rcl} |
|
1778 \indexdef{HOL}{command}{quotient\_type}\hypertarget{command.HOL.quotient-type}{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ |
1772 \indexdef{HOL}{command}{quotient\_type}\hypertarget{command.HOL.quotient-type}{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ |
1779 \indexdef{HOL}{command}{quotient\_definition}\hypertarget{command.HOL.quotient-definition}{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ |
1773 \indexdef{HOL}{command}{quotient\_definition}\hypertarget{command.HOL.quotient-definition}{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ |
1780 \indexdef{HOL}{command}{print\_quotmaps}\hypertarget{command.HOL.print-quotmaps}{\hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ |
1774 \indexdef{HOL}{command}{print\_quotmaps}\hypertarget{command.HOL.print-quotmaps}{\hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ |
1781 \indexdef{HOL}{command}{print\_quotients}\hypertarget{command.HOL.print-quotients}{\hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ |
1775 \indexdef{HOL}{command}{print\_quotients}\hypertarget{command.HOL.print-quotients}{\hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ |
1782 \indexdef{HOL}{command}{print\_quotconsts}\hypertarget{command.HOL.print-quotconsts}{\hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ |
1776 \indexdef{HOL}{command}{print\_quotconsts}\hypertarget{command.HOL.print-quotconsts}{\hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ |
1783 \end{matharray} |
1777 \end{matharray} |
1784 |
1778 |
|
1779 The quotient package defines a new quotient type given a raw type |
|
1780 and a partial equivalence relation. It also includes automation for |
|
1781 transporting definitions and theorems. It can automatically produce |
|
1782 definitions and theorems on the quotient type, given the |
|
1783 corresponding constants and facts on the raw type. |
|
1784 |
1785 \begin{railoutput} |
1785 \begin{railoutput} |
1786 \rail@begin{2}{} |
1786 \rail@begin{2}{} |
1787 \rail@term{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}}[] |
1787 \rail@term{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}}[] |
1788 \rail@plus |
1788 \rail@plus |
1789 \rail@nont{\isa{spec}}[] |
1789 \rail@nont{\isa{spec}}[] |
1849 \end{railoutput} |
1849 \end{railoutput} |
1850 |
1850 |
1851 |
1851 |
1852 \begin{description} |
1852 \begin{description} |
1853 |
1853 |
1854 \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types. The injection from a quotient type |
1854 \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types. The |
1855 to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t}, its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names. |
1855 injection from a quotient type to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t}, its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names. |
1856 |
1856 |
1857 \item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on the quotient type. |
1857 \item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on |
1858 |
1858 the quotient type. |
1859 \item \hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}} prints quotient map functions. |
1859 |
|
1860 \item \hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}} prints quotient map |
|
1861 functions. |
1860 |
1862 |
1861 \item \hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}} prints quotients. |
1863 \item \hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}} prints quotients. |
1862 |
1864 |
1863 \item \hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}} prints quotient constants. |
1865 \item \hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}} prints quotient constants. |
1864 |
1866 |
1875 \indexdef{HOL}{attribute}{coercion}\hypertarget{attribute.HOL.coercion}{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}} & : & \isa{attribute} \\ |
1877 \indexdef{HOL}{attribute}{coercion}\hypertarget{attribute.HOL.coercion}{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}} & : & \isa{attribute} \\ |
1876 \indexdef{HOL}{attribute}{coercion\_enabled}\hypertarget{attribute.HOL.coercion-enabled}{\hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}}} & : & \isa{attribute} \\ |
1878 \indexdef{HOL}{attribute}{coercion\_enabled}\hypertarget{attribute.HOL.coercion-enabled}{\hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}}} & : & \isa{attribute} \\ |
1877 \indexdef{HOL}{attribute}{coercion\_map}\hypertarget{attribute.HOL.coercion-map}{\hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}} & : & \isa{attribute} \\ |
1879 \indexdef{HOL}{attribute}{coercion\_map}\hypertarget{attribute.HOL.coercion-map}{\hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}} & : & \isa{attribute} \\ |
1878 \end{matharray} |
1880 \end{matharray} |
1879 |
1881 |
|
1882 Coercive subtyping allows the user to omit explicit type |
|
1883 conversions, also called \emph{coercions}. Type inference will add |
|
1884 them as necessary when parsing a term. See |
|
1885 \cite{traytel-berghofer-nipkow-2011} for details. |
|
1886 |
1880 \begin{railoutput} |
1887 \begin{railoutput} |
1881 \rail@begin{2}{} |
1888 \rail@begin{2}{} |
1882 \rail@term{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}}[] |
1889 \rail@term{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}}[] |
1883 \rail@bar |
1890 \rail@bar |
1884 \rail@nextbar{1} |
1891 \rail@nextbar{1} |
1896 \rail@endbar |
1903 \rail@endbar |
1897 \rail@end |
1904 \rail@end |
1898 \end{railoutput} |
1905 \end{railoutput} |
1899 |
1906 |
1900 |
1907 |
1901 Coercive subtyping allows the user to omit explicit type conversions, |
|
1902 also called \emph{coercions}. Type inference will add them as |
|
1903 necessary when parsing a term. See |
|
1904 \cite{traytel-berghofer-nipkow-2011} for details. |
|
1905 |
|
1906 \begin{description} |
1908 \begin{description} |
1907 |
1909 |
1908 \item \hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}~\isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} registers a new |
1910 \item \hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}~\isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} registers a new |
1909 coercion function \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} where \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} are nullary type constructors. Coercions are |
1911 coercion function \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} where \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} and |
1910 composed by the inference algorithm if needed. Note that the type |
1912 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} are type constructors without arguments. Coercions are |
1911 inference algorithm is complete only if the registered coercions form |
1913 composed by the inference algorithm if needed. Note that the type |
1912 a lattice. |
1914 inference algorithm is complete only if the registered coercions |
1913 |
1915 form a lattice. |
1914 |
1916 |
1915 \item \hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}~\isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} registers a new |
1917 \item \hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}~\isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} registers a |
1916 map function to lift coercions through type constructors. The function |
1918 new map function to lift coercions through type constructors. The |
1917 \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} must conform to the following type pattern |
1919 function \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} must conform to the following type pattern |
1918 |
1920 |
1919 \begin{matharray}{lll} |
1921 \begin{matharray}{lll} |
1920 \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & |
1922 \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & |
1921 \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ f\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} \\ |
1923 \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ f\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} \\ |
1922 \end{matharray} |
1924 \end{matharray} |
1923 |
1925 |
1924 where \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is a type constructor and \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} is of |
1926 where \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is a type constructor and \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} is of type |
1925 type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} or |
1927 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}}. Registering a map function |
1926 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}}. |
1928 overwrites any existing map function for this particular type |
1927 Registering a map function overwrites any existing map function for |
1929 constructor. |
1928 this particular type constructor. |
|
1929 |
|
1930 |
1930 |
1931 \item \hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}} enables the coercion |
1931 \item \hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}} enables the coercion |
1932 inference algorithm. |
1932 inference algorithm. |
1933 |
1933 |
1934 \end{description}% |
1934 \end{description}% |
1944 \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{method} \\ |
1944 \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{method} \\ |
1945 \indexdef{HOL}{attribute}{arith}\hypertarget{attribute.HOL.arith}{\hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{attribute} \\ |
1945 \indexdef{HOL}{attribute}{arith}\hypertarget{attribute.HOL.arith}{\hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{attribute} \\ |
1946 \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}}} & : & \isa{attribute} \\ |
1946 \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}}} & : & \isa{attribute} \\ |
1947 \end{matharray} |
1947 \end{matharray} |
1948 |
1948 |
1949 The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems |
1949 \begin{description} |
1950 (on types \isa{nat}, \isa{int}, \isa{real}). Any current |
1950 |
1951 facts are inserted into the goal before running the procedure. |
1951 \item \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} decides linear arithmetic problems (on |
1952 |
1952 types \isa{nat}, \isa{int}, \isa{real}). Any current facts |
1953 The \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} attribute declares facts that are |
1953 are inserted into the goal before running the procedure. |
1954 always supplied to the arithmetic provers implicitly. |
1954 |
1955 |
1955 \item \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} declares facts that are supplied to |
1956 The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}} attribute declares case split |
1956 the arithmetic provers implicitly. |
|
1957 |
|
1958 \item \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}} attribute declares case split |
1957 rules to be expanded before \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} is invoked. |
1959 rules to be expanded before \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} is invoked. |
1958 |
1960 |
1959 Note that a simpler (but faster) arithmetic prover is |
1961 \end{description} |
1960 already invoked by the Simplifier.% |
1962 |
|
1963 Note that a simpler (but faster) arithmetic prover is already |
|
1964 invoked by the Simplifier.% |
1961 \end{isamarkuptext}% |
1965 \end{isamarkuptext}% |
1962 \isamarkuptrue% |
1966 \isamarkuptrue% |
1963 % |
1967 % |
1964 \isamarkupsection{Intuitionistic proof search% |
1968 \isamarkupsection{Intuitionistic proof search% |
1965 } |
1969 } |
1979 \rail@endplus |
1983 \rail@endplus |
1980 \rail@end |
1984 \rail@end |
1981 \end{railoutput} |
1985 \end{railoutput} |
1982 |
1986 |
1983 |
1987 |
1984 The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof |
1988 \begin{description} |
1985 search, depending on specifically declared rules from the context, |
1989 |
1986 or given as explicit arguments. Chained facts are inserted into the |
1990 \item \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} performs intuitionistic proof search, |
1987 goal before commencing proof search. |
1991 depending on specifically declared rules from the context, or given |
|
1992 as explicit arguments. Chained facts are inserted into the goal |
|
1993 before commencing proof search. |
1988 |
1994 |
1989 Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, |
1995 Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, |
1990 \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the |
1996 \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the |
1991 ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' indicator refers to ``safe'' rules, which may be |
1997 ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' indicator refers to ``safe'' rules, which may be |
1992 applied aggressively (without considering back-tracking later). |
1998 applied aggressively (without considering back-tracking later). |
1993 Rules declared with ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' are ignored in proof search (the |
1999 Rules declared with ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' are ignored in proof search (the |
1994 single-step \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method still observes these). An |
2000 single-step \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method still observes these). An |
1995 explicit weight annotation may be given as well; otherwise the |
2001 explicit weight annotation may be given as well; otherwise the |
1996 number of rule premises will be taken into account here.% |
2002 number of rule premises will be taken into account here. |
|
2003 |
|
2004 \end{description}% |
1997 \end{isamarkuptext}% |
2005 \end{isamarkuptext}% |
1998 \isamarkuptrue% |
2006 \isamarkuptrue% |
1999 % |
2007 % |
2000 \isamarkupsection{Model Elimination and Resolution% |
2008 \isamarkupsection{Model Elimination and Resolution% |
2001 } |
2009 } |
2037 \rail@endbar |
2045 \rail@endbar |
2038 \rail@end |
2046 \rail@end |
2039 \end{railoutput} |
2047 \end{railoutput} |
2040 |
2048 |
2041 |
2049 |
2042 The \hyperlink{method.HOL.meson}{\mbox{\isa{meson}}} method implements Loveland's model elimination |
2050 \begin{description} |
2043 procedure \cite{loveland-78}. See \verb|~~/src/HOL/ex/Meson_Test.thy| for |
2051 |
2044 examples. |
2052 \item \hyperlink{method.HOL.meson}{\mbox{\isa{meson}}} implements Loveland's model elimination |
2045 |
2053 procedure \cite{loveland-78}. See \verb|~~/src/HOL/ex/Meson_Test.thy| for examples. |
2046 The \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}} method combines ordered resolution and ordered |
2054 |
2047 paramodulation to find first-order (or mildly higher-order) proofs. The first |
2055 \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}} combines ordered resolution and ordered |
2048 optional argument specifies a type encoding; see the Sledgehammer manual |
2056 paramodulation to find first-order (or mildly higher-order) proofs. |
2049 \cite{isabelle-sledgehammer} for details. The \verb|~~/src/HOL/Metis_Examples| directory contains several small theories |
2057 The first optional argument specifies a type encoding; see the |
2050 developed to a large extent using Metis.% |
2058 Sledgehammer manual \cite{isabelle-sledgehammer} for details. The |
|
2059 directory \verb|~~/src/HOL/Metis_Examples| contains several small |
|
2060 theories developed to a large extent using \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}. |
|
2061 |
|
2062 \end{description}% |
2051 \end{isamarkuptext}% |
2063 \end{isamarkuptext}% |
2052 \isamarkuptrue% |
2064 \isamarkuptrue% |
2053 % |
2065 % |
2054 \isamarkupsection{Coherent Logic% |
2066 \isamarkupsection{Coherent Logic% |
2055 } |
2067 } |
2069 \rail@endbar |
2081 \rail@endbar |
2070 \rail@end |
2082 \rail@end |
2071 \end{railoutput} |
2083 \end{railoutput} |
2072 |
2084 |
2073 |
2085 |
2074 The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of |
2086 \begin{description} |
2075 \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers |
2087 |
2076 applications in confluence theory, lattice theory and projective |
2088 \item \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} solves problems of \emph{Coherent |
2077 geometry. See \verb|~~/src/HOL/ex/Coherent.thy| for some |
2089 Logic} \cite{Bezem-Coquand:2005}, which covers applications in |
2078 examples.% |
2090 confluence theory, lattice theory and projective geometry. See |
|
2091 \verb|~~/src/HOL/ex/Coherent.thy| for some examples. |
|
2092 |
|
2093 \end{description}% |
2079 \end{isamarkuptext}% |
2094 \end{isamarkuptext}% |
2080 \isamarkuptrue% |
2095 \isamarkuptrue% |
2081 % |
2096 % |
2082 \isamarkupsection{Proving propositions% |
2097 \isamarkupsection{Proving propositions% |
2083 } |
2098 } |