src/HOLCF/Representable.thy
author wenzelm
Wed Mar 03 00:33:02 2010 +0100 (2010-03-03)
changeset 35431 8758fe1fc9f8
parent 33809 033831fd9ef3
child 35547 991a6af75978
permissions -rw-r--r--
cleanup type translations;
huffman@33589
     1
(*  Title:      HOLCF/Representable.thy
huffman@33589
     2
    Author:     Brian Huffman
huffman@33589
     3
*)
huffman@33589
     4
huffman@33588
     5
header {* Representable Types *}
huffman@33588
     6
huffman@33588
     7
theory Representable
huffman@33794
     8
imports Algebraic Universal Ssum Sprod One ConvexPD Fixrec
huffman@33794
     9
uses
huffman@33794
    10
  ("Tools/repdef.ML")
huffman@33794
    11
  ("Tools/Domain/domain_isomorphism.ML")
huffman@33588
    12
begin
huffman@33588
    13
huffman@33588
    14
subsection {* Class of representable types *}
huffman@33588
    15
huffman@33588
    16
text "Overloaded embedding and projection functions between
huffman@33588
    17
      a representable type and the universal domain."
huffman@33588
    18
huffman@33588
    19
class rep = bifinite +
huffman@33588
    20
  fixes emb :: "'a::pcpo \<rightarrow> udom"
huffman@33588
    21
  fixes prj :: "udom \<rightarrow> 'a::pcpo"
huffman@33588
    22
  assumes ep_pair_emb_prj: "ep_pair emb prj"
huffman@33588
    23
huffman@33588
    24
interpretation rep!:
huffman@33588
    25
  pcpo_ep_pair
huffman@33588
    26
    "emb :: 'a::rep \<rightarrow> udom"
huffman@33588
    27
    "prj :: udom \<rightarrow> 'a::rep"
huffman@33588
    28
  unfolding pcpo_ep_pair_def
huffman@33588
    29
  by (rule ep_pair_emb_prj)
huffman@33588
    30
huffman@33588
    31
lemmas emb_inverse = rep.e_inverse
huffman@33588
    32
lemmas emb_prj_below = rep.e_p_below
huffman@33588
    33
lemmas emb_eq_iff = rep.e_eq_iff
huffman@33588
    34
lemmas emb_strict = rep.e_strict
huffman@33588
    35
lemmas prj_strict = rep.p_strict
huffman@33588
    36
huffman@33588
    37
huffman@33588
    38
subsection {* Making @{term rep} the default class *}
huffman@33588
    39
huffman@33588
    40
text {*
huffman@33588
    41
  From now on, free type variables are assumed to be in class
huffman@33588
    42
  @{term rep}, unless specified otherwise.
huffman@33588
    43
*}
huffman@33588
    44
huffman@33588
    45
defaultsort rep
huffman@33588
    46
huffman@33588
    47
subsection {* Representations of types *}
huffman@33588
    48
huffman@33588
    49
text "A TypeRep is an algebraic deflation over the universe of values."
huffman@33588
    50
huffman@33588
    51
types TypeRep = "udom alg_defl"
wenzelm@35431
    52
translations (type) "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
huffman@33588
    53
huffman@33588
    54
definition
huffman@33588
    55
  Rep_of :: "'a::rep itself \<Rightarrow> TypeRep"
huffman@33588
    56
where
huffman@33588
    57
  "Rep_of TYPE('a::rep) =
