src/HOL/HOLCF/Library/Sum_Cpo.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 55931 62156e694f3d
child 61169 4de9ff3ea29a
permissions -rw-r--r--
modernized header;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Library/Sum_Cpo.thy
huffman@29130
     2
    Author:     Brian Huffman
huffman@29130
     3
*)
huffman@29130
     4
wenzelm@58880
     5
section {* The cpo of disjoint sums *}
huffman@29130
     6
huffman@29534
     7
theory Sum_Cpo
huffman@39974
     8
imports HOLCF
huffman@29130
     9
begin
huffman@29130
    10
huffman@35900
    11
subsection {* Ordering on sum type *}
huffman@29130
    12
haftmann@37678
    13
instantiation sum :: (below, below) below
huffman@29130
    14
begin
huffman@29130
    15
huffman@31076
    16
definition below_sum_def:
huffman@31076
    17
  "x \<sqsubseteq> y \<equiv> case x of
huffman@29130
    18
         Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
huffman@29130
    19
         Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
huffman@29130
    20
huffman@29130
    21
instance ..
huffman@29130
    22
end
huffman@29130
    23
huffman@40436
    24
lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y \<longleftrightarrow> x \<sqsubseteq> y"
huffman@31076
    25
unfolding below_sum_def by simp
huffman@29130
    26
huffman@40436
    27
lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y \<longleftrightarrow> x \<sqsubseteq> y"
huffman@31076
    28
unfolding below_sum_def by simp
huffman@29130
    29
huffman@31076
    30
lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
huffman@31076
    31
unfolding below_sum_def by simp
huffman@29130
    32
huffman@31076
    33
lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
huffman@31076
    34
unfolding below_sum_def by simp
huffman@29130
    35
huffman@29130
    36
lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
huffman@29130
    37
by simp
huffman@29130
    38
huffman@29130
    39
lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
huffman@29130
    40
by simp
huffman@29130
    41
huffman@31076
    42
lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
huffman@29130
    43
by (cases x, simp_all)
huffman@29130
    44
huffman@31076
    45
lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
huffman@29130
    46
by (cases x, simp_all)
huffman@29130
    47
huffman@31076
    48
lemmas sum_below_elims = Inl_belowE Inr_belowE
huffman@29130
    49
huffman@31076
    50
lemma sum_below_cases:
huffman@29130
    51
  "\<lbrakk>x \<sqsubseteq> y;
huffman@29130
    52
    \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
huffman@29130
    53
    \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
huffman@29130
    54
      \<Longrightarrow> R"
huffman@31076
    55
by (cases x, safe elim!: sum_below_elims, auto)
huffman@29130
    56
huffman@29130
    57
subsection {* Sum type is a complete partial order *}
huffman@29130
    58
haftmann@37678
    59
instance sum :: (po, po) po
huffman@29130
    60
proof
huffman@29130
    61
  fix x :: "'a + 'b"
huffman@29130
    62
  show "x \<sqsubseteq> x"
huffman@29130
    63
    by (induct x, simp_all)
huffman@29130
    64
next
huffman@29130
    65
  fix x y :: "'a + 'b"
huffman@29130
    66
  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
huffman@31076
    67
    by (induct x, auto elim!: sum_below_elims intro: below_antisym)
huffman@29130
    68
next
huffman@29130
    69
  fix x y z :: "'a + 'b"
huffman@29130
    70
  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
huffman@31076
    71
    by (induct x, auto elim!: sum_below_elims intro: below_trans)
huffman@29130
    72
qed
huffman@29130
    73
huffman@29130
    74
lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
huffman@31076
    75
by (rule monofunI, erule sum_below_cases, simp_all)
huffman@29130
    76
huffman@29130
    77
lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
huffman@31076
    78
by (rule monofunI, erule sum_below_cases, simp_all)
huffman@29130
    79
huffman@29130
    80
lemma sum_chain_cases:
huffman@29130
    81
  assumes Y: "chain Y"
huffman@29130
    82
  assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R"
huffman@29130
    83
  assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R"
huffman@29130
    84
  shows "R"
huffman@29130
    85
 apply (cases "Y 0")
huffman@29130
    86
  apply (rule A)
huffman@29130
    87
   apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
huffman@29130
    88
  apply (rule ext)
huffman@29130
    89
  apply (cut_tac j=i in chain_mono [OF Y le0], simp)
huffman@31076
    90
  apply (erule Inl_belowE, simp)
huffman@29130
    91
 apply (rule B)
huffman@29130
    92
  apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
