147 ; |
147 ; |
148 @@{attribute rotated} @{syntax int}? |
148 @@{attribute rotated} @{syntax int}? |
149 \<close>} |
149 \<close>} |
150 |
150 |
151 \<^descr> @{attribute tagged}~@{text "name value"} and @{attribute |
151 \<^descr> @{attribute tagged}~@{text "name value"} and @{attribute |
152 untagged}~@{text name} add and remove \emph{tags} of some theorem. |
152 untagged}~@{text name} add and remove \<^emph>\<open>tags\<close> of some theorem. |
153 Tags may be any list of string pairs that serve as formal comment. |
153 Tags may be any list of string pairs that serve as formal comment. |
154 The first string is considered the tag name, the second its value. |
154 The first string is considered the tag name, the second its value. |
155 Note that @{attribute untagged} removes any tags of the same name. |
155 Note that @{attribute untagged} removes any tags of the same name. |
156 |
156 |
157 \<^descr> @{attribute THEN}~@{text a} composes rules by resolution; it |
157 \<^descr> @{attribute THEN}~@{text a} composes rules by resolution; it |
393 a good candidate to be solved by a single call of @{method simp}: |
393 a good candidate to be solved by a single call of @{method simp}: |
394 \<close> |
394 \<close> |
395 |
395 |
396 lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops |
396 lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops |
397 |
397 |
398 text \<open>The above attempt \emph{fails}, because @{term "0"} and @{term |
398 text \<open>The above attempt \<^emph>\<open>fails\<close>, because @{term "0"} and @{term |
399 "op +"} in the HOL library are declared as generic type class |
399 "op +"} in the HOL library are declared as generic type class |
400 operations, without stating any algebraic laws yet. More specific |
400 operations, without stating any algebraic laws yet. More specific |
401 types are required to get access to certain standard simplifications |
401 types are required to get access to certain standard simplifications |
402 of the theory context, e.g.\ like this:\<close> |
402 of the theory context, e.g.\ like this:\<close> |
403 |
403 |
584 This congruence rule for conditional expressions can |
584 This congruence rule for conditional expressions can |
585 supply contextual information for simplifying the arms: |
585 supply contextual information for simplifying the arms: |
586 @{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow> |
586 @{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow> |
587 (if ?p then ?a else ?b) = (if ?q then ?c else ?d)"} |
587 (if ?p then ?a else ?b) = (if ?q then ?c else ?d)"} |
588 |
588 |
589 A congruence rule can also \emph{prevent} simplification of some |
589 A congruence rule can also \<^emph>\<open>prevent\<close> simplification of some |
590 arguments. Here is an alternative congruence rule for conditional |
590 arguments. Here is an alternative congruence rule for conditional |
591 expressions that conforms to non-strict functional evaluation: |
591 expressions that conforms to non-strict functional evaluation: |
592 @{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"} |
592 @{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"} |
593 |
593 |
594 Only the first argument is simplified; the others remain unchanged. |
594 Only the first argument is simplified; the others remain unchanged. |
615 monotonically through the theory hierarchy: forming a new theory, |
615 monotonically through the theory hierarchy: forming a new theory, |
616 the union of the simpsets of its imports are taken as starting |
616 the union of the simpsets of its imports are taken as starting |
617 point. Also note that definitional packages like @{command |
617 point. Also note that definitional packages like @{command |
618 "datatype"}, @{command "primrec"}, @{command "fun"} routinely |
618 "datatype"}, @{command "primrec"}, @{command "fun"} routinely |
619 declare Simplifier rules to the target context, while plain |
619 declare Simplifier rules to the target context, while plain |
620 @{command "definition"} is an exception in \emph{not} declaring |
620 @{command "definition"} is an exception in \<^emph>\<open>not\<close> declaring |
621 anything. |
621 anything. |
622 |
622 |
623 \<^medskip> |
623 \<^medskip> |
624 It is up the user to manipulate the current simpset further |
624 It is up the user to manipulate the current simpset further |
625 by explicitly adding or deleting theorems as simplification rules, |
625 by explicitly adding or deleting theorems as simplification rules, |
645 \<close> |
645 \<close> |
646 |
646 |
647 |
647 |
648 subsection \<open>Ordered rewriting with permutative rules\<close> |
648 subsection \<open>Ordered rewriting with permutative rules\<close> |
649 |
649 |
650 text \<open>A rewrite rule is \emph{permutative} if the left-hand side and |
650 text \<open>A rewrite rule is \<^emph>\<open>permutative\<close> if the left-hand side and |
651 right-hand side are the equal up to renaming of variables. The most |
651 right-hand side are the equal up to renaming of variables. The most |
652 common permutative rule is commutativity: @{text "?x + ?y = ?y + |
652 common permutative rule is commutativity: @{text "?x + ?y = ?y + |
653 ?x"}. Other examples include @{text "(?x - ?y) - ?z = (?x - ?z) - |
653 ?x"}. Other examples include @{text "(?x - ?y) - ?z = (?x - ?z) - |
654 ?y"} in arithmetic and @{text "insert ?x (insert ?y ?A) = insert ?y |
654 ?y"} in arithmetic and @{text "insert ?x (insert ?y ?A) = insert ?y |
655 (insert ?x ?A)"} for sets. Such rules are common enough to merit |
655 (insert ?x ?A)"} for sets. Such rules are common enough to merit |
656 special attention. |
656 special attention. |
657 |
657 |
658 Because ordinary rewriting loops given such rules, the Simplifier |
658 Because ordinary rewriting loops given such rules, the Simplifier |
659 employs a special strategy, called \emph{ordered rewriting}. |
659 employs a special strategy, called \<^emph>\<open>ordered rewriting\<close>. |
660 Permutative rules are detected and only applied if the rewriting |
660 Permutative rules are detected and only applied if the rewriting |
661 step decreases the redex wrt.\ a given term ordering. For example, |
661 step decreases the redex wrt.\ a given term ordering. For example, |
662 commutativity rewrites @{text "b + a"} to @{text "a + b"}, but then |
662 commutativity rewrites @{text "b + a"} to @{text "a + b"}, but then |
663 stops, because the redex cannot be decreased further in the sense of |
663 stops, because the redex cannot be decreased further in the sense of |
664 the term ordering. |
664 the term ordering. |
686 orientation, if used with commutativity, leads to looping in |
686 orientation, if used with commutativity, leads to looping in |
687 conjunction with the standard term order. |
687 conjunction with the standard term order. |
688 |
688 |
689 \<^item> To complete your set of rewrite rules, you must add not just |
689 \<^item> To complete your set of rewrite rules, you must add not just |
690 associativity (A) and commutativity (C) but also a derived rule |
690 associativity (A) and commutativity (C) but also a derived rule |
691 \emph{left-commutativity} (LC): @{text "f x (f y z) = f y (f x z)"}. |
691 \<^emph>\<open>left-commutativity\<close> (LC): @{text "f x (f y z) = f y (f x z)"}. |
692 |
692 |
693 |
693 |
694 Ordered rewriting with the combination of A, C, and LC sorts a term |
694 Ordered rewriting with the combination of A, C, and LC sorts a term |
695 lexicographically --- the rewriting engine imitates bubble-sort. |
695 lexicographically --- the rewriting engine imitates bubble-sort. |
696 \<close> |
696 \<close> |
816 rules. |
816 rules. |
817 |
817 |
818 Any successful result needs to be a (possibly conditional) rewrite |
818 Any successful result needs to be a (possibly conditional) rewrite |
819 rule @{text "t \<equiv> u"} that is applicable to the current redex. The |
819 rule @{text "t \<equiv> u"} that is applicable to the current redex. The |
820 rule will be applied just as any ordinary rewrite rule. It is |
820 rule will be applied just as any ordinary rewrite rule. It is |
821 expected to be already in \emph{internal form}, bypassing the |
821 expected to be already in \<^emph>\<open>internal form\<close>, bypassing the |
822 automatic preprocessing of object-level equivalences. |
822 automatic preprocessing of object-level equivalences. |
823 |
823 |
824 \begin{matharray}{rcl} |
824 \begin{matharray}{rcl} |
825 @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
825 @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
826 simproc & : & @{text attribute} \\ |
826 simproc & : & @{text attribute} \\ |
1025 |
1025 |
1026 \<^medskip> |
1026 \<^medskip> |
1027 \begin{warn} |
1027 \begin{warn} |
1028 If a premise of a congruence rule cannot be proved, then the |
1028 If a premise of a congruence rule cannot be proved, then the |
1029 congruence is ignored. This should only happen if the rule is |
1029 congruence is ignored. This should only happen if the rule is |
1030 \emph{conditional} --- that is, contains premises not of the form |
1030 \<^emph>\<open>conditional\<close> --- that is, contains premises not of the form |
1031 @{text "t = ?x"}. Otherwise it indicates that some congruence rule, |
1031 @{text "t = ?x"}. Otherwise it indicates that some congruence rule, |
1032 or possibly the subgoaler or solver, is faulty. |
1032 or possibly the subgoaler or solver, is faulty. |
1033 \end{warn} |
1033 \end{warn} |
1034 \<close> |
1034 \<close> |
1035 |
1035 |
1052 simplification, in case the solver failed to solve the simplified |
1052 simplification, in case the solver failed to solve the simplified |
1053 goal. If the looper succeeds, the simplification process is started |
1053 goal. If the looper succeeds, the simplification process is started |
1054 all over again. Each of the subgoals generated by the looper is |
1054 all over again. Each of the subgoals generated by the looper is |
1055 attacked in turn, in reverse order. |
1055 attacked in turn, in reverse order. |
1056 |
1056 |
1057 A typical looper is \emph{case splitting}: the expansion of a |
1057 A typical looper is \<^emph>\<open>case splitting\<close>: the expansion of a |
1058 conditional. Another possibility is to apply an elimination rule on |
1058 conditional. Another possibility is to apply an elimination rule on |
1059 the assumptions. More adventurous loopers could start an induction. |
1059 the assumptions. More adventurous loopers could start an induction. |
1060 |
1060 |
1061 \<^descr> @{text "ctxt setloop tac"} installs @{text "tac"} as the only |
1061 \<^descr> @{text "ctxt setloop tac"} installs @{text "tac"} as the only |
1062 looper tactic of @{text "ctxt"}. |
1062 looper tactic of @{text "ctxt"}. |
1136 conclusion; the options @{text no_asm} etc.\ tune the Simplifier in |
1136 conclusion; the options @{text no_asm} etc.\ tune the Simplifier in |
1137 the same way as the for the @{text simp} method. |
1137 the same way as the for the @{text simp} method. |
1138 |
1138 |
1139 Note that forward simplification restricts the Simplifier to its |
1139 Note that forward simplification restricts the Simplifier to its |
1140 most basic operation of term rewriting; solver and looper tactics |
1140 most basic operation of term rewriting; solver and looper tactics |
1141 (\secref{sec:simp-strategies}) are \emph{not} involved here. The |
1141 (\secref{sec:simp-strategies}) are \<^emph>\<open>not\<close> involved here. The |
1142 @{attribute simplified} attribute should be only rarely required |
1142 @{attribute simplified} attribute should be only rarely required |
1143 under normal circumstances. |
1143 under normal circumstances. |
1144 \<close> |
1144 \<close> |
1145 |
1145 |
1146 |
1146 |
1181 |
1181 |
1182 text \<open>Isabelle supports natural deduction, which is easy to use for |
1182 text \<open>Isabelle supports natural deduction, which is easy to use for |
1183 interactive proof. But natural deduction does not easily lend |
1183 interactive proof. But natural deduction does not easily lend |
1184 itself to automation, and has a bias towards intuitionism. For |
1184 itself to automation, and has a bias towards intuitionism. For |
1185 certain proofs in classical logic, it can not be called natural. |
1185 certain proofs in classical logic, it can not be called natural. |
1186 The \emph{sequent calculus}, a generalization of natural deduction, |
1186 The \<^emph>\<open>sequent calculus\<close>, a generalization of natural deduction, |
1187 is easier to automate. |
1187 is easier to automate. |
1188 |
1188 |
1189 A \textbf{sequent} has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"} |
1189 A \<^bold>\<open>sequent\<close> has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"} |
1190 and @{text "\<Delta>"} are sets of formulae.\footnote{For first-order |
1190 and @{text "\<Delta>"} are sets of formulae.\footnote{For first-order |
1191 logic, sequents can equivalently be made from lists or multisets of |
1191 logic, sequents can equivalently be made from lists or multisets of |
1192 formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is |
1192 formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is |
1193 \textbf{valid} if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or> |
1193 \<^bold>\<open>valid\<close> if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or> |
1194 Q\<^sub>n"}. Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which |
1194 Q\<^sub>n"}. Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which |
1195 is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals. A |
1195 is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals. A |
1196 sequent is \textbf{basic} if its left and right sides have a common |
1196 sequent is \<^bold>\<open>basic\<close> if its left and right sides have a common |
1197 formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially |
1197 formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially |
1198 valid. |
1198 valid. |
1199 |
1199 |
1200 Sequent rules are classified as \textbf{right} or \textbf{left}, |
1200 Sequent rules are classified as \<^bold>\<open>right\<close> or \<^bold>\<open>left\<close>, |
1201 indicating which side of the @{text "\<turnstile>"} symbol they operate on. |
1201 indicating which side of the @{text "\<turnstile>"} symbol they operate on. |
1202 Rules that operate on the right side are analogous to natural |
1202 Rules that operate on the right side are analogous to natural |
1203 deduction's introduction rules, and left rules are analogous to |
1203 deduction's introduction rules, and left rules are analogous to |
1204 elimination rules. The sequent calculus analogue of @{text "(\<longrightarrow>I)"} |
1204 elimination rules. The sequent calculus analogue of @{text "(\<longrightarrow>I)"} |
1205 is the rule |
1205 is the rule |
1339 |
1339 |
1340 subsection \<open>Rule declarations\<close> |
1340 subsection \<open>Rule declarations\<close> |
1341 |
1341 |
1342 text \<open>The proof tools of the Classical Reasoner depend on |
1342 text \<open>The proof tools of the Classical Reasoner depend on |
1343 collections of rules declared in the context, which are classified |
1343 collections of rules declared in the context, which are classified |
1344 as introduction, elimination or destruction and as \emph{safe} or |
1344 as introduction, elimination or destruction and as \<^emph>\<open>safe\<close> or |
1345 \emph{unsafe}. In general, safe rules can be attempted blindly, |
1345 \<^emph>\<open>unsafe\<close>. In general, safe rules can be attempted blindly, |
1346 while unsafe rules must be used with care. A safe rule must never |
1346 while unsafe rules must be used with care. A safe rule must never |
1347 reduce a provable goal to an unprovable set of subgoals. |
1347 reduce a provable goal to an unprovable set of subgoals. |
1348 |
1348 |
1349 The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P |
1349 The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P |
1350 \<or> Q"} to @{text "P"}, which might turn out as premature choice of an |
1350 \<or> Q"} to @{text "P"}, which might turn out as premature choice of an |
1391 declared to the Classical Reasoner, i.e.\ the @{ML_type claset} |
1391 declared to the Classical Reasoner, i.e.\ the @{ML_type claset} |
1392 within the context. |
1392 within the context. |
1393 |
1393 |
1394 \<^descr> @{attribute intro}, @{attribute elim}, and @{attribute dest} |
1394 \<^descr> @{attribute intro}, @{attribute elim}, and @{attribute dest} |
1395 declare introduction, elimination, and destruction rules, |
1395 declare introduction, elimination, and destruction rules, |
1396 respectively. By default, rules are considered as \emph{unsafe} |
1396 respectively. By default, rules are considered as \<^emph>\<open>unsafe\<close> |
1397 (i.e.\ not applied blindly without backtracking), while ``@{text |
1397 (i.e.\ not applied blindly without backtracking), while ``@{text |
1398 "!"}'' classifies as \emph{safe}. Rule declarations marked by |
1398 "!"}'' classifies as \<^emph>\<open>safe\<close>. Rule declarations marked by |
1399 ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\ |
1399 ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\ |
1400 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps |
1400 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps |
1401 of the @{method rule} method). The optional natural number |
1401 of the @{method rule} method). The optional natural number |
1402 specifies an explicit weight argument, which is ignored by the |
1402 specifies an explicit weight argument, which is ignored by the |
1403 automated reasoning tools, but determines the search order of single |
1403 automated reasoning tools, but determines the search order of single |
1700 a form of Modus Ponens: if there are assumptions @{text "P \<longrightarrow> Q"} and |
1700 a form of Modus Ponens: if there are assumptions @{text "P \<longrightarrow> Q"} and |
1701 @{text "P"}, then replace @{text "P \<longrightarrow> Q"} by @{text "Q"}. |
1701 @{text "P"}, then replace @{text "P \<longrightarrow> Q"} by @{text "Q"}. |
1702 |
1702 |
1703 The classical reasoning tools --- except @{method blast} --- allow |
1703 The classical reasoning tools --- except @{method blast} --- allow |
1704 to modify this basic proof strategy by applying two lists of |
1704 to modify this basic proof strategy by applying two lists of |
1705 arbitrary \emph{wrapper tacticals} to it. The first wrapper list, |
1705 arbitrary \<^emph>\<open>wrapper tacticals\<close> to it. The first wrapper list, |
1706 which is considered to contain safe wrappers only, affects @{method |
1706 which is considered to contain safe wrappers only, affects @{method |
1707 safe_step} and all the tactics that call it. The second one, which |
1707 safe_step} and all the tactics that call it. The second one, which |
1708 may contain unsafe wrappers, affects the unsafe parts of @{method |
1708 may contain unsafe wrappers, affects the unsafe parts of @{method |
1709 step}, @{method slow_step}, and the tactics that call them. A |
1709 step}, @{method slow_step}, and the tactics that call them. A |
1710 wrapper transforms each step of the search, for example by |
1710 wrapper transforms each step of the search, for example by |
1721 \<^descr> @{text "ctxt addSWrapper (name, wrapper)"} adds a new wrapper, |
1721 \<^descr> @{text "ctxt addSWrapper (name, wrapper)"} adds a new wrapper, |
1722 which should yield a safe tactic, to modify the existing safe step |
1722 which should yield a safe tactic, to modify the existing safe step |
1723 tactic. |
1723 tactic. |
1724 |
1724 |
1725 \<^descr> @{text "ctxt addSbefore (name, tac)"} adds the given tactic as a |
1725 \<^descr> @{text "ctxt addSbefore (name, tac)"} adds the given tactic as a |
1726 safe wrapper, such that it is tried \emph{before} each safe step of |
1726 safe wrapper, such that it is tried \<^emph>\<open>before\<close> each safe step of |
1727 the search. |
1727 the search. |
1728 |
1728 |
1729 \<^descr> @{text "ctxt addSafter (name, tac)"} adds the given tactic as a |
1729 \<^descr> @{text "ctxt addSafter (name, tac)"} adds the given tactic as a |
1730 safe wrapper, such that it is tried when a safe step of the search |
1730 safe wrapper, such that it is tried when a safe step of the search |
1731 would fail. |
1731 would fail. |
1736 \<^descr> @{text "ctxt addWrapper (name, wrapper)"} adds a new wrapper to |
1736 \<^descr> @{text "ctxt addWrapper (name, wrapper)"} adds a new wrapper to |
1737 modify the existing (unsafe) step tactic. |
1737 modify the existing (unsafe) step tactic. |
1738 |
1738 |
1739 \<^descr> @{text "ctxt addbefore (name, tac)"} adds the given tactic as an |
1739 \<^descr> @{text "ctxt addbefore (name, tac)"} adds the given tactic as an |
1740 unsafe wrapper, such that it its result is concatenated |
1740 unsafe wrapper, such that it its result is concatenated |
1741 \emph{before} the result of each unsafe step. |
1741 \<^emph>\<open>before\<close> the result of each unsafe step. |
1742 |
1742 |
1743 \<^descr> @{text "ctxt addafter (name, tac)"} adds the given tactic as an |
1743 \<^descr> @{text "ctxt addafter (name, tac)"} adds the given tactic as an |
1744 unsafe wrapper, such that it its result is concatenated \emph{after} |
1744 unsafe wrapper, such that it its result is concatenated \<^emph>\<open>after\<close> |
1745 the result of each unsafe step. |
1745 the result of each unsafe step. |
1746 |
1746 |
1747 \<^descr> @{text "ctxt delWrapper name"} deletes the unsafe wrapper with |
1747 \<^descr> @{text "ctxt delWrapper name"} deletes the unsafe wrapper with |
1748 the given name. |
1748 the given name. |
1749 |
1749 |