huffman@33588
    58
    (\<Squnion>i. alg_defl_principal (Abs_fin_defl
huffman@33588
    59
      (emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))"
huffman@33588
    60
huffman@33588
    61
syntax "_REP" :: "type \<Rightarrow> TypeRep"  ("(1REP/(1'(_')))")
wenzelm@35431
    62
translations "REP('t)" \<rightleftharpoons> "CONST Rep_of TYPE('t)"
huffman@33588
    63
huffman@33588
    64
lemma cast_REP:
huffman@33588
    65
  "cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)"
huffman@33588
    66
proof -
huffman@33588
    67
  let ?a = "\<lambda>i. emb oo approx i oo (prj::udom \<rightarrow> 'a)"
huffman@33588
    68
  have a: "\<And>i. finite_deflation (?a i)"
huffman@33588
    69
    apply (rule rep.finite_deflation_e_d_p)
huffman@33588
    70
    apply (rule finite_deflation_approx)
huffman@33588
    71
    done
huffman@33588
    72
  show ?thesis
huffman@33588
    73
    unfolding Rep_of_def
huffman@33588
    74
    apply (subst contlub_cfun_arg)
huffman@33588
    75
    apply (rule chainI)
huffman@33588
    76
    apply (rule alg_defl.principal_mono)
huffman@33588
    77
    apply (rule Abs_fin_defl_mono [OF a a])
huffman@33588
    78
    apply (rule chainE, simp)
huffman@33588
    79
    apply (subst cast_alg_defl_principal)
huffman@33588
    80
    apply (simp add: Abs_fin_defl_inverse a)
huffman@33588
    81
    apply (simp add: expand_cfun_eq lub_distribs)
huffman@33588
    82
    done
huffman@33588
    83
qed
huffman@33588
    84
huffman@33588
    85
lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a::rep) = cast\<cdot>REP('a)\<cdot>x"
huffman@33588
    86
by (simp add: cast_REP)
huffman@33588
    87
huffman@33588
    88
lemma in_REP_iff:
huffman@33588
    89
  "x ::: REP('a::rep) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
huffman@33588
    90
by (simp add: in_deflation_def cast_REP)
huffman@33588
    91
huffman@33588
    92
lemma prj_inverse:
huffman@33588
    93
  "x ::: REP('a::rep) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
huffman@33588
    94
by (simp only: in_REP_iff)
huffman@33588
    95
huffman@33588
    96
lemma emb_in_REP [simp]:
huffman@33588
    97
  "emb\<cdot>(x::'a::rep) ::: REP('a)"
huffman@33588
    98
by (simp add: in_REP_iff)
huffman@33588
    99
huffman@33588
   100
subsection {* Coerce operator *}
huffman@33588
   101
huffman@33588
   102
definition coerce :: "'a \<rightarrow> 'b"
huffman@33588
   103
where "coerce = prj oo emb"
huffman@33588
   104
huffman@33588
   105
lemma beta_coerce: "coerce\<cdot>x = prj\<cdot>(emb\<cdot>x)"
huffman@33588
   106
by (simp add: coerce_def)
huffman@33588
   107
huffman@33588
   108
lemma prj_emb: "prj\<cdot>(emb\<cdot>x) = coerce\<cdot>x"
huffman@33588
   109
by (simp add: coerce_def)
huffman@33588
   110
huffman@33588
   111
lemma coerce_strict [simp]: "coerce\<cdot>\<bottom> = \<bottom>"
huffman@33588
   112
by (simp add: coerce_def)
huffman@33588
   113
huffman@33588
   114
lemma coerce_eq_ID [simp]: "(coerce :: 'a \<rightarrow> 'a) = ID"
huffman@33588
   115
by (rule ext_cfun, simp add: beta_coerce)
huffman@33588
   116
huffman@33588
   117
lemma emb_coerce:
huffman@33588
   118
  "REP('a) \<sqsubseteq> REP('b)
huffman@33588
   119
   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = emb\<cdot>x"
huffman@33588
   120
 apply (simp add: beta_coerce)
huffman@33588
   121
 apply (rule prj_inverse)
huffman@33588
   122
 apply (erule subdeflationD)
huffman@33588
   123
 apply (rule emb_in_REP)
huffman@33588
   124
done
huffman@33588
   125
huffman@33588
   126
lemma coerce_prj:
huffman@33588
   127
  "REP('a) \<sqsubseteq> REP('b)
huffman@33588
   128
   \<Longrightarrow> (coerce::'b \<rightarrow> 'a)\<cdot>(prj\<cdot>x) = prj\<cdot>x"
huffman@33588
   129
 apply (simp add: coerce_def)
huffman@33588
   130
 apply (rule emb_eq_iff [THEN iffD1])
huffman@33588
   131
 apply (simp only: emb_prj)
huffman@33588
   132
 apply (rule deflation_below_comp1)
huffman@33588
   133
   apply (rule deflation_cast)
huffman@33588
   134
  apply (rule deflation_cast)
huffman@33588
   135
 apply (erule monofun_cfun_arg)
huffman@33588
   136
done
huffman@33588
   137
huffman@33588
   138
lemma coerce_coerce [simp]:
huffman@33588
   139
  "REP('a) \<sqsubseteq> REP('b)
huffman@33588
   140
   \<Longrightarrow> coerce\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = coerce\<cdot>x"
huffman@33588
   141
by (simp add: beta_coerce prj_inverse subdeflationD)
huffman@33588
   142
huffman@33588
   143
lemma coerce_inverse:
huffman@33588
   144
  "emb\<cdot>(x::'a) ::: REP('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
huffman@33588
   145
by (simp only: beta_coerce prj_inverse emb_inverse)
huffman@33588
   146
huffman@33588
   147
lemma coerce_type:
huffman@33588
   148
  "REP('a) \<sqsubseteq> REP('b)
huffman@33588
   149
   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: REP('a)"
huffman@33588
   150
by (simp add: beta_coerce prj_inverse subdeflationD)
huffman@33588
   151
huffman@33588
   152
lemma ep_pair_coerce:
huffman@33588
   153
  "REP('a) \<sqsubseteq> REP('b)
huffman@33588
   154
   \<Longrightarrow> ep_pair (coerce::'a \<rightarrow> 'b) (coerce::'b \<rightarrow> 'a)"
huffman@33588
   155
 apply (rule ep_pair.intro)
huffman@33588
   156
  apply simp
huffman@33588
   157
 apply (simp only: beta_coerce)
huffman@33588
   158
 apply (rule below_trans)
huffman@33588
   159
  apply (rule monofun_cfun_arg)
huffman@33588
   160
  apply (rule emb_prj_below)
huffman@33588
   161
 apply simp
huffman@33588
   162
done
huffman@33588
   163
huffman@33779
   164
text {* Isomorphism lemmas used internally by the domain package: *}
huffman@33779
   165
huffman@33779
   166
lemma domain_abs_iso:
huffman@33779
   167
  fixes abs and rep
huffman@33779
   168
  assumes REP: "REP('b) = REP('a)"
huffman@33779
   169
  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
huffman@33779
   170
  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
huffman@33779
   171
  shows "rep\<cdot>(abs\<cdot>x) = x"
huffman@33779
   172
unfolding abs_def rep_def by (simp add: REP)
huffman@33779
   173
huffman@33779
   174
lemma domain_rep_iso:
huffman@33779
   175
  fixes abs and rep
huffman@33779
   176
  assumes REP: "REP('b) = REP('a)"
huffman@33779
   177
  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
huffman@33779
   178
  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
huffman@33779
   179
  shows "abs\<cdot>(rep\<cdot>x) = x"
huffman@33779
   180
unfolding abs_def rep_def by (simp add: REP [symmetric])
huffman@33779
   181
huffman@33779
   182
huffman@33588
   183
subsection {* Proving a subtype is representable *}
huffman@33588
   184
huffman@33588
   185
text {*
huffman@33588
   186
  Temporarily relax type constraints for @{term "approx"},
huffman@33588
   187
  @{term emb}, and @{term prj}.
huffman@33588
   188
*}
huffman@33588
   189
huffman@33588
   190
setup {* Sign.add_const_constraint
huffman@33588
   191
  (@{const_name "approx"}, SOME @{typ "nat \<Rightarrow> 'a::cpo \<rightarrow> 'a"}) *}
huffman@33588
   192
huffman@33588
   193
setup {* Sign.add_const_constraint
huffman@33588
   194
  (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) *}
huffman@33588
   195
huffman@33588
   196
setup {* Sign.add_const_constraint
huffman@33588
   197
  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) *}
huffman@33588
   198
huffman@33679
   199
definition
huffman@33679
   200
  repdef_approx ::
huffman@33679
   201
    "('a::pcpo \<Rightarrow> udom) \<Rightarrow> (udom \<Rightarrow> 'a) \<Rightarrow> udom alg_defl \<Rightarrow> nat \<Rightarrow> 'a \<rightarrow> 'a"
huffman@33679
   202
where
huffman@33679
   203
  "repdef_approx Rep Abs t = (\<lambda>i. \<Lambda> x. Abs (cast\<cdot>(approx i\<cdot>t)\<cdot>(Rep x)))"
huffman@33679
   204
huffman@33588
   205
lemma typedef_rep_class:
huffman@33588
   206
  fixes Rep :: "'a::pcpo \<Rightarrow> udom"
huffman@33588
   207
  fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
huffman@33588
   208
  fixes t :: TypeRep
huffman@33588
   209
  assumes type: "type_definition Rep Abs {x. x ::: t}"
huffman@33588
   210
  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@33679
   211
  assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
huffman@33679
   212
  assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
huffman@33679
   213
  assumes approx: "(approx :: nat \<Rightarrow> 'a \<rightarrow> 'a) \<equiv> repdef_approx Rep Abs t"
huffman@33588
   214
  shows "OFCLASS('a, rep_class)"
huffman@33588
   215
proof
huffman@33588
   216
  have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
huffman@33588
   217
    by (simp add: adm_in_deflation)
huffman@33588
   218
  have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
huffman@33588
   219
    unfolding emb
huffman@33588
   220
    apply (rule beta_cfun)
huffman@33588
   221
    apply (rule typedef_cont_Rep [OF type below adm])
huffman@33588
   222
    done
huffman@33588
   223
  have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
huffman@33588
   224
    unfolding prj
huffman@33588
   225
    apply (rule beta_cfun)
huffman@33588
   226
    apply (rule typedef_cont_Abs [OF type below adm])
huffman@33588
   227
    apply simp_all
huffman@33588
   228
    done
huffman@33679
   229
  have cast_cast_approx:
huffman@33679
   230
    "\<And>i x. cast\<cdot>t\<cdot>(cast\<cdot>(approx i\<cdot>t)\<cdot>x) = cast\<cdot>(approx i\<cdot>t)\<cdot>x"
huffman@33679
   231
    apply (rule cast_fixed)
huffman@33679
   232
    apply (rule subdeflationD)
huffman@33679
   233
    apply (rule approx.below)
huffman@33679
   234
    apply (rule cast_in_deflation)
huffman@33679
   235
    done
huffman@33679
   236
  have approx':
huffman@33679
   237
    "approx = (\<lambda>i. \<Lambda>(x::'a). prj\<cdot>(cast\<cdot>(approx i\<cdot>t)\<cdot>(emb\<cdot>x)))"
huffman@33679
   238
    unfolding approx repdef_approx_def
huffman@33679
   239
    apply (subst cast_cast_approx [symmetric])
huffman@33679
   240
    apply (simp add: prj_beta [symmetric] emb_beta [symmetric])
huffman@33679
   241
    done
huffman@33588
   242
  have emb_in_deflation: "\<And>x::'a. emb\<cdot>x ::: t"
huffman@33588
   243
    using type_definition.Rep [OF type]
huffman@33588
   244
    by (simp add: emb_beta)
huffman@33588
   245
  have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
huffman@33588
   246
    unfolding prj_beta
huffman@33588
   247
    apply (simp add: cast_fixed [OF emb_in_deflation])
huffman@33588
   248
    apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
huffman@33588
   249
    done
huffman@33588
   250
  have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
huffman@33588
   251
    unfolding prj_beta emb_beta
huffman@33588
   252
    by (simp add: type_definition.Abs_inverse [OF type])
huffman@33588
   253
  show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
huffman@33588
   254
    apply default
huffman@33588
   255
    apply (simp add: prj_emb)
huffman@33588
   256
    apply (simp add: emb_prj cast.below)
huffman@33588
   257
    done
huffman@33588
   258
  show "chain (approx :: nat \<Rightarrow> 'a \<rightarrow> 'a)"
huffman@33679
   259
    unfolding approx' by simp
huffman@33588
   260
  show "\<And>x::'a. (\<Squnion>i. approx i\<cdot>x) = x"
huffman@33679
   261
    unfolding approx'
huffman@33588
   262
    apply (simp add: lub_distribs)
huffman@33588
   263
    apply (subst cast_fixed [OF emb_in_deflation])
huffman@33588
   264
    apply (rule prj_emb)
huffman@33588
   265
    done
huffman@33588
   266
  show "\<And>(i::nat) (x::'a). approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
huffman@33679
   267
    unfolding approx'
huffman@33588
   268
    apply simp
huffman@33588
   269
    apply (simp add: emb_prj)
huffman@33588
   270
    apply (simp add: cast_cast_approx)
huffman@33588
   271
    done
huffman@33588
   272
  show "\<And>i::nat. finite {x::'a. approx i\<cdot>x = x}"
huffman@33588
   273
    apply (rule_tac B="(\<lambda>x. prj\<cdot>x) ` {x. cast\<cdot>(approx i\<cdot>t)\<cdot>x = x}"
huffman@33588
   274
           in finite_subset)
huffman@33679
   275
    apply (clarsimp simp add: approx')
huffman@33588
   276
    apply (drule_tac f="\<lambda>x. emb\<cdot>x" in arg_cong)
huffman@33588
   277
    apply (rule image_eqI)
huffman@33588
   278
    apply (rule prj_emb [symmetric])
huffman@33588
   279
    apply (simp add: emb_prj)
huffman@33588
   280
    apply (simp add: cast_cast_approx)
huffman@33588
   281
    apply (rule finite_imageI)
huffman@33588
   282
    apply (simp add: cast_approx_fixed_iff)
huffman@33588
   283
    apply (simp add: Collect_conj_eq)
huffman@33588
   284
    apply (simp add: finite_fixes_approx)
huffman@33588
   285
    done
huffman@33588
   286
qed
huffman@33588
   287
huffman@33588
   288
text {* Restore original typing constraints *}
huffman@33588
   289
huffman@33588
   290
setup {* Sign.add_const_constraint
huffman@33588
   291
  (@{const_name "approx"}, SOME @{typ "nat \<Rightarrow> 'a::profinite \<rightarrow> 'a"}) *}
huffman@33588
   292
huffman@33588
   293
setup {* Sign.add_const_constraint
huffman@33588
   294
  (@{const_name emb}, SOME @{typ "'a::rep \<rightarrow> udom"}) *}
huffman@33588
   295
huffman@33588
   296
setup {* Sign.add_const_constraint
huffman@33588
   297
  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::rep"}) *}
huffman@33588
   298
huffman@33588
   299
lemma typedef_REP:
huffman@33588
   300
  fixes Rep :: "'a::rep \<Rightarrow> udom"
huffman@33588
   301
  fixes Abs :: "udom \<Rightarrow> 'a::rep"
huffman@33588
   302
  fixes t :: TypeRep
huffman@33588
   303
  assumes type: "type_definition Rep Abs {x. x ::: t}"
huffman@33588
   304
  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@33679
   305
  assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
huffman@33679
   306
  assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
huffman@33588
   307
  shows "REP('a) = t"
huffman@33588
   308
proof -
huffman@33588
   309
  have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
huffman@33588
   310
    by (simp add: adm_in_deflation)
huffman@33588
   311
  have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
huffman@33588
   312
    unfolding emb
huffman@33588
   313
    apply (rule beta_cfun)
huffman@33588
   314
    apply (rule typedef_cont_Rep [OF type below adm])
huffman@33588
   315
    done
huffman@33588
   316
  have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
huffman@33588
   317
    unfolding prj
huffman@33588
   318
    apply (rule beta_cfun)
huffman@33588
   319
    apply (rule typedef_cont_Abs [OF type below adm])
huffman@33588
   320
    apply simp_all
huffman@33588
   321
    done
huffman@33588
   322
  have emb_in_deflation: "\<And>x::'a. emb\<cdot>x ::: t"
huffman@33588
   323
    using type_definition.Rep [OF type]
huffman@33588
   324
    by (simp add: emb_beta)
huffman@33588
   325
  have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
huffman@33588
   326
    unfolding prj_beta
huffman@33588
   327
    apply (simp add: cast_fixed [OF emb_in_deflation])
huffman@33588
   328
    apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
huffman@33588
   329
    done
huffman@33588
   330
  have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
huffman@33588
   331
    unfolding prj_beta emb_beta
huffman@33588
   332
    by (simp add: type_definition.Abs_inverse [OF type])
huffman@33588
   333
  show "REP('a) = t"
huffman@33588
   334
    apply (rule cast_eq_imp_eq, rule ext_cfun)
huffman@33588
   335
    apply (simp add: cast_REP emb_prj)
huffman@33588
   336
    done
huffman@33588
   337
qed
huffman@33588
   338
huffman@33679
   339
lemma adm_mem_Collect_in_deflation: "adm (\<lambda>x. x \<in> {x. x ::: A})"
huffman@33679
   340
unfolding mem_Collect_eq by (rule adm_in_deflation)
huffman@33679
   341
huffman@33679
   342
use "Tools/repdef.ML"
huffman@33679
   343
huffman@33588
   344
huffman@33588
   345
subsection {* Instances of class @{text rep} *}
huffman@33588
   346
huffman@33588
   347
subsubsection {* Universal Domain *}
huffman@33588
   348
huffman@33588
   349
text "The Universal Domain itself is trivially representable."
huffman@33588
   350
huffman@33588
   351
instantiation udom :: rep
huffman@33588
   352
begin
huffman@33588
   353
huffman@33588
   354
definition emb_udom_def [simp]: "emb = (ID :: udom \<rightarrow> udom)"
huffman@33588
   355
definition prj_udom_def [simp]: "prj = (ID :: udom \<rightarrow> udom)"
huffman@33588
   356
huffman@33588
   357
instance
huffman@33588
   358
 apply (intro_classes)
huffman@33588
   359
 apply (simp_all add: ep_pair.intro)
huffman@33588
   360
done
huffman@33588
   361
huffman@33588
   362
end
huffman@33588
   363
huffman@33588
   364
subsubsection {* Lifted types *}
huffman@33588
   365
huffman@33588
   366
instantiation lift :: (countable) rep
huffman@33588
   367
begin
huffman@33588
   368
huffman@33588
   369
definition emb_lift_def:
huffman@33588
   370
  "emb = udom_emb oo (FLIFT x. Def (to_nat x))"
huffman@33588
   371
huffman@33588
   372
definition prj_lift_def:
huffman@33588
   373
  "prj = (FLIFT n. if (\<exists>x::'a::countable. n = to_nat x)
huffman@33588
   374
                    then Def (THE x::'a. n = to_nat x) else \<bottom>) oo udom_prj"
huffman@33588
   375
huffman@33588
   376
instance
huffman@33588
   377
 apply (intro_classes, unfold emb_lift_def prj_lift_def)
huffman@33588
   378
 apply (rule ep_pair_comp [OF _ ep_pair_udom])
huffman@33588
   379
 apply (rule ep_pair.intro)
huffman@33588
   380
  apply (case_tac x, simp, simp)
huffman@33588
   381
 apply (case_tac y, simp, clarsimp)
huffman@33588
   382
done
huffman@33588
   383
huffman@33588
   384
end
huffman@33588
   385
huffman@33588
   386
subsubsection {* Representable type constructors *}
huffman@33588
   387
huffman@33588
   388
text "Functions between representable types are representable."
huffman@33588
   389
huffman@33588
   390
instantiation "->" :: (rep, rep) rep
huffman@33588
   391
begin
huffman@33588
   392
huffman@33588
   393
definition emb_cfun_def: "emb = udom_emb oo cfun_map\<cdot>prj\<cdot>emb"
huffman@33588
   394
definition prj_cfun_def: "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj"
huffman@33588
   395
huffman@33588
   396
instance
huffman@33588
   397
 apply (intro_classes, unfold emb_cfun_def prj_cfun_def)
huffman@33588
   398
 apply (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj ep_pair_udom)
huffman@33588
   399
done
huffman@33588
   400
huffman@33588
   401
end
huffman@33588
   402
huffman@33588
   403
text "Strict products of representable types are representable."
huffman@33588
   404
huffman@33588
   405
instantiation "**" :: (rep, rep) rep
huffman@33588
   406
begin
huffman@33588
   407
huffman@33588
   408
definition emb_sprod_def: "emb = udom_emb oo sprod_map\<cdot>emb\<cdot>emb"
huffman@33588
   409
definition prj_sprod_def: "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj"
huffman@33588
   410
huffman@33588
   411
instance
huffman@33588
   412
 apply (intro_classes, unfold emb_sprod_def prj_sprod_def)
huffman@33588
   413
 apply (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj ep_pair_udom)
huffman@33588
   414
done
huffman@33588
   415
huffman@33588
   416
end
huffman@33588
   417
huffman@33588
   418
text "Strict sums of representable types are representable."
huffman@33588
   419
huffman@33588
   420
instantiation "++" :: (rep, rep) rep
huffman@33588
   421
begin
huffman@33588
   422
huffman@33588
   423
definition emb_ssum_def: "emb = udom_emb oo ssum_map\<cdot>emb\<cdot>emb"
huffman@33588
   424
definition prj_ssum_def: "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj"
huffman@33588
   425
huffman@33588
   426
instance
huffman@33588
   427
 apply (intro_classes, unfold emb_ssum_def prj_ssum_def)
huffman@33588
   428
 apply (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj ep_pair_udom)
huffman@33588
   429
done
huffman@33588
   430
huffman@33588
   431
end
huffman@33588
   432
huffman@33588
   433
text "Up of a representable type is representable."
huffman@33588
   434
huffman@33588
   435
instantiation "u" :: (rep) rep
huffman@33588
   436
begin
huffman@33588
   437
huffman@33588
   438
definition emb_u_def: "emb = udom_emb oo u_map\<cdot>emb"
huffman@33588
   439
definition prj_u_def: "prj = u_map\<cdot>prj oo udom_prj"
huffman@33588
   440
huffman@33588
   441
instance
huffman@33588
   442
 apply (intro_classes, unfold emb_u_def prj_u_def)
huffman@33588
   443
 apply (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj ep_pair_udom)
huffman@33588
   444
done
huffman@33588
   445
huffman@33588
   446
end
huffman@33588
   447
huffman@33588
   448
text "Cartesian products of representable types are representable."
huffman@33588
   449
huffman@33588
   450
instantiation "*" :: (rep, rep) rep
huffman@33588
   451
begin
huffman@33588
   452
huffman@33588
   453
definition emb_cprod_def: "emb = udom_emb oo cprod_map\<cdot>emb\<cdot>emb"
huffman@33588
   454
definition prj_cprod_def: "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj"
huffman@33588
   455
huffman@33588
   456
instance
huffman@33588
   457
 apply (intro_classes, unfold emb_cprod_def prj_cprod_def)
huffman@33588
   458
 apply (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj ep_pair_udom)
huffman@33588
   459
done
huffman@33588
   460
huffman@33588
   461
end
huffman@33588
   462
huffman@33588
   463
text "Upper powerdomain of a representable type is representable."
huffman@33588
   464
huffman@33588
   465
instantiation upper_pd :: (rep) rep
huffman@33588
   466
begin
huffman@33588
   467
huffman@33588
   468
definition emb_upper_pd_def: "emb = udom_emb oo upper_map\<cdot>emb"
huffman@33588
   469
definition prj_upper_pd_def: "prj = upper_map\<cdot>prj oo udom_prj"
huffman@33588
   470
huffman@33588
   471
instance
huffman@33588
   472
 apply (intro_classes, unfold emb_upper_pd_def prj_upper_pd_def)
huffman@33588
   473
 apply (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj ep_pair_udom)
huffman@33588
   474
done
huffman@33588
   475
huffman@33588
   476
end
huffman@33588
   477
huffman@33588
   478
text "Lower powerdomain of a representable type is representable."
huffman@33588
   479
huffman@33588
   480
instantiation lower_pd :: (rep) rep
huffman@33588
   481
begin
huffman@33588
   482
huffman@33588
   483
definition emb_lower_pd_def: "emb = udom_emb oo lower_map\<cdot>emb"
huffman@33588
   484
definition prj_lower_pd_def: "prj = lower_map\<cdot>prj oo udom_prj"
huffman@33588
   485
huffman@33588
   486
instance
huffman@33588
   487
 apply (intro_classes, unfold emb_lower_pd_def prj_lower_pd_def)
huffman@33588
   488
 apply (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj ep_pair_udom)
huffman@33588
   489
done
huffman@33588
   490
huffman@33588
   491
end
huffman@33588
   492
huffman@33588
   493
text "Convex powerdomain of a representable type is representable."
huffman@33588
   494
huffman@33588
   495
instantiation convex_pd :: (rep) rep
huffman@33588
   496
begin
huffman@33588
   497
huffman@33588
   498
definition emb_convex_pd_def: "emb = udom_emb oo convex_map\<cdot>emb"
huffman@33588
   499
definition prj_convex_pd_def: "prj = convex_map\<cdot>prj oo udom_prj"
huffman@33588
   500
huffman@33588
   501
instance
huffman@33588
   502
 apply (intro_classes, unfold emb_convex_pd_def prj_convex_pd_def)
huffman@33588
   503
 apply (intro ep_pair_comp ep_pair_convex_map ep_pair_emb_prj ep_pair_udom)
huffman@33588
   504
done
huffman@33588
   505
huffman@33588
   506
end
huffman@33588
   507
huffman@33588
   508
subsection {* Finite deflation lemmas *}
huffman@33588
   509
huffman@33588
   510
text "TODO: move these lemmas somewhere else"
huffman@33588
   511
huffman@33588
   512
lemma finite_compact_range_imp_finite_range:
huffman@33588
   513
  fixes d :: "'a::profinite \<rightarrow> 'b::cpo"
huffman@33588
   514
  assumes "finite ((\<lambda>x. d\<cdot>x) ` {x. compact x})"
huffman@33588
   515
  shows "finite (range (\<lambda>x. d\<cdot>x))"
huffman@33588
   516
proof (rule finite_subset [OF _ prems])
huffman@33588
   517
  {
huffman@33588
   518
    fix x :: 'a
huffman@33588
   519
    have "range (\<lambda>i. d\<cdot>(approx i\<cdot>x)) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
huffman@33588
   520
      by auto
huffman@33588
   521
    hence "finite (range (\<lambda>i. d\<cdot>(approx i\<cdot>x)))"
huffman@33588
   522
      using prems by (rule finite_subset)
huffman@33588
   523
    hence "finite_chain (\<lambda>i. d\<cdot>(approx i\<cdot>x))"
huffman@33588
   524
      by (simp add: finite_range_imp_finch)
huffman@33588
   525
    hence "\<exists>i. (\<Squnion>i. d\<cdot>(approx i\<cdot>x)) = d\<cdot>(approx i\<cdot>x)"
huffman@33588
   526
      by (simp add: finite_chain_def maxinch_is_thelub)
huffman@33588
   527
    hence "\<exists>i. d\<cdot>x = d\<cdot>(approx i\<cdot>x)"
huffman@33588
   528
      by (simp add: lub_distribs)
huffman@33588
   529
    hence "d\<cdot>x \<in> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
huffman@33588
   530
      by auto
huffman@33588
   531
  }
huffman@33588
   532
  thus "range (\<lambda>x. d\<cdot>x) \<subseteq> (\<lambda>x. d\<cdot>x) ` {x. compact x}"
huffman@33588
   533
    by clarsimp
huffman@33588
   534
qed
huffman@33588
   535
huffman@33588
   536
lemma finite_deflation_upper_map:
huffman@33588
   537
  assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>d)"
huffman@33588
   538
proof (intro finite_deflation.intro finite_deflation_axioms.intro)
huffman@33588
   539
  interpret d: finite_deflation d by fact
huffman@33588
   540
  have "deflation d" by fact
huffman@33588
   541
  thus "deflation (upper_map\<cdot>d)" by (rule deflation_upper_map)
huffman@33588
   542
  have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
huffman@33588
   543
  hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
huffman@33588
   544
    by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
huffman@33588
   545
  hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
huffman@33588
   546
  hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
huffman@33588
   547
    by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
huffman@33588
   548
  hence "finite (upper_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
huffman@33588
   549
  hence "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` range upper_principal)"
huffman@33588
   550
    apply (rule finite_subset [COMP swap_prems_rl])
huffman@33588
   551
    apply (clarsimp, rename_tac t)
huffman@33588
   552
    apply (induct_tac t rule: pd_basis_induct)
huffman@33588
   553
    apply (simp only: upper_unit_Rep_compact_basis [symmetric] upper_map_unit)
huffman@33588
   554
    apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
huffman@33588
   555
    apply clarsimp
huffman@33588
   556
    apply (rule imageI)
huffman@33588
   557
    apply (rule vimageI2)
huffman@33588
   558
    apply (simp add: Rep_PDUnit)
huffman@33588
   559
    apply (rule image_eqI)
huffman@33588
   560
    apply (erule sym)
huffman@33588
   561
    apply simp
huffman@33588
   562
    apply (rule exI)
huffman@33588
   563
    apply (rule Abs_compact_basis_inverse [symmetric])
huffman@33588
   564
    apply (simp add: d.compact)
huffman@33588
   565
    apply (simp only: upper_plus_principal [symmetric] upper_map_plus)
huffman@33588
   566
    apply clarsimp
huffman@33588
   567
    apply (rule imageI)
huffman@33588
   568
    apply (rule vimageI2)
huffman@33588
   569
    apply (simp add: Rep_PDPlus)
huffman@33588
   570
    done
huffman@33588
   571
  moreover have "{xs::'a upper_pd. compact xs} = range upper_principal"
huffman@33588
   572
    by (auto dest: upper_pd.compact_imp_principal)
huffman@33588
   573
  ultimately have "finite ((\<lambda>xs. upper_map\<cdot>d\<cdot>xs) ` {xs::'a upper_pd. compact xs})"
huffman@33588
   574
    by simp
huffman@33588
   575
  hence "finite (range (\<lambda>xs. upper_map\<cdot>d\<cdot>xs))"
huffman@33588
   576
    by (rule finite_compact_range_imp_finite_range)
huffman@33588
   577
  thus "finite {xs. upper_map\<cdot>d\<cdot>xs = xs}"
huffman@33588
   578
    by (rule finite_range_imp_finite_fixes)
huffman@33588
   579
qed
huffman@33588
   580
huffman@33588
   581
lemma finite_deflation_lower_map:
huffman@33588
   582
  assumes "finite_deflation d" shows "finite_deflation (lower_map\<cdot>d)"
huffman@33588
   583
proof (intro finite_deflation.intro finite_deflation_axioms.intro)
huffman@33588
   584
  interpret d: finite_deflation d by fact
huffman@33588
   585
  have "deflation d" by fact
huffman@33588
   586
  thus "deflation (lower_map\<cdot>d)" by (rule deflation_lower_map)
huffman@33588
   587
  have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
huffman@33588
   588
  hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
huffman@33588
   589
    by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
huffman@33588
   590
  hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
huffman@33588
   591
  hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
huffman@33588
   592
    by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
huffman@33588
   593
  hence "finite (lower_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
huffman@33588
   594
  hence "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` range lower_principal)"
huffman@33588
   595
    apply (rule finite_subset [COMP swap_prems_rl])
huffman@33588
   596
    apply (clarsimp, rename_tac t)
huffman@33588
   597
    apply (induct_tac t rule: pd_basis_induct)
huffman@33588
   598
    apply (simp only: lower_unit_Rep_compact_basis [symmetric] lower_map_unit)
huffman@33588
   599
    apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
huffman@33588
   600
    apply clarsimp
huffman@33588
   601
    apply (rule imageI)
huffman@33588
   602
    apply (rule vimageI2)
huffman@33588
   603
    apply (simp add: Rep_PDUnit)
huffman@33588
   604
    apply (rule image_eqI)
huffman@33588
   605
    apply (erule sym)
huffman@33588
   606
    apply simp
huffman@33588
   607
    apply (rule exI)
huffman@33588
   608
    apply (rule Abs_compact_basis_inverse [symmetric])
huffman@33588
   609
    apply (simp add: d.compact)
huffman@33588
   610
    apply (simp only: lower_plus_principal [symmetric] lower_map_plus)
huffman@33588
   611
    apply clarsimp
huffman@33588
   612
    apply (rule imageI)
huffman@33588
   613
    apply (rule vimageI2)
huffman@33588
   614
    apply (simp add: Rep_PDPlus)
huffman@33588
   615
    done
huffman@33588
   616
  moreover have "{xs::'a lower_pd. compact xs} = range lower_principal"
huffman@33588
   617
    by (auto dest: lower_pd.compact_imp_principal)
huffman@33588
   618
  ultimately have "finite ((\<lambda>xs. lower_map\<cdot>d\<cdot>xs) ` {xs::'a lower_pd. compact xs})"
huffman@33588
   619
    by simp
huffman@33588
   620
  hence "finite (range (\<lambda>xs. lower_map\<cdot>d\<cdot>xs))"
huffman@33588
   621
    by (rule finite_compact_range_imp_finite_range)
huffman@33588
   622
  thus "finite {xs. lower_map\<cdot>d\<cdot>xs = xs}"
huffman@33588
   623
    by (rule finite_range_imp_finite_fixes)
huffman@33588
   624
qed
huffman@33588
   625
huffman@33588
   626
lemma finite_deflation_convex_map:
huffman@33588
   627
  assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>d)"
huffman@33588
   628
proof (intro finite_deflation.intro finite_deflation_axioms.intro)
huffman@33588
   629
  interpret d: finite_deflation d by fact
huffman@33588
   630
  have "deflation d" by fact
huffman@33588
   631
  thus "deflation (convex_map\<cdot>d)" by (rule deflation_convex_map)
huffman@33588
   632
  have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
huffman@33588
   633
  hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
huffman@33588
   634
    by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
huffman@33588
   635
  hence "finite (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x)))" by simp
huffman@33588
   636
  hence "finite (Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))"
huffman@33588
   637
    by (rule finite_vimageI, simp add: inj_on_def Rep_pd_basis_inject)
huffman@33588
   638
  hence "finite (convex_principal ` Rep_pd_basis -` (Pow (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))))" by simp
huffman@33588
   639
  hence "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` range convex_principal)"
huffman@33588
   640
    apply (rule finite_subset [COMP swap_prems_rl])
huffman@33588
   641
    apply (clarsimp, rename_tac t)
huffman@33588
   642
    apply (induct_tac t rule: pd_basis_induct)
huffman@33588
   643
    apply (simp only: convex_unit_Rep_compact_basis [symmetric] convex_map_unit)
huffman@33588
   644
    apply (subgoal_tac "\<exists>b. d\<cdot>(Rep_compact_basis a) = Rep_compact_basis b")
huffman@33588
   645
    apply clarsimp
huffman@33588
   646
    apply (rule imageI)
huffman@33588
   647
    apply (rule vimageI2)
huffman@33588
   648
    apply (simp add: Rep_PDUnit)
huffman@33588
   649
    apply (rule image_eqI)
huffman@33588
   650
    apply (erule sym)
huffman@33588
   651
    apply simp
huffman@33588
   652
    apply (rule exI)
huffman@33588
   653
    apply (rule Abs_compact_basis_inverse [symmetric])
huffman@33588
   654
    apply (simp add: d.compact)
huffman@33588
   655
    apply (simp only: convex_plus_principal [symmetric] convex_map_plus)
huffman@33588
   656
    apply clarsimp
huffman@33588
   657
    apply (rule imageI)
huffman@33588
   658
    apply (rule vimageI2)
huffman@33588
   659
    apply (simp add: Rep_PDPlus)
huffman@33588
   660
    done
huffman@33588
   661
  moreover have "{xs::'a convex_pd. compact xs} = range convex_principal"
huffman@33588
   662
    by (auto dest: convex_pd.compact_imp_principal)
huffman@33588
   663
  ultimately have "finite ((\<lambda>xs. convex_map\<cdot>d\<cdot>xs) ` {xs::'a convex_pd. compact xs})"
huffman@33588
   664
    by simp
huffman@33588
   665
  hence "finite (range (\<lambda>xs. convex_map\<cdot>d\<cdot>xs))"
huffman@33588
   666
    by (rule finite_compact_range_imp_finite_range)
huffman@33588
   667
  thus "finite {xs. convex_map\<cdot>d\<cdot>xs = xs}"
huffman@33588
   668
    by (rule finite_range_imp_finite_fixes)
huffman@33588
   669
qed
huffman@33588
   670
huffman@33588
   671
subsection {* Type combinators *}
huffman@33588
   672
huffman@33588
   673
definition
huffman@33588
   674
  TypeRep_fun1 ::
huffman@33588
   675
    "((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
huffman@33588
   676
      \<Rightarrow> (TypeRep \<rightarrow> TypeRep)"
huffman@33588
   677
where
huffman@33588
   678
  "TypeRep_fun1 f =
huffman@33588
   679
    alg_defl.basis_fun (\<lambda>a.
huffman@33588
   680
      alg_defl_principal (
huffman@33588
   681
        Abs_fin_defl (udom_emb oo f\<cdot>(Rep_fin_defl a) oo udom_prj)))"
huffman@33588
   682
huffman@33588
   683
definition
huffman@33588
   684
  TypeRep_fun2 ::
huffman@33588
   685
    "((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
huffman@33588
   686
      \<Rightarrow> (TypeRep \<rightarrow> TypeRep \<rightarrow> TypeRep)"
huffman@33588
   687
where
huffman@33588
   688
  "TypeRep_fun2 f =
huffman@33588
   689
    alg_defl.basis_fun (\<lambda>a.
huffman@33588
   690
      alg_defl.basis_fun (\<lambda>b.
huffman@33588
   691
        alg_defl_principal (
huffman@33588
   692
          Abs_fin_defl (udom_emb oo
huffman@33588
   693
            f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj))))"
huffman@33588
   694
huffman@33784
   695
definition "cfun_defl = TypeRep_fun2 cfun_map"
huffman@33784
   696
definition "ssum_defl = TypeRep_fun2 ssum_map"
huffman@33784
   697
definition "sprod_defl = TypeRep_fun2 sprod_map"
huffman@33784
   698
definition "cprod_defl = TypeRep_fun2 cprod_map"
huffman@33784
   699
definition "u_defl = TypeRep_fun1 u_map"
huffman@33784
   700
definition "upper_defl = TypeRep_fun1 upper_map"
huffman@33784
   701
definition "lower_defl = TypeRep_fun1 lower_map"
huffman@33784
   702
definition "convex_defl = TypeRep_fun1 convex_map"
huffman@33588
   703
huffman@33588
   704
lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
huffman@33588
   705
unfolding below_fin_defl_def .
huffman@33588
   706
huffman@33588
   707
lemma cast_TypeRep_fun1:
huffman@33588
   708
  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
huffman@33588
   709
  shows "cast\<cdot>(TypeRep_fun1 f\<cdot>A) = udom_emb oo f\<cdot>(cast\<cdot>A) oo udom_prj"
huffman@33588
   710
proof -
huffman@33588
   711
  have 1: "\<And>a. finite_deflation (udom_emb oo f\<cdot>(Rep_fin_defl a) oo udom_prj)"
huffman@33588
   712
    apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom])
