theory Find
imports Main
begin
section \Find theorems with @{command find_theorems}\
text \
Theorems can be searched by name where \*\ wildcards are allowed.
One of the theorems found with the query below is @{thm gauss_sum_nat}.
\
find_theorems name: "gau*"
text \
You can also search theorems by specifying an arbitrary number of patterns.
Patterns are allowed to contain wildcards (\*\) constants, schematic variables, and types.
It is also possible to negate a pattern by prefixing it with a \-\.
If a negated pattern occurs in a theorem, it will not be considered by the search.
\
find_theorems "finite (?A::'a rel)"
find_theorems "finite _ \ _" "insert _ _" -"card _"
find_theorems "finite ?A \ finite ?B \ _ (?A \ ?B)"
text \
In addition to patterns, we can take the goal state into account to search for theorems.
The example below uses \intro\ to search for introduction rules that solve the current goal.
For the given goal, @{command find_theorems} finds the lemma @{thm bij_betw_byWitness} which we
instantiate accordingly.
Then, we solve the the first two subgoals with @{method simp_all}.
This leaves us with two subgoals: @{prop \(\x. x + 1) ` \ \ \\} and
@{prop \(\x. x - 1) ` \ \ \\}.
Searching with intro returns a lot of theorems since @{verbatim \\\} often occurs in the
conclusion of theorems.
To filter out irrelevant theorems, we pass the goal as a pattern with the appropriate wildcards.
Then, @{command find_theorems} gives us the lemma @{thm image_subsetI} with which we can solve the
remaining goals.
In addition to \intro\, there are also \elim\, \dest\, and \solves\ which work analogously.
\
lemma "bij_betw (\x. x + 1) \ \"
find_theorems intro
apply(intro bij_betw_byWitness[where ?f'="\x. x - 1"])
apply(simp_all)
find_theorems intro
find_theorems intro "_ ` _ \ _"
apply(simp_all add: image_subsetI)
done
text \
To search for theorems that simplify a given term, one can pass \simp\ and a term to
@{command find_theorems}.
In the example below, @{command find_theorems} returns the lemma @{thm rev_rev_ident} with which
we can rewrite @{term \rev (rev xs)\} to @{term \xs\}.
\
find_theorems simp: "rev (rev _)"
section \Find constants with @{command find_consts}\
text \
Finding constants (e.g. functions or definitions) can be done with the @{command find_consts}.
As with @{command find_theorems}, you can search for constants by name as seen below.
\
find_consts name: metric
text \
Perhaps more useful than searching for constants by name, it is possible to search for them by
type.
The default search returns all constants which contain the given type pattern.
If you are only interested in exact matches, then you can use the \strict\ annotation.
The example below illustrates this behaviour: the first search returns functions
@{term_type List.replicate} while the second only returns @{term_type List.subseqs}
(and some functions from @{theory HOL.Quickcheck_Narrowing}).
\
find_consts "'a \ 'a list"
find_consts strict: "'a \ 'a list"
text \
We can also use wildcards and negated patterns.
\
find_consts strict: "_ \ 'a list \ _ list"
find_consts strict: "_ \ 'a list \ _ list" -"('a \ 'b) list"
text \
Finally, type variables can also have class constraints.
\
find_consts "('a::ord) list \ ('a::ord) list"
end