1170 is better behaved in an infinite search space. However, quantifier |
1170 is better behaved in an infinite search space. However, quantifier |
1171 replication is too expensive to prove any but the simplest theorems.% |
1171 replication is too expensive to prove any but the simplest theorems.% |
1172 \end{isamarkuptext}% |
1172 \end{isamarkuptext}% |
1173 \isamarkuptrue% |
1173 \isamarkuptrue% |
1174 % |
1174 % |
|
1175 \isamarkupsubsection{Rule declarations% |
|
1176 } |
|
1177 \isamarkuptrue% |
|
1178 % |
|
1179 \begin{isamarkuptext}% |
|
1180 The proof tools of the Classical Reasoner depend on |
|
1181 collections of rules declared in the context, which are classified |
|
1182 as introduction, elimination or destruction and as \emph{safe} or |
|
1183 \emph{unsafe}. In general, safe rules can be attempted blindly, |
|
1184 while unsafe rules must be used with care. A safe rule must never |
|
1185 reduce a provable goal to an unprovable set of subgoals. |
|
1186 |
|
1187 The rule \isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}} is unsafe because it reduces \isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}} to \isa{{\isaliteral{22}{\isachardoublequote}}P{\isaliteral{22}{\isachardoublequote}}}, which might turn out as premature choice of an |
|
1188 unprovable subgoal. Any rule is unsafe whose premises contain new |
|
1189 unknowns. The elimination rule \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}} is |
|
1190 unsafe, since it is applied via elim-resolution, which discards the |
|
1191 assumption \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}} and replaces it by the weaker |
|
1192 assumption \isa{{\isaliteral{22}{\isachardoublequote}}P\ t{\isaliteral{22}{\isachardoublequote}}}. The rule \isa{{\isaliteral{22}{\isachardoublequote}}P\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}} is |
|
1193 unsafe for similar reasons. The quantifier duplication rule \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}} is unsafe in a different sense: |
|
1194 since it keeps the assumption \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}}, it is prone to |
|
1195 looping. In classical first-order logic, all rules are safe except |
|
1196 those mentioned above. |
|
1197 |
|
1198 The safe~/ unsafe distinction is vague, and may be regarded merely |
|
1199 as a way of giving some rules priority over others. One could argue |
|
1200 that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F723E}{\isasymor}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is unsafe, because repeated application of it |
|
1201 could generate exponentially many subgoals. Induction rules are |
|
1202 unsafe because inductive proofs are difficult to set up |
|
1203 automatically. Any inference is unsafe that instantiates an unknown |
|
1204 in the proof state --- thus matching must be used, rather than |
|
1205 unification. Even proof by assumption is unsafe if it instantiates |
|
1206 unknowns shared with other subgoals. |
|
1207 |
|
1208 \begin{matharray}{rcl} |
|
1209 \indexdef{}{command}{print\_claset}\hypertarget{command.print-claset}{\hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}claset}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ |
|
1210 \indexdef{}{attribute}{intro}\hypertarget{attribute.intro}{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\ |
|
1211 \indexdef{}{attribute}{elim}\hypertarget{attribute.elim}{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\ |
|
1212 \indexdef{}{attribute}{dest}\hypertarget{attribute.dest}{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\ |
|
1213 \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\ |
|
1214 \indexdef{}{attribute}{iff}\hypertarget{attribute.iff}{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}} & : & \isa{attribute} \\ |
|
1215 \indexdef{}{attribute}{swapped}\hypertarget{attribute.swapped}{\hyperlink{attribute.swapped}{\mbox{\isa{swapped}}}} & : & \isa{attribute} \\ |
|
1216 \end{matharray} |
|
1217 |
|
1218 \begin{railoutput} |
|
1219 \rail@begin{3}{} |
|
1220 \rail@bar |
|
1221 \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[] |
|
1222 \rail@nextbar{1} |
|
1223 \rail@term{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}}[] |
|
1224 \rail@nextbar{2} |
|
1225 \rail@term{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}}[] |
|
1226 \rail@endbar |
|
1227 \rail@bar |
|
1228 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[] |
|
1229 \rail@nextbar{1} |
|
1230 \rail@nextbar{2} |
|
1231 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[] |
|
1232 \rail@endbar |
|
1233 \rail@bar |
|
1234 \rail@nextbar{1} |
|
1235 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] |
|
1236 \rail@endbar |
|
1237 \rail@end |
|
1238 \rail@begin{1}{} |
|
1239 \rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[] |
|
1240 \rail@term{\isa{del}}[] |
|
1241 \rail@end |
|
1242 \rail@begin{3}{} |
|
1243 \rail@term{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}}[] |
|
1244 \rail@bar |
|
1245 \rail@bar |
|
1246 \rail@nextbar{1} |
|
1247 \rail@term{\isa{add}}[] |
|
1248 \rail@endbar |
|
1249 \rail@bar |
|
1250 \rail@nextbar{1} |
|
1251 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[] |
|
1252 \rail@endbar |
|
1253 \rail@nextbar{2} |
|
1254 \rail@term{\isa{del}}[] |
|
1255 \rail@endbar |
|
1256 \rail@end |
|
1257 \end{railoutput} |
|
1258 |
|
1259 |
|
1260 \begin{description} |
|
1261 |
|
1262 \item \hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}claset}}}} prints the collection of rules |
|
1263 declared to the Classical Reasoner, i.e.\ the \verb|claset| |
|
1264 within the context. |
|
1265 |
|
1266 \item \hyperlink{attribute.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.elim}{\mbox{\isa{elim}}}, and \hyperlink{attribute.dest}{\mbox{\isa{dest}}} |
|
1267 declare introduction, elimination, and destruction rules, |
|
1268 respectively. By default, rules are considered as \emph{unsafe} |
|
1269 (i.e.\ not applied blindly without backtracking), while ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' classifies as \emph{safe}. Rule declarations marked by |
|
1270 ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' coincide with those of Isabelle/Pure, cf.\ |
|
1271 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps |
|
1272 of the \hyperlink{method.rule}{\mbox{\isa{rule}}} method). The optional natural number |
|
1273 specifies an explicit weight argument, which is ignored by the |
|
1274 automated reasoning tools, but determines the search order of single |
|
1275 rule steps. |
|
1276 |
|
1277 Introduction rules are those that can be applied using ordinary |
|
1278 resolution. Their swapped forms are generated internally, which |
|
1279 will be applied using elim-resolution. Elimination rules are |
|
1280 applied using elim-resolution. Rules are sorted by the number of |
|
1281 new subgoals they will yield; rules that generate the fewest |
|
1282 subgoals will be tried first. Otherwise, later declarations take |
|
1283 precedence over earlier ones. |
|
1284 |
|
1285 Rules already present in the context with the same classification |
|
1286 are ignored. A warning is printed if the rule has already been |
|
1287 added with some other classification, but the rule is added anyway |
|
1288 as requested. |
|
1289 |
|
1290 \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} deletes all occurrences of a |
|
1291 rule from the classical context, regardless of its classification as |
|
1292 introduction~/ elimination~/ destruction and safe~/ unsafe. |
|
1293 |
|
1294 \item \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares logical equivalences to the |
|
1295 Simplifier and the Classical reasoner at the same time. |
|
1296 Non-conditional rules result in a safe introduction and elimination |
|
1297 pair; conditional ones are considered unsafe. Rules with negative |
|
1298 conclusion are automatically inverted (using \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{22}{\isachardoublequote}}}-elimination |
|
1299 internally). |
|
1300 |
|
1301 The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' version of \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares rules to |
|
1302 the Isabelle/Pure context only, and omits the Simplifier |
|
1303 declaration. |
|
1304 |
|
1305 \item \hyperlink{attribute.swapped}{\mbox{\isa{swapped}}} turns an introduction rule into an |
|
1306 elimination, by resolving with the classical swap principle \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ R\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequote}}} in the second position. This is mainly for |
|
1307 illustrative purposes: the Classical Reasoner already swaps rules |
|
1308 internally as explained above. |
|
1309 |
|
1310 \end{description}% |
|
1311 \end{isamarkuptext}% |
|
1312 \isamarkuptrue% |
|
1313 % |
1175 \isamarkupsubsection{Basic methods% |
1314 \isamarkupsubsection{Basic methods% |
1176 } |
1315 } |
1177 \isamarkuptrue% |
1316 \isamarkuptrue% |
1178 % |
1317 % |
1179 \begin{isamarkuptext}% |
1318 \begin{isamarkuptext}% |
1432 the ones related to the Simplifier are prefixed by \isa{simp} |
1571 the ones related to the Simplifier are prefixed by \isa{simp} |
1433 here. |
1572 here. |
1434 |
1573 |
1435 Facts provided by forward chaining are inserted into the goal before |
1574 Facts provided by forward chaining are inserted into the goal before |
1436 doing the search. |
1575 doing the search. |
1437 |
|
1438 \end{description}% |
|
1439 \end{isamarkuptext}% |
|
1440 \isamarkuptrue% |
|
1441 % |
|
1442 \isamarkupsubsection{Declaring rules% |
|
1443 } |
|
1444 \isamarkuptrue% |
|
1445 % |
|
1446 \begin{isamarkuptext}% |
|
1447 \begin{matharray}{rcl} |
|
1448 \indexdef{}{command}{print\_claset}\hypertarget{command.print-claset}{\hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}claset}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ |
|
1449 \indexdef{}{attribute}{intro}\hypertarget{attribute.intro}{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\ |
|
1450 \indexdef{}{attribute}{elim}\hypertarget{attribute.elim}{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\ |
|
1451 \indexdef{}{attribute}{dest}\hypertarget{attribute.dest}{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\ |
|
1452 \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\ |
|
1453 \indexdef{}{attribute}{iff}\hypertarget{attribute.iff}{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}} & : & \isa{attribute} \\ |
|
1454 \end{matharray} |
|
1455 |
|
1456 \begin{railoutput} |
|
1457 \rail@begin{3}{} |
|
1458 \rail@bar |
|
1459 \rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[] |
|
1460 \rail@nextbar{1} |
|
1461 \rail@term{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}}[] |
|
1462 \rail@nextbar{2} |
|
1463 \rail@term{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}}[] |
|
1464 \rail@endbar |
|
1465 \rail@bar |
|
1466 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[] |
|
1467 \rail@nextbar{1} |
|
1468 \rail@nextbar{2} |
|
1469 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[] |
|
1470 \rail@endbar |
|
1471 \rail@bar |
|
1472 \rail@nextbar{1} |
|
1473 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] |
|
1474 \rail@endbar |
|
1475 \rail@end |
|
1476 \rail@begin{1}{} |
|
1477 \rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[] |
|
1478 \rail@term{\isa{del}}[] |
|
1479 \rail@end |
|
1480 \rail@begin{3}{} |
|
1481 \rail@term{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}}[] |
|
1482 \rail@bar |
|
1483 \rail@bar |
|
1484 \rail@nextbar{1} |
|
1485 \rail@term{\isa{add}}[] |
|
1486 \rail@endbar |
|
1487 \rail@bar |
|
1488 \rail@nextbar{1} |
|
1489 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[] |
|
1490 \rail@endbar |
|
1491 \rail@nextbar{2} |
|
1492 \rail@term{\isa{del}}[] |
|
1493 \rail@endbar |
|
1494 \rail@end |
|
1495 \end{railoutput} |
|
1496 |
|
1497 |
|
1498 \begin{description} |
|
1499 |
|
1500 \item \hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}claset}}}} prints the collection of rules |
|
1501 declared to the Classical Reasoner, which is also known as |
|
1502 ``claset'' internally \cite{isabelle-ref}. |
|
1503 |
|
1504 \item \hyperlink{attribute.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.elim}{\mbox{\isa{elim}}}, and \hyperlink{attribute.dest}{\mbox{\isa{dest}}} |
|
1505 declare introduction, elimination, and destruction rules, |
|
1506 respectively. By default, rules are considered as \emph{unsafe} |
|
1507 (i.e.\ not applied blindly without backtracking), while ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' classifies as \emph{safe}. Rule declarations marked by |
|
1508 ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' coincide with those of Isabelle/Pure, cf.\ |
|
1509 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps |
|
1510 of the \hyperlink{method.rule}{\mbox{\isa{rule}}} method). The optional natural number |
|
1511 specifies an explicit weight argument, which is ignored by automated |
|
1512 tools, but determines the search order of single rule steps. |
|
1513 |
|
1514 \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} deletes introduction, |
|
1515 elimination, or destruction rules from the context. |
|
1516 |
|
1517 \item \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares logical equivalences to the |
|
1518 Simplifier and the Classical reasoner at the same time. |
|
1519 Non-conditional rules result in a ``safe'' introduction and |
|
1520 elimination pair; conditional ones are considered ``unsafe''. Rules |
|
1521 with negative conclusion are automatically inverted (using \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{22}{\isachardoublequote}}}-elimination internally). |
|
1522 |
|
1523 The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' version of \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares rules to |
|
1524 the Isabelle/Pure context only, and omits the Simplifier |
|
1525 declaration. |
|
1526 |
|
1527 \end{description}% |
|
1528 \end{isamarkuptext}% |
|
1529 \isamarkuptrue% |
|
1530 % |
|
1531 \isamarkupsubsection{Classical operations% |
|
1532 } |
|
1533 \isamarkuptrue% |
|
1534 % |
|
1535 \begin{isamarkuptext}% |
|
1536 \begin{matharray}{rcl} |
|
1537 \indexdef{}{attribute}{swapped}\hypertarget{attribute.swapped}{\hyperlink{attribute.swapped}{\mbox{\isa{swapped}}}} & : & \isa{attribute} \\ |
|
1538 \end{matharray} |
|
1539 |
|
1540 \begin{description} |
|
1541 |
|
1542 \item \hyperlink{attribute.swapped}{\mbox{\isa{swapped}}} turns an introduction rule into an |
|
1543 elimination, by resolving with the classical swap principle \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. |
|
1544 |
1576 |
1545 \end{description}% |
1577 \end{description}% |
1546 \end{isamarkuptext}% |
1578 \end{isamarkuptext}% |
1547 \isamarkuptrue% |
1579 \isamarkuptrue% |
1548 % |
1580 % |