huffman@33588
   713
    apply (rule f, rule finite_deflation_Rep_fin_defl)
huffman@33588
   714
    done
huffman@33588
   715
  show ?thesis
huffman@33588
   716
    by (induct A rule: alg_defl.principal_induct, simp)
huffman@33588
   717
       (simp only: TypeRep_fun1_def
huffman@33588
   718
                   alg_defl.basis_fun_principal
huffman@33588
   719
                   alg_defl.basis_fun_mono
huffman@33588
   720
                   alg_defl.principal_mono
huffman@33588
   721
                   Abs_fin_defl_mono [OF 1 1]
huffman@33588
   722
                   monofun_cfun below_refl
huffman@33588
   723
                   Rep_fin_defl_mono
huffman@33588
   724
                   cast_alg_defl_principal
huffman@33588
   725
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
huffman@33588
   726
qed
huffman@33588
   727
huffman@33588
   728
lemma cast_TypeRep_fun2:
huffman@33588
   729
  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
huffman@33588
   730
                finite_deflation (f\<cdot>a\<cdot>b)"
huffman@33588
   731
  shows "cast\<cdot>(TypeRep_fun2 f\<cdot>A\<cdot>B) = udom_emb oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
huffman@33588
   732
proof -
huffman@33588
   733
  have 1: "\<And>a b. finite_deflation
huffman@33588
   734
           (udom_emb oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj)"
huffman@33588
   735
    apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom])
