Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/Tools/Function/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 10 kB

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.0 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.