huffman@29130
    93
 apply (rule ext)
huffman@29130
    94
 apply (cut_tac j=i in chain_mono [OF Y le0], simp)
huffman@31076
    95
 apply (erule Inr_belowE, simp)
huffman@29130
    96
done
huffman@29130
    97
huffman@29130
    98
lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
huffman@29130
    99
 apply (rule is_lubI)
huffman@29130
   100
  apply (rule ub_rangeI)
huffman@40771
   101
  apply (simp add: is_lub_rangeD1)
huffman@29130
   102
 apply (frule ub_rangeD [where i=arbitrary])
huffman@31076
   103
 apply (erule Inl_belowE, simp)
huffman@40771
   104
 apply (erule is_lubD2)
huffman@29130
   105
 apply (rule ub_rangeI)
huffman@29130
   106
 apply (drule ub_rangeD, simp)
huffman@29130
   107
done
huffman@29130
   108
huffman@29130
   109
lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
huffman@29130
   110
 apply (rule is_lubI)
huffman@29130
   111
  apply (rule ub_rangeI)
huffman@40771
   112
  apply (simp add: is_lub_rangeD1)
huffman@29130
   113
 apply (frule ub_rangeD [where i=arbitrary])
huffman@31076
   114
 apply (erule Inr_belowE, simp)
huffman@40771
   115
 apply (erule is_lubD2)
huffman@29130
   116
 apply (rule ub_rangeI)
huffman@29130
   117
 apply (drule ub_rangeD, simp)
huffman@29130
   118
done
huffman@29130
   119
haftmann@37678
   120
instance sum :: (cpo, cpo) cpo
huffman@29130
   121
 apply intro_classes
huffman@29130
   122
 apply (erule sum_chain_cases, safe)
huffman@29130
   123
  apply (rule exI)
huffman@29130
   124
  apply (rule is_lub_Inl)
huffman@29130
   125
  apply (erule cpo_lubI)
huffman@29130
   126
 apply (rule exI)
huffman@29130
   127
 apply (rule is_lub_Inr)
huffman@29130
   128
 apply (erule cpo_lubI)
huffman@29130
   129
done
huffman@29130
   130
huffman@35900
   131
subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *}
huffman@29130
   132
huffman@29130
   133
lemma cont_Inl: "cont Inl"
huffman@31041
   134
by (intro contI is_lub_Inl cpo_lubI)
huffman@29130
   135
huffman@29130
   136
lemma cont_Inr: "cont Inr"
huffman@31041
   137
by (intro contI is_lub_Inr cpo_lubI)
huffman@31041
   138
huffman@37079
   139
lemmas cont2cont_Inl [simp, cont2cont] = cont_compose [OF cont_Inl]
huffman@37079
   140
lemmas cont2cont_Inr [simp, cont2cont] = cont_compose [OF cont_Inr]
huffman@29130
   141
huffman@29130
   142
lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
huffman@29130
   143
lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
huffman@29130
   144
huffman@29130
   145
lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
huffman@29130
   146
lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
huffman@29130
   147
blanchet@55414
   148
lemma cont_case_sum1:
huffman@29130
   149
  assumes f: "\<And>a. cont (\<lambda>x. f x a)"
huffman@29130
   150
  assumes g: "\<And>b. cont (\<lambda>x. g x b)"
huffman@29130
   151
  shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
huffman@29130
   152
by (induct y, simp add: f, simp add: g)
huffman@29130
   153
blanchet@55414
   154
lemma cont_case_sum2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (case_sum f g)"
huffman@29130
   155
apply (rule contI)
huffman@29130
   156
apply (erule sum_chain_cases)
huffman@29130
   157
apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
huffman@29130
   158
apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
huffman@29130
   159
done
huffman@29130
   160
blanchet@55414
   161
lemma cont2cont_case_sum:
huffman@29130
   162
  assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
huffman@29130
   163
  assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
huffman@29130
   164
  assumes h: "cont (\<lambda>x. h x)"
huffman@29130
   165
  shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
huffman@31041
   166
apply (rule cont_apply [OF h])
blanchet@55414
   167
apply (rule cont_case_sum2 [OF f2 g2])
blanchet@55414
   168
apply (rule cont_case_sum1 [OF f1 g1])
huffman@29130
   169
done
huffman@29130
   170
blanchet@55414
   171
lemma cont2cont_case_sum' [simp, cont2cont]:
huffman@31041
   172
  assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
huffman@31041
   173
  assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