huffman@33588
   736
    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
huffman@33588
   737
    done
huffman@33588
   738
  show ?thesis
huffman@33588
   739
    by (induct A B rule: alg_defl.principal_induct2, simp, simp)
huffman@33588
   740
       (simp only: TypeRep_fun2_def
huffman@33588
   741
                   alg_defl.basis_fun_principal
huffman@33588
   742
                   alg_defl.basis_fun_mono
huffman@33588
   743
                   alg_defl.principal_mono
huffman@33588
   744
                   Abs_fin_defl_mono [OF 1 1]
huffman@33588
   745
                   monofun_cfun below_refl
huffman@33588
   746
                   Rep_fin_defl_mono
huffman@33588
   747
                   cast_alg_defl_principal
huffman@33588
   748
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
huffman@33588
   749
qed
huffman@33588
   750
huffman@33784
   751
lemma cast_cfun_defl:
huffman@33784
   752
  "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
huffman@33784
   753
unfolding cfun_defl_def
huffman@33588
   754
apply (rule cast_TypeRep_fun2)
huffman@33588
   755
apply (erule (1) finite_deflation_cfun_map)
huffman@33588
   756
done
huffman@33588
   757
huffman@33784
   758
lemma cast_ssum_defl:
huffman@33784
   759
  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
huffman@33784
   760
unfolding ssum_defl_def
huffman@33588
   761
apply (rule cast_TypeRep_fun2)
huffman@33588
   762
apply (erule (1) finite_deflation_ssum_map)
huffman@33588
   763
done
huffman@33588
   764
huffman@33784
   765
lemma cast_sprod_defl:
huffman@33784
   766
  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
huffman@33784
   767
unfolding sprod_defl_def
huffman@33588
   768
apply (rule cast_TypeRep_fun2)
huffman@33588
   769
apply (erule (1) finite_deflation_sprod_map)
huffman@33588
   770
done
huffman@33588
   771
huffman@33784
   772
lemma cast_cprod_defl:
huffman@33784
   773
  "cast\<cdot>(cprod_defl\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
huffman@33784
   774
unfolding cprod_defl_def
huffman@33588
   775
apply (rule cast_TypeRep_fun2)
huffman@33588
   776
apply (erule (1) finite_deflation_cprod_map)
huffman@33588
   777
done
huffman@33588
   778
huffman@33784
   779
lemma cast_u_defl:
huffman@33784
   780
  "cast\<cdot>(u_defl\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj"
huffman@33784
   781
unfolding u_defl_def
huffman@33588
   782
apply (rule cast_TypeRep_fun1)
huffman@33588
   783
apply (erule finite_deflation_u_map)
huffman@33588
   784
done
huffman@33588
   785
huffman@33784
   786
lemma cast_upper_defl:
huffman@33784
   787
  "cast\<cdot>(upper_defl\<cdot>A) = udom_emb oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj"
huffman@33784
   788
unfolding upper_defl_def
huffman@33588
   789
apply (rule cast_TypeRep_fun1)
huffman@33588
   790
apply (erule finite_deflation_upper_map)
huffman@33588
   791
done
huffman@33588
   792
huffman@33784
   793
lemma cast_lower_defl:
huffman@33784
   794
  "cast\<cdot>(lower_defl\<cdot>A) = udom_emb oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj"
huffman@33784
   795
unfolding lower_defl_def
huffman@33588
   796
apply (rule cast_TypeRep_fun1)
huffman@33588
   797
apply (erule finite_deflation_lower_map)
huffman@33588
   798
done
huffman@33588
   799
huffman@33784
   800
lemma cast_convex_defl:
huffman@33784
   801
  "cast\<cdot>(convex_defl\<cdot>A) = udom_emb oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj"
huffman@33784
   802
unfolding convex_defl_def
huffman@33588
   803
apply (rule cast_TypeRep_fun1)
huffman@33588
   804
apply (erule finite_deflation_convex_map)
huffman@33588
   805
done
huffman@33588
   806
huffman@33588
   807
text {* REP of type constructor = type combinator *}
huffman@33588
   808
huffman@33784
   809
lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_defl\<cdot>REP('a)\<cdot>REP('b)"
huffman@33588
   810
apply (rule cast_eq_imp_eq, rule ext_cfun)
huffman@33784
   811
apply (simp add: cast_REP cast_cfun_defl)
huffman@33588
   812
apply (simp add: cfun_map_def)
huffman@33588
   813
apply (simp only: prj_cfun_def emb_cfun_def)
huffman@33588
   814
apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom])
huffman@33588
   815
