|
(* Title: HOL/Quotient_Examples/Lift_Set.thy
Author: Lukas Bulwahn and Ondrej Kuncar
*)
section \<open>Example of lifting definitions with the lifting infrastructure\<close>
theory Lift_Set
imports Main
begin
definition set where "set = (UNIV :: ('a \ bool) set)"
typedef 'a set = "set :: ('a \<Rightarrow> bool) set"
morphisms member Set
unfolding set_def by (rule UNIV_witness)
setup_lifting type_definition_set[unfolded set_def]
text \<open>Now, we can employ lift_definition to lift definitions.\<close>
lift_definition empty :: "'a set" is "bot :: 'a \ bool" .
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" .
term "Lift_Set.insert"
thm Lift_Set.insert_def
export_code empty insert in SML file_prefix set
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
