src/HOL/HOLCF/Representable.thy
author wenzelm
Mon, 19 Jan 2015 20:39:01 +0100
changeset 59409 b7cfe12acf2e
parent 58880 0baae4311a9f
child 61169 4de9ff3ea29a
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41437
diff changeset
     1
(*  Title:      HOL/HOLCF/Representable.thy
25903
5e59af604d4f new theory of bifinite domains
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
5e59af604d4f new theory of bifinite domains
huffman
parents:
diff changeset
     3
*)
5e59af604d4f new theory of bifinite domains
huffman
parents:
diff changeset
     4
58880
0baae4311a9f modernized header;
wenzelm
parents: 44781
diff changeset
     5
section {* Representable domains *}
25903
5e59af604d4f new theory of bifinite domains
huffman
parents:
diff changeset
     6
41285
efd23c1d9886 renamed Bifinite.thy to Representable.thy
huffman
parents: 41034
diff changeset
     7
theory Representable
44781
210b127e0b03 clarified import;
wenzelm
parents: 42151
diff changeset
     8
imports Algebraic Map_Functions "~~/src/HOL/Library/Countable"
25903
5e59af604d4f new theory of bifinite domains
huffman
parents:
diff changeset
     9
begin
5e59af604d4f new theory of bifinite domains
huffman
parents:
diff changeset
    10
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    11
default_sort cpo
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    12
41285
efd23c1d9886 renamed Bifinite.thy to Representable.thy
huffman
parents: 41034
diff changeset
    13
subsection {* Class of representable domains *}
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
    14
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
    15
text {*
40497
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
    16
  We define a ``domain'' as a pcpo that is isomorphic to some
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
    17
  algebraic deflation over the universal domain; this is equivalent
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
    18
  to being omega-bifinite.
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
    19
40497
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
    20
  A predomain is a cpo that, when lifted, becomes a domain.
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    21
  Predomains are represented by deflations over a lifted universal
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    22
  domain type.
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
    23
*}
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
    24
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    25
class predomain_syn = cpo +
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    26
  fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    27
  fixes liftprj :: "udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    28
  fixes liftdefl :: "'a itself \<Rightarrow> udom u defl"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    29
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    30
class predomain = predomain_syn +
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
    31
  assumes predomain_ep: "ep_pair liftemb liftprj"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    32
  assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
    33
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
    34
syntax "_LIFTDEFL" :: "type \<Rightarrow> logic"  ("(1LIFTDEFL/(1'(_')))")
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
    35
translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
    36
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
    37
definition liftdefl_of :: "udom defl \<rightarrow> udom u defl"
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
    38
  where "liftdefl_of = defl_fun1 ID ID u_map"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    39
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
    40
lemma cast_liftdefl_of: "cast\<cdot>(liftdefl_of\<cdot>t) = u_map\<cdot>(cast\<cdot>t)"
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
    41