done
huffman@33588
   816
huffman@33588
   817
huffman@33784
   818
lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_defl\<cdot>REP('a)\<cdot>REP('b)"
huffman@33588
   819
apply (rule cast_eq_imp_eq, rule ext_cfun)
huffman@33784
   820
apply (simp add: cast_REP cast_ssum_defl)
huffman@33588
   821
apply (simp add: prj_ssum_def)
huffman@33588
   822
apply (simp add: emb_ssum_def)
huffman@33588
   823
apply (simp add: ssum_map_map cfcomp1)
huffman@33588
   824
done
huffman@33588
   825
huffman@33784
   826
lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_defl\<cdot>REP('a)\<cdot>REP('b)"
huffman@33588
   827
apply (rule cast_eq_imp_eq, rule ext_cfun)
huffman@33784
   828
apply (simp add: cast_REP cast_sprod_defl)
huffman@33588
   829
apply (simp add: prj_sprod_def)
huffman@33588
   830
apply (simp add: emb_sprod_def)
huffman@33588
   831
apply (simp add: sprod_map_map cfcomp1)
huffman@33588
   832
done
huffman@33588
   833
huffman@33784
   834
lemma REP_cprod: "REP('a \<times> 'b) = cprod_defl\<cdot>REP('a)\<cdot>REP('b)"
huffman@33588
   835
