author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46008  c296c75f4cf4 
child 56020  f92479477c52 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/FOCUS/Stream_adm.thy 
17293  2 
Author: David von Oheimb, TU Muenchen 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

3 
*) 
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

4 

17293  5 
header {* Admissibility for streams *} 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

6 

17293  7 
theory Stream_adm 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40774
diff
changeset

8 
imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Continuity" 
17293  9 
begin 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

10 

19763  11 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

12 
stream_monoP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where 
43924  13 
"stream_monoP F = (\<exists>Q i. \<forall>P s. enat i \<le> #s \<longrightarrow> 
19763  14 
(s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P))" 
17293  15 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

16 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

17 
stream_antiP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where 
19763  18 
"stream_antiP F = (\<forall>P x. \<exists>Q i. 
43924  19 
(#x < enat i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and> 
20 
(enat i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> 

19763  21 
(y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P))))" 
17293  22 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

23 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

24 
antitonP :: "'a set => bool" where 
19763  25 
"antitonP P = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P)" 
17293  26 

27 

19759  28 
(*  *) 
29 

30 
section "admissibility" 

31 

40430
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

32 
lemma infinite_chain_adm_lemma: 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

33 
"\<lbrakk>Porder.chain Y; \<forall>i. P (Y i); 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

34 
\<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk> 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

35 
\<Longrightarrow> P (\<Squnion>i. Y i)" 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

36 
apply (case_tac "finite_chain Y") 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

37 
prefer 2 apply fast 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

38 
apply (unfold finite_chain_def) 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

39 
apply safe 
40771  40 
apply (erule lub_finch1 [THEN lub_eqI, THEN ssubst]) 
40430
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

41 
apply assumption 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

42 
apply (erule spec) 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

43 
done 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

44 

483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

45 
lemma increasing_chain_adm_lemma: 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

46 
"\<lbrakk>Porder.chain Y; \<forall>i. P (Y i); \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i); 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

47 
\<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk> 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

48 
\<Longrightarrow> P (\<Squnion>i. Y i)" 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

49 
apply (erule infinite_chain_adm_lemma) 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

50 
apply assumption 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

51 
apply (erule thin_rl) 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

52 
apply (unfold finite_chain_def) 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

53 
apply (unfold max_in_chain_def) 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

54 
apply (fast dest: le_imp_less_or_eq elim: chain_mono_less) 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

55 
done 
483a4876e428
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman
parents:
37110
diff
changeset

56 

19759  57 
lemma flatstream_adm_lemma: 
26451
f8a615f3bb31
avoid amiguity of Continuity.chain vs. Porder.chain;
wenzelm
parents:
26102
diff
changeset

58 
assumes 1: "Porder.chain Y" 
19759  59 
assumes 2: "!i. P (Y i)" 
43924  60 
assumes 3: "(!!Y. [ Porder.chain Y; !i. P (Y i); !k. ? j. enat k < #((Y j)::'a::flat stream)] 
27413  61 
==> P(LUB i. Y i))" 
62 
shows "P(LUB i. Y i)" 

46008
c296c75f4cf4
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
wenzelm
parents:
44019
diff
changeset

63 
apply (rule increasing_chain_adm_lemma [OF 1 2]) 
19759  64 
apply (erule 3, assumption) 
65 
apply (erule thin_rl) 

66 
apply (rule allI) 

67 
apply (case_tac "!j. stream_finite (Y j)") 

68 
apply ( rule chain_incr) 

69 
apply ( rule allI) 

70 
apply ( drule spec) 

71 
apply ( safe) 

72 
apply ( rule exI) 

73 
apply ( rule slen_strict_mono) 

74 
apply ( erule spec) 

75 
apply ( assumption) 

76 
apply ( assumption) 

43919  77 
apply (metis enat_ord_code(4) slen_infinite) 
19759  78 
done 
79 

80 
(* should be without reference to stream length? *) 

