Isabelle 的自动求解器找不到正确的定理

Question

陈述后

theorem "2=2"

伊莎贝尔建议如下：

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

但它没有找到更优雅的明显 HOL.refl。

这是为什么？为什么求解器只给出这些神秘的长标识符？

Answer 1

solve_direct 方法默认限制为 5 个解决方案。您可以更改它：

 declare [[solve_direct_max_solutions=1000]]

然后你会得到如下输出：

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

Isabelle 的自动求解器找不到正确的定理

Isabelle's automatic solver does not find the proper theorem

automation

isabelle