src/Pure/ex/Def_Examples.thy

Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique

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

Some examples for primitive definitions.
*)

theory Def_Examples
  imports Def
begin

section \<open>Global definitions\<close>

def "I x \<equiv> x"
def "K x y \<equiv> x"
def "S x y z \<equiv> (x z) (y z)"

lemma "I (I x) \<equiv> x"
  by simp

lemma "K a x \<equiv> K a y"
  by simp

lemma "S K K \<equiv> I"
  by simp


section \<open>Locale definitions\<close>

locale const =
  fixes a :: 'a
begin

def "fun b \<equiv> a"

lemma "fun x \<equiv> fun y"
  by simp

end

lemma "const.fun a x \<equiv> const.fun a y"
  by simp

end