26451
f8a615f3bb31
avoid amiguity of Continuity.chain vs. Porder.chain;
wenzelm
parents:
26102
diff
changeset

81 
lemma flatstream_admI: "[(!!Y. [ Porder.chain Y; !i. P (Y i); 
43924  82 
!k. ? j. enat k < #((Y j)::'a::flat stream)] ==> P(LUB i. Y i))]==> adm P" 
19759  83 
apply (unfold adm_def) 
84 
apply (intro strip) 

85 
apply (erule (1) flatstream_adm_lemma) 

86 
apply (fast) 

87 
done 

88 

89 

43921  90 
(* context (theory "Extended_Nat");*) 
43924  91 
lemma ile_lemma: "enat (i + j) <= x ==> enat i <= x" 
27101
864d29f11c9d
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
26838
diff
changeset

92 
by (rule order_trans) auto 
19759  93 

94 
lemma stream_monoP2I: 

95 
"!!X. stream_monoP F ==> !i. ? l. !x y. 

43924  96 
enat l <= #x > (x::'a::flat stream) << y > x:down_iterate F i > y:down_iterate F i" 
19759  97 
apply (unfold stream_monoP_def) 
98 
apply (safe) 

99 
apply (rule_tac x="i*ia" in exI) 

100 
apply (induct_tac "ia") 

101 
apply ( simp) 

102 
apply (simp) 

103 
apply (intro strip) 

104 
apply (erule allE, erule all_dupE, drule mp, erule ile_lemma) 

105 
apply (drule_tac P="%x. x" in subst, assumption) 

106 
apply (erule allE, drule mp, rule ile_lemma) back 

27101
864d29f11c9d
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
26838
diff
changeset

107 
apply ( erule order_trans) 
19759  108 
apply ( erule slen_mono) 
109 
apply (erule ssubst) 

110 
apply (safe) 

111 
apply ( erule (2) ile_lemma [THEN slen_take_lemma3, THEN subst]) 

112 
apply (erule allE) 

113 
apply (drule mp) 

114 
apply ( erule slen_rt_mult) 

115 
apply (erule allE) 

116 
apply (drule mp) 

117 
apply (erule monofun_rt_mult) 

118 
apply (drule (1) mp) 

119 
apply (assumption) 

120 
done 

121 

122 
lemma stream_monoP2_gfp_admI: "[ !i. ? l. !x y. 

43924  123 
enat l <= #x > (x::'a::flat stream) << y > x:down_iterate F i > y:down_iterate F i; 
19759  124 
down_cont F ] ==> adm (%x. x:gfp F)" 
125 
apply (erule INTER_down_iterate_is_gfp [THEN ssubst]) (* cont *) 

126 
apply (simp (no_asm)) 

127 
apply (rule adm_lemmas) 

128 
apply (rule flatstream_admI) 

129 
apply (erule allE) 

130 
apply (erule exE) 

131 
apply (erule allE, erule exE) 

132 
apply (erule allE, erule allE, drule mp) (* stream_monoP *) 

133 
apply ( drule ileI1) 

27101
864d29f11c9d
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
26838
diff
changeset

134 
apply ( drule order_trans) 
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43924
diff
changeset

135 
apply ( rule ile_eSuc) 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43924
diff
changeset

136 
apply ( drule eSuc_ile_mono [THEN iffD1]) 
19759  137 
apply ( assumption) 
138 
apply (drule mp) 

139 
apply ( erule is_ub_thelub) 

140 
apply (fast) 

141 
done 

142 

143 
lemmas fstream_gfp_admI = stream_monoP2I [THEN stream_monoP2_gfp_admI] 

144 

145 
lemma stream_antiP2I: 

146 
"!!X. [stream_antiP (F::(('a::flat stream)set => ('a stream set)))] 

147 
==> !i x y. x << y > y:down_iterate F i > x:down_iterate F i" 

