Theory Def_Examples

(*  Title:      Pure/ex/Def_Examples.thy
    Author:     Makarius

Some examples for primitive definitions.
*)

theory Def_Examples
  imports Def
begin

section ‹Global definitions›

def "I x ≡ x"
def "K x y ≡ x"
def "S x y z ≡ (x z) (y z)"

lemma "I (I x) ≡ x"
  by simp

lemma "K a x ≡ K a y"
  by simp

lemma "S K K ≡ I"
  by simp


section ‹Locale definitions›

locale const =
  fixes a :: 'a
begin

def "fun b ≡ a"

lemma "fun x ≡ fun y"
  by simp

end

lemma "const.fun a x ≡ const.fun a y"
  by simp

end