by (simp add: liftdefl_of_def cast_defl_fun1 ep_pair_def finite_deflation_u_map)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    42
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    43
class "domain" = predomain_syn + pcpo +
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    44
  fixes emb :: "'a \<rightarrow> udom"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    45
  fixes prj :: "udom \<rightarrow> 'a"
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    46
  fixes defl :: "'a itself \<Rightarrow> udom defl"
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
    47
  assumes ep_pair_emb_prj: "ep_pair emb prj"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
    48
  assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    49
  assumes liftemb_eq: "liftemb = u_map\<cdot>emb"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    50
  assumes liftprj_eq: "liftprj = u_map\<cdot>prj"
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
    51
  assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of\<cdot>(defl TYPE('a))"
31113
15cf300a742f move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents: 31076
diff changeset
    52
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    53
syntax "_DEFL" :: "type \<Rightarrow> logic"  ("(1DEFL/(1'(_')))")
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
    54
translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
    55
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    56
instance "domain" \<subseteq> predomain
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    57
proof
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    58
  show "ep_pair liftemb (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    59
    unfolding liftemb_eq liftprj_eq
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    60
    by (intro ep_pair_u_map ep_pair_emb_prj)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    61
  show "cast\<cdot>LIFTDEFL('a) = liftemb oo (liftprj::udom\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>)"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    62
    unfolding liftemb_eq liftprj_eq liftdefl_eq
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
    63
    by (simp add: cast_liftdefl_of cast_DEFL u_map_oo)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    64
qed
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    65
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    66
text {*
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    67
  Constants @{const liftemb} and @{const liftprj} imply class predomain.
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    68
*}
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    69
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    70
setup {*
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    71
  fold Sign.add_const_constraint
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    72
  [(@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"}),
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    73
   (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}),
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    74
   (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"})]
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    75
*}
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    76
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    77
interpretation predomain: pcpo_ep_pair liftemb liftprj
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    78
  unfolding pcpo_ep_pair_def by (rule predomain_ep)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    79
40497
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
    80
interpretation "domain": pcpo_ep_pair emb prj
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    81
  unfolding pcpo_ep_pair_def by (rule ep_pair_emb_prj)
33504
b4210cc3ac97 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents: 31113
diff changeset
    82
40497
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
    83
lemmas emb_inverse = domain.e_inverse
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
    84
lemmas emb_prj_below = domain.e_p_below
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
    85
lemmas emb_eq_iff = domain.e_eq_iff
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
    86
lemmas emb_strict = domain.e_strict
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
    87
lemmas prj_strict = domain.p_strict
33504
b4210cc3ac97 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents: 31113
diff changeset
    88
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
    89
subsection {* Domains are bifinite *}
33587
54f98d225163 add map_map lemmas
huffman
parents: 33504
diff changeset
    90
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
    91
lemma approx_chain_ep_cast:
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
    92
  assumes ep: "ep_pair (e::'a::pcpo \<rightarrow> 'b::bifinite) (p::'b \<rightarrow> 'a)"
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
    93
  assumes cast_t: "cast\<cdot>t = e oo p"
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
    94
  shows "\<exists>(a::nat \<Rightarrow> 'a::pcpo \<rightarrow> 'a). approx_chain a"
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
    95
proof -
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
    96
  interpret ep_pair e p by fact
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
    97
  obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
    98
  and t: "t = (\<Squnion>i. defl_principal (Y i))"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
    99
    by (rule defl.obtain_principal_chain)
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   100
  def approx \<equiv> "\<lambda>i. (p oo cast\<cdot>(defl_principal (Y i)) oo e) :: 'a \<rightarrow> 'a"
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   101
  have "approx_chain approx"
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   102
  proof (rule approx_chain.intro)
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   103
    show "chain (\<lambda>i. approx i)"
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   104
      unfolding approx_def by (simp add: Y)
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   105
    show "(\<Squnion>i. approx i) = ID"
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   106
      unfolding approx_def
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   107
      by (simp add: lub_distribs Y t [symmetric] cast_t cfun_eq_iff)
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   108
    show "\<And>i. finite_deflation (approx i)"
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   109
      unfolding approx_def
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   110
      apply (rule finite_deflation_p_d_e)
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   111
      apply (rule finite_deflation_cast)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   112
      apply (rule defl.compact_principal)
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   113
      apply (rule below_trans [OF monofun_cfun_fun])
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   114
      apply (rule is_ub_thelub, simp add: Y)
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   115
      apply (simp add: lub_distribs Y t [symmetric] cast_t)
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   116
      done
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   117
  qed
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   118
  thus "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a" by - (rule exI)
33504
b4210cc3ac97 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents: 31113
diff changeset
   119
qed
b4210cc3ac97 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents: 31113
diff changeset
   120
41286
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   121
instance "domain" \<subseteq> bifinite
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   122
by default (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   123
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   124
instance predomain \<subseteq> profinite
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   125
by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents: 41285
diff changeset
   126
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   127
subsection {* Universal domain ep-pairs *}
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   128
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   129
definition "u_emb = udom_emb (\<lambda>i. u_map\<cdot>(udom_approx i))"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   130
definition "u_prj = udom_prj (\<lambda>i. u_map\<cdot>(udom_approx i))"
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   131
41297
01b2de947cff rename function cprod_map to prod_map
huffman
parents: 41292
diff changeset
   132
definition "prod_emb = udom_emb (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
01b2de947cff rename function cprod_map to prod_map
huffman
parents: 41292
diff changeset
   133
definition "prod_prj = udom_prj (\<lambda>i. prod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   134
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   135
definition "sprod_emb = udom_emb (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   136
definition "sprod_prj = udom_prj (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   137
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   138
definition "ssum_emb = udom_emb (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   139
definition "ssum_prj = udom_prj (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   140
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   141
definition "sfun_emb = udom_emb (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   142
definition "sfun_prj = udom_prj (\<lambda>i. sfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   143
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   144
lemma ep_pair_u: "ep_pair u_emb u_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   145
  unfolding u_emb_def u_prj_def
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   146
  by (simp add: ep_pair_udom approx_chain_u_map)
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   147
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   148
lemma ep_pair_prod: "ep_pair prod_emb prod_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   149
  unfolding prod_emb_def prod_prj_def
41297
01b2de947cff rename function cprod_map to prod_map
huffman
parents: 41292
diff changeset
   150
  by (simp add: ep_pair_udom approx_chain_prod_map)
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   151
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   152
lemma ep_pair_sprod: "ep_pair sprod_emb sprod_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   153
  unfolding sprod_emb_def sprod_prj_def
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   154
  by (simp add: ep_pair_udom approx_chain_sprod_map)
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   155
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   156
lemma ep_pair_ssum: "ep_pair ssum_emb ssum_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   157
  unfolding ssum_emb_def ssum_prj_def
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   158
  by (simp add: ep_pair_udom approx_chain_ssum_map)
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   159
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   160
lemma ep_pair_sfun: "ep_pair sfun_emb sfun_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   161
  unfolding sfun_emb_def sfun_prj_def
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   162
  by (simp add: ep_pair_udom approx_chain_sfun_map)
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   163
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   164
subsection {* Type combinators *}
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   165
41437
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   166
definition u_defl :: "udom defl \<rightarrow> udom defl"
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   167
  where "u_defl = defl_fun1 u_emb u_prj u_map"
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   168
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   169
definition prod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
41297
01b2de947cff rename function cprod_map to prod_map
huffman
parents: 41292
diff changeset
   170
  where "prod_defl = defl_fun2 prod_emb prod_prj prod_map"
33504
b4210cc3ac97 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents: 31113
diff changeset
   171
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   172
definition sprod_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   173
  where "sprod_defl = defl_fun2 sprod_emb sprod_prj sprod_map"
33504
b4210cc3ac97 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents: 31113
diff changeset
   174
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   175
definition ssum_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   176
where "ssum_defl = defl_fun2 ssum_emb ssum_prj ssum_map"
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   177
41287
029a6fc1bfb8 type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents: 41286
diff changeset
   178
definition sfun_defl :: "udom defl \<rightarrow> udom defl \<rightarrow> udom defl"
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   179
  where "sfun_defl = defl_fun2 sfun_emb sfun_prj sfun_map"
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   180
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   181
lemma cast_u_defl:
41437
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   182
  "cast\<cdot>(u_defl\<cdot>A) = u_emb oo u_map\<cdot>(cast\<cdot>A) oo u_prj"
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   183
using ep_pair_u finite_deflation_u_map
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   184
unfolding u_defl_def by (rule cast_defl_fun1)
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   185
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   186
lemma cast_prod_defl:
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   187
  "cast\<cdot>(prod_defl\<cdot>A\<cdot>B) =
41297
01b2de947cff rename function cprod_map to prod_map
huffman
parents: 41292
diff changeset
   188
    prod_emb oo prod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo prod_prj"
01b2de947cff rename function cprod_map to prod_map
huffman
parents: 41292
diff changeset
   189
using ep_pair_prod finite_deflation_prod_map
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   190
unfolding prod_defl_def by (rule cast_defl_fun2)
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   191
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   192
lemma cast_sprod_defl:
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   193
  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) =
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   194
    sprod_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sprod_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   195
using ep_pair_sprod finite_deflation_sprod_map
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   196
unfolding sprod_defl_def by (rule cast_defl_fun2)
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   197
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   198
lemma cast_ssum_defl:
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   199
  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) =
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   200
    ssum_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo ssum_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   201
using ep_pair_ssum finite_deflation_ssum_map
40484
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   202
unfolding ssum_defl_def by (rule cast_defl_fun2)
768f7e264e2b reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
huffman
parents: 40086
diff changeset
   203
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   204
lemma cast_sfun_defl:
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   205
  "cast\<cdot>(sfun_defl\<cdot>A\<cdot>B) =
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   206
    sfun_emb oo sfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo sfun_prj"
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   207
using ep_pair_sfun finite_deflation_sfun_map
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   208
unfolding sfun_defl_def by (rule cast_defl_fun2)
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   209
41437
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   210
text {* Special deflation combinator for unpointed types. *}
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   211
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   212
definition u_liftdefl :: "udom u defl \<rightarrow> udom defl"
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   213
  where "u_liftdefl = defl_fun1 u_emb u_prj ID"
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   214
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   215
lemma cast_u_liftdefl:
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   216
  "cast\<cdot>(u_liftdefl\<cdot>A) = u_emb oo cast\<cdot>A oo u_prj"
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   217
unfolding u_liftdefl_def by (simp add: cast_defl_fun1 ep_pair_u)
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   218
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   219
lemma u_liftdefl_liftdefl_of:
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   220
  "u_liftdefl\<cdot>(liftdefl_of\<cdot>A) = u_defl\<cdot>A"
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   221
by (rule cast_eq_imp_eq)
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   222
   (simp add: cast_u_liftdefl cast_liftdefl_of cast_u_defl)
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   223
40506
4c5363173f88 section headings
huffman
parents: 40502
diff changeset
   224
subsection {* Class instance proofs *}
4c5363173f88 section headings
huffman
parents: 40502
diff changeset
   225
4c5363173f88 section headings
huffman
parents: 40502
diff changeset
   226
subsubsection {* Universal domain *}
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   227
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   228
instantiation udom :: "domain"
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   229
begin
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   230
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   231
definition [simp]:
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   232
  "emb = (ID :: udom \<rightarrow> udom)"
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   233
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   234
definition [simp]:
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   235
  "prj = (ID :: udom \<rightarrow> udom)"
25903
5e59af604d4f new theory of bifinite domains
huffman
parents:
diff changeset
   236
33504
b4210cc3ac97 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents: 31113
diff changeset
   237
definition
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   238
  "defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))"
33808
31169fdc5ae7 add map_ID lemmas
huffman
parents: 33587
diff changeset
   239
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   240
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   241
  "(liftemb :: udom u \<rightarrow> udom u) = u_map\<cdot>emb"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   242
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   243
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   244
  "(liftprj :: udom u \<rightarrow> udom u) = u_map\<cdot>prj"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   245
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   246
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
   247
  "liftdefl (t::udom itself) = liftdefl_of\<cdot>DEFL(udom)"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   248
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   249
instance proof
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   250
  show "ep_pair emb (prj :: udom \<rightarrow> udom)"
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   251
    by (simp add: ep_pair.intro)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   252
  show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)"
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   253
    unfolding defl_udom_def
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   254
    apply (subst contlub_cfun_arg)
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   255
    apply (rule chainI)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   256
    apply (rule defl.principal_mono)
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   257
    apply (simp add: below_fin_defl_def)
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   258
    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   259
    apply (rule chainE)
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   260
    apply (rule chain_udom_approx)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   261
    apply (subst cast_defl_principal)
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   262
    apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx)
33504
b4210cc3ac97 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents: 31113
diff changeset
   263
    done
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   264
qed (fact liftemb_udom_def liftprj_udom_def liftdefl_udom_def)+
33504
b4210cc3ac97 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents: 31113
diff changeset
   265
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   266
end
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   267
40506
4c5363173f88 section headings
huffman
parents: 40502
diff changeset
   268
subsubsection {* Lifted cpo *}
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   269
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   270
instantiation u :: (predomain) "domain"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   271
begin
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   272
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   273
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   274
  "emb = u_emb oo liftemb"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   275
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   276
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   277
  "prj = liftprj oo u_prj"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   278
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   279
definition
41437
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   280
  "defl (t::'a u itself) = u_liftdefl\<cdot>LIFTDEFL('a)"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   281
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   282
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   283
  "(liftemb :: 'a u u \<rightarrow> udom u) = u_map\<cdot>emb"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   284
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   285
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   286
  "(liftprj :: udom u \<rightarrow> 'a u u) = u_map\<cdot>prj"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   287
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   288
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
   289
  "liftdefl (t::'a u itself) = liftdefl_of\<cdot>DEFL('a u)"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   290
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   291
instance proof
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   292
  show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   293
    unfolding emb_u_def prj_u_def
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   294
    by (intro ep_pair_comp ep_pair_u predomain_ep)
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   295
  show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   296
    unfolding emb_u_def prj_u_def defl_u_def
41437
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   297
    by (simp add: cast_u_liftdefl cast_liftdefl assoc_oo)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   298
qed (fact liftemb_u_def liftprj_u_def liftdefl_u_def)+
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   299
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   300
end
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   301
41437
5bc117c382ec rename constant u_defl to u_liftdefl;
huffman
parents: 41436
diff changeset
   302
lemma DEFL_u: "DEFL('a::predomain u) = u_liftdefl\<cdot>LIFTDEFL('a)"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   303
by (rule defl_u_def)
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   304
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   305
subsubsection {* Strict function space *}
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   306
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   307
instantiation sfun :: ("domain", "domain") "domain"
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   308
begin
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   309
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   310
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   311
  "emb = sfun_emb oo sfun_map\<cdot>prj\<cdot>emb"
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   312
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   313
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   314
  "prj = sfun_map\<cdot>emb\<cdot>prj oo sfun_prj"
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   315
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   316
definition
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   317
  "defl (t::('a \<rightarrow>! 'b) itself) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   318
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   319
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   320
  "(liftemb :: ('a \<rightarrow>! 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   321
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   322
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   323
  "(liftprj :: udom u \<rightarrow> ('a \<rightarrow>! 'b) u) = u_map\<cdot>prj"
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   324
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   325
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
   326
  "liftdefl (t::('a \<rightarrow>! 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow>! 'b)"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   327
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   328
instance proof
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   329
  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   330
    unfolding emb_sfun_def prj_sfun_def
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   331
    by (intro ep_pair_comp ep_pair_sfun ep_pair_sfun_map ep_pair_emb_prj)
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   332
  show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   333
    unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   334
    by (simp add: cast_DEFL oo_def sfun_eq_iff sfun_map_map)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   335
qed (fact liftemb_sfun_def liftprj_sfun_def liftdefl_sfun_def)+
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   336
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   337
end
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   338
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   339
lemma DEFL_sfun:
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   340
  "DEFL('a::domain \<rightarrow>! 'b::domain) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   341
by (rule defl_sfun_def)
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   342
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   343
subsubsection {* Continuous function space *}
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   344
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   345
instantiation cfun :: (predomain, "domain") "domain"
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   346
begin
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   347
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   348
definition
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   349
  "emb = emb oo encode_cfun"
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   350
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   351
definition
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   352
  "prj = decode_cfun oo prj"
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   353
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   354
definition
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   355
  "defl (t::('a \<rightarrow> 'b) itself) = DEFL('a u \<rightarrow>! 'b)"
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   356
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   357
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   358
  "(liftemb :: ('a \<rightarrow> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   359
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   360
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   361
  "(liftprj :: udom u \<rightarrow> ('a \<rightarrow> 'b) u) = u_map\<cdot>prj"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   362
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   363
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
   364
  "liftdefl (t::('a \<rightarrow> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<rightarrow> 'b)"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   365
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   366
instance proof
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   367
  have "ep_pair encode_cfun decode_cfun"
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   368
    by (rule ep_pair.intro, simp_all)
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40506
diff changeset
   369
  thus "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   370
    unfolding emb_cfun_def prj_cfun_def
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   371
    using ep_pair_emb_prj by (rule ep_pair_comp)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   372
  show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   373
    unfolding emb_cfun_def prj_cfun_def defl_cfun_def
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   374
    by (simp add: cast_DEFL cfcomp1)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   375
qed (fact liftemb_cfun_def liftprj_cfun_def liftdefl_cfun_def)+
25903
5e59af604d4f new theory of bifinite domains
huffman
parents:
diff changeset
   376
39985
310f98585107 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents: 39974
diff changeset
   377
end
33504
b4210cc3ac97 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents: 31113
diff changeset
   378
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   379
lemma DEFL_cfun:
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   380
  "DEFL('a::predomain \<rightarrow> 'b::domain) = DEFL('a u \<rightarrow>! 'b)"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   381
by (rule defl_cfun_def)
39972
4244ff4f9649 add lemmas finite_deflation_imp_compact, cast_below_cast_iff
Brian Huffman <brianh@cs.pdx.edu>
parents: 37678
diff changeset
   382
40506
4c5363173f88 section headings
huffman
parents: 40502
diff changeset
   383
subsubsection {* Strict product *}
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   384
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   385
instantiation sprod :: ("domain", "domain") "domain"
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   386
begin
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   387
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   388
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   389
  "emb = sprod_emb oo sprod_map\<cdot>emb\<cdot>emb"
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   390
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   391
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   392
  "prj = sprod_map\<cdot>prj\<cdot>prj oo sprod_prj"
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   393
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   394
definition
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   395
  "defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   396
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   397
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   398
  "(liftemb :: ('a \<otimes> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   399
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   400
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   401
  "(liftprj :: udom u \<rightarrow> ('a \<otimes> 'b) u) = u_map\<cdot>prj"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   402
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   403
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
   404
  "liftdefl (t::('a \<otimes> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<otimes> 'b)"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   405
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   406
instance proof
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   407
  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   408
    unfolding emb_sprod_def prj_sprod_def
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   409
    by (intro ep_pair_comp ep_pair_sprod ep_pair_sprod_map ep_pair_emb_prj)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   410
  show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   411
    unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39989
diff changeset
   412
    by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   413
qed (fact liftemb_sprod_def liftprj_sprod_def liftdefl_sprod_def)+
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   414
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   415
end
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   416
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   417
lemma DEFL_sprod:
40497
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
   418
  "DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   419
by (rule defl_sprod_def)
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   420
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   421
subsubsection {* Cartesian product *}
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   422
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   423
definition prod_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   424
  where "prod_liftdefl = defl_fun2 (u_map\<cdot>prod_emb oo decode_prod_u)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   425
    (encode_prod_u oo u_map\<cdot>prod_prj) sprod_map"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   426
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   427
lemma cast_prod_liftdefl:
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   428
  "cast\<cdot>(prod_liftdefl\<cdot>a\<cdot>b) =
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   429
    (u_map\<cdot>prod_emb oo decode_prod_u) oo sprod_map\<cdot>(cast\<cdot>a)\<cdot>(cast\<cdot>b) oo
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   430
      (encode_prod_u oo u_map\<cdot>prod_prj)"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   431
unfolding prod_liftdefl_def
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   432
apply (rule cast_defl_fun2)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   433
apply (intro ep_pair_comp ep_pair_u_map ep_pair_prod)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   434
apply (simp add: ep_pair.intro)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   435
apply (erule (1) finite_deflation_sprod_map)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   436
done
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   437
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   438
instantiation prod :: (predomain, predomain) predomain
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   439
begin
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   440
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   441
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   442
  "liftemb = (u_map\<cdot>prod_emb oo decode_prod_u) oo
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   443
    (sprod_map\<cdot>liftemb\<cdot>liftemb oo encode_prod_u)"
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   444
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   445
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   446
  "liftprj = (decode_prod_u oo sprod_map\<cdot>liftprj\<cdot>liftprj) oo
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   447
    (encode_prod_u oo u_map\<cdot>prod_prj)"
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   448
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   449
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   450
  "liftdefl (t::('a \<times> 'b) itself) = prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   451
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   452
instance proof
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   453
  show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)"
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   454
    unfolding liftemb_prod_def liftprj_prod_def
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   455
    by (intro ep_pair_comp ep_pair_sprod_map ep_pair_u_map
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   456
       ep_pair_prod predomain_ep, simp_all add: ep_pair.intro)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   457
  show "cast\<cdot>LIFTDEFL('a \<times> 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a \<times> 'b) u)"
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   458
    unfolding liftemb_prod_def liftprj_prod_def liftdefl_prod_def
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   459
    by (simp add: cast_prod_liftdefl cast_liftdefl cfcomp1 sprod_map_map)
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   460
qed
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   461
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   462
end
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   463
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   464
instantiation prod :: ("domain", "domain") "domain"
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   465
begin
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   466
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   467
definition
41297
01b2de947cff rename function cprod_map to prod_map
huffman
parents: 41292
diff changeset
   468
  "emb = prod_emb oo prod_map\<cdot>emb\<cdot>emb"
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   469
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   470
definition
41297
01b2de947cff rename function cprod_map to prod_map
huffman
parents: 41292
diff changeset
   471
  "prj = prod_map\<cdot>prj\<cdot>prj oo prod_prj"
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   472
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   473
definition
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   474
  "defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   475
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   476
instance proof
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   477
  show 1: "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   478
    unfolding emb_prod_def prj_prod_def
