src/HOLCF/Representable.thy
author huffman
Tue, 02 Mar 2010 17:21:10 -0800
changeset 35525 fa231b86cb1e
parent 35514 a2cfa413eaab
child 35527 f4282471461d
permissions -rw-r--r--
proper names for types cfun, sprod, ssum
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33589
e7ba88cdf3a2 add title/author block
huffman
parents: 33588
diff changeset
     1
(*  Title:      HOLCF/Representable.thy
e7ba88cdf3a2 add title/author block
huffman
parents: 33588
diff changeset
     2
    Author:     Brian Huffman
e7ba88cdf3a2 add title/author block
huffman
parents: 33588
diff changeset
     3
*)
e7ba88cdf3a2 add title/author block
huffman
parents: 33588
diff changeset
     4
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
     5
header {* Representable Types *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
     6
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
     7
theory Representable
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents: 33809
diff changeset
     8
imports Algebraic Universal Ssum Sprod One Fixrec
33794
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
     9
uses
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
    10
  ("Tools/repdef.ML")
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents: 35473
diff changeset
    11
  ("Tools/holcf_library.ML")
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents: 35490
diff changeset
    12
  ("Tools/Domain/domain_take_proofs.ML")
33794
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
    13
  ("Tools/Domain/domain_isomorphism.ML")
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    14
begin
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    15
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    16
subsection {* Class of representable types *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    17
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    18
text "Overloaded embedding and projection functions between
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    19
      a representable type and the universal domain."
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    20
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    21
class rep = bifinite +
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    22
  fixes emb :: "'a::pcpo \<rightarrow> udom"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    23
  fixes prj :: "udom \<rightarrow> 'a::pcpo"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    24
  assumes ep_pair_emb_prj: "ep_pair emb prj"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    25
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    26
interpretation rep!:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    27
  pcpo_ep_pair
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    28
    "emb :: 'a::rep \<rightarrow> udom"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    29
    "prj :: udom \<rightarrow> 'a::rep"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    30
  unfolding pcpo_ep_pair_def
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    31
  by (rule ep_pair_emb_prj)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    32
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    33
lemmas emb_inverse = rep.e_inverse
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    34
lemmas emb_prj_below = rep.e_p_below
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    35
lemmas emb_eq_iff = rep.e_eq_iff
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    36
lemmas emb_strict = rep.e_strict
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    37
lemmas prj_strict = rep.p_strict
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    38
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    39
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    40
subsection {* Making @{term rep} the default class *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    41
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    42
text {*
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    43
  From now on, free type variables are assumed to be in class
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    44
  @{term rep}, unless specified otherwise.
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    45
*}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    46
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    47
defaultsort rep
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    48
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    49
subsection {* Representations of types *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    50
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    51
text "A TypeRep is an algebraic deflation over the universe of values."
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    52
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    53
types TypeRep = "udom alg_defl"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    54
translations "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    55
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    56
definition
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    57
  Rep_of :: "'a::rep itself \<Rightarrow> TypeRep"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    58
where
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    59
  "Rep_of TYPE('a::rep) =
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    60
    (\<Squnion>i. alg_defl_principal (Abs_fin_defl
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    61
      (emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    62
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    63
syntax "_REP" :: "type \<Rightarrow> TypeRep"  ("(1REP/(1'(_')))")
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    64
translations "REP(t)" \<rightleftharpoons> "CONST Rep_of TYPE(t)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    65
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    66
lemma cast_REP:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    67
  "cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    68
proof -
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    69
  let ?a = "\<lambda>i. emb oo approx i oo (prj::udom \<rightarrow> 'a)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    70
  have a: "\<And>i. finite_deflation (?a i)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    71
    apply (rule rep.finite_deflation_e_d_p)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    72
    apply (rule finite_deflation_approx)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    73
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    74
  show ?thesis
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    75
    unfolding Rep_of_def
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    76
    apply (subst contlub_cfun_arg)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    77
    apply (rule chainI)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    78
    apply (rule alg_defl.principal_mono)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    79
    apply (rule Abs_fin_defl_mono [OF a a])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    80
    apply (rule chainE, simp)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    81
    apply (subst cast_alg_defl_principal)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    82
    apply (simp add: Abs_fin_defl_inverse a)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    83
    apply (simp add: expand_cfun_eq lub_distribs)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    84
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    85
qed
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    86
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    87
lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a::rep) = cast\<cdot>REP('a)\<cdot>x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    88
by (simp add: cast_REP)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    89
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    90
lemma in_REP_iff:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    91
  "x ::: REP('a::rep) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    92
by (simp add: in_deflation_def cast_REP)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    93
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    94
lemma prj_inverse:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    95
  "x ::: REP('a::rep) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    96
by (simp only: in_REP_iff)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    97
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    98
lemma emb_in_REP [simp]:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
    99
  "emb\<cdot>(x::'a::rep) ::: REP('a)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   100
by (simp add: in_REP_iff)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   101
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   102
subsection {* Coerce operator *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   103
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   104
definition coerce :: "'a \<rightarrow> 'b"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   105
where "coerce = prj oo emb"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   106
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   107
lemma beta_coerce: "coerce\<cdot>x = prj\<cdot>(emb\<cdot>x)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   108
by (simp add: coerce_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   109
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   110
lemma prj_emb: "prj\<cdot>(emb\<cdot>x) = coerce\<cdot>x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   111
by (simp add: coerce_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   112
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   113
lemma coerce_strict [simp]: "coerce\<cdot>\<bottom> = \<bottom>"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   114
by (simp add: coerce_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   115
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   116
lemma coerce_eq_ID [simp]: "(coerce :: 'a \<rightarrow> 'a) = ID"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   117
by (rule ext_cfun, simp add: beta_coerce)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   118
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   119
lemma emb_coerce:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   120
  "REP('a) \<sqsubseteq> REP('b)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   121
   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = emb\<cdot>x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   122
 apply (simp add: beta_coerce)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   123
 apply (rule prj_inverse)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   124
 apply (erule subdeflationD)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   125
 apply (rule emb_in_REP)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   126
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   127
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   128
lemma coerce_prj:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   129
  "REP('a) \<sqsubseteq> REP('b)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   130
   \<Longrightarrow> (coerce::'b \<rightarrow> 'a)\<cdot>(prj\<cdot>x) = prj\<cdot>x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   131
 apply (simp add: coerce_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   132
 apply (rule emb_eq_iff [THEN iffD1])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   133
 apply (simp only: emb_prj)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   134
 apply (rule deflation_below_comp1)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   135
   apply (rule deflation_cast)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   136
  apply (rule deflation_cast)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   137
 apply (erule monofun_cfun_arg)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   138
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   139
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   140
lemma coerce_coerce [simp]:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   141
  "REP('a) \<sqsubseteq> REP('b)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   142
   \<Longrightarrow> coerce\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) = coerce\<cdot>x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   143
by (simp add: beta_coerce prj_inverse subdeflationD)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   144
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   145
lemma coerce_inverse:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   146
  "emb\<cdot>(x::'a) ::: REP('b) \<Longrightarrow> coerce\<cdot>(coerce\<cdot>x :: 'b) = x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   147
by (simp only: beta_coerce prj_inverse emb_inverse)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   148
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   149
lemma coerce_type:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   150
  "REP('a) \<sqsubseteq> REP('b)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   151
   \<Longrightarrow> emb\<cdot>((coerce::'a \<rightarrow> 'b)\<cdot>x) ::: REP('a)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   152
by (simp add: beta_coerce prj_inverse subdeflationD)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   153
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   154
lemma ep_pair_coerce:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   155
  "REP('a) \<sqsubseteq> REP('b)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   156
   \<Longrightarrow> ep_pair (coerce::'a \<rightarrow> 'b) (coerce::'b \<rightarrow> 'a)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   157
 apply (rule ep_pair.intro)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   158
  apply simp
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   159
 apply (simp only: beta_coerce)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   160
 apply (rule below_trans)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   161
  apply (rule monofun_cfun_arg)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   162
  apply (rule emb_prj_below)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   163
 apply simp
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   164
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   165
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   166
text {* Isomorphism lemmas used internally by the domain package: *}
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   167
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   168
lemma domain_abs_iso:
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   169
  fixes abs and rep
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   170
  assumes REP: "REP('b) = REP('a)"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   171
  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   172
  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   173
  shows "rep\<cdot>(abs\<cdot>x) = x"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   174
unfolding abs_def rep_def by (simp add: REP)
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   175
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   176
lemma domain_rep_iso:
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   177
  fixes abs and rep
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   178
  assumes REP: "REP('b) = REP('a)"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   179
  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   180
  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   181
  shows "abs\<cdot>(rep\<cdot>x) = x"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   182
unfolding abs_def rep_def by (simp add: REP [symmetric])
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   183
35480
7a1f285cad25 domain_isomorphism package proves deflation rules for map functions
huffman
parents: 35479
diff changeset
   184
lemma deflation_abs_rep:
7a1f285cad25 domain_isomorphism package proves deflation rules for map functions
huffman
parents: 35479
diff changeset
   185
  fixes abs and rep and d
35489
dd02201d95b6 add function define_take_functions
huffman
parents: 35480
diff changeset
   186
  assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
dd02201d95b6 add function define_take_functions
huffman
parents: 35480
diff changeset
   187
  assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
35480
7a1f285cad25 domain_isomorphism package proves deflation rules for map functions
huffman
parents: 35479
diff changeset
   188
  shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
35489
dd02201d95b6 add function define_take_functions
huffman
parents: 35480
diff changeset
   189
by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
35480
7a1f285cad25 domain_isomorphism package proves deflation rules for map functions
huffman
parents: 35479
diff changeset
   190
35490
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   191
lemma deflation_chain_min:
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   192
  assumes chain: "chain d"
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   193
  assumes defl: "\<And>i. deflation (d i)"
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   194
  shows "d i\<cdot>(d j\<cdot>x) = d (min i j)\<cdot>x"
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   195
proof (rule linorder_le_cases)
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   196
  assume "i \<le> j"
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   197
  with chain have "d i \<sqsubseteq> d j" by (rule chain_mono)
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   198
  then have "d i\<cdot>(d j\<cdot>x) = d i\<cdot>x"
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   199
    by (rule deflation_below_comp1 [OF defl defl])
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   200
  moreover from `i \<le> j` have "min i j = i" by simp
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   201
  ultimately show ?thesis by simp
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   202
next
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   203
  assume "j \<le> i"
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   204
  with chain have "d j \<sqsubseteq> d i" by (rule chain_mono)
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   205
  then have "d i\<cdot>(d j\<cdot>x) = d j\<cdot>x"
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   206
    by (rule deflation_below_comp2 [OF defl defl])
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   207
  moreover from `j \<le> i` have "min i j = j" by simp
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   208
  ultimately show ?thesis by simp
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   209
qed
63f8121c6585 generate take_take rules
huffman
parents: 35489
diff changeset
   210
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   211
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   212
subsection {* Proving a subtype is representable *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   213
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   214
text {*
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   215
  Temporarily relax type constraints for @{term "approx"},
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   216
  @{term emb}, and @{term prj}.
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   217
*}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   218
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   219
setup {* Sign.add_const_constraint
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   220
  (@{const_name "approx"}, SOME @{typ "nat \<Rightarrow> 'a::cpo \<rightarrow> 'a"}) *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   221
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   222
setup {* Sign.add_const_constraint
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   223
  (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"}) *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   224
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   225
setup {* Sign.add_const_constraint
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   226
  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"}) *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   227
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   228
definition
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   229
  repdef_approx ::
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   230
    "('a::pcpo \<Rightarrow> udom) \<Rightarrow> (udom \<Rightarrow> 'a) \<Rightarrow> udom alg_defl \<Rightarrow> nat \<Rightarrow> 'a \<rightarrow> 'a"
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   231
where
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   232
  "repdef_approx Rep Abs t = (\<lambda>i. \<Lambda> x. Abs (cast\<cdot>(approx i\<cdot>t)\<cdot>(Rep x)))"
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   233
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   234
lemma typedef_rep_class:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   235
  fixes Rep :: "'a::pcpo \<Rightarrow> udom"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   236
  fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   237
  fixes t :: TypeRep
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   238
  assumes type: "type_definition Rep Abs {x. x ::: t}"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   239
  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   240
  assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   241
  assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   242
  assumes approx: "(approx :: nat \<Rightarrow> 'a \<rightarrow> 'a) \<equiv> repdef_approx Rep Abs t"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   243
  shows "OFCLASS('a, rep_class)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   244
proof
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   245
  have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   246
    by (simp add: adm_in_deflation)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   247
  have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   248
    unfolding emb
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   249
    apply (rule beta_cfun)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   250
    apply (rule typedef_cont_Rep [OF type below adm])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   251
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   252
  have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   253
    unfolding prj
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   254
    apply (rule beta_cfun)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   255
    apply (rule typedef_cont_Abs [OF type below adm])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   256
    apply simp_all
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   257
    done
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   258
  have cast_cast_approx:
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   259
    "\<And>i x. cast\<cdot>t\<cdot>(cast\<cdot>(approx i\<cdot>t)\<cdot>x) = cast\<cdot>(approx i\<cdot>t)\<cdot>x"
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   260
    apply (rule cast_fixed)
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   261
    apply (rule subdeflationD)
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   262
    apply (rule approx.below)
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   263
    apply (rule cast_in_deflation)
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   264
    done
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   265
  have approx':
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   266
    "approx = (\<lambda>i. \<Lambda>(x::'a). prj\<cdot>(cast\<cdot>(approx i\<cdot>t)\<cdot>(emb\<cdot>x)))"
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   267
    unfolding approx repdef_approx_def
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   268
    apply (subst cast_cast_approx [symmetric])
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   269
    apply (simp add: prj_beta [symmetric] emb_beta [symmetric])
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   270
    done
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   271
  have emb_in_deflation: "\<And>x::'a. emb\<cdot>x ::: t"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   272
    using type_definition.Rep [OF type]
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   273
    by (simp add: emb_beta)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   274
  have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   275
    unfolding prj_beta
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   276
    apply (simp add: cast_fixed [OF emb_in_deflation])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   277
    apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   278
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   279
  have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   280
    unfolding prj_beta emb_beta
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   281
    by (simp add: type_definition.Abs_inverse [OF type])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   282
  show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   283
    apply default
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   284
    apply (simp add: prj_emb)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   285
    apply (simp add: emb_prj cast.below)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   286
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   287
  show "chain (approx :: nat \<Rightarrow> 'a \<rightarrow> 'a)"
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   288
    unfolding approx' by simp
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   289
  show "\<And>x::'a. (\<Squnion>i. approx i\<cdot>x) = x"
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   290
    unfolding approx'
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   291
    apply (simp add: lub_distribs)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   292
    apply (subst cast_fixed [OF emb_in_deflation])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   293
    apply (rule prj_emb)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   294
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   295
  show "\<And>(i::nat) (x::'a). approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   296
    unfolding approx'
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   297
    apply simp
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   298
    apply (simp add: emb_prj)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   299
    apply (simp add: cast_cast_approx)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   300
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   301
  show "\<And>i::nat. finite {x::'a. approx i\<cdot>x = x}"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   302
    apply (rule_tac B="(\<lambda>x. prj\<cdot>x) ` {x. cast\<cdot>(approx i\<cdot>t)\<cdot>x = x}"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   303
           in finite_subset)
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   304
    apply (clarsimp simp add: approx')
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   305
    apply (drule_tac f="\<lambda>x. emb\<cdot>x" in arg_cong)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   306
    apply (rule image_eqI)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   307
    apply (rule prj_emb [symmetric])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   308
    apply (simp add: emb_prj)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   309
    apply (simp add: cast_cast_approx)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   310
    apply (rule finite_imageI)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   311
    apply (simp add: cast_approx_fixed_iff)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   312
    apply (simp add: Collect_conj_eq)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   313
    apply (simp add: finite_fixes_approx)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   314
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   315
qed
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   316
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   317
text {* Restore original typing constraints *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   318
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   319
setup {* Sign.add_const_constraint
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   320
  (@{const_name "approx"}, SOME @{typ "nat \<Rightarrow> 'a::profinite \<rightarrow> 'a"}) *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   321
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   322
setup {* Sign.add_const_constraint
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   323
  (@{const_name emb}, SOME @{typ "'a::rep \<rightarrow> udom"}) *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   324
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   325
setup {* Sign.add_const_constraint
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   326
  (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::rep"}) *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   327
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   328
lemma typedef_REP:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   329
  fixes Rep :: "'a::rep \<Rightarrow> udom"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   330
  fixes Abs :: "udom \<Rightarrow> 'a::rep"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   331
  fixes t :: TypeRep
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   332
  assumes type: "type_definition Rep Abs {x. x ::: t}"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   333
  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   334
  assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   335
  assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   336
  shows "REP('a) = t"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   337
proof -
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   338
  have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   339
    by (simp add: adm_in_deflation)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   340
  have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   341
    unfolding emb
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   342
    apply (rule beta_cfun)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   343
    apply (rule typedef_cont_Rep [OF type below adm])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   344
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   345
  have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   346
    unfolding prj
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   347
    apply (rule beta_cfun)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   348
    apply (rule typedef_cont_Abs [OF type below adm])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   349
    apply simp_all
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   350
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   351
  have emb_in_deflation: "\<And>x::'a. emb\<cdot>x ::: t"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   352
    using type_definition.Rep [OF type]
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   353
    by (simp add: emb_beta)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   354
  have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   355
    unfolding prj_beta
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   356
    apply (simp add: cast_fixed [OF emb_in_deflation])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   357
    apply (simp add: emb_beta type_definition.Rep_inverse [OF type])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   358
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   359
  have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   360
    unfolding prj_beta emb_beta
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   361
    by (simp add: type_definition.Abs_inverse [OF type])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   362
  show "REP('a) = t"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   363
    apply (rule cast_eq_imp_eq, rule ext_cfun)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   364
    apply (simp add: cast_REP emb_prj)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   365
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   366
qed
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   367
33679
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   368
lemma adm_mem_Collect_in_deflation: "adm (\<lambda>x. x \<in> {x. x ::: A})"
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   369
unfolding mem_Collect_eq by (rule adm_in_deflation)
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   370
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   371
use "Tools/repdef.ML"
331712879666 automate definition of representable domains from algebraic deflations
huffman
parents: 33589
diff changeset
   372
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   373
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   374
subsection {* Instances of class @{text rep} *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   375
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   376
subsubsection {* Universal Domain *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   377
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   378
text "The Universal Domain itself is trivially representable."
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   379
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   380
instantiation udom :: rep
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   381
begin
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   382
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   383
definition emb_udom_def [simp]: "emb = (ID :: udom \<rightarrow> udom)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   384
definition prj_udom_def [simp]: "prj = (ID :: udom \<rightarrow> udom)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   385
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   386
instance
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   387
 apply (intro_classes)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   388
 apply (simp_all add: ep_pair.intro)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   389
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   390
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   391
end
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   392
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   393
subsubsection {* Lifted types *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   394
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   395
instantiation lift :: (countable) rep
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   396
begin
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   397
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   398
definition emb_lift_def:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   399
  "emb = udom_emb oo (FLIFT x. Def (to_nat x))"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   400
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   401
definition prj_lift_def:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   402
  "prj = (FLIFT n. if (\<exists>x::'a::countable. n = to_nat x)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   403
                    then Def (THE x::'a. n = to_nat x) else \<bottom>) oo udom_prj"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   404
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   405
instance
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   406
 apply (intro_classes, unfold emb_lift_def prj_lift_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   407
 apply (rule ep_pair_comp [OF _ ep_pair_udom])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   408
 apply (rule ep_pair.intro)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   409
  apply (case_tac x, simp, simp)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   410
 apply (case_tac y, simp, clarsimp)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   411
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   412
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   413
end
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   414
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   415
subsubsection {* Representable type constructors *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   416
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   417
text "Functions between representable types are representable."
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   418
35525
fa231b86cb1e proper names for types cfun, sprod, ssum
huffman
parents: 35514
diff changeset
   419
instantiation cfun :: (rep, rep) rep
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   420
begin
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   421
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   422
definition emb_cfun_def: "emb = udom_emb oo cfun_map\<cdot>prj\<cdot>emb"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   423
definition prj_cfun_def: "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   424
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   425
instance
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   426
 apply (intro_classes, unfold emb_cfun_def prj_cfun_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   427
 apply (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj ep_pair_udom)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   428
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   429
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   430
end
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   431
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   432
text "Strict products of representable types are representable."
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   433
35525
fa231b86cb1e proper names for types cfun, sprod, ssum
huffman
parents: 35514
diff changeset
   434
instantiation sprod :: (rep, rep) rep
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   435
begin
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   436
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   437
definition emb_sprod_def: "emb = udom_emb oo sprod_map\<cdot>emb\<cdot>emb"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   438
definition prj_sprod_def: "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   439
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   440
instance
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   441
 apply (intro_classes, unfold emb_sprod_def prj_sprod_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   442
 apply (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj ep_pair_udom)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   443
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   444
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   445
end
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   446
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   447
text "Strict sums of representable types are representable."
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   448
35525
fa231b86cb1e proper names for types cfun, sprod, ssum
huffman
parents: 35514
diff changeset
   449
instantiation ssum :: (rep, rep) rep
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   450
begin
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   451
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   452
definition emb_ssum_def: "emb = udom_emb oo ssum_map\<cdot>emb\<cdot>emb"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   453
definition prj_ssum_def: "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   454
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   455
instance
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   456
 apply (intro_classes, unfold emb_ssum_def prj_ssum_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   457
 apply (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj ep_pair_udom)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   458
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   459
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   460
end
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   461
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   462
text "Up of a representable type is representable."
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   463
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   464
instantiation "u" :: (rep) rep
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   465
begin
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   466
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   467
definition emb_u_def: "emb = udom_emb oo u_map\<cdot>emb"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   468
definition prj_u_def: "prj = u_map\<cdot>prj oo udom_prj"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   469
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   470
instance
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   471
 apply (intro_classes, unfold emb_u_def prj_u_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   472
 apply (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj ep_pair_udom)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   473
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   474
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   475
end
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   476
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   477
text "Cartesian products of representable types are representable."
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   478
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   479
instantiation "*" :: (rep, rep) rep
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   480
begin
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   481
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   482
definition emb_cprod_def: "emb = udom_emb oo cprod_map\<cdot>emb\<cdot>emb"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   483
definition prj_cprod_def: "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   484
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   485
instance
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   486
 apply (intro_classes, unfold emb_cprod_def prj_cprod_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   487
 apply (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj ep_pair_udom)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   488
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   489
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   490
end
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   491
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   492
subsection {* Type combinators *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   493
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   494
definition
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   495
  TypeRep_fun1 ::
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   496
    "((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   497
      \<Rightarrow> (TypeRep \<rightarrow> TypeRep)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   498
where
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   499
  "TypeRep_fun1 f =
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   500
    alg_defl.basis_fun (\<lambda>a.
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   501
      alg_defl_principal (
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   502
        Abs_fin_defl (udom_emb oo f\<cdot>(Rep_fin_defl a) oo udom_prj)))"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   503
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   504
definition
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   505
  TypeRep_fun2 ::
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   506
    "((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a))
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   507
      \<Rightarrow> (TypeRep \<rightarrow> TypeRep \<rightarrow> TypeRep)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   508
where
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   509
  "TypeRep_fun2 f =
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   510
    alg_defl.basis_fun (\<lambda>a.
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   511
      alg_defl.basis_fun (\<lambda>b.
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   512
        alg_defl_principal (
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   513
          Abs_fin_defl (udom_emb oo
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   514
            f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj))))"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   515
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   516
definition "cfun_defl = TypeRep_fun2 cfun_map"
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   517
definition "ssum_defl = TypeRep_fun2 ssum_map"
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   518
definition "sprod_defl = TypeRep_fun2 sprod_map"
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   519
definition "cprod_defl = TypeRep_fun2 cprod_map"
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   520
definition "u_defl = TypeRep_fun1 u_map"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   521
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   522
lemma Rep_fin_defl_mono: "a \<sqsubseteq> b \<Longrightarrow> Rep_fin_defl a \<sqsubseteq> Rep_fin_defl b"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   523
unfolding below_fin_defl_def .
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   524
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   525
lemma cast_TypeRep_fun1:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   526
  assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   527
  shows "cast\<cdot>(TypeRep_fun1 f\<cdot>A) = udom_emb oo f\<cdot>(cast\<cdot>A) oo udom_prj"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   528
proof -
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   529
  have 1: "\<And>a. finite_deflation (udom_emb oo f\<cdot>(Rep_fin_defl a) oo udom_prj)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   530
    apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   531
    apply (rule f, rule finite_deflation_Rep_fin_defl)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   532
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   533
  show ?thesis
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   534
    by (induct A rule: alg_defl.principal_induct, simp)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   535
       (simp only: TypeRep_fun1_def
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   536
                   alg_defl.basis_fun_principal
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   537
                   alg_defl.basis_fun_mono
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   538
                   alg_defl.principal_mono
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   539
                   Abs_fin_defl_mono [OF 1 1]
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   540
                   monofun_cfun below_refl
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   541
                   Rep_fin_defl_mono
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   542
                   cast_alg_defl_principal
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   543
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   544
qed
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   545
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   546
lemma cast_TypeRep_fun2:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   547
  assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   548
                finite_deflation (f\<cdot>a\<cdot>b)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   549
  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"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   550
proof -
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   551
  have 1: "\<And>a b. finite_deflation
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   552
           (udom_emb oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   553
    apply (rule ep_pair.finite_deflation_e_d_p [OF ep_pair_udom])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   554
    apply (rule f, (rule finite_deflation_Rep_fin_defl)+)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   555
    done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   556
  show ?thesis
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   557
    by (induct A B rule: alg_defl.principal_induct2, simp, simp)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   558
       (simp only: TypeRep_fun2_def
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   559
                   alg_defl.basis_fun_principal
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   560
                   alg_defl.basis_fun_mono
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   561
                   alg_defl.principal_mono
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   562
                   Abs_fin_defl_mono [OF 1 1]
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   563
                   monofun_cfun below_refl
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   564
                   Rep_fin_defl_mono
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   565
                   cast_alg_defl_principal
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   566
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   567
qed
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   568
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   569
lemma cast_cfun_defl:
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   570
  "cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) = udom_emb oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   571
unfolding cfun_defl_def
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   572
apply (rule cast_TypeRep_fun2)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   573
apply (erule (1) finite_deflation_cfun_map)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   574
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   575
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   576
lemma cast_ssum_defl:
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   577
  "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = udom_emb oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   578
unfolding ssum_defl_def
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   579
apply (rule cast_TypeRep_fun2)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   580
apply (erule (1) finite_deflation_ssum_map)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   581
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   582
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   583
lemma cast_sprod_defl:
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   584
  "cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = udom_emb oo sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   585
unfolding sprod_defl_def
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   586
apply (rule cast_TypeRep_fun2)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   587
apply (erule (1) finite_deflation_sprod_map)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   588
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   589
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   590
lemma cast_cprod_defl:
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   591
  "cast\<cdot>(cprod_defl\<cdot>A\<cdot>B) = udom_emb oo cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   592
unfolding cprod_defl_def
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   593
apply (rule cast_TypeRep_fun2)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   594
apply (erule (1) finite_deflation_cprod_map)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   595
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   596
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   597
lemma cast_u_defl:
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   598
  "cast\<cdot>(u_defl\<cdot>A) = udom_emb oo u_map\<cdot>(cast\<cdot>A) oo udom_prj"
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   599
unfolding u_defl_def
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   600
apply (rule cast_TypeRep_fun1)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   601
apply (erule finite_deflation_u_map)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   602
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   603
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   604
text {* REP of type constructor = type combinator *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   605
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   606
lemma REP_cfun: "REP('a \<rightarrow> 'b) = cfun_defl\<cdot>REP('a)\<cdot>REP('b)"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   607
apply (rule cast_eq_imp_eq, rule ext_cfun)
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   608
apply (simp add: cast_REP cast_cfun_defl)
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   609
apply (simp add: cfun_map_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   610
apply (simp only: prj_cfun_def emb_cfun_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   611
apply (simp add: expand_cfun_eq ep_pair.e_eq_iff [OF ep_pair_udom])
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   612
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   613
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   614
lemma REP_ssum: "REP('a \<oplus> 'b) = ssum_defl\<cdot>REP('a)\<cdot>REP('b)"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   615
apply (rule cast_eq_imp_eq, rule ext_cfun)
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   616
apply (simp add: cast_REP cast_ssum_defl)
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   617
apply (simp add: prj_ssum_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   618
apply (simp add: emb_ssum_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   619
apply (simp add: ssum_map_map cfcomp1)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   620
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   621
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   622
lemma REP_sprod: "REP('a \<otimes> 'b) = sprod_defl\<cdot>REP('a)\<cdot>REP('b)"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   623
apply (rule cast_eq_imp_eq, rule ext_cfun)
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   624
apply (simp add: cast_REP cast_sprod_defl)
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   625
apply (simp add: prj_sprod_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   626
apply (simp add: emb_sprod_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   627
apply (simp add: sprod_map_map cfcomp1)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   628
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   629
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   630
lemma REP_cprod: "REP('a \<times> 'b) = cprod_defl\<cdot>REP('a)\<cdot>REP('b)"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   631
apply (rule cast_eq_imp_eq, rule ext_cfun)
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   632
apply (simp add: cast_REP cast_cprod_defl)
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   633
apply (simp add: prj_cprod_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   634
apply (simp add: emb_cprod_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   635
apply (simp add: cprod_map_map cfcomp1)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   636
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   637
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   638
lemma REP_up: "REP('a u) = u_defl\<cdot>REP('a)"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   639
apply (rule cast_eq_imp_eq, rule ext_cfun)
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   640
apply (simp add: cast_REP cast_u_defl)
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   641
apply (simp add: prj_u_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   642
apply (simp add: emb_u_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   643
apply (simp add: u_map_map cfcomp1)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   644
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   645
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   646
lemmas REP_simps =
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   647
  REP_cfun
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   648
  REP_ssum
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   649
  REP_sprod
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   650
  REP_cprod
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   651
  REP_up
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   652
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   653
subsection {* Isomorphic deflations *}
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   654
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   655
definition
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   656
  isodefl :: "('a::rep \<rightarrow> 'a) \<Rightarrow> udom alg_defl \<Rightarrow> bool"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   657
where
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   658
  "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   659
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   660
lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   661
unfolding isodefl_def by (simp add: ext_cfun)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   662
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   663
lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   664
unfolding isodefl_def by (simp add: ext_cfun)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   665
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   666
lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   667
unfolding isodefl_def
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   668
by (drule cfun_fun_cong [where x="\<bottom>"], simp)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   669
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   670
lemma isodefl_imp_deflation:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   671
  fixes d :: "'a::rep \<rightarrow> 'a"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   672
  assumes "isodefl d t" shows "deflation d"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   673
proof
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   674
  note prems [unfolded isodefl_def, simp]
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   675
  fix x :: 'a
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   676
  show "d\<cdot>(d\<cdot>x) = d\<cdot>x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   677
    using cast.idem [of t "emb\<cdot>x"] by simp
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   678
  show "d\<cdot>x \<sqsubseteq> x"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   679
    using cast.below [of t "emb\<cdot>x"] by simp
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   680
qed
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   681
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   682
lemma isodefl_ID_REP: "isodefl (ID :: 'a \<rightarrow> 'a) REP('a)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   683
unfolding isodefl_def by (simp add: cast_REP)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   684
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   685
lemma isodefl_REP_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) REP('a) \<Longrightarrow> d = ID"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   686
unfolding isodefl_def
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   687
apply (simp add: cast_REP)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   688
apply (simp add: expand_cfun_eq)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   689
apply (rule allI)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   690
apply (drule_tac x="emb\<cdot>x" in spec)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   691
apply simp
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   692
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   693
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   694
lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   695
unfolding isodefl_def by (simp add: expand_cfun_eq)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   696
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   697
lemma adm_isodefl:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   698
  "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   699
unfolding isodefl_def by simp
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   700
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   701
lemma isodefl_lub:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   702
  assumes "chain d" and "chain t"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   703
  assumes "\<And>i. isodefl (d i) (t i)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   704
  shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   705
using prems unfolding isodefl_def
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   706
by (simp add: contlub_cfun_arg contlub_cfun_fun)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   707
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   708
lemma isodefl_fix:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   709
  assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   710
  shows "isodefl (fix\<cdot>f) (fix\<cdot>g)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   711
unfolding fix_def2
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   712
apply (rule isodefl_lub, simp, simp)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   713
apply (induct_tac i)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   714
apply (simp add: isodefl_bottom)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   715
apply (simp add: prems)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   716
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   717
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   718
lemma isodefl_coerce:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   719
  fixes d :: "'a \<rightarrow> 'a"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   720
  assumes REP: "REP('b) = REP('a)"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   721
  shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   722
unfolding isodefl_def
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   723
apply (simp add: expand_cfun_eq)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   724
apply (simp add: emb_coerce coerce_prj REP)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   725
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   726
33779
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   727
lemma isodefl_abs_rep:
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   728
  fixes abs and rep and d
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   729
  assumes REP: "REP('b) = REP('a)"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   730
  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   731
  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   732
  shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   733
unfolding abs_def rep_def using REP by (rule isodefl_coerce)
b8efeea2cebd remove one_typ and tr_typ; add abs/rep lemmas
huffman
parents: 33679
diff changeset
   734
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   735
lemma isodefl_cfun:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   736
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   737
    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   738
apply (rule isodeflI)
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   739
apply (simp add: cast_cfun_defl cast_isodefl)
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   740
apply (simp add: emb_cfun_def prj_cfun_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   741
apply (simp add: cfun_map_map cfcomp1)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   742
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   743
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   744
lemma isodefl_ssum:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   745
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   746
    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   747
apply (rule isodeflI)
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   748
apply (simp add: cast_ssum_defl cast_isodefl)
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   749
apply (simp add: emb_ssum_def prj_ssum_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   750
apply (simp add: ssum_map_map isodefl_strict)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   751
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   752
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   753
lemma isodefl_sprod:
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   754
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   755
    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   756
apply (rule isodeflI)
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   757
apply (simp add: cast_sprod_defl cast_isodefl)
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   758
apply (simp add: emb_sprod_def prj_sprod_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   759
apply (simp add: sprod_map_map isodefl_strict)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   760
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   761
33786
d280c5ebd7d7 add lemma isodefl_cprod
huffman
parents: 33784
diff changeset
   762
lemma isodefl_cprod:
d280c5ebd7d7 add lemma isodefl_cprod
huffman
parents: 33784
diff changeset
   763
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
d280c5ebd7d7 add lemma isodefl_cprod
huffman
parents: 33784
diff changeset
   764
    isodefl (cprod_map\<cdot>d1\<cdot>d2) (cprod_defl\<cdot>t1\<cdot>t2)"
d280c5ebd7d7 add lemma isodefl_cprod
huffman
parents: 33784
diff changeset
   765
apply (rule isodeflI)
d280c5ebd7d7 add lemma isodefl_cprod
huffman
parents: 33784
diff changeset
   766
apply (simp add: cast_cprod_defl cast_isodefl)
d280c5ebd7d7 add lemma isodefl_cprod
huffman
parents: 33784
diff changeset
   767
apply (simp add: emb_cprod_def prj_cprod_def)
d280c5ebd7d7 add lemma isodefl_cprod
huffman
parents: 33784
diff changeset
   768
apply (simp add: cprod_map_map cfcomp1)
d280c5ebd7d7 add lemma isodefl_cprod
huffman
parents: 33784
diff changeset
   769
done
d280c5ebd7d7 add lemma isodefl_cprod
huffman
parents: 33784
diff changeset
   770
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   771
lemma isodefl_u:
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   772
  "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   773
apply (rule isodeflI)
33784
7e434813752f change naming convention for deflation combinators
huffman
parents: 33779
diff changeset
   774
apply (simp add: cast_u_defl cast_isodefl)
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   775
apply (simp add: emb_u_def prj_u_def)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   776
apply (simp add: u_map_map)
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   777
done
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   778
33794
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   779
subsection {* Constructing Domain Isomorphisms *}
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   780
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents: 35473
diff changeset
   781
use "Tools/holcf_library.ML"
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents: 35490
diff changeset
   782
use "Tools/Domain/domain_take_proofs.ML"
33794
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   783
use "Tools/Domain/domain_isomorphism.ML"
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   784
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   785
setup {*
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   786
  fold Domain_Isomorphism.add_type_constructor
35525
fa231b86cb1e proper names for types cfun, sprod, ssum
huffman
parents: 35514
diff changeset
   787
    [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
35479
dffffe36344a store deflation thms for map functions in theory data
huffman
parents: 35475
diff changeset
   788
        @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
33794
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   789
35525
fa231b86cb1e proper names for types cfun, sprod, ssum
huffman
parents: 35514
diff changeset
   790
     (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
35479
dffffe36344a store deflation thms for map functions in theory data
huffman
parents: 35475
diff changeset
   791
        @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
33794
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   792
35525
fa231b86cb1e proper names for types cfun, sprod, ssum
huffman
parents: 35514
diff changeset
   793
     (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
35479
dffffe36344a store deflation thms for map functions in theory data
huffman
parents: 35475
diff changeset
   794
        @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
33794
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   795
35479
dffffe36344a store deflation thms for map functions in theory data
huffman
parents: 35475
diff changeset
   796
     (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
dffffe36344a store deflation thms for map functions in theory data
huffman
parents: 35475
diff changeset
   797
        @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
33794
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   798
35479
dffffe36344a store deflation thms for map functions in theory data
huffman
parents: 35475
diff changeset
   799
     (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm REP_up},
dffffe36344a store deflation thms for map functions in theory data
huffman
parents: 35475
diff changeset
   800
        @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})]
33794
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   801
*}
364bc92ba081 set up domain_isomorphism package in Representable.thy
huffman
parents: 33786
diff changeset
   802
33588
ea9becc59636 theory of representable cpos
huffman
parents:
diff changeset
   803
end