See [1] for an example (edit: although this may not be the best example nowadays, see below):
Quoting:
> Consider the conjecture "length(tl xs) <= length xs", which states that the length of a list’s tail (its "cdr") is less than or equal to the length of the entire list.
> Thanks to Vampire, Sledgehammer finds the following proof: by (metis append_Nil2 append_eq_conv_conj drop_eq_Nil drop_tl tl.simps(1))
Those are all the lemmas that were needed to prove the theorem. They were selected completely automatically.
AFAIU the "metis" procedure tries to fit the lemmas together so that they prove the theorem, and I believe the HOL kernel gives high assurance that if "metis" succeeds, then the theorem was proven correctly (but my understanding may be wrong here).
Note that Sledgehammer may even automatically find and return a human-readable proof, which for the example above, it returns something like this:
proof –
have “tl [] = []” by (metis tl.simps(1))
hence “∃u. xs @ u = xs ∧ tl u = []” by (metis append_Nil2)
hence “tl (drop (length xs) xs) = []” by (metis append_eq_conv_conj)
hence “drop (length xs) (tl xs) = []” by (metis drop_tl)
thus “length (tl xs) <= length xs” by (metis drop_eq_Nil)
qed
Edit: That said, note that at least nowadays Isabelle/HOL seems to be able prove the above theorem by simplification alone ("by simp"), so this may not be the best example.
metis is a first-order automated theorem prover. the metis tactic will handle encoding the goal as a first-order problem, using ~just the rules you provide it, invoking actual-metis, and reconstructing a proof (in the kernel logic) from the output proof. so, it is impossible to prove things that are false using the metis tactic (ie, metis is entirely out of the TCB).
re: the simplifier, I feel like it's a bad example because coming up with good simp rules and knowing when to add them and when not to when writing new code in Isabelle/HOL is almost an art.
Quoting:
> Consider the conjecture "length(tl xs) <= length xs", which states that the length of a list’s tail (its "cdr") is less than or equal to the length of the entire list.
> Thanks to Vampire, Sledgehammer finds the following proof: by (metis append_Nil2 append_eq_conv_conj drop_eq_Nil drop_tl tl.simps(1))
Those are all the lemmas that were needed to prove the theorem. They were selected completely automatically.
AFAIU the "metis" procedure tries to fit the lemmas together so that they prove the theorem, and I believe the HOL kernel gives high assurance that if "metis" succeeds, then the theorem was proven correctly (but my understanding may be wrong here).
Note that Sledgehammer may even automatically find and return a human-readable proof, which for the example above, it returns something like this:
Edit: That said, note that at least nowadays Isabelle/HOL seems to be able prove the above theorem by simplification alone ("by simp"), so this may not be the best example.[1] http://people.irisa.fr/Thomas.Genet/ACF/BiblioIsabelle/isabe...