Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Lift_Set.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.