huffman@31041
   174
  assumes h: "cont (\<lambda>x. h x)"
huffman@31041
   175
  shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
blanchet@55414
   176
using assms by (simp add: cont2cont_case_sum prod_cont_iff)
huffman@31041
   177
huffman@41321
   178
text {* Continuity of map function. *}
huffman@41321
   179
blanchet@55931
   180
lemma map_sum_eq: "map_sum f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
huffman@41321
   181
by (rule ext, case_tac x, simp_all)
huffman@41321
   182
blanchet@55931
   183
lemma cont2cont_map_sum [simp, cont2cont]:
huffman@41321
   184
  assumes f: "cont (\<lambda>(x, y). f x y)"
huffman@41321
   185
  assumes g: "cont (\<lambda>(x, y). g x y)"
huffman@41321
   186
  assumes h: "cont (\<lambda>x. h x)"
blanchet@55931
   187
  shows "cont (\<lambda>x. map_sum (\<lambda>y. f x y) (\<lambda>y. g x y) (h x))"
blanchet@55931
   188
using assms by (simp add: map_sum_eq prod_cont_iff)
huffman@41321
   189
huffman@29130
   190
subsection {* Compactness and chain-finiteness *}
huffman@29130
   191
huffman@29130
   192
lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
huffman@29130
   193
apply (rule compactI2)
huffman@29130
   194
apply (erule sum_chain_cases, safe)
huffman@29130
   195
apply (simp add: lub_Inl)
huffman@29130
   196
apply (erule (2) compactD2)
huffman@29130
   197
apply (simp add: lub_Inr)
huffman@29130
   198
done
huffman@29130
   199
huffman@29130
   200
lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)"
huffman@29130
   201
apply (rule compactI2)
huffman@29130
   202
apply (erule sum_chain_cases, safe)
huffman@29130
   203
apply (simp add: lub_Inl)
huffman@29130
   204
apply (simp add: lub_Inr)
huffman@29130
   205
apply (erule (2) compactD2)
huffman@29130
   206
done
huffman@29130
   207
huffman@29130
   208
lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a"
huffman@29130
   209
unfolding compact_def
huffman@29130
   210
by (drule adm_subst [OF cont_Inl], simp)
huffman@29130
   211
huffman@29130
   212
lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a"
huffman@29130
   213
unfolding compact_def
huffman@29130
   214
by (drule adm_subst [OF cont_Inr], simp)
huffman@29130
   215
huffman@29130
   216
lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a"
huffman@29130
   217
by (safe elim!: compact_Inl compact_Inl_rev)
huffman@29130
   218
huffman@29130
   219
lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
huffman@29130
   220
by (safe elim!: compact_Inr compact_Inr_rev)
huffman@29130
   221
haftmann@37678
   222
instance sum :: (chfin, chfin) chfin
huffman@29130
   223
apply intro_classes
huffman@29130
   224
apply (erule compact_imp_max_in_chain)
huffman@29130
   225
apply (case_tac "\<Squnion>i. Y i", simp_all)
huffman@29130
   226
done
huffman@29130
   227
haftmann@37678
   228
instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo
huffman@31076
   229
by intro_classes (simp add: below_sum_def split: sum.split)
huffman@29130
   230
huffman@40495
   231
subsection {* Using sum types with fixrec *}
huffman@40495
   232
huffman@40495
   233
definition
huffman@40495
   234
  "match_Inl = (\<Lambda> x k. case x of Inl a \<Rightarrow> k\<cdot>a | Inr b \<Rightarrow> Fixrec.fail)"
huffman@40495
   235
huffman@40495
   236
definition
huffman@40495
   237
  "match_Inr = (\<Lambda> x k. case x of Inl a \<Rightarrow> Fixrec.fail | Inr b \<Rightarrow> k\<cdot>b)"
huffman@40495
   238
huffman@40495
   239
lemma match_Inl_simps [simp]:
huffman@40495
   240
  "match_Inl\<cdot>(Inl a)\<cdot>k = k\<cdot>a"
huffman@40495
   241
  "match_Inl\<cdot>(Inr b)\<cdot>k = Fixrec.fail"
huffman@40495
   242
unfolding match_Inl_def by simp_all
huffman@40495
   243
huffman@40495
   244
lemma match_Inr_simps [simp]:
huffman@40495
   245
  "match_Inr\<cdot>(Inl a)\<cdot>k = Fixrec.fail"
huffman@40495
   246
  "match_Inr\<cdot>(Inr b)\<cdot>k = k\<cdot>b"
