automation - 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更优雅的显而易见的东西。

为什么是这样？为什么求解器只提供这些神秘的长标识符？

标签： automationisabelle

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