|
(* 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)
¤
|
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.
|
