Quelle Lift_Set.thy Sprache: 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

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.