41297
01b2de947cff rename function cprod_map to prod_map
huffman
parents: 41292
diff changeset
   479
    by (intro ep_pair_comp ep_pair_prod ep_pair_prod_map ep_pair_emb_prj)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   480
  show 2: "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   481
    unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
41297
01b2de947cff rename function cprod_map to prod_map
huffman
parents: 41292
diff changeset
   482
    by (simp add: cast_DEFL oo_def cfun_eq_iff prod_map_map)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   483
  show 3: "liftemb = u_map\<cdot>(emb :: 'a \<times> 'b \<rightarrow> udom)"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   484
    unfolding emb_prod_def liftemb_prod_def liftemb_eq
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   485
    unfolding encode_prod_u_def decode_prod_u_def
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   486
    by (rule cfun_eqI, case_tac x, simp, clarsimp)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   487
  show 4: "liftprj = u_map\<cdot>(prj :: udom \<rightarrow> 'a \<times> 'b)"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   488
    unfolding prj_prod_def liftprj_prod_def liftprj_eq
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   489
    unfolding encode_prod_u_def decode_prod_u_def
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   490
    apply (rule cfun_eqI, case_tac x, simp)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   491
    apply (rename_tac y, case_tac "prod_prj\<cdot>y", simp)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   492
    done
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
   493
  show 5: "LIFTDEFL('a \<times> 'b) = liftdefl_of\<cdot>DEFL('a \<times> 'b)"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   494
    by (rule cast_eq_imp_eq)
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
   495
      (simp add: cast_liftdefl cast_liftdefl_of cast_DEFL 2 3 4 u_map_oo)
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   496
qed
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   497
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   498
end
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   499
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   500
lemma DEFL_prod:
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   501
  "DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   502
