src/HOLCF/Deflation.thy
author ballarin
Thu Oct 16 17:19:47 2008 +0200 (2008-10-16)
changeset 28611 983c1855a7af
parent 27681 8cedebf55539
child 28613 15a41d3fa959
permissions -rw-r--r--
More occurrences of 'includes' gone.
huffman@27401
     1
(*  Title:      HOLCF/Deflation.thy
huffman@27401
     2
    ID:         $Id$
huffman@27401
     3
    Author:     Brian Huffman
huffman@27401
     4
*)
huffman@27401
     5
huffman@27401
     6
header {* Continuous Deflations and Embedding-Projection Pairs *}
huffman@27401
     7
huffman@27401
     8
theory Deflation
huffman@27401
     9
imports Cfun
huffman@27401
    10
begin
huffman@27401
    11
huffman@27401
    12
defaultsort cpo
huffman@27401
    13
huffman@27401
    14
subsection {* Continuous deflations *}
huffman@27401
    15
huffman@27401
    16
locale deflation =
huffman@27401
    17
  fixes d :: "'a \<rightarrow> 'a"
huffman@27401
    18
  assumes idem: "\<And>x. d\<cdot>(d\<cdot>x) = d\<cdot>x"
huffman@27401
    19
  assumes less: "\<And>x. d\<cdot>x \<sqsubseteq> x"
huffman@27401
    20
begin
huffman@27401
    21
huffman@27401
    22
lemma less_ID: "d \<sqsubseteq> ID"
huffman@27401
    23
by (rule less_cfun_ext, simp add: less)
huffman@27401
    24
huffman@27401
    25
text {* The set of fixed points is the same as the range. *}
huffman@27401
    26
huffman@27401
    27
lemma fixes_eq_range: "{x. d\<cdot>x = x} = range (\<lambda>x. d\<cdot>x)"
huffman@27401
    28
by (auto simp add: eq_sym_conv idem)
huffman@27401
    29
huffman@27401
    30
lemma range_eq_fixes: "range (\<lambda>x. d\<cdot>x) = {x. d\<cdot>x = x}"
huffman@27401
    31
by (auto simp add: eq_sym_conv idem)
huffman@27401
    32
huffman@27401
    33
text {*
huffman@27401
    34
  The pointwise ordering on deflation functions coincides with
huffman@27401
    35
  the subset ordering of their sets of fixed-points.
huffman@27401
    36
*}
huffman@27401
    37
huffman@27401
    38
lemma lessI:
huffman@27401
    39
  assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
huffman@27401
    40
proof (rule less_cfun_ext)
huffman@27401
    41
  fix x
huffman@27401
    42
  from less have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
huffman@27401
    43
  also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
huffman@27401
    44
  finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" .
huffman@27401
    45
qed
huffman@27401
    46
huffman@27401
    47
lemma lessD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
huffman@27401
    48
proof (rule antisym_less)
huffman@27401
    49
  from less show "d\<cdot>x \<sqsubseteq> x" .
huffman@27401
    50
next
huffman@27401
    51
  assume "f \<sqsubseteq> d"
huffman@27401
    52
  hence "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
huffman@27401
    53
  also assume "f\<cdot>x = x"
huffman@27401
    54
  finally show "x \<sqsubseteq> d\<cdot>x" .
huffman@27401
    55
qed
huffman@27401
    56
huffman@27401
    57
end
huffman@27401
    58
huffman@27401
    59
lemma adm_deflation: "adm (\<lambda>d. deflation d)"
huffman@27401
    60
by (simp add: deflation_def)
huffman@27401
    61
huffman@27401
    62
lemma deflation_ID: "deflation ID"
huffman@27401
    63
by (simp add: deflation.intro)
huffman@27401
    64
huffman@27401
    65
lemma deflation_UU: "deflation \<bottom>"
huffman@27401
    66
by (simp add: deflation.intro)
huffman@27401
    67
huffman@27401
    68
lemma deflation_less_iff:
huffman@27401
    69
  "\<lbrakk>deflation p; deflation q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
huffman@27401
    70
 apply safe
huffman@27401
    71
  apply (simp add: deflation.lessD)
huffman@27401
    72
 apply (simp add: deflation.lessI)
