1(* Title: HOL/HOLCF/FOCUS/Stream_adm.thy 2 Author: David von Oheimb, TU Muenchen 3*) 4 5section \<open>Admissibility for streams\<close> 6 7theory Stream_adm 8imports "HOLCF-Library.Stream" "HOL-Library.Order_Continuity" 9begin 10 11definition 12 stream_monoP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where 13 "stream_monoP F = (\<exists>Q i. \<forall>P s. enat i \<le> #s \<longrightarrow> 14 (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P))" 15 16definition 17 stream_antiP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where 18 "stream_antiP F = (\<forall>P x. \<exists>Q i. 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> 21 (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P))))" 22 23definition 24 antitonP :: "'a set => bool" where 25 "antitonP P = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P)" 26 27 28(* ----------------------------------------------------------------------- *) 29 30section "admissibility" 31 32lemma infinite_chain_adm_lemma: 33 "\<lbrakk>Porder.chain Y; \<forall>i. P (Y i); 34 \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk> 35 \<Longrightarrow> P (\<Squnion>i. Y i)" 36apply (case_tac "finite_chain Y") 37prefer 2 apply fast 38apply (unfold finite_chain_def) 39apply safe 40apply (erule lub_finch1 [THEN lub_eqI, THEN ssubst]) 41apply assumption 42apply (erule spec) 43done 44 45lemma increasing_chain_adm_lemma: 46 "\<lbrakk>Porder.chain Y; \<forall>i. P (Y i); \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i); 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> 48 \<Longrightarrow> P (\<Squnion>i. Y i)" 49apply (erule infinite_chain_adm_lemma) 50apply assumption 51apply (erule thin_rl) 52apply (unfold finite_chain_def) 53apply (unfold max_in_chain_def) 54apply (fast dest: le_imp_less_or_eq elim: chain_mono_less) 55done 56 57lemma flatstream_adm_lemma: 58 assumes 1: "Porder.chain Y" 59 assumes 2: "\<forall>i. P (Y i)" 60 assumes 3: "(\<And>Y. [| Porder.chain Y; \<forall>i. P (Y i); \<forall>k. \<exists>j. enat k < #((Y j)::'a::flat stream)|] 61 ==> P(LUB i. Y i))" 62 shows "P(LUB i. Y i)" 63apply (rule increasing_chain_adm_lemma [OF 1 2]) 64apply (erule 3, assumption) 65apply (erule thin_rl) 66apply (rule allI) 67apply (case_tac "\<forall>j. stream_finite (Y j)") 68apply ( rule chain_incr) 69apply ( rule allI) 70apply ( drule spec) 71apply ( safe) 72apply ( rule exI) 73apply ( rule slen_strict_mono) 74apply ( erule spec) 75apply ( assumption) 76apply ( assumption) 77apply (metis enat_ord_code(4) slen_infinite) 78done 79 80(* should be without reference to stream length? *) 81lemma flatstream_admI: "[|(\<And>Y. [| Porder.chain Y; \<forall>i. P (Y i); 82 \<forall>k. \<exists>j. enat k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P" 83apply (unfold adm_def) 84apply (intro strip) 85apply (erule (1) flatstream_adm_lemma) 86apply (fast) 87done 88 89 90(* context (theory "Extended_Nat");*) 91lemma ile_lemma: "enat (i + j) <= x ==> enat i <= x" 92 by (rule order_trans) auto 93 94lemma stream_monoP2I: 95"\<And>X. stream_monoP F \<Longrightarrow> \<forall>i. \<exists>l. \<forall>x y. 96 enat l \<le> #x \<longrightarrow> (x::'a::flat stream) << y --> x \<in> (F ^^ i) top \<longrightarrow> y \<in> (F ^^ i) top" 97apply (unfold stream_monoP_def) 98apply (safe) 99apply (rule_tac x="i*ia" in exI) 100apply (induct_tac "ia") 101apply ( simp) 102apply (simp) 103apply (intro strip) 104apply (erule allE, erule all_dupE, drule mp, erule ile_lemma) 105apply (drule_tac P="%x. x" in subst, assumption) 106apply (erule allE, drule mp, rule ile_lemma) back 107apply ( erule order_trans) 108apply ( erule slen_mono) 109apply (erule ssubst) 110apply (safe) 111apply ( erule (2) ile_lemma [THEN slen_take_lemma3, THEN subst]) 112apply (erule allE) 113apply (drule mp) 114apply ( erule slen_rt_mult) 115apply (erule allE) 116apply (drule mp) 117apply (erule monofun_rt_mult) 118apply (drule (1) mp) 119apply (assumption) 120done 121 122lemma stream_monoP2_gfp_admI: "[| \<forall>i. \<exists>l. \<forall>x y. 123 enat l \<le> #x \<longrightarrow> (x::'a::flat stream) << y \<longrightarrow> x \<in> (F ^^ i) top \<longrightarrow> y \<in> (F ^^ i) top; 124 inf_continuous F |] ==> adm (\<lambda>x. x \<in> gfp F)" 125apply (erule inf_continuous_gfp[of F, THEN ssubst]) 126apply (simp (no_asm)) 127apply (rule adm_lemmas) 128apply (rule flatstream_admI) 129apply (erule allE) 130apply (erule exE) 131apply (erule allE, erule exE) 132apply (erule allE, erule allE, drule mp) (* stream_monoP *) 133apply ( drule ileI1) 134apply ( drule order_trans) 135apply ( rule ile_eSuc) 136apply ( drule eSuc_ile_mono [THEN iffD1]) 137apply ( assumption) 138apply (drule mp) 139apply ( erule is_ub_thelub) 140apply (fast) 141done 142 143lemmas fstream_gfp_admI = stream_monoP2I [THEN stream_monoP2_gfp_admI] 144 145lemma stream_antiP2I: 146"\<And>X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|] 147 ==> \<forall>i x y. x << y \<longrightarrow> y \<in> (F ^^ i) top \<longrightarrow> x \<in> (F ^^ i) top" 148apply (unfold stream_antiP_def) 149apply (rule allI) 150apply (induct_tac "i") 151apply ( simp) 152apply (simp) 153apply (intro strip) 154apply (erule allE, erule all_dupE, erule exE, erule exE) 155apply (erule conjE) 156apply (case_tac "#x < enat i") 157apply ( fast) 158apply (unfold linorder_not_less) 159apply (drule (1) mp) 160apply (erule all_dupE, drule mp, rule below_refl) 161apply (erule ssubst) 162apply (erule allE, drule (1) mp) 163apply (drule_tac P="%x. x" in subst, assumption) 164apply (erule conjE, rule conjI) 165apply ( erule slen_take_lemma3 [THEN ssubst], assumption) 166apply ( assumption) 167apply (erule allE, erule allE, drule mp, erule monofun_rt_mult) 168apply (drule (1) mp) 169apply (assumption) 170done 171 172lemma stream_antiP2_non_gfp_admI: 173"\<And>X. [|\<forall>i x y. x << y \<longrightarrow> y \<in> (F ^^ i) top \<longrightarrow> x \<in> (F ^^ i) top; inf_continuous F |] 174 ==> adm (\<lambda>u. \<not> u \<in> gfp F)" 175apply (unfold adm_def) 176apply (simp add: inf_continuous_gfp) 177apply (fast dest!: is_ub_thelub) 178done 179 180lemmas fstream_non_gfp_admI = stream_antiP2I [THEN stream_antiP2_non_gfp_admI] 181 182 183 184(**new approach for adm********************************************************) 185 186section "antitonP" 187 188lemma antitonPD: "[| antitonP P; y \<in> P; x<<y |] ==> x \<in> P" 189apply (unfold antitonP_def) 190apply auto 191done 192 193lemma antitonPI: "\<forall>x y. y \<in> P \<longrightarrow> x<<y --> x \<in> P \<Longrightarrow> antitonP P" 194apply (unfold antitonP_def) 195apply (fast) 196done 197 198lemma antitonP_adm_non_P: "antitonP P \<Longrightarrow> adm (\<lambda>u. u \<notin> P)" 199apply (unfold adm_def) 200apply (auto dest: antitonPD elim: is_ub_thelub) 201done 202 203lemma 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)" 205apply (simp) 206apply (rule antitonP_adm_non_P) 207apply (rule antitonPI) 208apply (drule gfp_upperbound) 209apply (fast) 210done 211 212lemma adm_set: 213"{\<Squnion>i. Y i |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<subseteq> P \<Longrightarrow> adm (\<lambda>x. x\<in>P)" 214apply (unfold adm_def) 215apply (fast) 216done 217 218lemma 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)" 220apply (simp) 221apply (rule adm_set) 222apply (erule gfp_upperbound) 223done 224 225end 226