src/HOL/HOLCF/Powerdomains.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62175 8ffc4d0e652d
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Powerdomains.thy
huffman@35473
     2
    Author:     Brian Huffman
huffman@35473
     3
*)
huffman@35473
     4
wenzelm@62175
     5
section \<open>Powerdomains\<close>
huffman@35473
     6
huffman@35473
     7
theory Powerdomains
huffman@39974
     8
imports ConvexPD Domain
huffman@35473
     9
begin
huffman@35473
    10
wenzelm@62175
    11
subsection \<open>Universal domain embeddings\<close>
huffman@41289
    12
huffman@41290
    13
definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))"
huffman@41290
    14
definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))"
huffman@41289
    15
huffman@41290
    16
definition "lower_emb = udom_emb (\<lambda>i. lower_map\<cdot>(udom_approx i))"
huffman@41290
    17
definition "lower_prj = udom_prj (\<lambda>i. lower_map\<cdot>(udom_approx i))"
huffman@41289
    18
huffman@41290
    19
definition "convex_emb = udom_emb (\<lambda>i. convex_map\<cdot>(udom_approx i))"
huffman@41290
    20
definition "convex_prj = udom_prj (\<lambda>i. convex_map\<cdot>(udom_approx i))"
huffman@41289
    21
huffman@41290
    22
lemma ep_pair_upper: "ep_pair upper_emb upper_prj"
huffman@41290
    23
  unfolding upper_emb_def upper_prj_def
huffman@41290
    24
  by (simp add: ep_pair_udom approx_chain_upper_map)
huffman@41289
    25
huffman@41290
    26
lemma ep_pair_lower: "ep_pair lower_emb lower_prj"
huffman@41290
    27
  unfolding lower_emb_def lower_prj_def
huffman@41290
    28
  by (simp add: ep_pair_udom approx_chain_lower_map)
huffman@41289
    29
huffman@41290
    30
lemma ep_pair_convex: "ep_pair convex_emb convex_prj"
huffman@41290
    31
  unfolding convex_emb_def convex_prj_def
huffman@41290
    32
  by (simp add: ep_pair_udom approx_chain_convex_map)
huffman@41289
    33
wenzelm@62175
    34
subsection \<open>Deflation combinators\<close>
huffman@41289
    35
huffman@41289
    36
definition upper_defl :: "udom defl \<rightarrow> udom defl"
huffman@41290
    37
  where "upper_defl = defl_fun1 upper_emb upper_prj upper_map"
huffman@41289
    38
huffman@41289
    39
definition lower_defl :: "udom defl \<rightarrow> udom defl"
huffman@41290
    40
  where "lower_defl = defl_fun1 lower_emb lower_prj lower_map"
huffman@41289
    41
huffman@41289
    42
definition convex_defl :: "udom defl \<rightarrow> udom defl"
huffman@41290
    43
  where "convex_defl = defl_fun1 convex_emb convex_prj convex_map"
huffman@41289
    44
huffman@41289
    45
lemma cast_upper_defl:
huffman@41290
    46
  "cast\<cdot>(upper_defl\<cdot>A) = upper_emb oo upper_map\<cdot>(cast\<cdot>A) oo upper_prj"
huffman@41290
    47
using ep_pair_upper finite_deflation_upper_map
huffman@41289
    48
unfolding upper_defl_def by (rule cast_defl_fun1)
huffman@41289
    49
huffman@41289
    50
lemma cast_lower_defl:
huffman@41290
    51
  "cast\<cdot>(lower_defl\<cdot>A) = lower_emb oo lower_map\<cdot>(cast\<cdot>A) oo lower_prj"
huffman@41290
    52
using ep_pair_lower finite_deflation_lower_map
huffman@41289
    53
unfolding lower_defl_def by (rule cast_defl_fun1)
huffman@41289
    54
huffman@41289
    55
lemma cast_convex_defl:
huffman@41290
    56
  "cast\<cdot>(convex_defl\<cdot>A) = convex_emb oo convex_map\<cdot>(cast\<cdot>A) oo convex_prj"
huffman@41290
    57
using ep_pair_convex finite_deflation_convex_map
huffman@41289
    58
unfolding convex_defl_def by (rule cast_defl_fun1)
huffman@41289
    59
wenzelm@62175
    60
subsection \<open>Domain class instances\<close>
huffman@41289
    61
huffman@41292
    62
instantiation upper_pd :: ("domain") "domain"
huffman@41289
    63
begin
huffman@41289
    64
huffman@41289
    65
definition
huffman@41290
    66
  "emb = upper_emb oo upper_map\<cdot>emb"
huffman@41289
    67
huffman@41289
    68
definition
huffman@41290
    69
  "prj = upper_map\<cdot>prj oo upper_prj"
huffman@41289
    70
huffman@41289
    71
definition
huffman@41289
    72
  "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
huffman@41289
    73
huffman@41289
    74
definition
huffman@41292
    75
  "(liftemb :: 'a upper_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
huffman@41289
    76
huffman@41289
    77
definition
huffman@41292
    78
  "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj"
huffman@41289
    79
huffman@41292
    80
definition
huffman@41436
    81
  "liftdefl (t::'a upper_pd itself) = liftdefl_of\<cdot>DEFL('a upper_pd)"
huffman@41292
    82
huffman@41292
    83
instance proof
huffman@41289
    84
  show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
huffman@41289
    85
    unfolding emb_upper_pd_def prj_upper_pd_def
huffman@41290
    86
    by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj)
huffman@41289
    87
next
huffman@41289
    88
  show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
huffman@41289
    89
    unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
huffman@41289
    90
    by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
huffman@41292
    91
