933 @{method_def slow} & : & @{text method} \\ |
933 @{method_def slow} & : & @{text method} \\ |
934 @{method_def best} & : & @{text method} \\ |
934 @{method_def best} & : & @{text method} \\ |
935 @{method_def fastsimp} & : & @{text method} \\ |
935 @{method_def fastsimp} & : & @{text method} \\ |
936 @{method_def slowsimp} & : & @{text method} \\ |
936 @{method_def slowsimp} & : & @{text method} \\ |
937 @{method_def bestsimp} & : & @{text method} \\ |
937 @{method_def bestsimp} & : & @{text method} \\ |
|
938 @{method_def deepen} & : & @{text method} \\ |
938 \end{matharray} |
939 \end{matharray} |
939 |
940 |
940 @{rail " |
941 @{rail " |
941 @@{method blast} @{syntax nat}? (@{syntax clamod} * ) |
942 @@{method blast} @{syntax nat}? (@{syntax clamod} * ) |
942 ; |
943 ; |
946 ; |
947 ; |
947 (@@{method fast} | @@{method slow} | @@{method best}) (@{syntax clamod} * ) |
948 (@@{method fast} | @@{method slow} | @@{method best}) (@{syntax clamod} * ) |
948 ; |
949 ; |
949 (@@{method fastsimp} | @@{method slowsimp} | @@{method bestsimp}) |
950 (@@{method fastsimp} | @@{method slowsimp} | @@{method bestsimp}) |
950 (@{syntax clasimpmod} * ) |
951 (@{syntax clasimpmod} * ) |
|
952 ; |
|
953 @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * ) |
951 ; |
954 ; |
952 @{syntax_def clamod}: |
955 @{syntax_def clamod}: |
953 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs} |
956 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs} |
954 ; |
957 ; |
955 @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') | |
958 @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') | |
1030 even the step of proving a subgoal by assumption. |
1033 even the step of proving a subgoal by assumption. |
1031 |
1034 |
1032 \item @{method fastsimp}, @{method slowsimp}, @{method bestsimp} are |
1035 \item @{method fastsimp}, @{method slowsimp}, @{method bestsimp} are |
1033 like @{method fast}, @{method slow}, @{method best}, respectively, |
1036 like @{method fast}, @{method slow}, @{method best}, respectively, |
1034 but use the Simplifier as additional wrapper. |
1037 but use the Simplifier as additional wrapper. |
|
1038 |
|
1039 \item @{method deepen} works by exhaustive search up to a certain |
|
1040 depth. The start depth is 4 (unless specified explicitly), and the |
|
1041 depth is increased iteratively up to 10. Unsafe rules are modified |
|
1042 to preserve the formula they act on, so that it be used repeatedly. |
|
1043 This method can prove more goals than @{method fast}, but is much |
|
1044 slower, for example if the assumptions have many universal |
|
1045 quantifiers. |
1035 |
1046 |
1036 \end{description} |
1047 \end{description} |
1037 |
1048 |
1038 Any of the above methods support additional modifiers of the context |
1049 Any of the above methods support additional modifiers of the context |
1039 of classical (and simplifier) rules, but the ones related to the |
1050 of classical (and simplifier) rules, but the ones related to the |