src/HOLCF/Representable.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40497 d2e876d6da8c
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman@33589
     1
(*  Title:      HOLCF/Representable.thy
huffman@33589
     2
    Author:     Brian Huffman
huffman@33589
     3
*)
huffman@33589
     4
huffman@33588
     5
header {* Representable Types *}
huffman@33588
     6
huffman@33588
     7
theory Representable
huffman@39987
     8
imports Algebraic Bifinite Universal Ssum One Fixrec Domain_Aux
huffman@33794
     9
uses
huffman@33794
    10
  ("Tools/repdef.ML")
huffman@33794
    11
  ("Tools/Domain/domain_isomorphism.ML")
huffman@33588
    12
begin
huffman@33588
    13
huffman@40497
    14
default_sort "domain"
huffman@33588
    15
huffman@33588
    16
subsection {* Representations of types *}
huffman@33588
    17
huffman@39989
    18
lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
huffman@39989
    19
by (simp add: cast_DEFL)
huffman@33588
    20
huffman@40037
    21
lemma emb_prj_emb:
huffman@40037
    22
  fixes x :: "'a"
huffman@40037
    23
  assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
huffman@40037
    24
  shows "emb\<cdot>(prj\<cdot>(emb\<cdot>x) :: 'b) = emb\<cdot>x"
huffman@40037
    25
unfolding emb_prj
huffman@40037
    26
apply (rule cast.belowD)
huffman@40037
    27
apply (rule monofun_cfun_arg [OF assms])
huffman@40037
    28
apply (simp add: cast_DEFL)
huffman@33588
    29
done
huffman@33588
    30
huffman@40037
    31
lemma prj_emb_prj:
huffman@40037
    32
  assumes "DEFL('a) \<sqsubseteq> DEFL('b)"
huffman@40037
    33
  shows "prj\<cdot>(emb\<cdot>(prj\<cdot>x :: 'b)) = (prj\<cdot>x :: 'a)"
huffman@33588
    34
 apply (rule emb_eq_iff [THEN iffD1])
huffman@33588
    35
 apply (simp only: emb_prj)
huffman@33588
    36
 apply (rule deflation_below_comp1)
huffman@33588
    37
   apply (rule deflation_cast)
huffman@33588
    38
  apply (rule deflation_cast)
huffman@40037
    39
 apply (rule monofun_cfun_arg [OF assms])
huffman@33588
    40
done
huffman@33588
    41
huffman@33779
    42
text {* Isomorphism lemmas used internally by the domain package: *}
huffman@33779
    43
huffman@33779
    44
lemma domain_abs_iso:
huffman@33779
    45
  fixes abs and rep
huffman@39989
    46
  assumes DEFL: "DEFL('b) = DEFL('a)"
huffman@40037
    47
  assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
huffman@40037
    48
  assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
huffman@33779
    49
  shows "rep\<cdot>(abs\<cdot>x) = x"
huffman@40037
    50
unfolding abs_def rep_def
huffman@40037
    51
by (simp add: emb_prj_emb DEFL)
huffman@33779
    52
huffman@33779
    53
lemma domain_rep_iso:
huffman@33779
    54
  fixes abs and rep
huffman@39989
    55
  assumes DEFL: "DEFL('b) = DEFL('a)"
huffman@40037
    56
  assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
huffman@40037
    57
  assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
huffman@33779
    58
  shows "abs\<cdot>(rep\<cdot>x) = x"
huffman@40037
    59
unfolding abs_def rep_def
huffman@40037
    60
by (simp add: emb_prj_emb DEFL)
huffman@33779
    61
huffman@40038
    62
subsection {* Deflations as sets *}
huffman@40038
    63
huffman@40038
    64
definition defl_set :: "defl \<Rightarrow> udom set"
huffman@40038
    65
where "defl_set A = {x. cast\<cdot>A\<cdot>x = x}"
huffman@40038
    66
huffman@40038
    67
lemma adm_defl_set: "adm (\<lambda>x. x \<in> defl_set A)"
huffman@40038
    68
