Isabelle order type-class关于lambda表达式

Question

我在Isabelle的标准库中发现了这个表达式，并试图查看value对它的处理

value "(λ x::bool . ¬x) ≤ (λ x . x)"

输出False。这里的≤是什么意思?理想情况下，我在哪里可以找到它的确切的instantiation?当我按Ctrl+单击lambda符号时，jEdit不会带我去任何地方。λ是元逻辑的一部分吗?它在哪里定义?

Answer 1

这个和其他很多东西都是在Main库中的Lattices.thy理论中定义的

https://isabelle.in.tum.de/library/HOL/HOL/Lattices.html

subsection ‹Lattice on <^typ>‹_ ⇒ _››
instantiation "fun" :: (type, semilattice_sup) semilattice_sup
begin
definition "f ⊔ g = (λx. f x ⊔ g x)"
lemma sup_apply [simp, code]: "(f ⊔ g) x = f x ⊔ g x"
by (simp add: sup_fun_def)
instance
by standard (simp_all add: le_fun_def)
end