src/HOL/HOLCF/Powerdomains.thy
author wenzelm
Mon, 19 Jan 2015 20:39:01 +0100
changeset 59409 b7cfe12acf2e
parent 58880 0baae4311a9f
child 62175 8ffc4d0e652d
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41436
diff changeset
     1
(*  Title:      HOL/HOLCF/Powerdomains.thy
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
     3
*)
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
     4
58880
0baae4311a9f modernized header;
wenzelm
parents: 42151
diff changeset
     5
section {* Powerdomains *}
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
     6
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
     7
theory Powerdomains
39974
b525988432e9 major reorganization/simplification of HOLCF type classes:
huffman
parents: 39973
diff changeset
     8
imports ConvexPD Domain
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
     9
begin
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
    10
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    11
subsection {* Universal domain embeddings *}
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    12
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    13
definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    14
definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    15
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    16
definition "lower_emb = udom_emb (\<lambda>i. lower_map\<cdot>(udom_approx i))"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    17
definition "lower_prj = udom_prj (\<lambda>i. lower_map\<cdot>(udom_approx i))"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    18
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    19
definition "convex_emb = udom_emb (\<lambda>i. convex_map\<cdot>(udom_approx i))"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    20
definition "convex_prj = udom_prj (\<lambda>i. convex_map\<cdot>(udom_approx i))"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    21
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    22
lemma ep_pair_upper: "ep_pair upper_emb upper_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    23
  unfolding upper_emb_def upper_prj_def
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    24
  by (simp add: ep_pair_udom approx_chain_upper_map)
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    25
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    26
lemma ep_pair_lower: "ep_pair lower_emb lower_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    27
  unfolding lower_emb_def lower_prj_def
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    28
  by (simp add: ep_pair_udom approx_chain_lower_map)
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    29
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    30
lemma ep_pair_convex: "ep_pair convex_emb convex_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    31
  unfolding convex_emb_def convex_prj_def
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    32
  by (simp add: ep_pair_udom approx_chain_convex_map)
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    33
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    34
subsection {* Deflation combinators *}
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    35
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    36
definition upper_defl :: "udom defl \<rightarrow> udom defl"
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    37
  where "upper_defl = defl_fun1 upper_emb upper_prj upper_map"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    38
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    39
definition lower_defl :: "udom defl \<rightarrow> udom defl"
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    40
  where "lower_defl = defl_fun1 lower_emb lower_prj lower_map"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    41
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    42
definition convex_defl :: "udom defl \<rightarrow> udom defl"
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    43
  where "convex_defl = defl_fun1 convex_emb convex_prj convex_map"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    44
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    45
lemma cast_upper_defl:
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    46
  "cast\<cdot>(upper_defl\<cdot>A) = upper_emb oo upper_map\<cdot>(cast\<cdot>A) oo upper_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    47
using ep_pair_upper finite_deflation_upper_map
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    48
unfolding upper_defl_def by (rule cast_defl_fun1)
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    49
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    50
lemma cast_lower_defl:
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    51
  "cast\<cdot>(lower_defl\<cdot>A) = lower_emb oo lower_map\<cdot>(cast\<cdot>A) oo lower_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    52
using ep_pair_lower finite_deflation_lower_map
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    53
unfolding lower_defl_def by (rule cast_defl_fun1)
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    54
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    55
lemma cast_convex_defl:
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    56
  "cast\<cdot>(convex_defl\<cdot>A) = convex_emb oo convex_map\<cdot>(cast\<cdot>A) oo convex_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    57
using ep_pair_convex finite_deflation_convex_map
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    58
unfolding convex_defl_def by (rule cast_defl_fun1)
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    59
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    60
subsection {* Domain class instances *}
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    61
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    62
instantiation upper_pd :: ("domain") "domain"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    63
begin
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    64
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    65
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    66
  "emb = upper_emb oo upper_map\<cdot>emb"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    67
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    68
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    69
  "prj = upper_map\<cdot>prj oo upper_prj"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    70
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    71
definition
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    72
  "defl (t::'a upper_pd itself) = upper_defl\<cdot>DEFL('a)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    73
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    74
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    75
  "(liftemb :: 'a upper_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    76
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    77
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    78
  "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    79
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    80
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41292
diff changeset
    81
  "liftdefl (t::'a upper_pd itself) = liftdefl_of\<cdot>DEFL('a upper_pd)"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    82
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    83
instance proof
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    84
  show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    85
    unfolding emb_upper_pd_def prj_upper_pd_def
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    86
    by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj)
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    87
next
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    88
  show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    89
    unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    90
    by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    91
