伊莎贝尔证明翻译问题

Question

我定义了几个这样的翻译：

consts
  "time" :: "i"
  "sig" :: "i ⇒ i"
  "BaseChTy" :: "i"

syntax
  "time" :: "i"
  "sig" :: "i ⇒ i"
translations
  "time" ⇌ "CONST int"
  "sig(A)" ⇌ "CONST int → A"

那么，我想证明这样一个定理：

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"

应该是一个很简单的定理，应该用定理Pi_mono一步证明：

thm Pi_mono
?B ⊆ ?C ⟹ ?A → ?B ⊆ ?A → ?C

所以我这样做了：

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"

apply(drule Pi_mono[of _ _ "time"])
(*Output:
goal (1 subgoal):
 1. sig(A) ⊆ sig(B) ⟹ sig(A) ⊆ sig(B)
*)

apply(simp)
(*Output:
Failed ...
*)

既然前提已经和目标一样了，应该马上证明，但是没有。我可以知道我在翻译定义中做错了什么吗？我试图将定理更改为：

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ (time → A) ⊆ (time → B)"
(*Output:
goal (1 subgoal):
 1. A ⊆ B ⟹ sig(A) ⊆ sig(B)
*)

apply(drule Pi_mono[of _ _ "time"])
(*Output:
goal (1 subgoal):
 1. sig(A) ⊆ sig(B) ⟹ sig(A) ⊆ sig(B)
*)

apply(simp)
(*Output:
Success ...
*)

然后马上就可以了，但是翻译应该不会是一样的吧？

更新：感谢 Mathias Fleury 的回复，我试图做一个简化的跟踪，它显示了这样的东西：

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"
using [[show_sorts]] apply(drule Pi_mono[of _ _ "time"])
using [[simp_trace]] apply(simp)
oops

(*
Output:
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
sig(A::i) ⊆ sig(B::i) ⟹ sig(A) ⊆ sig(B) 
[1]Adding rewrite rule "??.unknown":
sig(A::i) ⊆ sig(B::i) ≡ True 
*)

而 时间 -> A 版本显示：

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ time → A ⊆ time → B"
using [[show_sorts]] apply(drule Pi_mono[of _ _ "time"])
using [[simp_trace]] apply(simp)
oops

(*
Output:
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
sig(A::i) ⊆ sig(B::i) ⟹ sig(A) ⊆ sig(B) 
[1]Adding rewrite rule "??.unknown":
sig(A::i) ⊆ sig(B::i) ≡ True 
[1]Applying instance of rewrite rule "??.unknown":
sig(A::i) ⊆ sig(B::i) ≡ True 
[1]Rewriting:
sig(A::i) ⊆ sig(B::i) ≡ True
*)

为什么这次的版本可以应用rewrite rule的实例继续证明，而原来的却不行？

Answer 1

感谢您在评论中提到的导入（感谢），我可以重现该问题。问题是翻译，你需要做一些像

syntax
  "sig" :: "i ⇒ i" (‹sig(_)›)
translations
  "sig(A)" == "CONST int → A"

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"
  apply(rule Pi_mono)
  apply assumption
  done

只是为了扩展我的评论并解释我是如何发现问题出在翻译上的。我看了统一失败：

theorem ⟦ A ⊆ B ⟧ ⟹ time → A ⊆ time → B
  supply[[unify_trace_failure]]
   apply (rule PI_mono)

错误信息表明sig和Pi不统一。这已经很奇怪了。为了确定问题出在翻译上，我查看了底层术语：

ML ‹@{print}@{term ‹sig(A)›}›

它显示了基础术语，我们可以看到翻译不起作用，我查看了库中的其他翻译来解决问题。

伊莎贝尔证明翻译问题

Isabelle proving with translation issue

isabelle