如何在 Isabelle/HOL 项中包含有关变量类型的语句

Question

我有以下简单的 Isabelle/HOL 理论：

theory Max_Of_Two_Integers_Real
  imports Main
    "HOL-Library.Multiset"
    "HOL-Library.Code_Target_Numeral"
    "HOL-Library.Code_Target_Nat"
    "HOL-Library.Code_Abstract_Nat"
begin

definition two_integer_max_case_def :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case_def a b = (case a > b of True ⇒ a | False ⇒ b)"

lemma spec_final:
  fixes a :: nat and b :: nat
  assumes "a > b" (* and "b < a" *)
  shows "two_integer_max_case_def a b = a"
  using assms by (simp add: two_integer_max_case_def_def) 

lemma spec_1:
  fixes a :: nat and b :: nat
  shows "a > b ⟹ two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def) 

lemma spec_2:
  shows " (a ∈ nat set) ∧ (b ∈ nat set) ∧  (a > b) ⟹ two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def)

end

三个引理试图表达和证明相同的陈述，但我正在逐步尝试将信息从假设和修正转移到术语。前 2 个引理是正确的，但第三个（最后一个）引理在语法上失败并显示错误消息：

Type unification failed: Clash of types "_ ⇒ _" and "int"

Type error in application: incompatible operand type

Operator:  nat :: int ⇒ nat
Operand:   set :: ??'a list ⇒ ??'a set

我在这个引理中的目标是将类型信息从补丁移到 term/statement?我如何在术语（内部语法）中声明变量类型？

如果我试图避免 fixes 子句（可能在其中声明变量），也许我应该使用完整的 ForAll 表达式，例如：

lemma spec_final_3:
  shows "∀ a :: nat . ∀ b :: nat . ( (a > b) ⟹ two_integer_max_case_def a b = a)"
  by (simp add: two_integer_max_case_def_def)

但它在语法上也失败了，并显示错误消息：

Inner syntax error: unexpected end of input⌂
Failed to parse prop

所以 - 是否可以直接在术语中包含类型声明（不带 fixes 子句），术语中的 fixes 子句和类型声明之间有什么区别吗？也许这种差异在（半）自动证明期间开始出现，例如，当应用简化策略或其他一些策略时？

Answer 1

nat set 被解释为函数（输入不正确）。自然数集可以表示为UNIV :: nat set。然后，spec_2 读取

lemma spec_2:
  shows "a ∈ (UNIV :: nat set) ∧ b ∈ (UNIV :: nat set) ∧ a > b ⟹
         two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def)

然而，更自然的方法是在 spec_1 中包含类型信息，而不包含 fixes 子句：

lemma spec_1':
  shows "(a :: nat) > (b :: nat) ⟹ two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def)

∀属于HOL，所以在spec_final_3中应该使用HOL蕴涵：

lemma spec_final_3:
  shows "∀ a :: nat. ∀ b :: nat. a > b ⟶ two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def)

spec_1 也可以使用明确的元逻辑限定（和蕴涵）重写，看起来类似于 spec_final_3:

lemma spec_1'':
  shows "⋀ a :: nat. ⋀ b :: nat. a > b ⟹ two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def)

如何在 Isabelle/HOL 项中包含有关变量类型的语句

How to include statement about type of the variable in the Isabelle/HOL term

isabelle