huffman@27401
    73
done
huffman@27401
    74
huffman@27401
    75
text {*
huffman@27401
    76
  The composition of two deflations is equal to
huffman@27401
    77
  the lesser of the two (if they are comparable).
huffman@27401
    78
*}
huffman@27401
    79
huffman@27401
    80
lemma deflation_less_comp1:
ballarin@28611
    81
  assumes "deflation f"
ballarin@28611
    82
  assumes "deflation g"
huffman@27401
    83
  shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
huffman@27401
    84
proof (rule antisym_less)
ballarin@28611
    85
  interpret g: deflation [g] by fact
huffman@27401
    86
  from g.less show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
huffman@27401
    87
next
ballarin@28611
    88
  interpret f: deflation [f] by fact
huffman@27401
    89
  assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
huffman@27401
    90
  hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
huffman@27401
    91
  also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
huffman@27401
    92
  finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" .
huffman@27401
    93
qed
huffman@27401
    94
huffman@27401
    95
lemma deflation_less_comp2:
huffman@27401
    96
  "\<lbrakk>deflation f; deflation g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
huffman@27401
    97
by (simp only: deflation.lessD deflation.idem)
huffman@27401
    98
huffman@27401
    99
huffman@27401
   100
subsection {* Deflations with finite range *}
huffman@27401
   101
huffman@27401
   102
lemma finite_range_imp_finite_fixes:
huffman@27401
   103
  "finite (range f) \<Longrightarrow> finite {x. f x = x}"
huffman@27401
   104
proof -
huffman@27401
   105
  have "{x. f x = x} \<subseteq> range f"
huffman@27401
   106
    by (clarify, erule subst, rule rangeI)
huffman@27401
   107
  moreover assume "finite (range f)"
huffman@27401
   108
  ultimately show "finite {x. f x = x}"
huffman@27401
   109
    by (rule finite_subset)
huffman@27401
   110
qed
huffman@27401
   111
huffman@27401
   112
locale finite_deflation = deflation +
huffman@27401
   113
  assumes finite_fixes: "finite {x. d\<cdot>x = x}"
huffman@27401
   114
begin
huffman@27401
   115
huffman@27401
   116
lemma finite_range: "finite (range (\<lambda>x. d\<cdot>x))"
huffman@27401
   117
by (simp add: range_eq_fixes finite_fixes)
huffman@27401
   118
huffman@27401
   119
lemma finite_image: "finite ((\<lambda>x. d\<cdot>x) ` A)"
huffman@27401
   120
by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])
huffman@27401
   121
huffman@27401
   122
lemma compact: "compact (d\<cdot>x)"
huffman@27401
   123
proof (rule compactI2)
huffman@27401
   124
  fix Y :: "nat \<Rightarrow> 'a"
huffman@27401
   125
  assume Y: "chain Y"
huffman@27401
   126
  have "finite_chain (\<lambda>i. d\<cdot>(Y i))"
huffman@27401
   127
  proof (rule finite_range_imp_finch)
huffman@27401
   128
    show "chain (\<lambda>i. d\<cdot>(Y i))"
huffman@27401
   129
      using Y by simp
huffman@27401
   130
    have "range (\<lambda>i. d\<cdot>(Y i)) \<subseteq> range (\<lambda>x. d\<cdot>x)"
huffman@27401
   131
      by clarsimp
huffman@27401
   132
    thus "finite (range (\<lambda>i. d\<cdot>(Y i)))"
huffman@27401
   133
      using finite_range by (rule finite_subset)
huffman@27401
   134
  qed
huffman@27401
   135
  hence "\<exists>j. (\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)"
huffman@27401
   136
    by (simp add: finite_chain_def maxinch_is_thelub Y)
huffman@27401
   137
  then obtain j where j: "(\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)" ..
huffman@27401
   138
huffman@27401
   139
  assume "d\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
huffman@27401
   140
  hence "d\<cdot>(d\<cdot>x) \<sqsubseteq> d\<cdot>(\<Squnion>i. Y i)"
huffman@27401
   141
    by (rule monofun_cfun_arg)
huffman@27401
   142
  hence "d\<cdot>x \<sqsubseteq> (\<Squnion>i. d\<cdot>(Y i))"
