src/HOL/HOLCF/Library/Nat_Discrete.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 62175 8ffc4d0e652d
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/Library/Nat_Discrete.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section {* Discrete cpo instance for naturals *}
     6 
     7 theory Nat_Discrete
     8 imports HOLCF
     9 begin
    10 
    11 text {* Discrete cpo instance for @{typ nat}. *}
    12 
    13 instantiation nat :: discrete_cpo
    14 begin
    15 
    16 definition below_nat_def:
    17   "(x::nat) \<sqsubseteq> y \<longleftrightarrow> x = y"
    18 
    19 instance proof
    20 qed (rule below_nat_def)
    21 
    22 end
    23 
    24 text {*
    25   TODO: implement a command to automate discrete predomain instances.
    26 *}
    27 
    28 instantiation nat :: predomain
    29 begin
    30 
    31 definition
    32   "(liftemb :: nat u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
    33 
    34 definition
    35   "(liftprj :: udom u \<rightarrow> nat u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
    36 
    37 definition
    38   "liftdefl \<equiv> (\<lambda>(t::nat itself). LIFTDEFL(nat discr))"
    39 
    40 instance proof
    41   show "ep_pair liftemb (liftprj :: udom u \<rightarrow> nat u)"
    42     unfolding liftemb_nat_def liftprj_nat_def
    43     apply (rule ep_pair_comp)
    44     apply (rule ep_pair_u_map)
    45     apply (simp add: ep_pair.intro)
    46     apply (rule predomain_ep)
    47     done
    48   show "cast\<cdot>LIFTDEFL(nat) = liftemb oo (liftprj :: udom u \<rightarrow> nat u)"
    49     unfolding liftemb_nat_def liftprj_nat_def liftdefl_nat_def
    50     apply (simp add: cast_liftdefl cfcomp1 u_map_map)
    51     apply (simp add: ID_def [symmetric] u_map_ID)
    52     done
    53 qed
    54 
    55 end
    56 
    57 end