by (rule defl_prod_def)
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   503
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   504
lemma LIFTDEFL_prod:
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   505
  "LIFTDEFL('a::predomain \<times> 'b::predomain) =
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   506
    prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
40830
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   507
by (rule liftdefl_prod_def)
158d18502378 simplify predomain instances
huffman
parents: 40774
diff changeset
   508
41034
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   509
subsubsection {* Unit type *}
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   510
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   511
instantiation unit :: "domain"
41034
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   512
begin
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   513
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   514
definition
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   515
  "emb = (\<bottom> :: unit \<rightarrow> udom)"
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   516
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   517
definition
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   518
  "prj = (\<bottom> :: udom \<rightarrow> unit)"
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   519
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   520
definition
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   521
  "defl (t::unit itself) = \<bottom>"
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   522
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   523
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   524
  "(liftemb :: unit u \<rightarrow> udom u) = u_map\<cdot>emb"
41034
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   525
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   526
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   527
  "(liftprj :: udom u \<rightarrow> unit u) = u_map\<cdot>prj"
41034
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   528
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   529
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
   530
  "liftdefl (t::unit itself) = liftdefl_of\<cdot>DEFL(unit)"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   531
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   532
instance proof
41034
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   533
  show "ep_pair emb (prj :: udom \<rightarrow> unit)"
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   534
    unfolding emb_unit_def prj_unit_def
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   535
    by (simp add: ep_pair.intro)
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   536
  show "cast\<cdot>DEFL(unit) = emb oo (prj :: udom \<rightarrow> unit)"
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   537
    unfolding emb_unit_def prj_unit_def defl_unit_def by simp
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   538
qed (fact liftemb_unit_def liftprj_unit_def liftdefl_unit_def)+
41034
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   539
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   540
end
ce5d9e73fb98 instance unit :: domain
huffman
parents: 40830
diff changeset
   541