qed (fact liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def)+
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    92
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    93
end
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    94
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    95
instantiation lower_pd :: ("domain") "domain"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    96
begin
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    97
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
    98
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
    99
  "emb = lower_emb oo lower_map\<cdot>emb"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   100
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   101
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
   102
  "prj = lower_map\<cdot>prj oo lower_prj"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   103
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   104
definition
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   105
  "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   106
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   107
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   108
  "(liftemb :: 'a lower_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   109
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   110
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   111
  "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   112
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   113
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41292
diff changeset
   114
  "liftdefl (t::'a lower_pd itself) = liftdefl_of\<cdot>DEFL('a lower_pd)"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   115
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   116
instance proof
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   117
  show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   118
    unfolding emb_lower_pd_def prj_lower_pd_def
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
   119
    by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj)
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   120
next
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   121
  show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   122
    unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   123
    by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   124
qed (fact liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def)+
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   125
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   126
end
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   127
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   128
instantiation convex_pd :: ("domain") "domain"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   129
begin
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   130
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   131
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
   132
  "emb = convex_emb oo convex_map\<cdot>emb"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   133
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   134
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
   135
  "prj = convex_map\<cdot>prj oo convex_prj"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   136
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   137
definition
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   138
  "defl (t::'a convex_pd itself) = convex_defl\<cdot>DEFL('a)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   139
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   140
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   141
  "(liftemb :: 'a convex_pd u \<rightarrow> udom u) = u_map\<cdot>emb"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   142
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   143
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   144
  "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj"
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   145
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   146
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41292
diff changeset
   147
  "liftdefl (t::'a convex_pd itself) = liftdefl_of\<cdot>DEFL('a convex_pd)"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   148
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   149
instance proof
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   150
  show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   151
    unfolding emb_convex_pd_def prj_convex_pd_def
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41289
diff changeset
   152
    by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj)
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   153
next
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   154
  show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   155
    unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   156
    by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   157
qed (fact liftemb_convex_pd_def liftprj_convex_pd_def liftdefl_convex_pd_def)+
41289
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   158
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   159
end
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   160
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   161
lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   162
by (rule defl_upper_pd_def)
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   163
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   164
lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   165
by (rule defl_lower_pd_def)
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   166
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   167
lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   168
by (rule defl_convex_pd_def)
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   169
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   170
subsection {* Isomorphic deflations *}
f655912ac235 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents: 40774
diff changeset
   171
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   172
lemma isodefl_upper:
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39974
diff changeset
   173
  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   174
apply (rule isodeflI)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39974
diff changeset
   175
apply (simp add: cast_upper_defl cast_isodefl)
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   176
apply (simp add: emb_upper_pd_def prj_upper_pd_def)
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   177
apply (simp add: upper_map_map)
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   178
done
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   179
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   180
lemma isodefl_lower:
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39974
diff changeset
   181
  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   182
apply (rule isodeflI)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39974
diff changeset
   183
apply (simp add: cast_lower_defl cast_isodefl)
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   184
apply (simp add: emb_lower_pd_def prj_lower_pd_def)
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   185
apply (simp add: lower_map_map)
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   186
done
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   187
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   188
lemma isodefl_convex:
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39974
diff changeset
   189
  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   190
apply (rule isodeflI)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39974
diff changeset
   191
apply (simp add: cast_convex_defl cast_isodefl)
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   192
apply (simp add: emb_convex_pd_def prj_convex_pd_def)
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   193
apply (simp add: convex_map_map)
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   194
done
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   195
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   196
subsection {* Domain package setup for powerdomains *}
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   197
40216
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents: 39989
diff changeset
   198
lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents: 39989
diff changeset
   199
lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents: 39989
diff changeset
   200
lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents: 39989
diff changeset
   201
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents: 39989
diff changeset
   202
lemmas [domain_deflation] =
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents: 39989
diff changeset
   203
  deflation_upper_map deflation_lower_map deflation_convex_map
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents: 39989
diff changeset
   204
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   205
setup {*
40737
2037021f034f remove map function names from domain package theory data
huffman
parents: 40487
diff changeset
   206
  fold Domain_Take_Proofs.add_rec_type
2037021f034f remove map function names from domain package theory data
huffman
parents: 40487
diff changeset
   207
    [(@{type_name "upper_pd"}, [true]),
2037021f034f remove map function names from domain package theory data
huffman
parents: 40487
diff changeset
   208
     (@{type_name "lower_pd"}, [true]),
2037021f034f remove map function names from domain package theory data
huffman
parents: 40487
diff changeset
   209
     (@{type_name "convex_pd"}, [true])]
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   210
*}
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   211
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents:
diff changeset
   212
end