author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46868  6c250adbe101 
child 58880  0baae4311a9f 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Deflation.thy 
27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

2 
Author: Brian Huffman 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

3 
*) 
4edc81f93e35
New theory of deflations and embeddingprojection 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 eppairs *} 
27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

6 

4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

9 
begin 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

10 

36452  11 
default_sort cpo 
27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

12 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

13 
subsection {* Continuous deflations *} 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

14 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

15 
locale deflation = 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

16 
fixes d :: "'a \<rightarrow> 'a" 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

19 
begin 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

23 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

24 
text {* The set of fixed points is the same as the range. *} 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

25 

4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

27 
by (auto simp add: eq_sym_conv idem) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

28 

4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

30 
by (auto simp add: eq_sym_conv idem) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

31 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

32 
text {* 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

33 
The pointwise ordering on deflation functions coincides with 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

34 
the subset ordering of their sets of fixedpoints. 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

35 
*} 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection 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 embeddingprojection 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 embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

43 
finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" . 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

44 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

49 
next 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

50 
assume "f \<sqsubseteq> d" 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

52 
also assume "f\<cdot>x = x" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

53 
finally show "x \<sqsubseteq> d\<cdot>x" . 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

54 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

55 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

56 
end 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

57 

33503  58 
lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>" 
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41182
diff
changeset

59 
by (rule deflation.below [THEN bottomI]) 
33503  60 

27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

61 
lemma adm_deflation: "adm (\<lambda>d. deflation d)" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

62 
by (simp add: deflation_def) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

63 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

64 
lemma deflation_ID: "deflation ID" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

65 
by (simp add: deflation.intro) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

66 

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41182
diff
changeset

67 
lemma deflation_bottom: "deflation \<bottom>" 
27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

68 
by (simp add: deflation.intro) 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection 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 embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

75 
done 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

76 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

77 
text {* 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

78 
The composition of two deflations is equal to 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

79 
the lesser of the two (if they are comparable). 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

80 
*} 
4edc81f93e35
New theory of deflations and embeddingprojection 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  83 
assumes "deflation f" 
84 
assumes "deflation g" 

27401
4edc81f93e35
New theory of deflations and embeddingprojection 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  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 embeddingprojection pairs
huffman
parents:
diff
changeset

89 
next 
29237  90 
interpret f: deflation f by fact 
27401
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection 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 embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

94 
finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" . 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

95 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

100 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

101 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

102 
subsection {* Deflations with finite range *} 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

103 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

104 
lemma finite_range_imp_finite_fixes: 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

105 
"finite (range f) \<Longrightarrow> finite {x. f x = x}" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

106 
proof  
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

107 
have "{x. f x = x} \<subseteq> range f" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

108 
by (clarify, erule subst, rule rangeI) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

109 
moreover assume "finite (range f)" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

110 
ultimately show "finite {x. f x = x}" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

111 
by (rule finite_subset) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

112 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

113 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

114 
locale finite_deflation = deflation + 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

115 
assumes finite_fixes: "finite {x. d\<cdot>x = x}" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

116 
begin 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

117 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

118 
lemma finite_range: "finite (range (\<lambda>x. d\<cdot>x))" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

119 
by (simp add: range_eq_fixes finite_fixes) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

120 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

121 
lemma finite_image: "finite ((\<lambda>x. d\<cdot>x) ` A)" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

122 
by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range]) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

123 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

124 
lemma compact: "compact (d\<cdot>x)" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

125 
proof (rule compactI2) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

126 
fix Y :: "nat \<Rightarrow> 'a" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

127 
assume Y: "chain Y" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

128 
have "finite_chain (\<lambda>i. d\<cdot>(Y i))" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

129 
proof (rule finite_range_imp_finch) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

130 
show "chain (\<lambda>i. d\<cdot>(Y i))" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

131 
using Y by simp 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

133 
by clarsimp 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

134 
thus "finite (range (\<lambda>i. d\<cdot>(Y i)))" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

