普通常量定义与 lambda 常量定义

Question

我有这两个定义。为什么他们展开不同？我如何证明 "oops"-ed 引理？（一般来说，在 Isabelle 中，这两个定义在内部有什么区别？）

（请不要引导我访问外部链接，因为我通常会被那里的信息淹没。）

  definition "f x y = x+y"
  definition "g ≡ λx y. x+y"

  value "f 1 2" (* "1 + (1 + 1)" :: "'a" *)
  value "g 1 2" (* "1 + (1 + 1)" :: "'a" *)

  value "f 1"   (* "op + 1" :: "'a ⇒ 'a" *)
  value "g 1"   (* "op + 1" :: "'a ⇒ 'a" *)

  value "f"     (* "op +" :: "'a ⇒ 'a ⇒ 'a" *)
  value "g"     (* "op +" :: "'a ⇒ 'a ⇒ 'a" *)


  lemma "f x y≡g x y" 
    apply (simp add:f_def g_def)
  done 

  lemma "f x ≡g x"
    apply (simp add:f_def g_def)
    (* f x ≡ op + x *)
  oops

  lemma "f ≡ g"
    apply (simp add:f_def g_def)
    (* f ≡ op + *)
  oops

Answer 1

左边带有显式参数的定义（如 f x y = x + y）和右边带有 lambda 的定义（如 g = (%x y. x + y)）之间的区别在于你从中得到了什么样的定义方程.

前者为

f_def: "f ?x ?y = ?x + ?y"

（即，如果 f 的所有参数都存在，则此等式 仅适用 ，因此它既不适用于单独的 f 也不适用于 f部分应用 f x，例如）和后者

g_def: "g = op +"

(其中 op + 只是 %x y. x + y 的语法糖；请注意，与前者相反，此等式适用于 every 出现g 随便）。

有两种常用技术可用于处理部分应用函数与具有显式参数列表的函数。

属性 [abs_def] 将带参数的等式转换为带 lambda 的等式。例如，f_def [abs_def] 结果为 f = op +。
引理 ext（对于 外延性）显式地向函数之间的方程添加参数。
```
ext: "(!!x. ?f x = ?g x) ⟹ ?f = ?g"
```

对于您的引理，这两种技术中的任何一种都足够了。在您的证明尝试中将 [abs_def] 添加到每次出现的 f_def 或执行以下操作。

lemma "f x = g x"
apply (intro ext)
apply (simp add: f_def g_def)
done

lemma "f = g"
apply (intro ext)
apply (simp add: f_def g_def)
done

其中 intro 尽可能频繁地应用 ext（由函数类型决定）。

注意我在上面的证明中使用了HOL等式（op =）而不是纯等式（op ≡）。虽然两者在逻辑上是等价的，但引理 ext 仅适用于前者。作为一般规则：对于 Isabelle/HOL 尽可能坚持 op =。

普通常量定义与 lambda 常量定义

Normal constant definition versus lambda constant definition

lambda

isabelle

theorem-proving