apply (rule cast_eq_imp_eq, rule ext_cfun)
huffman@33784
   836
apply (simp add: cast_REP cast_cprod_defl)
huffman@33588
   837
apply (simp add: prj_cprod_def)
huffman@33588
   838
apply (simp add: emb_cprod_def)
huffman@33588
   839
apply (simp add: cprod_map_map cfcomp1)
huffman@33588
   840
done
huffman@33588
   841
huffman@33784
   842
lemma REP_up: "REP('a u) = u_defl\<cdot>REP('a)"
huffman@33588
   843
apply (rule cast_eq_imp_eq, rule ext_cfun)
huffman@33784
   844
apply (simp add: cast_REP cast_u_defl)
huffman@33588
   845
apply (simp add: prj_u_def)
huffman@33588
   846
apply (simp add: emb_u_def)
huffman@33588
   847
apply (simp add: u_map_map cfcomp1)
huffman@33588
   848
done
huffman@33588
   849
huffman@33784
   850
lemma REP_upper: "REP('a upper_pd) = upper_defl\<cdot>REP('a)"
huffman@33588
   851
apply (rule cast_eq_imp_eq, rule ext_cfun)
huffman@33784
   852
apply (simp add: cast_REP cast_upper_defl)
huffman@33588
   853
apply (simp add: prj_upper_pd_def)
huffman@33588
   854
