my forest
isa: proof methods
+38
-10
+6
-10
trees/isa/isa-002N.tree
+6
-10
trees/isa/isa-002N.tree
···
19
19
\transclude{isa-002H}
20
20
\transclude{isa-002I}
21
21
\transclude{isa-002J}
22
-
\ul{
23
-
\li{safe vs unsafe rules}
24
-
\li{intro, elim, clarify, blast, (fast,slow,best)}
25
-
\li{automation: clarsimp, auto, fastforce (slowsimp, bestsimp), force}
26
-
\li{sledgehammer, try, find_theorems}
27
-
\li{clarify, clarsimp}
28
-
\li{structured proofs}
29
-
\li{calculational proofs}
30
-
\li{examples examples examples}
31
-
}
22
+
\transclude{isa-002P}
23
+
\transclude{isa-002O}
24
+
\transclude{isa-002Q}
25
+
\transclude{isa-002R}
26
+
\transclude{isa-002S}
27
+
\transclude{isa-002T}
+4
trees/isa/isa-002O.tree
+4
trees/isa/isa-002O.tree
···
1
+
\date{2025-12-05T00:59:21Z}
2
+
\author{liamoc}
3
+
\title{Safe vs Unsafe Rules}
4
+
\p{Rules such as \code{conjI}, \code{impI}, or \code{disjE} that cannot change a \em{provable} goal into \em{unprovable} goal(s) are called \em{safe}. Isabelle's automation strategies like safe rules because they can apply them without fear, or the need for backtracking. You can mark a rule as safe by marking it \code{[intro!]} or \code{[elim!]}. This can also be done locally when invoking methods like [[isa-002P]].}
+7
trees/isa/isa-002P.tree
+7
trees/isa/isa-002P.tree
···
1
+
\date{2025-12-05T01:02:28Z}
2
+
\author{liamoc}
3
+
\taxon{Proof Method}
4
+
\title{\code{blast}, \code{fast}, \code{slow}, and \code{best}}
5
+
\p{\code{blast} is a method for \em{automatic} classical first-order reasoning, based on a tableaux prover. \code{apply blast} attempts a thorough search using sets of \code{intro} and \code{elim} rules. Like [[isa-001H]], rules can be annotated with \code{ [intro] } and \code{[elim]} annotations, or they can be passed locally to \code{blast} (i.e. \code{apply (blast intro: nandI1 nandI2 elim: nandE)})
6
+
}
7
+
\p{ The methods \code{fast}, \code{slow}, and \code{best} use a different classical proof search engine than \code{blast}, each with a different proof search strategy. \code{fast} performs a quick, depth-bounded search, and is generally faster. \code{slow} is a more exhaustive search and more backtracking, and \code{best} performs a best-first search strategy using a heuristic based on the size of the goal. In general, if \code{fast} or \code{blast} can solve your goal, it will be the most efficient at solving it, whereas \code{slow} and \code{best} are only used if no other automated technique works.}
+5
trees/isa/isa-002Q.tree
+5
trees/isa/isa-002Q.tree
···
1
+
\date{2025-12-05T03:15:07Z}
2
+
\author{liamoc}
3
+
\taxon{Proof Method}
4
+
\title{\code{safe} and \code{clarify}}
5
+
\p{The method \code{safe} applies only [\em{safe}](isa-002O) rules to the current goal. The method \code{clarify} is similar, but it only applies [\em{safe}](isa-002O) rules that \em{do not split the goal into multiple subgoals}. Like [\code{blast} etc.](isa-002P), rules can be added to these methods with \code{intro!:} etc.}
+5
trees/isa/isa-002R.tree
+5
trees/isa/isa-002R.tree
···
1
+
\date{2025-12-05T03:15:07Z}
2
+
\author{liamoc}
3
+
\taxon{Proof Method}
4
+
\title{\code{clarsimp}, \code{slowsimp}, \code{bestsimp} and \code{fastforce}}
5
+
\p{\code{clarsimp} the combination of [clarify](isa-002Q) and [simp](isa-001H), and is very useful when doing exploratory proving. \code{slowsimp} is the combination of [slow](isa-002P) and [simp](isa-001H). \code{bestsimp} is the combination of [best](isa-002P) and [simp](isa-001H). The combination of [fast](isa-002P) and [simp](isa-001H) is, for inexplicable reasons, called \code{fastforce}.}
+6
trees/isa/isa-002S.tree
+6
trees/isa/isa-002S.tree
···
1
+
\date{2025-12-05T03:15:07Z}
2
+
\author{liamoc}
3
+
\taxon{Proof Method}
4
+
\title{\code{force} and \code{auto}}
5
+
\p{\code{force} is a very thorough proof search that can often solve goals other methods can't. It can be thought of as a very thorough version of [\code{blast}](isa-002P) combined with [\code{simp}](isa-001H). The method \code{auto}, by contrast, is a more lightweight search that attempts to simulateneously solve \em{all} goals, rather than just the first one. Unlike the other automated methods, \code{auto} will leave behind goals that it is unable to prove.}
6
+
\p{Because the behaviour of \code{auto} differs greatly between Isabelle versions and is very sensitive to what theories are loaded, it's considered bad style to use \code{auto} as anything but the \em{final} step in a proof, but it can nonetheless be useful to see what goals \code{auto} outputs to see where it's getting stuck.}
+5
trees/isa/isa-002T.tree
+5
trees/isa/isa-002T.tree
···
1
+
\date{2025-12-05T03:27:40Z}
2
+
\author{liamoc}
3
+
\title{\code{try} and the famous Isabelle sledgehammer.}
4
+
\p{Isabelle includes a feature called the \em{sledgehammer} that invokes external proof search procedures (such as SMT solvers) and provides them with lemmas that appear to be relevant. If the tools find a proof, it can often replay them in Isabelle's proof kernel, giving an Isabelle proof that matches what the external proof tool found. }
5
+
\p{To invoke this procedure on a goal, searching automatically for related lemmas, type the word \code{try} in an open subgoal.}