src/HOLCF/Deflation.thy
author huffman
Wed, 10 Nov 2010 17:56:08 -0800
changeset 40502 8e92772bc0e8
parent 40327 1dfdbd66093a
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/Deflation.thy
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
     3
*)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
     4
35901
12f09bf2c77f fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents: 35794
diff changeset
     5
header {* Continuous deflations and ep-pairs *}
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
     6
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
     7
theory Deflation
40502
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents: 40327
diff changeset
     8
imports Plain_HOLCF
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
     9
begin
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    10
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 35901
diff changeset
    11
default_sort cpo
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    12
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    13
subsection {* Continuous deflations *}
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    14
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    15
locale deflation =
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    16
  fixes d :: "'a \<rightarrow> 'a"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    17
  assumes idem: "\<And>x. d\<cdot>(d\<cdot>x) = d\<cdot>x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    18
  assumes below: "\<And>x. d\<cdot>x \<sqsubseteq> x"
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    19
begin
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    20
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    21
lemma below_ID: "d \<sqsubseteq> ID"
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39985
diff changeset
    22
by (rule cfun_belowI, simp add: below)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    23
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    24
text {* The set of fixed points is the same as the range. *}
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    25
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    26
lemma fixes_eq_range: "{x. d\<cdot>x = x} = range (\<lambda>x. d\<cdot>x)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    27
by (auto simp add: eq_sym_conv idem)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    28
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    29
lemma range_eq_fixes: "range (\<lambda>x. d\<cdot>x) = {x. d\<cdot>x = x}"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    30
by (auto simp add: eq_sym_conv idem)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    31
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    32
text {*
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    33
  The pointwise ordering on deflation functions coincides with
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    34
  the subset ordering of their sets of fixed-points.
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    35
*}
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    36
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    37
lemma belowI:
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    38
  assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39985
diff changeset
    39
proof (rule cfun_belowI)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    40
  fix x
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    41
  from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    42
  also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    43
  finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" .
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    44
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    45
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    46
lemma belowD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    47
proof (rule below_antisym)
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    48
  from below show "d\<cdot>x \<sqsubseteq> x" .
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    49
next
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    50
  assume "f \<sqsubseteq> d"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    51
  hence "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    52
  also assume "f\<cdot>x = x"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    53
  finally show "x \<sqsubseteq> d\<cdot>x" .
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    54
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    55
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    56
end
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    57
33503
3496616b2171 lemma deflation_strict
huffman
parents: 31076
diff changeset
    58
lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
3496616b2171 lemma deflation_strict
huffman
parents: 31076
diff changeset
    59
by (rule deflation.below [THEN UU_I])
3496616b2171 lemma deflation_strict
huffman
parents: 31076
diff changeset
    60
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    61
lemma adm_deflation: "adm (\<lambda>d. deflation d)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    62
by (simp add: deflation_def)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    63
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    64
lemma deflation_ID: "deflation ID"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    65
by (simp add: deflation.intro)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    66
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    67
lemma deflation_UU: "deflation \<bottom>"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    68
by (simp add: deflation.intro)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    69
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    70
lemma deflation_below_iff:
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    71
  "\<lbrakk>deflation p; deflation q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    72
 apply safe
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    73
  apply (simp add: deflation.belowD)
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    74
 apply (simp add: deflation.belowI)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    75
done
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    76
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    77
text {*
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    78
  The composition of two deflations is equal to
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    79
  the lesser of the two (if they are comparable).
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    80
*}
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    81
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    82
lemma deflation_below_comp1:
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
    83
  assumes "deflation f"
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
    84
  assumes "deflation g"
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    85
  shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    86
proof (rule below_antisym)
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28613
diff changeset
    87
  interpret g: deflation g by fact
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    88
  from g.below show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    89
next
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28613
diff changeset
    90
  interpret f: deflation f by fact
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    91
  assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    92
  hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    93
  also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    94
  finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" .
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    95
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    96
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    97
lemma deflation_below_comp2:
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
    98
  "\<lbrakk>deflation f; deflation g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
    99
by (simp only: deflation.belowD deflation.idem)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   100
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   101
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   102
subsection {* Deflations with finite range *}
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   103
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   104
lemma finite_range_imp_finite_fixes:
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   105
  "finite (range f) \<Longrightarrow> finite {x. f x = x}"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   106
proof -
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   107
  have "{x. f x = x} \<subseteq> range f"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   108
    by (clarify, erule subst, rule rangeI)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   109
  moreover assume "finite (range f)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   110
  ultimately show "finite {x. f x = x}"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   111
    by (rule finite_subset)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   112
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   113
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   114
locale finite_deflation = deflation +
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   115
  assumes finite_fixes: "finite {x. d\<cdot>x = x}"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   116