apply (simp add: emb_upper_pd_def)
huffman@33588
   855
apply (simp add: upper_map_map cfcomp1)
huffman@33588
   856
done
huffman@33588
   857
huffman@33784
   858
lemma REP_lower: "REP('a lower_pd) = lower_defl\<cdot>REP('a)"
huffman@33588
   859
apply (rule cast_eq_imp_eq, rule ext_cfun)
huffman@33784
   860
apply (simp add: cast_REP cast_lower_defl)
huffman@33588
   861
apply (simp add: prj_lower_pd_def)
huffman@33588
   862
apply (simp add: emb_lower_pd_def)
huffman@33588
   863
apply (simp add: lower_map_map cfcomp1)
huffman@33588
   864
done
huffman@33588
   865
huffman@33784
   866
lemma REP_convex: "REP('a convex_pd) = convex_defl\<cdot>REP('a)"
huffman@33588
   867
apply (rule cast_eq_imp_eq, rule ext_cfun)
huffman@33784
   868
apply (simp add: cast_REP cast_convex_defl)
huffman@33588
   869
apply (simp add: prj_convex_pd_def)
huffman@33588
   870
apply (simp add: emb_convex_pd_def)
huffman@33588
   871
apply (simp add: convex_map_map cfcomp1)
huffman@33588
   872
done
huffman@33588
   873
huffman@33588
   874
lemmas REP_simps =
huffman@33588
   875
  REP_cfun
huffman@33588
   876
  REP_ssum
huffman@33588
   877
  REP_sprod
huffman@33588
   878
  REP_cprod
huffman@33588
   879
  REP_up
huffman@33588
   880
  REP_upper
huffman@33588
   881
  REP_lower
huffman@33588
   882
  REP_convex
huffman@33588
   883
huffman@33588
   884
subsection {* Isomorphic deflations *}
huffman@33588
   885
huffman@33588
   886
definition
huffman@33588
   887
  isodefl :: "('a::rep \<rightarrow> 'a) \<Rightarrow> udom alg_defl \<Rightarrow> bool"
huffman@33588
   888
where
huffman@33588
   889
  "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
huffman@33588
   890
huffman@33588
   891
lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
huffman@33588
   892
unfolding isodefl_def by (simp add: ext_cfun)
huffman@33588
   893
huffman@33588
   894
lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
huffman@33588
   895
unfolding isodefl_def by (simp add: ext_cfun)
huffman@33588
   896
huffman@33588
   897
lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
huffman@33588
   898
unfolding isodefl_def
huffman@33588
   899
by (drule cfun_fun_cong [where x="\<bottom>"], simp)
huffman@33588
   900
huffman@33588
   901
lemma isodefl_imp_deflation:
huffman@33588
   902
  fixes d :: "'a::rep \<rightarrow> 'a"
huffman@33588
   903
  assumes "isodefl d t" shows "deflation d"
huffman@33588
   904
proof
huffman@33588
   905
  note prems [unfolded isodefl_def, simp]
huffman@33588
   906
  fix x :: 'a
huffman@33588
   907
  show "d\<cdot>(d\<cdot>x) = d\<cdot>x"
huffman@33588
   908
    using cast.idem [of t "emb\<cdot>x"] by simp
huffman@33588
   909
  show "d\<cdot>x \<sqsubseteq> x"
huffman@33588
   910
    using cast.below [of t "emb\<cdot>x"] by simp
huffman@33588
   911
qed
huffman@33588
   912
huffman@33588
   913
lemma isodefl_ID_REP: "isodefl (ID :: 'a \<rightarrow> 'a) REP('a)"
huffman@33588
   914
unfolding isodefl_def by (simp add: cast_REP)
huffman@33588
   915
huffman@33588
   916
lemma isodefl_REP_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) REP('a) \<Longrightarrow> d = ID"
huffman@33588
   917
unfolding isodefl_def
huffman@33588
   918
apply (simp add: cast_REP)
huffman@33588
   919
apply (simp add: expand_cfun_eq)
huffman@33588
   920
apply (rule allI)
huffman@33588
   921
apply (drule_tac x="emb\<cdot>x" in spec)
huffman@33588
   922
apply simp
huffman@33588
   923
done
huffman@33588
   924
huffman@33588
   925
lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
huffman@33588
   926
unfolding isodefl_def by (simp add: expand_cfun_eq)
huffman@33588
   927
huffman@33588
   928
lemma adm_isodefl:
huffman@33588
   929
  "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
huffman@33588
   930
unfolding isodefl_def by simp
huffman@33588
   931
huffman@33588
   932
lemma isodefl_lub:
huffman@33588
   933
  assumes "chain d" and "chain t"
huffman@33588
   934
  assumes "\<And>i. isodefl (d i) (t i)"
huffman@33588
   935
  shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)"
