products/sources/formale Sprachen/Isabelle/HOL/TLA/Memory/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: latex.xml   Sprache: Isabelle

Original von: 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

¤ Dauer der Verarbeitung: 0.16 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