148 
apply (unfold stream_antiP_def) 

149 
apply (rule allI) 

150 
apply (induct_tac "i") 

151 
apply ( simp) 

152 
apply (simp) 

153 
apply (intro strip) 

154 
apply (erule allE, erule all_dupE, erule exE, erule exE) 

155 
apply (erule conjE) 

43924  156 
apply (case_tac "#x < enat i") 
19759  157 
apply ( fast) 
26102  158 
apply (unfold linorder_not_less) 
19759  159 
apply (drule (1) mp) 
40431  160 
apply (erule all_dupE, drule mp, rule below_refl) 
19759  161 
apply (erule ssubst) 
162 
apply (erule allE, drule (1) mp) 

163 
apply (drule_tac P="%x. x" in subst, assumption) 

164 
apply (erule conjE, rule conjI) 

165 
apply ( erule slen_take_lemma3 [THEN ssubst], assumption) 

166 
apply ( assumption) 

167 
apply (erule allE, erule allE, drule mp, erule monofun_rt_mult) 

168 
apply (drule (1) mp) 

169 
apply (assumption) 

170 
done 

171 

172 
lemma stream_antiP2_non_gfp_admI: 

173 
"!!X. [!i x y. x << y > y:down_iterate F i > x:down_iterate F i; down_cont F ] 

174 
==> adm (%u. ~ u:gfp F)" 

175 
apply (unfold adm_def) 

176 
apply (simp add: INTER_down_iterate_is_gfp) 

177 
apply (fast dest!: is_ub_thelub) 

178 
done 

179 

180 
lemmas fstream_non_gfp_admI = stream_antiP2I [THEN stream_antiP2_non_gfp_admI] 

181 

182 

183 

184 
(**new approach for adm********************************************************) 

185 

186 
section "antitonP" 

187 

188 
lemma antitonPD: "[ antitonP P; y:P; x<<y ] ==> x:P" 

189 
apply (unfold antitonP_def) 

190 
apply auto 

191 
done 

192 

193 
lemma antitonPI: "!x y. y:P > x<<y > x:P ==> antitonP P" 

194 
apply (unfold antitonP_def) 

195 
apply (fast) 

196 
done 

197 

198 
lemma antitonP_adm_non_P: "antitonP P ==> adm (%u. u~:P)" 

199 
apply (unfold adm_def) 

200 
apply (auto dest: antitonPD elim: is_ub_thelub) 

201 
done 

202 

203 
lemma def_gfp_adm_nonP: "P \<equiv> gfp F \<Longrightarrow> {y. \<exists>x::'a::pcpo. y \<sqsubseteq> x \<and> x \<in> P} \<subseteq> F {y. \<exists>x. y \<sqsubseteq> x \<and> x \<in> P} \<Longrightarrow> 

204 
adm (\<lambda>u. u\<notin>P)" 

205 
apply (simp) 

206 
apply (rule antitonP_adm_non_P) 

207 
apply (rule antitonPI) 

208 
apply (drule gfp_upperbound) 

209 
apply (fast) 

210 
done 

211 

212 
lemma adm_set: 

27413  213 
"{\<Squnion>i. Y i Y. Porder.chain Y & (\<forall>i. Y i \<in> P)} \<subseteq> P \<Longrightarrow> adm (\<lambda>x. x\<in>P)" 
19759  214 
apply (unfold adm_def) 
215 
apply (fast) 

216 
done 

217 

27413  218 
lemma def_gfp_admI: "P \<equiv> gfp F \<Longrightarrow> {\<Squnion>i. Y i Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<subseteq> 
219 
F {\<Squnion>i. Y i Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<Longrightarrow> adm (\<lambda>x. x\<in>P)" 

19759  220 
apply (simp) 
221 
apply (rule adm_set) 

222 
apply (erule gfp_upperbound) 

223 
done 

224 

11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

225 
end 