huffman@27401
   143
    by (simp add: contlub_cfun_arg Y idem)
huffman@27401
   144
  hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)"
huffman@27401
   145
    using j by simp
huffman@27401
   146
  hence "d\<cdot>x \<sqsubseteq> Y j"
huffman@27401
   147
    using less by (rule trans_less)
huffman@27401
   148
  thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
huffman@27401
   149
qed
huffman@27401
   150
huffman@27401
   151
end
huffman@27401
   152
huffman@27401
   153
huffman@27401
   154
subsection {* Continuous embedding-projection pairs *}
huffman@27401
   155
huffman@27401
   156
locale ep_pair =
huffman@27401
   157
  fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a"
huffman@27401
   158
  assumes e_inverse [simp]: "\<And>x. p\<cdot>(e\<cdot>x) = x"
huffman@27401
   159
  and e_p_less: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
huffman@27401
   160
begin
huffman@27401
   161
huffman@27401
   162
lemma e_less_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
huffman@27401
   163
proof
huffman@27401
   164
  assume "e\<cdot>x \<sqsubseteq> e\<cdot>y"
huffman@27401
   165
  hence "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
huffman@27401
   166
  thus "x \<sqsubseteq> y" by simp
huffman@27401
   167
next
huffman@27401
   168
  assume "x \<sqsubseteq> y"
huffman@27401
   169
  thus "e\<cdot>x \<sqsubseteq> e\<cdot>y" by (rule monofun_cfun_arg)
huffman@27401
   170
qed
huffman@27401
   171
huffman@27401
   172
lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y"
huffman@27401
   173
unfolding po_eq_conv e_less_iff ..
huffman@27401
   174
huffman@27401
   175
lemma p_eq_iff:
huffman@27401
   176
  "\<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
   177
by (safe, erule subst, erule subst, simp)
huffman@27401
   178
huffman@27401
   179
lemma p_inverse: "(\<exists>x. y = e\<cdot>x) = (e\<cdot>(p\<cdot>y) = y)"
huffman@27401
   180
by (auto, rule exI, erule sym)
huffman@27401
   181
huffman@27401
   182
lemma e_less_iff_less_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
huffman@27401
   183
proof
huffman@27401
   184
  assume "e\<cdot>x \<sqsubseteq> y"
huffman@27401
   185
  then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>y" by (rule monofun_cfun_arg)
huffman@27401
   186
  then show "x \<sqsubseteq> p\<cdot>y" by simp
huffman@27401
   187
next
huffman@27401
   188
  assume "x \<sqsubseteq> p\<cdot>y"
huffman@27401
   189
  then have "e\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>y)" by (rule monofun_cfun_arg)
huffman@27401
   190
  then show "e\<cdot>x \<sqsubseteq> y" using e_p_less by (rule trans_less)
huffman@27401
   191
qed
huffman@27401
   192
huffman@27401
   193
lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
huffman@27401
   194
proof -
huffman@27401
   195
  assume "compact (e\<cdot>x)"
huffman@27401
   196
  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
huffman@27401
   197
  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
huffman@27401
   198
  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
huffman@27401
   199
  thus "compact x" by (rule compactI)
huffman@27401
   200
qed
huffman@27401
   201
huffman@27401
   202
lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
huffman@27401
   203
proof -
huffman@27401
   204
  assume "compact x"
huffman@27401
   205
  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
huffman@27401
   206
  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
huffman@27401
   207
  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_less_iff_less_p)
huffman@27401
   208
  thus "compact (e\<cdot>x)" by (rule compactI)
huffman@27401
   209
qed
huffman@27401
   210
huffman@27401
   211
lemma compact_e_iff: "compact (e\<cdot>x) \<longleftrightarrow> compact x"
huffman@27401
   212
by (rule iffI [OF compact_e_rev compact_e])
huffman@27401
   213
huffman@27401
   214
text {* Deflations from ep-pairs *}
huffman@27401
   215
huffman@27401
   216
lemma deflation_e_p: "deflation (e oo p)"
huffman@27401
   217
by (simp add: deflation.intro e_p_less)
huffman@27401
   218
huffman@27401
   219
lemma deflation_e_d_p:
ballarin@28611
   220
  assumes "deflation d"