huffman@40495
   247
unfolding match_Inr_def by simp_all
huffman@40495
   248
huffman@40495
   249
setup {*
huffman@40495
   250
  Fixrec.add_matchers
huffman@40495
   251
    [ (@{const_name Inl}, @{const_name match_Inl}),
huffman@40495
   252
      (@{const_name Inr}, @{const_name match_Inr}) ]
huffman@40495
   253
*}
huffman@40495
   254
huffman@40496
   255
subsection {* Disjoint sum is a predomain *}
huffman@40496
   256
huffman@40496
   257
definition
huffman@40496
   258
  "encode_sum_u =
huffman@40496
   259
    (\<Lambda>(up\<cdot>x). case x of Inl a \<Rightarrow> sinl\<cdot>(up\<cdot>a) | Inr b \<Rightarrow> sinr\<cdot>(up\<cdot>b))"
huffman@40496
   260
huffman@40496
   261
definition
huffman@40496
   262
  "decode_sum_u = sscase\<cdot>(\<Lambda>(up\<cdot>a). up\<cdot>(Inl a))\<cdot>(\<Lambda>(up\<cdot>b). up\<cdot>(Inr b))"
huffman@40496
   263
huffman@40496
   264
lemma decode_encode_sum_u [simp]: "decode_sum_u\<cdot>(encode_sum_u\<cdot>x) = x"
huffman@40496
   265
unfolding decode_sum_u_def encode_sum_u_def
huffman@40496
   266
by (case_tac x, simp, rename_tac y, case_tac y, simp_all)
huffman@40496
   267
huffman@40496
   268
lemma encode_decode_sum_u [simp]: "encode_sum_u\<cdot>(decode_sum_u\<cdot>x) = x"
huffman@40496
   269
unfolding decode_sum_u_def encode_sum_u_def
huffman@40496
   270
apply (case_tac x, simp)
huffman@40496
   271
apply (rename_tac a, case_tac a, simp, simp)
huffman@40496
   272
apply (rename_tac b, case_tac b, simp, simp)
huffman@40496
   273
done
huffman@40496
   274
huffman@41321
   275
text {* A deflation combinator for making unpointed types *}
huffman@41321
   276
huffman@41321
   277
definition udefl :: "udom defl \<rightarrow> udom u defl"
huffman@41321
   278
  where "udefl = defl_fun1 (strictify\<cdot>up) (fup\<cdot>ID) ID"
huffman@41321
   279
huffman@41292
   280
lemma ep_pair_strictify_up:
huffman@41292
   281
  "ep_pair (strictify\<cdot>up) (fup\<cdot>ID)"
huffman@41292
   282
apply (rule ep_pair.intro)
huffman@41292
   283
apply (simp add: strictify_conv_if)
huffman@41292
   284
apply (case_tac y, simp, simp add: strictify_conv_if)
huffman@41292
   285
done
huffman@41292
   286
huffman@41321
   287
lemma cast_udefl:
huffman@41321
   288
  "cast\<cdot>(udefl\<cdot>t) = strictify\<cdot>up oo cast\<cdot>t oo fup\<cdot>ID"
huffman@41321
   289
unfolding udefl_def by (simp add: cast_defl_fun1 ep_pair_strictify_up)
huffman@41321
   290
huffman@41321
   291
definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
huffman@41437
   292
  where "sum_liftdefl = (\<Lambda> a b. udefl\<cdot>(ssum_defl\<cdot>(u_liftdefl\<cdot>a)\<cdot>(u_liftdefl\<cdot>b)))"
huffman@41321
   293
huffman@41321
   294
lemma u_emb_bottom: "u_emb\<cdot>\<bottom> = \<bottom>"
huffman@41321
   295
by (rule pcpo_ep_pair.e_strict [unfolded pcpo_ep_pair_def, OF ep_pair_u])
huffman@41321
   296
huffman@41321
   297
(*
huffman@41292
   298
definition sum_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
huffman@41292
   299
  where "sum_liftdefl = defl_fun2 (u_map\<cdot>emb oo strictify\<cdot>up)
huffman@41292
   300
    (fup\<cdot>ID oo u_map\<cdot>prj) ssum_map"
huffman@41321
   301
*)
huffman@41292
   302
huffman@40496
   303
instantiation sum :: (predomain, predomain) predomain
huffman@40496
   304
begin
huffman@40496
   305
huffman@40496
   306
definition
huffman@41321
   307
  "liftemb = (strictify\<cdot>up oo ssum_emb) oo