135 
using finite_range by (rule finite_subset) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

136 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

138 
by (simp add: finite_chain_def maxinch_is_thelub Y) 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

140 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

141 
assume "d\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)" 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

143 
by (rule monofun_cfun_arg) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

144 
hence "d\<cdot>x \<sqsubseteq> (\<Squnion>i. d\<cdot>(Y i))" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

145 
by (simp add: contlub_cfun_arg Y idem) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

146 
hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

147 
using j by simp 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

150 
thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" .. 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

151 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

152 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

153 
end 
4edc81f93e35
New theory of deflations and embeddingprojection 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 

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41182
diff
changeset

163 
lemma finite_deflation_bottom: "finite_deflation \<bottom>" 
39971
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 embeddingprojection pairs
huffman
parents:
diff
changeset

166 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

167 
subsection {* Continuous embeddingprojection pairs *} 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

168 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

169 
locale ep_pair = 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

170 
fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a" 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

173 
begin 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

176 
proof 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

177 
assume "e\<cdot>x \<sqsubseteq> e\<cdot>y" 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

179 
thus "x \<sqsubseteq> y" by simp 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

180 
next 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

181 
assume "x \<sqsubseteq> y" 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

183 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

184 

4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

187 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

188 
lemma p_eq_iff: 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

190 
by (safe, erule subst, erule subst, simp) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

191 

4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

193 
by (auto, rule exI, erule sym) 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

196 
proof 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

197 
assume "e\<cdot>x \<sqsubseteq> y" 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

199 
then show "x \<sqsubseteq> p\<cdot>y" by simp 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

200 
next 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

201 
assume "x \<sqsubseteq> p\<cdot>y" 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

204 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

205 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

206 
lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

207 
proof  
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

208 
assume "compact (e\<cdot>x)" 
41182  209 
hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (rule compactD) 
210 
hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2]) 

211 
hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by simp 

27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

212 
thus "compact x" by (rule compactI) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

213 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

214 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

215 
lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

216 
proof  
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

217 
assume "compact x" 
41182  218 
hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by (rule compactD) 
219 
hence "adm (\<lambda>y. x \<notsqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2]) 

220 
hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (simp add: e_below_iff_below_p) 

27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

221 
thus "compact (e\<cdot>x)" by (rule compactI) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

222 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

223 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

224 
lemma compact_e_iff: "compact (e\<cdot>x) \<longleftrightarrow> compact x" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

225 
by (rule iffI [OF compact_e_rev compact_e]) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

226 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

227 
text {* Deflations from eppairs *} 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

228 

4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

231 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

232 
lemma deflation_e_d_p: 
28611  233 
assumes "deflation d" 
27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

234 
shows "deflation (e oo d oo p)" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

235 
proof 
29237  236 
interpret deflation d by fact 
27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

237 
fix x :: 'b 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

239 
by (simp add: idem) 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

242 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

243 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

244 
lemma finite_deflation_e_d_p: 
28611  245 
assumes "finite_deflation d" 
27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

246 
shows "finite_deflation (e oo d oo p)" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

247 
proof 
29237  248 
interpret finite_deflation d by fact 
27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

249 
fix x :: 'b 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

251 
by (simp add: idem) 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

255 
by (simp add: finite_image) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

256 
hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

257 
by (simp add: image_image) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

258 
thus "finite {x. (e oo d oo p)\<cdot>x = x}" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

259 
by (rule finite_range_imp_finite_fixes) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

260 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

261 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

262 
lemma deflation_p_d_e: 
28611  263 
assumes "deflation d" 
27401
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

265 
shows "deflation (p oo d oo e)" 
28611  266 
proof  
29237  267 
interpret d: deflation d by fact 
28613  268 
{ 
269 
fix x 

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  272 
hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)" 
273 
by (rule monofun_cfun_arg) 

274 
hence "(p oo d oo e)\<cdot>x \<sqsubseteq> x" 

275 
by simp 

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  278 
show ?thesis 
28613  279 
proof 
280 
fix x 

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  283 
next 
284 
fix x 

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  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  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)))))" 
290 
by (intro monofun_cfun_arg d) 