huffman@27401
   221
  shows "deflation (e oo d oo p)"
huffman@27401
   222
proof
ballarin@28611
   223
  interpret deflation [d] by fact
huffman@27401
   224
  fix x :: 'b
huffman@27401
   225
  show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
huffman@27401
   226
    by (simp add: idem)
huffman@27401
   227
  show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
huffman@27401
   228
    by (simp add: e_less_iff_less_p less)
huffman@27401
   229
qed
huffman@27401
   230
huffman@27401
   231
lemma finite_deflation_e_d_p:
ballarin@28611
   232
  assumes "finite_deflation d"
huffman@27401
   233
  shows "finite_deflation (e oo d oo p)"
huffman@27401
   234
proof
ballarin@28611
   235
  interpret finite_deflation [d] by fact
huffman@27401
   236
  fix x :: 'b
huffman@27401
   237
  show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
huffman@27401
   238
    by (simp add: idem)
huffman@27401
   239
  show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
huffman@27401
   240
    by (simp add: e_less_iff_less_p less)
huffman@27401
   241
  have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))"
huffman@27401
   242
    by (simp add: finite_image)
huffman@27401
   243
  hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
huffman@27401
   244
    by (simp add: image_image)
huffman@27401
   245
  thus "finite {x. (e oo d oo p)\<cdot>x = x}"
huffman@27401
   246
    by (rule finite_range_imp_finite_fixes)
huffman@27401
   247
qed
huffman@27401
   248
huffman@27401
   249
lemma deflation_p_d_e:
ballarin@28611
   250
  assumes "deflation d"
huffman@27401
   251
  assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
huffman@27401
   252
  shows "deflation (p oo d oo e)"
ballarin@28611
   253
proof -
ballarin@28611
   254
  interpret d: deflation [d] by fact
ballarin@28611
   255
  show ?thesis
ballarin@28611
   256
   apply (default, simp_all)
ballarin@28611
   257
    apply (rule antisym_less)
ballarin@28611
   258
     apply (rule monofun_cfun_arg)
ballarin@28611
   259
     apply (rule trans_less [OF d])
ballarin@28611
   260
     apply (simp add: e_p_less)
ballarin@28611
   261
    apply (rule monofun_cfun_arg)
ballarin@28611
   262
    apply (rule rev_trans_less)
ballarin@28611
   263
    apply (rule monofun_cfun_arg)
ballarin@28611
   264
    apply (rule d)
ballarin@28611
   265
    apply (simp add: d.idem)
ballarin@28611
   266
   apply (rule sq_ord_less_eq_trans)
ballarin@28611
   267
    apply (rule monofun_cfun_arg)
ballarin@28611
   268
    apply (rule d.less)
ballarin@28611
   269
   apply (rule e_inverse)
ballarin@28611
   270
  done
ballarin@28611
   271
qed
huffman@27401
   272
huffman@27401
   273
lemma finite_deflation_p_d_e:
ballarin@28611
   274
  assumes "finite_deflation d"
huffman@27401
   275
  assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
huffman@27401
   276
  shows "finite_deflation (p oo d oo e)"
ballarin@28611
   277
proof -
ballarin@28611
   278
  interpret d: finite_deflation [d] by fact
ballarin@28611
   279
  show ?thesis
ballarin@28611
   280
   apply (rule finite_deflation.intro)
ballarin@28611
   281
    apply (rule deflation_p_d_e)
ballarin@28611
   282
     apply (rule `finite_deflation d` [THEN finite_deflation.axioms(1)])
ballarin@28611
   283
    apply (rule d)
ballarin@28611
   284
   apply (rule finite_deflation_axioms.intro)
ballarin@28611
   285
   apply (rule finite_range_imp_finite_fixes)
ballarin@28611
   286
   apply (simp add: range_composition [where f="\<lambda>x. p\<cdot>x"])
ballarin@28611
   287
   apply (simp add: range_composition [where f="\<lambda>x. d\<cdot>x"])
ballarin@28611
   288
   apply (simp add: d.finite_image)
ballarin@28611
   289
  done
ballarin@28611
   290
qed
huffman@27401
   291
huffman@27401
   292
end
huffman@27401
   293
