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