begin
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   117
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   118
lemma finite_range: "finite (range (\<lambda>x. d\<cdot>x))"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   119
by (simp add: range_eq_fixes finite_fixes)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   120
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   121
lemma finite_image: "finite ((\<lambda>x. d\<cdot>x) ` A)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   122
by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   123
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   124
lemma compact: "compact (d\<cdot>x)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   125
proof (rule compactI2)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   126
  fix Y :: "nat \<Rightarrow> 'a"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   127
  assume Y: "chain Y"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   128
  have "finite_chain (\<lambda>i. d\<cdot>(Y i))"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   129
  proof (rule finite_range_imp_finch)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   130
    show "chain (\<lambda>i. d\<cdot>(Y i))"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   131
      using Y by simp
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   132
    have "range (\<lambda>i. d\<cdot>(Y i)) \<subseteq> range (\<lambda>x. d\<cdot>x)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   133
      by clarsimp
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   134
    thus "finite (range (\<lambda>i. d\<cdot>(Y i)))"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   135
      using finite_range by (rule finite_subset)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   136
  qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   137
  hence "\<exists>j. (\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   138
    by (simp add: finite_chain_def maxinch_is_thelub Y)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   139
  then obtain j where j: "(\<Squnion>i. d\<cdot>(Y i)) = d\<cdot>(Y j)" ..
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   140
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   141
  assume "d\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   142
  hence "d\<cdot>(d\<cdot>x) \<sqsubseteq> d\<cdot>(\<Squnion>i. Y i)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   143
    by (rule monofun_cfun_arg)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   144
  hence "d\<cdot>x \<sqsubseteq> (\<Squnion>i. d\<cdot>(Y i))"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   145
    by (simp add: contlub_cfun_arg Y idem)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   146
  hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   147
    using j by simp
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   148
  hence "d\<cdot>x \<sqsubseteq> Y j"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   149
    using below by (rule below_trans)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   150
  thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   151
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   152
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   153
end
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   154
39973
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   155
lemma finite_deflation_intro:
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   156
  "deflation d \<Longrightarrow> finite {x. d\<cdot>x = x} \<Longrightarrow> finite_deflation d"
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   157
by (intro finite_deflation.intro finite_deflation_axioms.intro)
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   158
39971
2949af5e6b9c move lemmas to Deflation.thy
Brian Huffman <brianh@cs.pdx.edu>
parents: 36452
diff changeset
   159
lemma finite_deflation_imp_deflation:
2949af5e6b9c move lemmas to Deflation.thy
Brian Huffman <brianh@cs.pdx.edu>
parents: 36452
diff changeset
   160
  "finite_deflation d \<Longrightarrow> deflation d"
2949af5e6b9c move lemmas to Deflation.thy
Brian Huffman <brianh@cs.pdx.edu>
parents: 36452
diff changeset
   161
unfolding finite_deflation_def by simp
2949af5e6b9c move lemmas to Deflation.thy
Brian Huffman <brianh@cs.pdx.edu>
parents: 36452
diff changeset
   162
2949af5e6b9c move lemmas to Deflation.thy
Brian Huffman <brianh@cs.pdx.edu>
parents: 36452
diff changeset
   163
lemma finite_deflation_UU: "finite_deflation \<bottom>"
2949af5e6b9c move lemmas to Deflation.thy
Brian Huffman <brianh@cs.pdx.edu>
parents: 36452
diff changeset
   164
by default simp_all
2949af5e6b9c move lemmas to Deflation.thy
Brian Huffman <brianh@cs.pdx.edu>
parents: 36452
diff changeset
   165
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   166
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   167
subsection {* Continuous embedding-projection pairs *}
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   168
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   169
locale ep_pair =
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   170
  fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   171
  assumes e_inverse [simp]: "\<And>x. p\<cdot>(e\<cdot>x) = x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   172
  and e_p_below: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   173