291 
hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))" 

292 
by (simp only: d.idem) 

293 
thus "(p oo d oo e)\<cdot>x \<sqsubseteq> (p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x)" 

294 
by simp 

295 
qed 

296 
qed 

28611  297 
qed 
27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

298 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

299 
lemma finite_deflation_p_d_e: 
28611  300 
assumes "finite_deflation d" 
27401
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

302 
shows "finite_deflation (p oo d oo e)" 
28611  303 
proof  
29237  304 
interpret d: finite_deflation d by fact 
28611  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  307 
have "deflation d" .. 
308 
thus "deflation (p oo d oo e)" 

309 
using d by (rule deflation_p_d_e) 

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  319 
qed 
28611  320 
qed 
27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

321 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

322 
end 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

323 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

324 
subsection {* Uniqueness of eppairs *} 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

325 

28613  326 
lemma ep_pair_unique_e_lemma: 
35168  327 
assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p" 
28613  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  330 
fix x 
331 
have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x" 

35168  332 
by (rule ep_pair.e_p_below [OF 1]) 
28613  333 
thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x" 
35168  334 
by (simp only: ep_pair.e_inverse [OF 2]) 
28613  335 
qed 
336 

27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

337 
lemma ep_pair_unique_e: 
4edc81f93e35
New theory of deflations and embeddingprojection 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  340 

341 
lemma ep_pair_unique_p_lemma: 

35168  342 
assumes 1: "ep_pair e p1" and 2: "ep_pair e p2" 
28613  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  345 
fix x 
346 
have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x" 

35168  347 
by (rule ep_pair.e_p_below [OF 1]) 
28613  348 
hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x" 
349 
by (rule monofun_cfun_arg) 

350 
thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x" 

35168  351 
by (simp only: ep_pair.e_inverse [OF 2]) 
28613  352 
qed 
27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

353 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

354 
lemma ep_pair_unique_p: 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

357 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

358 
subsection {* Composing eppairs *} 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

359 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

360 
lemma ep_pair_ID_ID: "ep_pair ID ID" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

361 
by default simp_all 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

362 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

363 
lemma ep_pair_comp: 
28613  364 
assumes "ep_pair e1 p1" and "ep_pair e2 p2" 
365 
shows "ep_pair (e2 oo e1) (p1 oo p2)" 

366 
proof 

29237  367 
interpret ep1: ep_pair e1 p1 by fact 
368 
interpret ep2: ep_pair e2 p2 by fact 

28613  369 
fix x y 
370 
show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x" 

371 
by simp 

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  374 
hence "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)" 
375 
by (rule monofun_cfun_arg) 

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  378 
finally show "(e2 oo e1)\<cdot>((p1 oo p2)\<cdot>y) \<sqsubseteq> y" 
379 
by simp 

380 
qed 

27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

381 

46868  382 
locale pcpo_ep_pair = ep_pair e p 
383 
for e :: "'a::pcpo \<rightarrow> 'b::pcpo" 

384 
and p :: "'b::pcpo \<rightarrow> 'a::pcpo" 

27401
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

385 
begin 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

386 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

387 
lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

388 
proof  
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

389 
have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal) 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

392 
finally show "e\<cdot>\<bottom> = \<bottom>" by simp 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

393 
qed 
4edc81f93e35
New theory of deflations and embeddingprojection 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 embeddingprojection pairs
huffman
parents:
diff
changeset

396 
by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict]) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

397 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

398 
lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

399 
by simp 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

400 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

401 
lemma p_strict [simp]: "p\<cdot>\<bottom> = \<bottom>" 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

402 
by (rule e_inverse [where x="\<bottom>", unfolded e_strict]) 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

403 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

404 
lemmas stricts = e_strict p_strict 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

405 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

406 
end 
4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

407 

4edc81f93e35
New theory of deflations and embeddingprojection pairs
huffman
parents:
diff
changeset

408 
end 