huffman@27401
   294
subsection {* Uniqueness of ep-pairs *}
huffman@27401
   295
huffman@27401
   296
lemma ep_pair_unique_e:
huffman@27401
   297
  "\<lbrakk>ep_pair e1 p; ep_pair e2 p\<rbrakk> \<Longrightarrow> e1 = e2"
huffman@27401
   298
 apply (rule ext_cfun)
huffman@27401
   299
 apply (rule antisym_less)
huffman@27401
   300
  apply (subgoal_tac "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x")
huffman@27401
   301
   apply (simp add: ep_pair.e_inverse)
huffman@27401
   302
  apply (erule ep_pair.e_p_less)
huffman@27401
   303
 apply (subgoal_tac "e2\<cdot>(p\<cdot>(e1\<cdot>x)) \<sqsubseteq> e1\<cdot>x")
huffman@27401
   304
  apply (simp add: ep_pair.e_inverse)
huffman@27401
   305
 apply (erule ep_pair.e_p_less)
huffman@27401
   306
done
huffman@27401
   307
huffman@27401
   308
lemma ep_pair_unique_p:
huffman@27401
   309
  "\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
huffman@27401
   310
 apply (rule ext_cfun)
huffman@27401
   311
 apply (rule antisym_less)
huffman@27401
   312
  apply (subgoal_tac "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x")
huffman@27401
   313
   apply (simp add: ep_pair.e_inverse)
huffman@27401
   314
  apply (rule monofun_cfun_arg)
huffman@27401
   315
  apply (erule ep_pair.e_p_less)
huffman@27401
   316
 apply (subgoal_tac "p1\<cdot>(e\<cdot>(p2\<cdot>x)) \<sqsubseteq> p1\<cdot>x")
huffman@27401
   317
  apply (simp add: ep_pair.e_inverse)
huffman@27401
   318
 apply (rule monofun_cfun_arg)
huffman@27401
   319
 apply (erule ep_pair.e_p_less)
huffman@27401
   320
done
huffman@27401
   321
huffman@27401
   322
subsection {* Composing ep-pairs *}
huffman@27401
   323
huffman@27401
   324
lemma ep_pair_ID_ID: "ep_pair ID ID"
huffman@27401
   325
by default simp_all
huffman@27401
   326
huffman@27401
   327
lemma ep_pair_comp:
huffman@27401
   328
  "\<lbrakk>ep_pair e1 p1; ep_pair e2 p2\<rbrakk>
huffman@27401
   329
    \<Longrightarrow> ep_pair (e2 oo e1) (p1 oo p2)"
huffman@27401
   330
 apply (rule ep_pair.intro)
huffman@27401
   331
  apply (simp add: ep_pair.e_inverse)
huffman@27401
   332
 apply (simp, rule trans_less)
huffman@27401
   333
  apply (rule monofun_cfun_arg)
huffman@27401
   334
  apply (erule ep_pair.e_p_less)
huffman@27401
   335
 apply (erule ep_pair.e_p_less)
huffman@27401
   336
done
huffman@27401
   337
haftmann@27681
   338
locale pcpo_ep_pair = ep_pair +
huffman@27401
   339
  constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
huffman@27401
   340
  constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
huffman@27401
   341
begin
huffman@27401
   342
huffman@27401
   343
lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
huffman@27401
   344
proof -
huffman@27401
   345
  have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal)
huffman@27401
   346
  hence "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
huffman@27401
   347
  also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_less)
huffman@27401
   348
  finally show "e\<cdot>\<bottom> = \<bottom>" by simp
huffman@27401
   349
qed
huffman@27401
   350
huffman@27401
   351
lemma e_defined_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
huffman@27401
   352
by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
huffman@27401
   353
huffman@27401
   354
lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
huffman@27401
   355
by simp
huffman@27401
   356
huffman@27401
   357
lemma p_strict [simp]: "p\<cdot>\<bottom> = \<bottom>"
huffman@27401
   358
by (rule e_inverse [where x="\<bottom>", unfolded e_strict])
huffman@27401
   359
huffman@27401
   360
lemmas stricts = e_strict p_strict
huffman@27401
   361
huffman@27401
   362
end
huffman@27401
   363
huffman@27401
   364
end