begin
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   174
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   175
lemma e_below_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   176
proof
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   177
  assume "e\<cdot>x \<sqsubseteq> e\<cdot>y"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   178
  hence "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   179
  thus "x \<sqsubseteq> y" by simp
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   180
next
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   181
  assume "x \<sqsubseteq> y"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   182
  thus "e\<cdot>x \<sqsubseteq> e\<cdot>y" by (rule monofun_cfun_arg)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   183
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   184
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   185
lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   186
unfolding po_eq_conv e_below_iff ..
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   187
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   188
lemma p_eq_iff:
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   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"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   190
by (safe, erule subst, erule subst, simp)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   191
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   192
lemma p_inverse: "(\<exists>x. y = e\<cdot>x) = (e\<cdot>(p\<cdot>y) = y)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   193
by (auto, rule exI, erule sym)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   194
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   195
lemma e_below_iff_below_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   196
proof
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   197
  assume "e\<cdot>x \<sqsubseteq> y"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   198
  then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>y" by (rule monofun_cfun_arg)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   199
  then show "x \<sqsubseteq> p\<cdot>y" by simp
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   200
next
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   201
  assume "x \<sqsubseteq> p\<cdot>y"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   202
  then have "e\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>y)" by (rule monofun_cfun_arg)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   203
  then show "e\<cdot>x \<sqsubseteq> y" using e_p_below by (rule below_trans)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   204
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   205
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   206
lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   207
proof -
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   208
  assume "compact (e\<cdot>x)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   209
  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
40327
1dfdbd66093a renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
huffman
parents: 40321
diff changeset
   210
  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   211
  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   212
  thus "compact x" by (rule compactI)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   213
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   214
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   215
lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   216
proof -
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   217
  assume "compact x"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   218
  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
40327
1dfdbd66093a renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
huffman
parents: 40321
diff changeset
   219
  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   220
  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   221
  thus "compact (e\<cdot>x)" by (rule compactI)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   222
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   223
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   224
lemma compact_e_iff: "compact (e\<cdot>x) \<longleftrightarrow> compact x"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   225
by (rule iffI [OF compact_e_rev compact_e])
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   226
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   227
text {* Deflations from ep-pairs *}
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   228
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   229
lemma deflation_e_p: "deflation (e oo p)"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   230
by (simp add: deflation.intro e_p_below)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   231
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   232
lemma deflation_e_d_p:
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
   233
  assumes "deflation d"
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   234
  shows "deflation (e oo d oo p)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   235
proof
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28613
diff changeset
   236
  interpret deflation d by fact
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   237
  fix x :: 'b
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   238
  show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   239
    by (simp add: idem)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   240
  show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   241
    by (simp add: e_below_iff_below_p below)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   242
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   243
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   244
lemma finite_deflation_e_d_p:
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
   245
  assumes "finite_deflation d"
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   246
  shows "finite_deflation (e oo d oo p)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   247
proof
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28613
diff changeset
   248
  interpret finite_deflation d by fact
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   249
  fix x :: 'b
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   250
  show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   251
    by (simp add: idem)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   252
  show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   253
    by (simp add: e_below_iff_below_p below)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   254
  have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   255
    by (simp add: finite_image)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   256
  hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   257
    by (simp add: image_image)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   258
  thus "finite {x. (e oo d oo p)\<cdot>x = x}"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   259
    by (rule finite_range_imp_finite_fixes)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   260
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   261
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   262
lemma deflation_p_d_e:
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
   263
  assumes "deflation d"
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   264
  assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   265
  shows "deflation (p oo d oo e)"
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
   266
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28613
diff changeset
   267
  interpret d: deflation d by fact
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   268
  {
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   269
    fix x
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   270
    have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   271
      by (rule d.below)
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   272
    hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   273
      by (rule monofun_cfun_arg)
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   274
    hence "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   275
      by simp
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   276
  }
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   277
  note p_d_e_below = this
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
   278
  show ?thesis
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   279
  proof
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   280
    fix x
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   281
    show "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   282
      by (rule p_d_e_below)
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   283
  next
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   284
    fix x
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   285
    show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   286
    proof (rule below_antisym)
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   287
      show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) \<sqsubseteq> (p oo d oo e)\<cdot>x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   288
        by (rule p_d_e_below)
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   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)))))"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   290
        by (intro monofun_cfun_arg d)
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   291
      hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   292
        by (simp only: d.idem)
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   293
      thus "(p oo d oo e)\<cdot>x \<sqsubseteq> (p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x)"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   294
        by simp
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   295
    qed
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   296
  qed
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
   297
qed
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   298
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   299
lemma finite_deflation_p_d_e:
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
   300
  assumes "finite_deflation d"
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   301
  assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   302
  shows "finite_deflation (p oo d oo e)"
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
   303
proof -
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28613
diff changeset
   304
  interpret d: finite_deflation d by fact
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
   305
  show ?thesis
39973
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   306
  proof (rule finite_deflation_intro)
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   307
    have "deflation d" ..
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   308
    thus "deflation (p oo d oo e)"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   309
      using d by (rule deflation_p_d_e)
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   310
  next
39973
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   311
    have "finite ((\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   312
      by (rule d.finite_image)
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   313
    hence "finite ((\<lambda>x. p\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. e\<cdot>x))"
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   314
      by (rule finite_imageI)
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   315
    hence "finite (range (\<lambda>x. (p oo d oo e)\<cdot>x))"
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   316
      by (simp add: image_image)
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   317
    thus "finite {x. (p oo d oo e)\<cdot>x = x}"