huffman@33588
   936
using prems unfolding isodefl_def
huffman@33588
   937
by (simp add: contlub_cfun_arg contlub_cfun_fun)
huffman@33588
   938
huffman@33588
   939
lemma isodefl_fix:
huffman@33588
   940
  assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)"
huffman@33588
   941
  shows "isodefl (fix\<cdot>f) (fix\<cdot>g)"
huffman@33588
   942
unfolding fix_def2
huffman@33588
   943
apply (rule isodefl_lub, simp, simp)
huffman@33588
   944
apply (induct_tac i)
huffman@33588
   945
apply (simp add: isodefl_bottom)
huffman@33588
   946
apply (simp add: prems)
huffman@33588
   947
done
huffman@33588
   948
huffman@33588
   949
lemma isodefl_coerce:
huffman@33588
   950
  fixes d :: "'a \<rightarrow> 'a"
huffman@33588
   951
  assumes REP: "REP('b) = REP('a)"
huffman@33588
   952
  shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
huffman@33588
   953
unfolding isodefl_def
huffman@33588
   954
apply (simp add: expand_cfun_eq)
huffman@33588
   955
apply (simp add: emb_coerce coerce_prj REP)
huffman@33588
   956
done
huffman@33588
   957
huffman@33779
   958
lemma isodefl_abs_rep:
huffman@33779
   959
  fixes abs and rep and d
huffman@33779
   960
  assumes REP: "REP('b) = REP('a)"
huffman@33779
   961
  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
huffman@33779
   962
  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
huffman@33779
   963
  shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
huffman@33779
   964
unfolding abs_def rep_def using REP by (rule isodefl_coerce)
huffman@33779
   965
huffman@33588
   966
lemma isodefl_cfun:
huffman@33588
   967
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@33784
   968
    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
huffman@33588
   969
apply (rule isodeflI)
huffman@33784
   970
apply (simp add: cast_cfun_defl cast_isodefl)
huffman@33588
   971
apply (simp add: emb_cfun_def prj_cfun_def)
huffman@33588
   972
apply (simp add: cfun_map_map cfcomp1)
huffman@33588
   973
done
huffman@33588
   974
huffman@33588
   975
lemma isodefl_ssum:
huffman@33588
   976
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@33784
   977
    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
huffman@33588
   978
apply (rule isodeflI)
huffman@33784
   979
apply (simp add: cast_ssum_defl cast_isodefl)
huffman@33588
   980
apply (simp add: emb_ssum_def prj_ssum_def)
huffman@33588
   981
apply (simp add: ssum_map_map isodefl_strict)
huffman@33588
   982
done
huffman@33588
   983
huffman@33588
   984
lemma isodefl_sprod:
huffman@33588
   985
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@33784
   986
    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
huffman@33588
   987
apply (rule isodeflI)
huffman@33784
   988
apply (simp add: cast_sprod_defl cast_isodefl)
huffman@33588
   989
apply (simp add: emb_sprod_def prj_sprod_def)
huffman@33588
   990
apply (simp add: sprod_map_map isodefl_strict)
huffman@33588
   991
done
huffman@33588
   992
huffman@33786
   993
lemma isodefl_cprod:
huffman@33786
   994
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@33786
   995
    isodefl (cprod_map\<cdot>d1\<cdot>d2) (cprod_defl\<cdot>t1\<cdot>t2)"
huffman@33786
   996
apply (rule isodeflI)
huffman@33786
   997
apply (simp add: cast_cprod_defl cast_isodefl)
huffman@33786
   998
apply (simp add: emb_cprod_def prj_cprod_def)
huffman@33786
   999
apply (simp add: cprod_map_map cfcomp1)
huffman@33786
  1000
done
huffman@33786
  1001
huffman@33588
  1002
lemma isodefl_u:
huffman@33784
  1003
  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
huffman@33588
  1004
apply (rule isodeflI)
huffman@33784
  1005
apply (simp add: cast_u_defl cast_isodefl)
huffman@33588
  1006
apply (simp add: emb_u_def prj_u_def)
huffman@33588
  1007
apply (simp add: u_map_map)
huffman@33588
  1008
done
huffman@33588
  1009
huffman@33588
  1010
lemma isodefl_upper:
huffman@33784
  1011
  "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
huffman@33588
  1012
apply (rule isodeflI)
huffman@33784
  1013
apply (simp add: cast_upper_defl cast_isodefl)
huffman@33588
  1014
apply (simp add: emb_upper_pd_def prj_upper_pd_def)
huffman@33588
  1015
apply (simp add: upper_map_map)
huffman@33588
  1016
done
huffman@33588
  1017
huffman@33588
  1018
lemma isodefl_lower:
huffman@33784
  1019
  "isodefl d t \<Longrightarrow> isodefl (lower_map\<cdot>d) (lower_defl\<cdot>t)"
huffman@33588
  1020
apply (rule isodeflI)
huffman@33784
  1021
apply (simp add: cast_lower_defl cast_isodefl)
huffman@33588
  1022
apply (simp add: emb_lower_pd_def prj_lower_pd_def)
huffman@33588
  1023
apply (simp add: lower_map_map)
huffman@33588
  1024
done
huffman@33588
  1025
huffman@33588
  1026
lemma isodefl_convex:
huffman@33784
  1027
  "isodefl d t \<Longrightarrow> isodefl (convex_map\<cdot>d) (convex_defl\<cdot>t)"
huffman@33588
  1028
apply (rule isodeflI)
huffman@33784
  1029
apply (simp add: cast_convex_defl cast_isodefl)
huffman@33588
  1030
apply (simp add: emb_convex_pd_def prj_convex_pd_def)
huffman@33588
  1031
apply (simp add: convex_map_map)
huffman@33588
  1032
done
huffman@33588
  1033
huffman@33794
  1034
subsection {* Constructing Domain Isomorphisms *}
huffman@33794
  1035
huffman@33794
  1036
use "Tools/Domain/domain_isomorphism.ML"
huffman@33794
  1037
huffman@33794
  1038
setup {*
huffman@33794
  1039
  fold Domain_Isomorphism.add_type_constructor
huffman@33794
  1040
    [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map},
huffman@33809
  1041
        @{thm REP_cfun}, @{thm isodefl_cfun}, @{thm cfun_map_ID}),
huffman@33794
  1042
huffman@33794
  1043
     (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map},
huffman@33809
  1044
        @{thm REP_ssum}, @{thm isodefl_ssum}, @{thm ssum_map_ID}),
huffman@33794
  1045
huffman@33794
  1046
     (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map},
huffman@33809
  1047
        @{thm REP_sprod}, @{thm isodefl_sprod}, @{thm sprod_map_ID}),
huffman@33794
  1048
huffman@33794
  1049
     (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map},
huffman@33809
  1050
        @{thm REP_cprod}, @{thm isodefl_cprod}, @{thm cprod_map_ID}),
huffman@33794
  1051
huffman@33794
  1052
     (@{type_name "u"}, @{term u_defl}, @{const_name u_map},
huffman@33809
  1053
        @{thm REP_up}, @{thm isodefl_u}, @{thm u_map_ID}),
huffman@33794
  1054
huffman@33794
  1055
     (@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
huffman@33809
  1056
        @{thm REP_upper}, @{thm isodefl_upper}, @{thm upper_map_ID}),
huffman@33794
  1057
huffman@33794
  1058
     (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
huffman@33809
  1059
        @{thm REP_lower}, @{thm isodefl_lower}, @{thm lower_map_ID}),
huffman@33794
  1060
huffman@33794
  1061
     (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
huffman@33809
  1062
        @{thm REP_convex}, @{thm isodefl_convex}, @{thm convex_map_ID})]
huffman@33794
  1063
*}
huffman@33794
  1064
huffman@33588
  1065
end