src/HOLCF/Powerdomains.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40487 1320a0747974
child 40737 2037021f034f
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman@35473
     1
(*  Title:      HOLCF/Powerdomains.thy
huffman@35473
     2
    Author:     Brian Huffman
huffman@35473
     3
*)
huffman@35473
     4
huffman@35473
     5
header {* Powerdomains *}
huffman@35473
     6
huffman@35473
     7
theory Powerdomains
huffman@39974
     8
imports ConvexPD Domain
huffman@35473
     9
begin
huffman@35473
    10
huffman@35473
    11
lemma isodefl_upper:
huffman@39989
    12
  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
huffman@35473
    13
apply (rule isodeflI)
huffman@39989
    14
apply (simp add: cast_upper_defl cast_isodefl)
huffman@35473
    15
apply (simp add: emb_upper_pd_def prj_upper_pd_def)
huffman@35473
    16
apply (simp add: upper_map_map)
huffman@35473
    17
done
huffman@35473
    18
huffman@35473
    19
lemma isodefl_lower:
huffman@39989
    20
  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
huffman@35473
    21
apply (rule isodeflI)
huffman@39989
    22
apply (simp add: cast_lower_defl cast_isodefl)
huffman@35473
    23
apply (simp add: emb_lower_pd_def prj_lower_pd_def)
huffman@35473
    24
apply (simp add: lower_map_map)
huffman@35473
    25
done
huffman@35473
    26
huffman@35473
    27
lemma isodefl_convex:
huffman@39989
    28
  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
huffman@35473
    29
apply (rule isodeflI)
huffman@39989
    30
apply (simp add: cast_convex_defl cast_isodefl)
huffman@35473
    31
apply (simp add: emb_convex_pd_def prj_convex_pd_def)
huffman@35473
    32
apply (simp add: convex_map_map)
huffman@35473
    33
done
huffman@35473
    34
huffman@35473
    35
subsection {* Domain package setup for powerdomains *}
huffman@35473
    36
huffman@40216
    37
lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex
huffman@40216
    38
lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID
huffman@40216
    39
lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex
huffman@40216
    40
huffman@40216
    41
lemmas [domain_deflation] =
huffman@40216
    42
  deflation_upper_map deflation_lower_map deflation_convex_map
huffman@40216
    43
huffman@35473
    44
setup {*
huffman@40487
    45
  fold Domain_Take_Proofs.add_map_function
huffman@40487
    46
    [(@{type_name "upper_pd"}, @{const_name upper_map}, [true]),
huffman@40487
    47
     (@{type_name "lower_pd"}, @{const_name lower_map}, [true]),
huffman@40487
    48
     (@{type_name "convex_pd"}, @{const_name convex_map}, [true])]
huffman@35473
    49
*}
huffman@35473
    50
huffman@35473
    51
end