unfolding defl_set_def by simp
huffman@40038
    69
huffman@40038
    70
lemma defl_set_bottom: "\<bottom> \<in> defl_set A"
huffman@40038
    71
unfolding defl_set_def by simp
huffman@40038
    72
huffman@40038
    73
lemma defl_set_cast [simp]: "cast\<cdot>A\<cdot>x \<in> defl_set A"
huffman@40038
    74
unfolding defl_set_def by simp
huffman@40038
    75
huffman@40038
    76
lemma defl_set_subset_iff: "defl_set A \<subseteq> defl_set B \<longleftrightarrow> A \<sqsubseteq> B"
huffman@40038
    77
apply (simp add: defl_set_def subset_eq cast_below_cast [symmetric])
huffman@40038
    78
apply (auto simp add: cast.belowI cast.belowD)
huffman@40038
    79
done
huffman@40038
    80
huffman@33588
    81
subsection {* Proving a subtype is representable *}
huffman@33588
    82
huffman@40491
    83
text {* Temporarily relax type constraints. *}
huffman@33588
    84
huffman@40037
    85
setup {*
huffman@40037
    86
  fold Sign.add_const_constraint
huffman@40037
    87
  [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
huffman@40037
    88
  , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
huffman@40491
    89
  , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::pcpo"})
huffman@40491
    90
  , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> defl"})
huffman@40491
    91
  , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom"})
huffman@40491
    92
  , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
huffman@40037
    93
*}
huffman@33588
    94
huffman@33588
    95
lemma typedef_rep_class:
huffman@33588
    96
  fixes Rep :: "'a::pcpo \<Rightarrow> udom"
huffman@33588
    97
  fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
huffman@39989
    98
  fixes t :: defl
huffman@40038
    99
  assumes type: "type_definition Rep Abs (defl_set t)"
huffman@33588
   100
  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
huffman@33679
   101
  assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
huffman@33679
   102
  assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
huffman@39989
   103
  assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"
huffman@40491
   104
  assumes liftemb: "(liftemb :: 'a u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
huffman@40491
   105
  assumes liftprj: "(liftprj :: udom \<rightarrow> 'a u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
huffman@40491
   106
  assumes liftdefl: "(liftdefl :: 'a itself \<Rightarrow> defl) \<equiv> (\<lambda>t. u_defl\<cdot>DEFL('a))"
huffman@40494
   107
  shows "OFCLASS('a, liftdomain_class)"
huffman@40491
   108
using liftemb [THEN meta_eq_to_obj_eq]
huffman@40491
   109
using liftprj [THEN meta_eq_to_obj_eq]
huffman@40494
   110
proof (rule liftdomain_class_intro)
huffman@33588
   111
  have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
huffman@33588
   112
    unfolding emb
huffman@33588
   113
    apply (rule beta_cfun)
huffman@40038
   114
    apply (rule typedef_cont_Rep [OF type below adm_defl_set])
huffman@33588
   115
    done
huffman@33588
   116
  have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
huffman@33588
   117
    unfolding prj
huffman@33588
   118
    apply (rule beta_cfun)
huffman@40038
   119
    apply (rule typedef_cont_Abs [OF type below adm_defl_set])
huffman@33588
   120
    apply simp_all
huffman@33588
   121
    done
huffman@40038
   122
  have prj_emb: "\<And>x::'a. prj\<cdot>(emb\<cdot>x) = x"
huffman@33588
   123
    using type_definition.Rep [OF type]
huffman@40038
   124
    unfolding prj_beta emb_beta defl_set_def
huffman@40038
   125
    by (simp add: type_definition.Rep_inverse [OF type])
huffman@33588
   126
  have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
huffman@33588
   127
    unfolding prj_beta emb_beta
huffman@33588
   128
    by (simp add: type_definition.Abs_inverse [OF type])
huffman@39974
   129
  show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
huffman@39974
   130
    apply default
huffman@39974
   131
    apply (simp add: prj_emb)
huffman@39974
   132
    apply (simp add: emb_prj cast.below)
huffman@33588
   133
    done
huffman@39989
   134
  show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
huffman@40002
   135
    by (rule cfun_eqI, simp add: defl emb_prj)
huffman@40491
   136
  show "LIFTDEFL('a) = u_defl\<cdot>DEFL('a)"
huffman@40491
   137
    unfolding liftdefl ..
huffman@33588
   138
qed
huffman@33588
   139
huffman@39989
   140
lemma typedef_DEFL:
huffman@39989
   141
  assumes "defl \<equiv> (\<lambda>a::'a::pcpo itself. t)"
huffman@39989
   142
  shows "DEFL('a::pcpo) = t"
huffman@39974
   143
unfolding assms ..
huffman@39974
   144
huffman@40037
   145
text {* Restore original typing constraints. *}
huffman@39974
   146
huffman@40037
   147
setup {*
huffman@40037
   148
  fold Sign.add_const_constraint
huffman@40497
   149
  [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> defl"})
huffman@40497
   150
  , (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"})
huffman@40497
   151
  , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"})
huffman@40491
   152
  , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"})
huffman@40491
   153
  , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"})
huffman@40491
   154
  , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
huffman@40037
   155
*}
huffman@39974
   156
huffman@33679
   157
use "Tools/repdef.ML"
huffman@33679
   158
huffman@33588
   159
subsection {* Isomorphic deflations *}
huffman@33588
   160
huffman@33588
   161
definition
huffman@39989
   162
  isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> defl \<Rightarrow> bool"
huffman@33588
   163
where
huffman@33588
   164
  "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
huffman@33588
   165
huffman@33588
   166
lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
huffman@40002
   167
unfolding isodefl_def by (simp add: cfun_eqI)
huffman@33588
   168
huffman@33588
   169
lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
huffman@40002
   170
unfolding isodefl_def by (simp add: cfun_eqI)
huffman@33588
   171
huffman@33588
   172
lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
huffman@33588
   173
unfolding isodefl_def
huffman@33588
   174
by (drule cfun_fun_cong [where x="\<bottom>"], simp)
huffman@33588
   175
huffman@33588
   176
lemma isodefl_imp_deflation:
huffman@39986
   177
  fixes d :: "'a \<rightarrow> 'a"
huffman@33588
   178
  assumes "isodefl d t" shows "deflation d"
huffman@33588
   179
proof
huffman@39974
   180
  note assms [unfolded isodefl_def, simp]
huffman@33588
   181
  fix x :: 'a
huffman@33588
   182
  show "d\<cdot>(d\<cdot>x) = d\<cdot>x"
huffman@33588
   183
    using cast.idem [of t "emb\<cdot>x"] by simp
huffman@33588
   184
  show "d\<cdot>x \<sqsubseteq> x"
huffman@33588
   185
    using cast.below [of t "emb\<cdot>x"] by simp
huffman@33588
   186
qed
huffman@33588
   187
huffman@39989
   188
lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \<rightarrow> 'a) DEFL('a)"
huffman@39989
   189
unfolding isodefl_def by (simp add: cast_DEFL)
huffman@33588
   190
huffman@40491
   191
lemma isodefl_LIFTDEFL:
huffman@40491
   192
  "isodefl (u_map\<cdot>(ID :: 'a \<rightarrow> 'a)) LIFTDEFL('a::predomain)"
huffman@40491
   193
unfolding u_map_ID DEFL_u [symmetric]
huffman@40491
   194
by (rule isodefl_ID_DEFL)
huffman@40491
   195
huffman@39989
   196
lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
huffman@33588
   197
unfolding isodefl_def
huffman@39989
   198
apply (simp add: cast_DEFL)
huffman@40002
   199
apply (simp add: cfun_eq_iff)
huffman@33588
   200
apply (rule allI)
huffman@33588
   201
apply (drule_tac x="emb\<cdot>x" in spec)
huffman@33588
   202
apply simp
huffman@33588
   203
done
huffman@33588
   204
huffman@33588
   205
lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
huffman@40002
   206
unfolding isodefl_def by (simp add: cfun_eq_iff)
huffman@33588
   207
huffman@33588
   208
lemma adm_isodefl:
huffman@33588
   209
  "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
huffman@33588
   210
unfolding isodefl_def by simp
huffman@33588
   211
huffman@33588
   212
lemma isodefl_lub:
huffman@33588
   213
  assumes "chain d" and "chain t"
huffman@33588
   214
  assumes "\<And>i. isodefl (d i) (t i)"
huffman@33588
   215
  shows "isodefl (\<Squnion>i. d i) (\<Squnion>i. t i)"
huffman@33588
   216
using prems unfolding isodefl_def
huffman@33588
   217
by (simp add: contlub_cfun_arg contlub_cfun_fun)
huffman@33588
   218
huffman@33588
   219
lemma isodefl_fix:
huffman@33588
   220
  assumes "\<And>d t. isodefl d t \<Longrightarrow> isodefl (f\<cdot>d) (g\<cdot>t)"
huffman@33588
   221
  shows "isodefl (fix\<cdot>f) (fix\<cdot>g)"
huffman@33588
   222
unfolding fix_def2
huffman@33588
   223
apply (rule isodefl_lub, simp, simp)
huffman@33588
   224
apply (induct_tac i)
huffman@33588
   225
apply (simp add: isodefl_bottom)
huffman@39974
   226
apply (simp add: assms)
huffman@33588
   227
done
huffman@33588
   228
huffman@33779
   229
lemma isodefl_abs_rep:
huffman@33779
   230
  fixes abs and rep and d
huffman@39989
   231
  assumes DEFL: "DEFL('b) = DEFL('a)"
huffman@40037
   232
  assumes abs_def: "(abs :: 'a \<rightarrow> 'b) \<equiv> prj oo emb"
huffman@40037
   233
  assumes rep_def: "(rep :: 'b \<rightarrow> 'a) \<equiv> prj oo emb"
huffman@33779
   234
  shows "isodefl d t \<Longrightarrow> isodefl (abs oo d oo rep) t"
huffman@40037
   235
unfolding isodefl_def
huffman@40037
   236
by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)
huffman@33779
   237
huffman@33588
   238
lemma isodefl_cfun:
huffman@33588
   239
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@39989
   240
    isodefl (cfun_map\<cdot>d1\<cdot>d2) (cfun_defl\<cdot>t1\<cdot>t2)"
huffman@33588
   241
apply (rule isodeflI)
huffman@39989
   242
apply (simp add: cast_cfun_defl cast_isodefl)
huffman@33588
   243
apply (simp add: emb_cfun_def prj_cfun_def)
huffman@33588
   244
apply (simp add: cfun_map_map cfcomp1)
huffman@33588
   245
done
huffman@33588
   246
huffman@33588
   247
lemma isodefl_ssum:
huffman@33588
   248
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@39989
   249
    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
huffman@33588
   250
apply (rule isodeflI)
huffman@39989
   251
apply (simp add: cast_ssum_defl cast_isodefl)
huffman@33588
   252
apply (simp add: emb_ssum_def prj_ssum_def)
huffman@33588
   253
apply (simp add: ssum_map_map isodefl_strict)
huffman@33588
   254
done
huffman@33588
   255
huffman@33588
   256
lemma isodefl_sprod:
huffman@33588
   257
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@39989
   258
    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
huffman@33588
   259
apply (rule isodeflI)
huffman@39989
   260
apply (simp add: cast_sprod_defl cast_isodefl)
huffman@33588
   261
apply (simp add: emb_sprod_def prj_sprod_def)
huffman@33588
   262
apply (simp add: sprod_map_map isodefl_strict)
huffman@33588
   263
done
huffman@33588
   264
huffman@33786
   265
lemma isodefl_cprod:
huffman@33786
   266
  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
huffman@39989
   267
    isodefl (cprod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
huffman@33786
   268
apply (rule isodeflI)
huffman@39989
   269
apply (simp add: cast_prod_defl cast_isodefl)
huffman@39974
   270
apply (simp add: emb_prod_def prj_prod_def)
huffman@33786
   271
apply (simp add: cprod_map_map cfcomp1)
huffman@33786
   272
done
huffman@33786
   273
huffman@33588
   274
lemma isodefl_u:
huffman@40494
   275
  fixes d :: "'a::liftdomain \<rightarrow> 'a"
huffman@40491
   276
  shows "isodefl (d :: 'a \<rightarrow> 'a) t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
huffman@33588
   277
apply (rule isodeflI)
huffman@39989
   278
apply (simp add: cast_u_defl cast_isodefl)
huffman@40494
   279
apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq)
huffman@33588
   280
apply (simp add: u_map_map)
huffman@33588
   281
done
huffman@33588
   282
huffman@40493
   283
lemma encode_prod_u_map:
huffman@40493
   284
  "encode_prod_u\<cdot>(u_map\<cdot>(cprod_map\<cdot>f\<cdot>g)\<cdot>(decode_prod_u\<cdot>x))
huffman@40493
   285
    = sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
huffman@40493
   286
unfolding encode_prod_u_def decode_prod_u_def
huffman@40493
   287
apply (case_tac x, simp, rename_tac a b)
huffman@40493
   288
apply (case_tac a, simp, case_tac b, simp, simp)
huffman@40493
   289
done
huffman@40493
   290
huffman@40491
   291
lemma isodefl_cprod_u:
huffman@40493
   292
  assumes "isodefl (u_map\<cdot>d1) t1" and "isodefl (u_map\<cdot>d2) t2"
huffman@40493
   293
  shows "isodefl (u_map\<cdot>(cprod_map\<cdot>d1\<cdot>d2)) (sprod_defl\<cdot>t1\<cdot>t2)"
huffman@40493
   294
using assms unfolding isodefl_def
huffman@40493
   295
apply (simp add: emb_u_def prj_u_def liftemb_prod_def liftprj_prod_def)
huffman@40493
   296
apply (simp add: emb_u_def [symmetric] prj_u_def [symmetric])
huffman@40493
   297
apply (simp add: cfcomp1 encode_prod_u_map cast_sprod_defl sprod_map_map)
huffman@40493
   298
done
huffman@40491
   299
huffman@33794
   300
subsection {* Constructing Domain Isomorphisms *}
huffman@33794
   301
huffman@33794
   302
use "Tools/Domain/domain_isomorphism.ML"
huffman@33794
   303
huffman@40216
   304
setup Domain_Isomorphism.setup
huffman@40216
   305
huffman@40216
   306
lemmas [domain_defl_simps] =
huffman@40216
   307
  DEFL_cfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
huffman@40494
   308
  liftdefl_eq LIFTDEFL_prod
huffman@40216
   309
huffman@40216
   310
lemmas [domain_map_ID] =
huffman@40216
   311
  cfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
huffman@40216
   312
huffman@40216
   313
lemmas [domain_isodefl] =
huffman@40494
   314
  isodefl_u isodefl_cfun isodefl_ssum isodefl_sprod
huffman@40494
   315
  isodefl_cprod isodefl_cprod_u
huffman@40216
   316
huffman@40216
   317
lemmas [domain_deflation] =
huffman@40216
   318
  deflation_cfun_map deflation_ssum_map deflation_sprod_map
huffman@40216
   319
  deflation_cprod_map deflation_u_map
huffman@40216
   320
huffman@33794
   321
setup {*
huffman@40487
   322
  fold Domain_Take_Proofs.add_map_function
huffman@40487
   323
    [(@{type_name cfun}, @{const_name cfun_map}, [true, true]),
huffman@40487
   324
     (@{type_name ssum}, @{const_name ssum_map}, [true, true]),
huffman@40487
   325
     (@{type_name sprod}, @{const_name sprod_map}, [true, true]),
huffman@40487
   326
     (@{type_name prod}, @{const_name cprod_map}, [true, true]),
huffman@40487
   327
     (@{type_name "u"}, @{const_name u_map}, [true])]
huffman@33794
   328
*}
huffman@33794
   329
huffman@33588
   330
end