huffman@41321
   308
    (ssum_map\<cdot>(u_emb oo liftemb)\<cdot>(u_emb oo liftemb) oo encode_sum_u)"
huffman@40496
   309
huffman@40496
   310
definition
huffman@41321
   311
  "liftprj = (decode_sum_u oo ssum_map\<cdot>(liftprj oo u_prj)\<cdot>(liftprj oo u_prj))
huffman@41321
   312
    oo (ssum_prj oo fup\<cdot>ID)"
huffman@40496
   313
huffman@40496
   314
definition
huffman@41292
   315
  "liftdefl (t::('a + 'b) itself) = sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
huffman@40496
   316
huffman@40496
   317
instance proof
huffman@41292
   318
  show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
huffman@40496
   319
    unfolding liftemb_sum_def liftprj_sum_def
huffman@41321
   320
    by (intro ep_pair_comp ep_pair_ssum_map ep_pair_u predomain_ep
huffman@41321
   321
      ep_pair_ssum ep_pair_strictify_up, simp add: ep_pair.intro)
huffman@41292
   322
  show "cast\<cdot>LIFTDEFL('a + 'b) = liftemb oo (liftprj :: udom u \<rightarrow> ('a + 'b) u)"
huffman@40496
   323
    unfolding liftemb_sum_def liftprj_sum_def liftdefl_sum_def
huffman@41437
   324
    by (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl
huffman@41321
   325
      cast_liftdefl cfcomp1 ssum_map_map u_emb_bottom)
huffman@40496
   326
qed
huffman@40496
   327
huffman@29130
   328
end
huffman@40496
   329
huffman@41321
   330
subsection {* Configuring domain package to work with sum type *}
huffman@41321
   331
huffman@41321
   332
lemma liftdefl_sum [domain_defl_simps]:
huffman@41321
   333
  "LIFTDEFL('a::predomain + 'b::predomain) =
huffman@41321
   334
    sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
huffman@41321
   335
by (rule liftdefl_sum_def)
huffman@41321
   336
blanchet@55931
   337
abbreviation map_sum'
blanchet@55931
   338
  where "map_sum' f g \<equiv> Abs_cfun (map_sum (Rep_cfun f) (Rep_cfun g))"
huffman@41321
   339
blanchet@55931
   340
lemma map_sum_ID [domain_map_ID]: "map_sum' ID ID = ID"
blanchet@55931
   341
by (simp add: ID_def cfun_eq_iff map_sum.identity id_def)
huffman@41321
   342
blanchet@55931
   343
lemma deflation_map_sum [domain_deflation]:
blanchet@55931
   344
  "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (map_sum' d1 d2)"
huffman@41321
   345
apply default
huffman@41321
   346
apply (induct_tac x, simp_all add: deflation.idem)
huffman@41321
   347
apply (induct_tac x, simp_all add: deflation.below)
huffman@41321
   348
done
huffman@41321
   349
blanchet@55931
   350
lemma encode_sum_u_map_sum:
blanchet@55931
   351
  "encode_sum_u\<cdot>(u_map\<cdot>(map_sum' f g)\<cdot>(decode_sum_u\<cdot>x))
huffman@41321
   352
    = ssum_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
huffman@41321
   353
apply (induct x, simp add: decode_sum_u_def encode_sum_u_def)
huffman@41321
   354
apply (case_tac x, simp, simp add: decode_sum_u_def encode_sum_u_def)
huffman@41321
   355
apply (case_tac y, simp, simp add: decode_sum_u_def encode_sum_u_def)
huffman@41321
   356
done
huffman@41321
   357
huffman@41321
   358
lemma isodefl_sum [domain_isodefl]:
huffman@41321
   359
  fixes d :: "'a::predomain \<rightarrow> 'a"
huffman@41321
   360
  assumes "isodefl' d1 t1" and "isodefl' d2 t2"
blanchet@55931
   361
  shows "isodefl' (map_sum' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)"
huffman@41321
   362
using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def
huffman@41437
   363
apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl)
blanchet@55931
   364
apply (simp add: cfcomp1 encode_sum_u_map_sum)
huffman@41321
   365
apply (simp add: ssum_map_map u_emb_bottom)
huffman@41321
   366
done
huffman@41321
   367
huffman@41321
   368
setup {*
huffman@41321
   369
  Domain_Take_Proofs.add_rec_type (@{type_name "sum"}, [true, true])
huffman@41321
   370
*}
huffman@41321
   371
huffman@40496
   372
end