header {* Example of lifting definitions with the lifting infrastructure *}

theory Lift_Set

imports Main

begin

definition set where "set = (UNIV :: ('a => bool) set)"

typedef 'a set = "set :: ('a => bool) set"

morphisms member Set

unfolding set_def by auto

setup_lifting type_definition_set[unfolded set_def]

text {* Now, we can employ lift_definition to lift definitions. *}

lift_definition empty :: "'a set" is "bot :: 'a => bool" done

term "Lift_Set.empty"

thm Lift_Set.empty_def

lift_definition insert :: "'a => 'a set => 'a set" is "λ x P y. y = x ∨ P y" done

term "Lift_Set.insert"

thm Lift_Set.insert_def

export_code empty insert in SML

end