Search code examples
isabelle

Isabelle order type-class on lambda expressions

I found this expression somewhere in Isabelle's standard library and tried to see what value does with it

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

It outputs False. What is the meaning of ≤ here? Ideally, where can I find the exact instantiation of it? When I Ctrl+Click on the lambda symbol, jEdit doesn't take me anywhere. Is λ part of meta logic then? Where is it defined?

Solution

  • This and many other things are defined in Lattices.thy theory in Main library

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

    under the following section.

    
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