Isabelle's automatic solver does not find the proper theorem

Question

After stating

theorem "2=2"

Isabelle suggests the following:

proof (prove)
goal (1 subgoal):
 1. 2 = 2 
Auto solve_direct: the current goal can be solved directly with
  BNF_Composition.DEADID.map_ident: ?t = ?t
  BNF_Composition.DEADID.rel_refl: ?x = ?x
  BNF_Composition.DEADID.rel_refl_strong: ?x = ?x
  Basic_BNF_LFPs.xtor_rel: ?R (Basic_BNF_LFPs.xtor ?x) (Basic_BNF_LFPs.xtor ?y) = ?R ?x ?y
  Basic_BNF_LFPs.xtor_set: ?f (Basic_BNF_LFPs.xtor ?x) = ?f ?x

but it does not find the obvious HOL.refl which is more elegant for this.

Why is this? Why the solver comes up with these arcane long identifiers only?

Answer 1

The solve_direct method has a default limit of 5 solutions. You can change it with:

 declare [[solve_direct_max_solutions=1000]] 

Then you will get the following output:

Auto solve_direct: the current goal can be solved directly with
BNF_Composition.DEADID.map_ident: ?t = ?t
BNF_Composition.DEADID.rel_refl: ?x = ?x
BNF_Composition.DEADID.rel_refl_strong: ?x = ?x
Basic_BNF_LFPs.xtor_rel: ?R (Basic_BNF_LFPs.xtor ?x) (Basic_BNF_LFPs.xtor ?y) = ?R ?x ?y
Basic_BNF_LFPs.xtor_set: ?f (Basic_BNF_LFPs.xtor ?x) = ?f ?x
Complete_Lattices.Inf.INF_id_eq: ?Inf (id ` ?A) = ?Inf ?A
Complete_Lattices.Inf.INF_identity_eq: ?Inf ((λx. x) ` ?A) = ?Inf ?A
Complete_Lattices.Inf.INF_image: ?Inf (?g ` ?f ` ?A) = ?Inf ((?g ∘ ?f) ` ?A)
Complete_Lattices.Sup.SUP_id_eq: ?Sup (id ` ?A) = ?Sup ?A
Complete_Lattices.Sup.SUP_identity_eq: ?Sup ((λx. x) ` ?A) = ?Sup ?A
Complete_Lattices.Sup.SUP_image: ?Sup (?g ` ?f ` ?A) = ?Sup ((?g ∘ ?f) ` ?A)
HOL.refl: ?t = ?t
SMT.z3_rule(160): ?t = ?t