products/sources/formale sprachen/Isabelle/HOL/Quotient_Examples/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: _CoqProject   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.2 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff