src/HOLCF/Deflation.thy
author huffman
Fri Oct 29 17:15:28 2010 -0700 (2010-10-29)
changeset 40327 1dfdbd66093a
parent 40321 d065b195ec89
child 40502 8e92772bc0e8
permissions -rw-r--r--
renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
huffman@27401
     1
(*  Title:      HOLCF/Deflation.thy
huffman@27401
     2
    Author:     Brian Huffman
huffman@27401
     3
*)
huffman@27401
     4
huffman@35901
     5
header {* Continuous deflations and ep-pairs *}
huffman@27401
     6
huffman@27401
     7
theory Deflation
huffman@27401
     8
imports Cfun
huffman@27401
     9
begin
huffman@27401
    10
wenzelm@36452
    11
default_sort cpo
huffman@27401
    12
huffman@27401
    13
subsection {* Continuous deflations *}
huffman@27401
    14
huffman@27401
    15
locale deflation =
huffman@27401
    16
  fixes d :: "'a \<rightarrow> 'a"
huffman@27401
    17
  assumes idem: "\<And>x. d\<cdot>(d\<cdot>x) = d\<cdot>x"
huffman@31076
    18
  assumes below: "\<And>x. d\<cdot>x \<sqsubseteq> x"
huffman@27401
    19
begin
huffman@27401
    20
huffman@31076
    21
lemma below_ID: "d \<sqsubseteq> ID"
huffman@40002
    22
by (rule cfun_belowI, simp add: below)
huffman@27401
    23
huffman@27401
    24
text {* The set of fixed points is the same as the range. *}
huffman@27401
    25
huffman@27401
    26
lemma fixes_eq_range: "{x. d\<cdot>x = x} = range (\<lambda>x. d\<cdot>x)"
huffman@27401
    27
by (auto simp add: eq_sym_conv idem)
huffman@27401
    28
huffman@27401
    29
lemma range_eq_fixes: "range (\<lambda>x. d\<cdot>x) = {x. d\<cdot>x = x}"
huffman@27401
    30
by (auto simp add: eq_sym_conv idem)
huffman@27401
    31
huffman@27401
    32
text {*
huffman@27401
    33
  The pointwise ordering on deflation functions coincides with
huffman@27401
    34
  the subset ordering of their sets of fixed-points.
huffman@27401
    35
*}
huffman@27401
    36
huffman@31076
    37
lemma belowI:
huffman@27401
    38
  assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
huffman@40002
    39
proof (rule cfun_belowI)
huffman@27401
    40
  fix x
huffman@31076
    41
  from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
huffman@27401
    42
  also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
huffman@27401
    43
  finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" .
huffman@27401
    44
qed
huffman@27401
    45
huffman@31076
    46
lemma belowD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
huffman@31076
    47
proof (rule below_antisym)
huffman@31076
    48
  from below show "d\<cdot>x \<sqsubseteq> x" .
huffman@27401
    49
next
huffman@27401
    50
  assume "f \<sqsubseteq> d"
huffman@27401
    51
  hence "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
huffman@27401
    52
  also assume "f\<cdot>x = x"
huffman@27401
    53
  finally show "x \<sqsubseteq> d\<cdot>x" .
huffman@27401
    54
qed
huffman@27401
    55
huffman@27401
    56
end
huffman@27401
    57
huffman@33503
    58
lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
huffman@33503
    59
by (rule deflation.below [THEN UU_I])
huffman@33503
    60
huffman@27401
    61
lemma adm_deflation: "adm (\<lambda>d. deflation d)"
huffman@27401
    62
by (simp add: deflation_def)
huffman@27401
    63
huffman@27401
    64
lemma deflation_ID: "deflation ID"
huffman@27401
    65
by (simp add: deflation.intro)
huffman@27401
    66
huffman@27401
    67
lemma deflation_UU: "deflation \<bottom>"
huffman@27401
    68
by (simp add: deflation.intro)
huffman@27401
    69
huffman@31076
    70
lemma deflation_below_iff:
huffman@27401
    71
  "\<lbrakk>deflation p; deflation q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
huffman@27401
    72
 apply safe
huffman@31076
    73
  apply (simp add: deflation.belowD)
huffman@31076
    74
 apply (simp add: deflation.belowI)
huffman@27401
    75
done
huffman@27401
    76
huffman@27401
    77
text {*
huffman@27401
    78
  The composition of two deflations is equal to
huffman@27401
    79
  the lesser of the two (if they are comparable).
huffman@27401
    80
*}
huffman@27401
    81
huffman@31076
    82
lemma deflation_below_comp1:
ballarin@28611
    83
  assumes "deflation f"
ballarin@28611
    84
  assumes "deflation g"
huffman@27401
    85
  shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
huffman@31076
    86
proof (rule below_antisym)
ballarin@29237
    87
  interpret g: deflation g by fact
huffman@31076
    88
  from g.below show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
huffman@27401
    89
next
ballarin@29237
    90
  interpret f: deflation f by fact
huffman@27401
    91
  assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
huffman@27401
    92
  hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
huffman@27401
    93
  also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
huffman@27401
    94
  finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" .
huffman@27401
    95
qed
huffman@27401
    96
huffman@31076
    97
lemma deflation_below_comp2:
huffman@27401
    98
  "\<lbrakk>deflation f; deflation g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
huffman@31076
    99
by (simp only: deflation.belowD deflation.idem)
huffman@27401
   100
huffman@27401
   101
huffman@27401
   102
subsection {* Deflations with finite range *}
huffman@27401
   103
huffman@27401
   104
lemma finite_range_imp_finite_fixes:
huffman@27401
   105
  "finite (range f) \<Longrightarrow> finite {x. f x = x}"
huffman@27401
   106
proof -
huffman@27401
   107
  have "{x. f x = x} \<subseteq> range f"
huffman@27401
   108
    by (clarify, erule subst, rule rangeI)
huffman@27401
   109
  moreover assume "finite (range f)"
huffman@27401
   110
  ultimately show "finite {x. f x = x}"
huffman@27401
   111
    by (rule finite_subset)
huffman@27401
   112
qed
huffman@27401
   113
huffman@27401
   114
locale finite_deflation = deflation +
huffman@27401
   115
  assumes finite_fixes: "finite {x. d\<cdot>x = x}"
huffman@27401
   116
begin
huffman@27401
   117
huffman@27401
   118
lemma finite_range: "finite (range (\<lambda>x. d\<cdot>x))"
huffman@27401
   119
by (simp add: range_eq_fixes finite_fixes)
huffman@27401
   120
huffman@27401
   121
lemma finite_image: "finite ((\<lambda>x. d\<cdot>x) ` A)"
huffman@27401
   122
by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])
huffman@27401
   123
huffman@27401
   124
lemma compact: "compact (d\<cdot>x)"
huffman@27401
   125
proof (rule compactI2)
huffman@27401
   126
  fix Y :: "nat \<Rightarrow> 'a"
huffman@27401
   127
  assume Y: "chain Y"
huffman@27401
   128
  have "finite_chain (\<lambda>i. d\<cdot>(Y i))"
huffman@27401
   129
  proof (rule finite_range_imp_finch)
huffman@27401
   130
    show "chain (\<lambda>i. d\<cdot>(Y i))"
huffman@27401
   131
      using Y by simp
huffman@27401
   132
    have "range (\<lambda>i. d\<cdot>(Y i)) \<subseteq> range (\<lambda>x. d\<cdot>x)"
huffman@27401
   133
      by clarsimp
huffman@27401
   134
    thus "finite (range (\<lambda>i. d\<cdot>(Y i)))"
huffman@27401
   135
      using finite_range by (rule finite_subset)
huffman@27401
   136
  qed
huffman@27401
   137
  hence "\<exists>j. (\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)"
huffman@27401
   138
    by (simp add: finite_chain_def maxinch_is_thelub Y)
huffman@27401
   139
  then obtain j where j: "(\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)" ..
huffman@27401
   140
huffman@27401
   141
  assume "d\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
huffman@27401
   142
  hence "d\<cdot>(d\<cdot>x) \<sqsubseteq> d\<cdot>(\<Squnion>i. Y i)"
huffman@27401
   143
    by (rule monofun_cfun_arg)
huffman@27401
   144
  hence "d\<cdot>x \<sqsubseteq> (\<Squnion>i. d\<cdot>(Y i))"
huffman@27401
   145
    by (simp add: contlub_cfun_arg Y idem)
huffman@27401
   146
  hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)"
huffman@27401
   147
    using j by simp
huffman@27401
   148
  hence "d\<cdot>x \<sqsubseteq> Y j"
huffman@31076
   149
    using below by (rule below_trans)
huffman@27401
   150
  thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
huffman@27401
   151
qed
huffman@27401
   152
huffman@27401
   153
end
huffman@27401
   154
brianh@39973
   155
lemma finite_deflation_intro:
brianh@39973
   156
  "deflation d \<Longrightarrow> finite {x. d\<cdot>x = x} \<Longrightarrow> finite_deflation d"
brianh@39973
   157
by (intro finite_deflation.intro finite_deflation_axioms.intro)
brianh@39973
   158
brianh@39971
   159
lemma finite_deflation_imp_deflation:
brianh@39971
   160
  "finite_deflation d \<Longrightarrow> deflation d"
brianh@39971
   161
unfolding finite_deflation_def by simp
brianh@39971
   162
brianh@39971
   163
lemma finite_deflation_UU: "finite_deflation \<bottom>"
brianh@39971
   164
by default simp_all
brianh@39971
   165
huffman@27401
   166
huffman@27401
   167
subsection {* Continuous embedding-projection pairs *}
huffman@27401
   168
huffman@27401
   169
locale ep_pair =
huffman@27401
   170
  fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a"
huffman@27401
   171
  assumes e_inverse [simp]: "\<And>x. p\<cdot>(e\<cdot>x) = x"
huffman@31076
   172
  and e_p_below: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
huffman@27401
   173
begin
huffman@27401
   174
huffman@31076
   175
lemma e_below_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
huffman@27401
   176
proof
huffman@27401
   177
  assume "e\<cdot>x \<sqsubseteq> e\<cdot>y"
huffman@27401
   178
  hence "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
huffman@27401
   179
  thus "x \<sqsubseteq> y" by simp
huffman@27401
   180
next
huffman@27401
   181
  assume "x \<sqsubseteq> y"
huffman@27401
   182
  thus "e\<cdot>x \<sqsubseteq> e\<cdot>y" by (rule monofun_cfun_arg)
huffman@27401
   183
qed
huffman@27401
   184
huffman@27401
   185
lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y"
huffman@31076
   186
unfolding po_eq_conv e_below_iff ..
huffman@27401
   187
huffman@27401
   188
lemma p_eq_iff:
huffman@27401
   189
  "\<lbrakk>e\<cdot>(p\<cdot>x) = x; e\<cdot>(p\<cdot>y) = y\<rbrakk> \<Longrightarrow> p\<cdot>x = p\<cdot>y \<longleftrightarrow> x = y"
huffman@27401
   190
by (safe, erule subst, erule subst, simp)
huffman@27401
   191
huffman@27401
   192
lemma p_inverse: "(\<exists>x. y = e\<cdot>x) = (e\<cdot>(p\<cdot>y) = y)"
huffman@27401
   193
by (auto, rule exI, erule sym)
huffman@27401
   194
huffman@31076
   195
lemma e_below_iff_below_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
huffman@27401
   196
proof
huffman@27401
   197
  assume "e\<cdot>x \<sqsubseteq> y"
huffman@27401
   198
  then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>y" by (rule monofun_cfun_arg)
huffman@27401
   199
  then show "x \<sqsubseteq> p\<cdot>y" by simp
huffman@27401
   200
next
huffman@27401
   201
  assume "x \<sqsubseteq> p\<cdot>y"
huffman@27401
   202
  then have "e\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>y)" by (rule monofun_cfun_arg)
huffman@31076
   203
  then show "e\<cdot>x \<sqsubseteq> y" using e_p_below by (rule below_trans)
huffman@27401
   204
qed
huffman@27401
   205
huffman@27401
   206
lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
huffman@27401
   207
proof -
huffman@27401
   208
  assume "compact (e\<cdot>x)"
huffman@27401
   209
  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
huffman@40327
   210
  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
huffman@27401
   211
  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
huffman@27401
   212
  thus "compact x" by (rule compactI)
huffman@27401
   213
qed
huffman@27401
   214
huffman@27401
   215
lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
huffman@27401
   216
proof -
huffman@27401
   217
  assume "compact x"
huffman@27401
   218
  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
huffman@40327
   219
  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
huffman@31076
   220
  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
huffman@27401
   221
  thus "compact (e\<cdot>x)" by (rule compactI)
huffman@27401
   222
qed
huffman@27401
   223
huffman@27401
   224
lemma compact_e_iff: "compact (e\<cdot>x) \<longleftrightarrow> compact x"
huffman@27401
   225
by (rule iffI [OF compact_e_rev compact_e])
huffman@27401
   226
huffman@27401
   227
text {* Deflations from ep-pairs *}
huffman@27401
   228
huffman@27401
   229
lemma deflation_e_p: "deflation (e oo p)"
huffman@31076
   230
by (simp add: deflation.intro e_p_below)
huffman@27401
   231
huffman@27401
   232
lemma deflation_e_d_p:
ballarin@28611
   233
  assumes "deflation d"
huffman@27401
   234
  shows "deflation (e oo d oo p)"
huffman@27401
   235
proof
ballarin@29237
   236
  interpret deflation d by fact
huffman@27401
   237
  fix x :: 'b
huffman@27401
   238
  show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
huffman@27401
   239
    by (simp add: idem)
huffman@27401
   240
  show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
huffman@31076
   241
    by (simp add: e_below_iff_below_p below)
huffman@27401
   242
qed
huffman@27401
   243
huffman@27401
   244
lemma finite_deflation_e_d_p:
ballarin@28611
   245
  assumes "finite_deflation d"
huffman@27401
   246
  shows "finite_deflation (e oo d oo p)"
huffman@27401
   247
proof
ballarin@29237
   248
  interpret finite_deflation d by fact
huffman@27401
   249
  fix x :: 'b
huffman@27401
   250
  show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
huffman@27401
   251
    by (simp add: idem)
huffman@27401
   252
  show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
huffman@31076
   253
    by (simp add: e_below_iff_below_p below)
huffman@27401
   254
  have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))"
huffman@27401
   255
    by (simp add: finite_image)
huffman@27401
   256
  hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
huffman@27401
   257
    by (simp add: image_image)
huffman@27401
   258
  thus "finite {x. (e oo d oo p)\<cdot>x = x}"
huffman@27401
   259
    by (rule finite_range_imp_finite_fixes)
huffman@27401
   260
qed
huffman@27401
   261
huffman@27401
   262
lemma deflation_p_d_e:
ballarin@28611
   263
  assumes "deflation d"
huffman@27401
   264
  assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
huffman@27401
   265
  shows "deflation (p oo d oo e)"
ballarin@28611
   266
proof -
ballarin@29237
   267
  interpret d: deflation d by fact
huffman@28613
   268
  {
huffman@28613
   269
    fix x
huffman@28613
   270
    have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
huffman@31076
   271
      by (rule d.below)
huffman@28613
   272
    hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)"
huffman@28613
   273
      by (rule monofun_cfun_arg)
huffman@28613
   274
    hence "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
huffman@28613
   275
      by simp
huffman@28613
   276
  }
huffman@31076
   277
  note p_d_e_below = this
ballarin@28611
   278
  show ?thesis
huffman@28613
   279
  proof
huffman@28613
   280
    fix x
huffman@28613
   281
    show "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
huffman@31076
   282
      by (rule p_d_e_below)
huffman@28613
   283
  next
huffman@28613
   284
    fix x
huffman@28613
   285
    show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x"
huffman@31076
   286
    proof (rule below_antisym)
huffman@28613
   287
      show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) \<sqsubseteq> (p oo d oo e)\<cdot>x"
huffman@31076
   288
        by (rule p_d_e_below)
huffman@28613
   289
      have "p\<cdot>(d\<cdot>(d\<cdot>(d\<cdot>(e\<cdot>x)))) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
huffman@28613
   290
        by (intro monofun_cfun_arg d)
huffman@28613
   291
      hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
huffman@28613
   292
        by (simp only: d.idem)
huffman@28613
   293
      thus "(p oo d oo e)\<cdot>x \<sqsubseteq> (p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x)"
huffman@28613
   294
        by simp
huffman@28613
   295
    qed
huffman@28613
   296
  qed
ballarin@28611
   297
qed
huffman@27401
   298
huffman@27401
   299
lemma finite_deflation_p_d_e:
ballarin@28611
   300
  assumes "finite_deflation d"
huffman@27401
   301
  assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
huffman@27401
   302
  shows "finite_deflation (p oo d oo e)"
ballarin@28611
   303
proof -
ballarin@29237
   304
  interpret d: finite_deflation d by fact
ballarin@28611
   305
  show ?thesis
brianh@39973
   306
  proof (rule finite_deflation_intro)
huffman@28613
   307
    have "deflation d" ..
huffman@28613
   308
    thus "deflation (p oo d oo e)"
huffman@28613
   309
      using d by (rule deflation_p_d_e)
huffman@28613
   310
  next
brianh@39973
   311
    have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
brianh@39973
   312
      by (rule d.finite_image)
brianh@39973
   313
    hence "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
brianh@39973
   314
      by (rule finite_imageI)
brianh@39973
   315
    hence "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
brianh@39973
   316
      by (simp add: image_image)
brianh@39973
   317
    thus "finite {x. (p oo d oo e)\<cdot>x = x}"
brianh@39973
   318
      by (rule finite_range_imp_finite_fixes)
huffman@28613
   319
  qed
ballarin@28611
   320
qed
huffman@27401
   321
huffman@27401
   322
end
huffman@27401
   323
huffman@27401
   324
subsection {* Uniqueness of ep-pairs *}
huffman@27401
   325
huffman@28613
   326
lemma ep_pair_unique_e_lemma:
huffman@35168
   327
  assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
huffman@28613
   328
  shows "e1 \<sqsubseteq> e2"
huffman@40002
   329
proof (rule cfun_belowI)
huffman@28613
   330
  fix x
huffman@28613
   331
  have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
huffman@35168
   332
    by (rule ep_pair.e_p_below [OF 1])
huffman@28613
   333
  thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
huffman@35168
   334
    by (simp only: ep_pair.e_inverse [OF 2])
huffman@28613
   335
qed
huffman@28613
   336
huffman@27401
   337
lemma ep_pair_unique_e:
huffman@27401
   338
  "\<lbrakk>ep_pair e1 p; ep_pair e2 p\<rbrakk> \<Longrightarrow> e1 = e2"
huffman@31076
   339
by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
huffman@28613
   340
huffman@28613
   341
lemma ep_pair_unique_p_lemma:
huffman@35168
   342
  assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
huffman@28613
   343
  shows "p1 \<sqsubseteq> p2"
huffman@40002
   344
proof (rule cfun_belowI)
huffman@28613
   345
  fix x
huffman@28613
   346
  have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
huffman@35168
   347
    by (rule ep_pair.e_p_below [OF 1])
huffman@28613
   348
  hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
huffman@28613
   349
    by (rule monofun_cfun_arg)
huffman@28613
   350
  thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
huffman@35168
   351
    by (simp only: ep_pair.e_inverse [OF 2])
huffman@28613
   352
qed
huffman@27401
   353
huffman@27401
   354
lemma ep_pair_unique_p:
huffman@27401
   355
  "\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
huffman@31076
   356
by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
huffman@27401
   357
huffman@27401
   358
subsection {* Composing ep-pairs *}
huffman@27401
   359
huffman@27401
   360
lemma ep_pair_ID_ID: "ep_pair ID ID"
huffman@27401
   361
by default simp_all
huffman@27401
   362
huffman@27401
   363
lemma ep_pair_comp:
huffman@28613
   364
  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
huffman@28613
   365
  shows "ep_pair (e2 oo e1) (p1 oo p2)"
huffman@28613
   366
proof
ballarin@29237
   367
  interpret ep1: ep_pair e1 p1 by fact
ballarin@29237
   368
  interpret ep2: ep_pair e2 p2 by fact
huffman@28613
   369
  fix x y
huffman@28613
   370
  show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
huffman@28613
   371
    by simp
huffman@28613
   372
  have "e1\<cdot>(p1\<cdot>(p2\<cdot>y)) \<sqsubseteq> p2\<cdot>y"
huffman@31076
   373
    by (rule ep1.e_p_below)
huffman@28613
   374
  hence "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)"
huffman@28613
   375
    by (rule monofun_cfun_arg)
huffman@28613
   376
  also have "e2\<cdot>(p2\<cdot>y) \<sqsubseteq> y"
huffman@31076
   377
    by (rule ep2.e_p_below)
huffman@28613
   378
  finally show "(e2 oo e1)\<cdot>((p1 oo p2)\<cdot>y) \<sqsubseteq> y"
huffman@28613
   379
    by simp
huffman@28613
   380
qed
huffman@27401
   381
haftmann@27681
   382
locale pcpo_ep_pair = ep_pair +
huffman@27401
   383
  constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
huffman@27401
   384
  constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
huffman@27401
   385
begin
huffman@27401
   386
huffman@27401
   387
lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
huffman@27401
   388
proof -
huffman@27401
   389
  have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal)
huffman@27401
   390
  hence "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
huffman@31076
   391
  also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_below)
huffman@27401
   392
  finally show "e\<cdot>\<bottom> = \<bottom>" by simp
huffman@27401
   393
qed
huffman@27401
   394
huffman@40321
   395
lemma e_bottom_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
huffman@27401
   396
by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
huffman@27401
   397
huffman@27401
   398
lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
huffman@27401
   399
by simp
huffman@27401
   400
huffman@27401
   401
lemma p_strict [simp]: "p\<cdot>\<bottom> = \<bottom>"
huffman@27401
   402
by (rule e_inverse [where x="\<bottom>", unfolded e_strict])
huffman@27401
   403
huffman@27401
   404
lemmas stricts = e_strict p_strict
huffman@27401
   405
huffman@27401
   406
end
huffman@27401
   407
huffman@39985
   408
subsection {* Map operator for continuous functions *}
huffman@39985
   409
huffman@39985
   410
lemma ep_pair_cfun_map:
huffman@39985
   411
  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
huffman@39985
   412
  shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)"
huffman@39985
   413
proof
huffman@39985
   414
  interpret e1p1: ep_pair e1 p1 by fact
huffman@39985
   415
  interpret e2p2: ep_pair e2 p2 by fact
huffman@39985
   416
  fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
huffman@40002
   417
    by (simp add: cfun_eq_iff)
huffman@39985
   418
  fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
huffman@40002
   419
    apply (rule cfun_belowI, simp)
huffman@39985
   420
    apply (rule below_trans [OF e2p2.e_p_below])
huffman@39985
   421
    apply (rule monofun_cfun_arg)
huffman@39985
   422
    apply (rule e1p1.e_p_below)
huffman@39985
   423
    done
huffman@39985
   424
qed
huffman@39985
   425
huffman@39985
   426
lemma deflation_cfun_map:
huffman@39985
   427
  assumes "deflation d1" and "deflation d2"
huffman@39985
   428
  shows "deflation (cfun_map\<cdot>d1\<cdot>d2)"
huffman@39985
   429
proof
huffman@39985
   430
  interpret d1: deflation d1 by fact
huffman@39985
   431
  interpret d2: deflation d2 by fact
huffman@39985
   432
  fix f
huffman@39985
   433
  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
huffman@40002
   434
    by (simp add: cfun_eq_iff d1.idem d2.idem)
huffman@39985
   435
  show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
huffman@40002
   436
    apply (rule cfun_belowI, simp)
huffman@39985
   437
    apply (rule below_trans [OF d2.below])
huffman@39985
   438
    apply (rule monofun_cfun_arg)
huffman@39985
   439
    apply (rule d1.below)
huffman@39985
   440
    done
huffman@39985
   441
qed
huffman@39985
   442
huffman@39985
   443
lemma finite_range_cfun_map:
huffman@39985
   444
  assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
huffman@39985
   445
  assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
huffman@39985
   446
  shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))"  (is "finite (range ?h)")
huffman@39985
   447
proof (rule finite_imageD)
huffman@39985
   448
  let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
huffman@39985
   449
  show "finite (?f ` range ?h)"
huffman@39985
   450
  proof (rule finite_subset)
huffman@39985
   451
    let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
huffman@39985
   452
    show "?f ` range ?h \<subseteq> ?B"
huffman@39985
   453
      by clarsimp
huffman@39985
   454
    show "finite ?B"
huffman@39985
   455
      by (simp add: a b)
huffman@39985
   456
  qed
huffman@39985
   457
  show "inj_on ?f (range ?h)"
huffman@40002
   458
  proof (rule inj_onI, rule cfun_eqI, clarsimp)
huffman@39985
   459
    fix x f g
huffman@39985
   460
    assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
huffman@39985
   461
    hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
huffman@39985
   462
      by (rule equalityD1)
huffman@39985
   463
    hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
huffman@39985
   464
      by (simp add: subset_eq)
huffman@39985
   465
    then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
huffman@39985
   466
      by (rule rangeE)
huffman@39985
   467
    thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
huffman@39985
   468
      by clarsimp
huffman@39985
   469
  qed
huffman@39985
   470
qed
huffman@39985
   471
huffman@39985
   472
lemma finite_deflation_cfun_map:
huffman@39985
   473
  assumes "finite_deflation d1" and "finite_deflation d2"
huffman@39985
   474
  shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)"
huffman@39985
   475
proof (rule finite_deflation_intro)
huffman@39985
   476
  interpret d1: finite_deflation d1 by fact
huffman@39985
   477
  interpret d2: finite_deflation d2 by fact
huffman@39985
   478
  have "deflation d1" and "deflation d2" by fact+
huffman@39985
   479
  thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map)
huffman@39985
   480
  have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))"
huffman@39985
   481
    using d1.finite_range d2.finite_range
huffman@39985
   482
    by (rule finite_range_cfun_map)
huffman@39985
   483
  thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
huffman@39985
   484
    by (rule finite_range_imp_finite_fixes)
huffman@39985
   485
qed
huffman@39985
   486
huffman@39985
   487
text {* Finite deflations are compact elements of the function space *}
huffman@39985
   488
huffman@39985
   489
lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
huffman@39985
   490
apply (frule finite_deflation_imp_deflation)
huffman@39985
   491
apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
huffman@39985
   492
apply (simp add: cfun_map_def deflation.idem eta_cfun)
huffman@39985
   493
apply (rule finite_deflation.compact)
huffman@39985
   494
apply (simp only: finite_deflation_cfun_map)
huffman@39985
   495
done
huffman@39985
   496
huffman@27401
   497
end