qed (fact liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def)+
huffman@41289
    92
huffman@41289
    93
end
huffman@41289
    94
huffman@41292
    95
instantiation lower_pd :: ("domain") "domain"
huffman@41289
    96
begin
huffman@41289
    97
huffman@41289
    98
definition
huffman@41290
    99
  "emb = lower_emb oo lower_map\<cdot>emb"
huffman@41289
   100
huffman@41289
   101
definition
huffman@41290
   102
  "prj = lower_map\<cdot>prj oo lower_prj"
huffman@41289
   103
huffman@41289
   104
definition
huffman@41289
   105
  "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
huffman@41289
   106
huffman@41289
   107
definition
huffman@41292
   108
  "(liftemb :: 'a lower_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
huffman@41289
   109
huffman@41289
   110
definition
huffman@41292
   111
  "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj"
huffman@41289
   112
huffman@41292
   113
definition
huffman@41436
   114
  "liftdefl (t::'a lower_pd itself) = liftdefl_of\<cdot>DEFL('a lower_pd)"
huffman@41292
   115
huffman@41292
   116
instance proof
huffman@41289
   117
  show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
huffman@41289
   118
    unfolding emb_lower_pd_def prj_lower_pd_def
huffman@41290
   119
    by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj)
huffman@41289
   120
next
huffman@41289
   121
  show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
huffman@41289
   122
    unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
huffman@41289
   123
    by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
huffman@41292
   124
qed (fact liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def)+
huffman@41289
   125
huffman@41289
   126
end
huffman@41289
   127
huffman@41292
   128
instantiation convex_pd :: ("domain") "domain"
huffman@41289
   129
begin
huffman@41289
   130
huffman@41289
   131
definition
huffman@41290
   132
  "emb = convex_emb oo convex_map\<cdot>emb"
huffman@41289
   133
huffman@41289
   134
definition
huffman@41290
   135
  "prj = convex_map\<cdot>prj oo convex_prj"
huffman@41289
   136
huffman@41289
   137
definition
huffman@41289
   138
  "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
huffman@41289
   139
huffman@41289
   140
definition
huffman@41292
   141
  "(liftemb :: 'a convex_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
huffman@41289
   142
huffman@41289
   143
definition
huffman@41292
   144
  "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj"
huffman@41289
   145
huffman@41292
   146
definition
huffman@41436
   147
  "liftdefl (t::'a convex_pd itself) = liftdefl_of\<cdot>DEFL('a convex_pd)"
huffman@41292
   148
huffman@41292
   149
instance proof
huffman@41289
   150
  show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
huffman@41289
   151
    unfolding emb_convex_pd_def prj_convex_pd_def
huffman@41290
   152
    by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj)
huffman@41289
   153
next
huffman@41289
   154
  show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
huffman@41289
   155
    unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
huffman@41289
   156
    by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
huffman@41292
   157
qed (fact liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def)+
huffman@41289
   158
huffman@41289
   159
end
huffman@41289
   160
huffman@41289
   161
lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)"
huffman@41289
   162
by (rule defl_upper_pd_def)
huffman@41289
   163
huffman@41289
   164
lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)"
huffman@41289
   165
by (rule defl_lower_pd_def)
huffman@41289
   166
huffman@41289
   167
lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
huffman@41289
   168
by (rule defl_convex_pd_def)
huffman@41289
   169
wenzelm@62175
   170
subsection \<open>Isomorphic deflations\<close>
huffman@41289
   171
huffman@35473
   172
lemma isodefl_upper:
huffman@39989
   173
  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
huffman@35473
   174
apply (rule isodeflI)
huffman@39989
   175
apply (simp add: cast_upper_defl cast_isodefl)
huffman@35473
   176
apply (simp add: emb_upper_pd_def prj_upper_pd_def)
huffman@35473
   177
apply (simp add: upper_map_map)
huffman@35473
   178
done
huffman@35473
   179
huffman@35473
   180
lemma isodefl_lower:
huffman@39989
   181
  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
huffman@35473
   182
apply (rule isodeflI)
huffman@39989
   183
apply (simp add: cast_lower_defl cast_isodefl)
huffman@35473
   184
apply (simp add: emb_lower_pd_def prj_lower_pd_def)
huffman@35473
   185
apply (simp add: lower_map_map)
huffman@35473
   186
done
huffman@35473
   187
huffman@35473
   188
lemma isodefl_convex:
huffman@39989
   189
  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
huffman@35473
   190
apply (rule isodeflI)
huffman@39989
   191
apply (simp add: cast_convex_defl cast_isodefl)
huffman@35473
   192
apply (simp add: emb_convex_pd_def prj_convex_pd_def)
huffman@35473
   193
apply (simp add: convex_map_map)
huffman@35473
   194
done
huffman@35473
   195
wenzelm@62175
   196
subsection \<open>Domain package setup for powerdomains\<close>
huffman@35473
   197
huffman@40216
   198
lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex
huffman@40216
   199
lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID
huffman@40216
   200
lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex
huffman@40216
   201
huffman@40216
   202
lemmas [domain_deflation] =
huffman@40216
   203
  deflation_upper_map deflation_lower_map deflation_convex_map
huffman@40216
   204
wenzelm@62175
   205
setup \<open>
huffman@40737
   206
  fold Domain_Take_Proofs.add_rec_type
huffman@40737
   207
    [(@{type_name "upper_pd"}, [true]),
huffman@40737
   208
     (@{type_name "lower_pd"}, [true]),
huffman@40737
   209
     (@{type_name "convex_pd"}, [true])]
wenzelm@62175
   210
\<close>
huffman@35473
   211
huffman@35473
   212
end