40506
4c5363173f88 section headings
huffman
parents: 40502
diff changeset
   542
subsubsection {* Discrete cpo *}
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   543
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   544
instantiation discr :: (countable) predomain
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   545
begin
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   546
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   547
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   548
  "(liftemb :: 'a discr u \<rightarrow> udom u) = strictify\<cdot>up oo udom_emb discr_approx"
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   549
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   550
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   551
  "(liftprj :: udom u \<rightarrow> 'a discr u) = udom_prj discr_approx oo fup\<cdot>ID"
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   552
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   553
definition
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   554
  "liftdefl (t::'a discr itself) =
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   555
    (\<Squnion>i. defl_principal (Abs_fin_defl (liftemb oo discr_approx i oo (liftprj::udom u \<rightarrow> 'a discr u))))"
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   556
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   557
instance proof
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   558
  show 1: "ep_pair liftemb (liftprj :: udom u \<rightarrow> 'a discr u)"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   559
    unfolding liftemb_discr_def liftprj_discr_def
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   560
    apply (intro ep_pair_comp ep_pair_udom [OF discr_approx])
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   561
    apply (rule ep_pair.intro)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   562
    apply (simp add: strictify_conv_if)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   563
    apply (case_tac y, simp, simp add: strictify_conv_if)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   564
    done
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   565
  show "cast\<cdot>LIFTDEFL('a discr) = liftemb oo (liftprj :: udom u \<rightarrow> 'a discr u)"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   566
    unfolding liftdefl_discr_def
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   567
    apply (subst contlub_cfun_arg)
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   568
    apply (rule chainI)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   569
    apply (rule defl.principal_mono)
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   570
    apply (simp add: below_fin_defl_def)
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   571
    apply (simp add: Abs_fin_defl_inverse
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   572
        ep_pair.finite_deflation_e_d_p [OF 1]
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   573
        approx_chain.finite_deflation_approx [OF discr_approx])
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   574
    apply (intro monofun_cfun below_refl)
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   575
    apply (rule chainE)
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   576
    apply (rule chain_discr_approx)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   577
    apply (subst cast_defl_principal)
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   578
    apply (simp add: Abs_fin_defl_inverse
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   579
        ep_pair.finite_deflation_e_d_p [OF 1]
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   580
        approx_chain.finite_deflation_approx [OF discr_approx])
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   581
    apply (simp add: lub_distribs)
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   582
    done
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   583
qed
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   584
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   585
end
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   586
40506
4c5363173f88 section headings
huffman
parents: 40502
diff changeset
   587
subsubsection {* Strict sum *}
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   588
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   589
instantiation ssum :: ("domain", "domain") "domain"
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   590
begin
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   591
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   592
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   593
  "emb = ssum_emb oo ssum_map\<cdot>emb\<cdot>emb"
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   594
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   595
definition
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   596
  "prj = ssum_map\<cdot>prj\<cdot>prj oo ssum_prj"
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   597
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   598
definition
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   599
  "defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   600
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   601
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   602
  "(liftemb :: ('a \<oplus> 'b) u \<rightarrow> udom u) = u_map\<cdot>emb"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   603
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   604
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   605
  "(liftprj :: udom u \<rightarrow> ('a \<oplus> 'b) u) = u_map\<cdot>prj"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   606
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   607
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
   608
  "liftdefl (t::('a \<oplus> 'b) itself) = liftdefl_of\<cdot>DEFL('a \<oplus> 'b)"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   609
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   610
instance proof
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   611
  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   612
    unfolding emb_ssum_def prj_ssum_def
41290
e9c9577d88b5 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
huffman
parents: 41287
diff changeset
   613
    by (intro ep_pair_comp ep_pair_ssum ep_pair_ssum_map ep_pair_emb_prj)
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   614
  show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   615
    unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39989
diff changeset
   616
    by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   617
qed (fact liftemb_ssum_def liftprj_ssum_def liftdefl_ssum_def)+
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   618
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   619
end
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   620
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   621
lemma DEFL_ssum:
40497
d2e876d6da8c rename class 'bifinite' to 'domain'
huffman
parents: 40494
diff changeset
   622
  "DEFL('a::domain \<oplus> 'b::domain) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
39989
ad60d7311f43 renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents: 39987
diff changeset
   623
by (rule defl_ssum_def)
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   624
40506
4c5363173f88 section headings
huffman
parents: 40502
diff changeset
   625
subsubsection {* Lifted HOL type *}
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   626
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   627
instantiation lift :: (countable) "domain"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   628
begin
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   629
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   630
definition
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   631
  "emb = emb oo (\<Lambda> x. Rep_lift x)"
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   632
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   633
definition
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   634
  "prj = (\<Lambda> y. Abs_lift y) oo prj"
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   635
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   636
definition
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   637
  "defl (t::'a lift itself) = DEFL('a discr u)"
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   638
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   639
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   640
  "(liftemb :: 'a lift u \<rightarrow> udom u) = u_map\<cdot>emb"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   641
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   642
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   643
  "(liftprj :: udom u \<rightarrow> 'a lift u) = u_map\<cdot>prj"
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   644
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   645
definition
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41297
diff changeset
   646
  "liftdefl (t::'a lift itself) = liftdefl_of\<cdot>DEFL('a lift)"
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   647
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   648
instance proof
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   649
  note [simp] = cont_Rep_lift cont_Abs_lift Rep_lift_inverse Abs_lift_inverse
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   650
  have "ep_pair (\<Lambda>(x::'a lift). Rep_lift x) (\<Lambda> y. Abs_lift y)"
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   651
    by (simp add: ep_pair_def)
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   652
  thus "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   653
    unfolding emb_lift_def prj_lift_def
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   654
    using ep_pair_emb_prj by (rule ep_pair_comp)
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   655
  show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   656
    unfolding emb_lift_def prj_lift_def defl_lift_def cast_DEFL
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   657
    by (simp add: cfcomp1)
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41290
diff changeset
   658
qed (fact liftemb_lift_def liftprj_lift_def liftdefl_lift_def)+
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   659
39987
8c2f449af35a move all bifinite class instances to Bifinite.thy
huffman
parents: 39986
diff changeset
   660
end
40491
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   661
6de5839e2fb3 add 'predomain' class: unpointed version of bifinite
huffman
parents: 40484
diff changeset
   662
end