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


products/sources/formale Sprachen/Isabelle/HOL/HOLCF/Library/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 1 kB

Quelle Nat_Discrete.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/Library/Nat_Discrete.thy
    Author:     Brian Huffman
*)

section \<open>Discrete cpo instance for naturals\<close>

theory Nat_Discrete
imports HOLCF
begin

text \<open>Discrete cpo instance for \<^typ>\<open>nat\<close>.\<close>

instantiation nat :: discrete_cpo
begin

definition below_nat_def:
  "(x::nat) \ y \ x = y"

instance proof
qed (rule below_nat_def)

end

text \<open>
  TODO: implement a command to automate discrete predomain instances.
\<close>

instantiation nat :: predomain
begin

definition
  "(liftemb :: nat u \ udom u) \ liftemb oo u_map\(\ x. Discr x)"

definition
  "(liftprj :: udom u \ nat u) \ u_map\(\ y. undiscr y) oo liftprj"

definition
  "liftdefl \ (\(t::nat itself). LIFTDEFL(nat discr))"

instance proof
  show "ep_pair liftemb (liftprj :: udom u \ nat u)"
    unfolding liftemb_nat_def liftprj_nat_def
    apply (rule ep_pair_comp)
    apply (rule ep_pair_u_map)
    apply (simp add: ep_pair.intro)
    apply (rule predomain_ep)
    done
  show "cast\LIFTDEFL(nat) = liftemb oo (liftprj :: udom u \ nat u)"
    unfolding liftemb_nat_def liftprj_nat_def liftdefl_nat_def
    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
    apply (simp add: ID_def [symmetric] u_map_ID)
    done
qed

end

end

quality96%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

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.