c62b4ff97bfc add lemma finite_deflation_intro
Brian Huffman <brianh@cs.pdx.edu>
parents: 39971
diff changeset
   318
      by (rule finite_range_imp_finite_fixes)
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   319
  qed
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27681
diff changeset
   320
qed
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   321
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   322
end
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   323
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   324
subsection {* Uniqueness of ep-pairs *}
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   325
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   326
lemma ep_pair_unique_e_lemma:
35168
07b3112e464b fix warnings about duplicate simp rules
huffman
parents: 33503
diff changeset
   327
  assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   328
  shows "e1 \<sqsubseteq> e2"
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39985
diff changeset
   329
proof (rule cfun_belowI)
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   330
  fix x
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   331
  have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
35168
07b3112e464b fix warnings about duplicate simp rules
huffman
parents: 33503
diff changeset
   332
    by (rule ep_pair.e_p_below [OF 1])
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   333
  thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
35168
07b3112e464b fix warnings about duplicate simp rules
huffman
parents: 33503
diff changeset
   334
    by (simp only: ep_pair.e_inverse [OF 2])
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   335
qed
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   336
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   337
lemma ep_pair_unique_e:
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   338
  "\<lbrakk>ep_pair e1 p; ep_pair e2 p\<rbrakk> \<Longrightarrow> e1 = e2"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   339
by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   340
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   341
lemma ep_pair_unique_p_lemma:
35168
07b3112e464b fix warnings about duplicate simp rules
huffman
parents: 33503
diff changeset
   342
  assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   343
  shows "p1 \<sqsubseteq> p2"
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39985
diff changeset
   344
proof (rule cfun_belowI)
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   345
  fix x
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   346
  have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
35168
07b3112e464b fix warnings about duplicate simp rules
huffman
parents: 33503
diff changeset
   347
    by (rule ep_pair.e_p_below [OF 1])
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   348
  hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   349
    by (rule monofun_cfun_arg)
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   350
  thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
35168
07b3112e464b fix warnings about duplicate simp rules
huffman
parents: 33503
diff changeset
   351
    by (simp only: ep_pair.e_inverse [OF 2])
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   352
qed
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   353
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   354
lemma ep_pair_unique_p:
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   355
  "\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   356
by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   357
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   358
subsection {* Composing ep-pairs *}
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   359
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   360
lemma ep_pair_ID_ID: "ep_pair ID ID"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   361
by default simp_all
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   362
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   363
lemma ep_pair_comp:
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   364
  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   365
  shows "ep_pair (e2 oo e1) (p1 oo p2)"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   366
proof
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28613
diff changeset
   367
  interpret ep1: ep_pair e1 p1 by fact
e90d9d51106b More porting to new locales.
ballarin
parents: 28613
diff changeset
   368
  interpret ep2: ep_pair e2 p2 by fact
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   369
  fix x y
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   370
  show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   371
    by simp
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   372
  have "e1\<cdot>(p1\<cdot>(p2\<cdot>y)) \<sqsubseteq> p2\<cdot>y"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   373
    by (rule ep1.e_p_below)
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   374
  hence "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   375
    by (rule monofun_cfun_arg)
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   376
  also have "e2\<cdot>(p2\<cdot>y) \<sqsubseteq> y"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   377
    by (rule ep2.e_p_below)
28613
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   378
  finally show "(e2 oo e1)\<cdot>((p1 oo p2)\<cdot>y) \<sqsubseteq> y"
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   379
    by simp
15a41d3fa959 rewrite more proofs in Isar style
huffman
parents: 28611
diff changeset
   380
qed
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   381
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27401
diff changeset
   382
locale pcpo_ep_pair = ep_pair +
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   383
  constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   384
  constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   385
begin
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   386
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   387
lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   388
proof -
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   389
  have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal)
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   390
  hence "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29252
diff changeset
   391
  also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_below)
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   392
  finally show "e\<cdot>\<bottom> = \<bottom>" by simp
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   393
qed
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   394
40321
d065b195ec89 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents: 40002
diff changeset
   395
lemma e_bottom_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
27401
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   396
by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   397
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   398
lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   399
by simp
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   400
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   401
lemma p_strict [simp]: "p\<cdot>\<bottom> = \<bottom>"
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   402
by (rule e_inverse [where x="\<bottom>", unfolded e_strict])
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   403
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   404
lemmas stricts = e_strict p_strict
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   405
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   406
end
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   407
4edc81f93e35 New theory of deflations and embedding-projection pairs
huffman
parents:
diff changeset
   408
end