src/HOLCF/Powerdomains.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 39989 ad60d7311f43
child 40216 366309dfaf60
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      HOLCF/Powerdomains.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Powerdomains *}
     6 
     7 theory Powerdomains
     8 imports ConvexPD Domain
     9 begin
    10 
    11 lemma isodefl_upper:
    12   "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
    13 apply (rule isodeflI)
    14 apply (simp add: cast_upper_defl cast_isodefl)
    15 apply (simp add: emb_upper_pd_def prj_upper_pd_def)
    16 apply (simp add: upper_map_map)
    17 done
    18 
    19 lemma isodefl_lower:
    20   "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
    21 apply (rule isodeflI)
    22 apply (simp add: cast_lower_defl cast_isodefl)
    23 apply (simp add: emb_lower_pd_def prj_lower_pd_def)
    24 apply (simp add: lower_map_map)
    25 done
    26 
    27 lemma isodefl_convex:
    28   "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
    29 apply (rule isodeflI)
    30 apply (simp add: cast_convex_defl cast_isodefl)
    31 apply (simp add: emb_convex_pd_def prj_convex_pd_def)
    32 apply (simp add: convex_map_map)
    33 done
    34 
    35 subsection {* Domain package setup for powerdomains *}
    36 
    37 setup {*
    38   fold Domain_Isomorphism.add_type_constructor
    39     [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
    40         @{thm DEFL_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
    41           @{thm deflation_upper_map}),
    42 
    43      (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
    44         @{thm DEFL_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
    45           @{thm deflation_lower_map}),
    46 
    47      (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
    48         @{thm DEFL_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
    49           @{thm deflation_convex_map})]
    50 *}
    51 
    52 end