src/HOLCF/FOCUS/Buffer_adm.thy
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/FOCUS/Buffer_adm.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,300 +0,0 @@
     1.4 -(*  Title:      HOLCF/FOCUS/Buffer_adm.thy
     1.5 -    Author:     David von Oheimb, TU Muenchen
     1.6 -*)
     1.7 -
     1.8 -header {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
     1.9 -
    1.10 -theory Buffer_adm
    1.11 -imports Buffer Stream_adm
    1.12 -begin
    1.13 -
    1.14 -declare Fin_0 [simp]
    1.15 -
    1.16 -lemma BufAC_Asm_d2: "a\<leadsto>s:BufAC_Asm ==> ? d. a=Md d"
    1.17 -by (drule BufAC_Asm_unfold [THEN iffD1], auto)
    1.18 -
    1.19 -lemma BufAC_Asm_d3:
    1.20 -    "a\<leadsto>b\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\<bullet> & s:BufAC_Asm"
    1.21 -by (drule BufAC_Asm_unfold [THEN iffD1], auto)
    1.22 -
    1.23 -lemma BufAC_Asm_F_def3:
    1.24 - "(s:BufAC_Asm_F A) = (s=<> | 
    1.25 -  (? d. ft\<cdot>s=Def(Md d)) & (rt\<cdot>s=<> | ft\<cdot>(rt\<cdot>s)=Def \<bullet> & rt\<cdot>(rt\<cdot>s):A))"
    1.26 -by (unfold BufAC_Asm_F_def, auto)
    1.27 -
    1.28 -lemma cont_BufAC_Asm_F: "down_cont BufAC_Asm_F"
    1.29 -by (auto simp add: down_cont_def BufAC_Asm_F_def3)
    1.30 -
    1.31 -lemma BufAC_Cmt_F_def3:
    1.32 - "((s,t):BufAC_Cmt_F C) = (!d x.
    1.33 -    (s = <>       --> t = <>                   ) & 
    1.34 -    (s = Md d\<leadsto><>  --> t = <>                   ) & 
    1.35 -    (s = Md d\<leadsto>\<bullet>\<leadsto>x --> ft\<cdot>t = Def d & (x,rt\<cdot>t):C))"
    1.36 -apply (unfold BufAC_Cmt_F_def)
    1.37 -apply (subgoal_tac "!d x. (s = Md d\<leadsto>\<bullet>\<leadsto>x --> (? y. t = d\<leadsto>y & (x,y):C)) = 
    1.38 -                     (s = Md d\<leadsto>\<bullet>\<leadsto>x --> ft\<cdot>t = Def d & (x,rt\<cdot>t):C)")
    1.39 -apply (simp)
    1.40 -apply (auto intro: surjectiv_scons [symmetric])
    1.41 -done
    1.42 -
    1.43 -lemma cont_BufAC_Cmt_F: "down_cont BufAC_Cmt_F"
    1.44 -by (auto simp add: down_cont_def BufAC_Cmt_F_def3)
    1.45 -
    1.46 -
    1.47 -(**** adm_BufAC_Asm ***********************************************************)
    1.48 -
    1.49 -lemma BufAC_Asm_F_stream_monoP: "stream_monoP BufAC_Asm_F"
    1.50 -apply (unfold BufAC_Asm_F_def stream_monoP_def)
    1.51 -apply (rule_tac x="{x. (? d. x = Md d\<leadsto>\<bullet>\<leadsto><>)}" in exI)
    1.52 -apply (rule_tac x="Suc (Suc 0)" in exI)
    1.53 -apply (clarsimp)
    1.54 -done
    1.55 -
    1.56 -lemma adm_BufAC_Asm: "adm (%x. x:BufAC_Asm)"
    1.57 -apply (unfold BufAC_Asm_def)
    1.58 -apply (rule cont_BufAC_Asm_F [THEN BufAC_Asm_F_stream_monoP [THEN fstream_gfp_admI]])
    1.59 -done
    1.60 -
    1.61 -
    1.62 -(**** adm_non_BufAC_Asm *******************************************************)
    1.63 -
    1.64 -lemma BufAC_Asm_F_stream_antiP: "stream_antiP BufAC_Asm_F"
    1.65 -apply (unfold stream_antiP_def BufAC_Asm_F_def)
    1.66 -apply (intro strip)
    1.67 -apply (rule_tac x="{x. (? d. x = Md d\<leadsto>\<bullet>\<leadsto><>)}" in exI)
    1.68 -apply (rule_tac x="Suc (Suc 0)" in exI)
    1.69 -apply (rule conjI)
    1.70 -prefer 2
    1.71 -apply ( intro strip)
    1.72 -apply ( drule slen_mono)
    1.73 -apply ( drule (1) order_trans)
    1.74 -apply (force)+
    1.75 -done
    1.76 -
    1.77 -lemma adm_non_BufAC_Asm: "adm (%u. u~:BufAC_Asm)"
    1.78 -apply (unfold BufAC_Asm_def)
    1.79 -apply (rule cont_BufAC_Asm_F [THEN BufAC_Asm_F_stream_antiP [THEN fstream_non_gfp_admI]])
    1.80 -done
    1.81 -
    1.82 -(**** adm_BufAC ***************************************************************)
    1.83 -
    1.84 -(*adm_non_BufAC_Asm*)
    1.85 -lemma BufAC_Asm_cong [rule_format]: "!f ff. f:BufEq --> ff:BufEq --> s:BufAC_Asm --> f\<cdot>s = ff\<cdot>s"
    1.86 -apply (rule fstream_ind2)
    1.87 -apply (simp add: adm_non_BufAC_Asm)
    1.88 -apply   (force dest: Buf_f_empty)
    1.89 -apply  (force dest!: BufAC_Asm_d2
    1.90 -              dest: Buf_f_d elim: ssubst)
    1.91 -apply (safe dest!: BufAC_Asm_d3)
    1.92 -apply (drule Buf_f_d_req)+
    1.93 -apply (fast elim: ssubst)
    1.94 -done
    1.95 -
    1.96 -(*adm_non_BufAC_Asm,BufAC_Asm_cong*)
    1.97 -lemma BufAC_Cmt_d_req:
    1.98 -"!!X. [|f:BufEq; s:BufAC_Asm; (s, f\<cdot>s):BufAC_Cmt|] ==> (a\<leadsto>b\<leadsto>s, f\<cdot>(a\<leadsto>b\<leadsto>s)):BufAC_Cmt"
    1.99 -apply (rule BufAC_Cmt_unfold [THEN iffD2])
   1.100 -apply (intro strip)
   1.101 -apply (frule Buf_f_d_req)
   1.102 -apply (auto elim: BufAC_Asm_cong [THEN subst])
   1.103 -done
   1.104 -
   1.105 -(*adm_BufAC_Asm*)
   1.106 -lemma BufAC_Asm_antiton: "antitonP BufAC_Asm"
   1.107 -apply (rule antitonPI)
   1.108 -apply (rule allI)
   1.109 -apply (rule fstream_ind2)
   1.110 -apply (  rule adm_lemmas)+
   1.111 -apply (   rule cont_id)
   1.112 -apply (   rule adm_BufAC_Asm)
   1.113 -apply (  safe)
   1.114 -apply (  rule BufAC_Asm_empty)
   1.115 -apply ( force dest!: fstream_prefix
   1.116 -              dest: BufAC_Asm_d2 intro: BufAC_Asm_d)
   1.117 -apply ( force dest!: fstream_prefix
   1.118 -              dest: BufAC_Asm_d3 intro!: BufAC_Asm_d_req)
   1.119 -done
   1.120 -
   1.121 -(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
   1.122 -lemma BufAC_Cmt_2stream_monoP: "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> 
   1.123 -                     (x,f\<cdot>x):down_iterate BufAC_Cmt_F i --> 
   1.124 -                     (s,f\<cdot>s):down_iterate BufAC_Cmt_F i"
   1.125 -apply (rule_tac x="%i. 2*i" in exI)
   1.126 -apply (rule allI)
   1.127 -apply (induct_tac "i")
   1.128 -apply ( simp)
   1.129 -apply (simp add: add_commute)
   1.130 -apply (intro strip)
   1.131 -apply (subst BufAC_Cmt_F_def3)
   1.132 -apply (drule_tac P="%x. x" in BufAC_Cmt_F_def3 [THEN subst])
   1.133 -apply safe
   1.134 -apply (   erule Buf_f_empty)
   1.135 -apply (  erule Buf_f_d)
   1.136 -apply ( drule Buf_f_d_req)
   1.137 -apply ( safe, erule ssubst, simp)
   1.138 -apply clarsimp
   1.139 -apply (rename_tac i d xa ya t)
   1.140 -(*
   1.141 - 1. \<And>i d xa ya t.
   1.142 -       \<lbrakk>f \<in> BufEq;
   1.143 -          \<forall>x s. s \<in> BufAC_Asm \<longrightarrow>
   1.144 -                x \<sqsubseteq> s \<longrightarrow>
   1.145 -                Fin (2 * i) < #x \<longrightarrow>
   1.146 -                (x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow>
   1.147 -                (s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i;
   1.148 -          Md d\<leadsto>\<bullet>\<leadsto>xa \<in> BufAC_Asm; Fin (2 * i) < #ya; f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>t;
   1.149 -          (ya, t) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa\<rbrakk>
   1.150 -       \<Longrightarrow> (xa, rt\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>xa))) \<in> down_iterate BufAC_Cmt_F i
   1.151 -*)
   1.152 -apply (rotate_tac 2)
   1.153 -apply (drule BufAC_Asm_prefix2)
   1.154 -apply (frule Buf_f_d_req, erule exE, erule conjE, rotate_tac -1, erule ssubst)
   1.155 -apply (frule Buf_f_d_req, erule exE, erule conjE)
   1.156 -apply (            subgoal_tac "f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya")
   1.157 -prefer 2
   1.158 -apply ( assumption)
   1.159 -apply (            rotate_tac -1)
   1.160 -apply (            simp)
   1.161 -apply (erule subst)
   1.162 -(*
   1.163 - 1. \<And>i d xa ya t ff ffa.
   1.164 -       \<lbrakk>f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya; Fin (2 * i) < #ya;
   1.165 -          (ya, ffa\<cdot>ya) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa; f \<in> BufEq;
   1.166 -          \<forall>x s. s \<in> BufAC_Asm \<longrightarrow>
   1.167 -                x \<sqsubseteq> s \<longrightarrow>
   1.168 -                Fin (2 * i) < #x \<longrightarrow>
   1.169 -                (x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow>
   1.170 -                (s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i;
   1.171 -          xa \<in> BufAC_Asm; ff \<in> BufEq; ffa \<in> BufEq\<rbrakk>
   1.172 -       \<Longrightarrow> (xa, ff\<cdot>xa) \<in> down_iterate BufAC_Cmt_F i
   1.173 -*)
   1.174 -apply (drule spec, drule spec, drule (1) mp)
   1.175 -apply (drule (1) mp)
   1.176 -apply (drule (1) mp)
   1.177 -apply (erule impE)
   1.178 -apply ( subst BufAC_Asm_cong, assumption)
   1.179 -prefer 3 apply assumption
   1.180 -apply assumption
   1.181 -apply ( erule (1) BufAC_Asm_antiton [THEN antitonPD])
   1.182 -apply (subst BufAC_Asm_cong, assumption)
   1.183 -prefer 3 apply assumption
   1.184 -apply assumption
   1.185 -apply assumption
   1.186 -done
   1.187 -
   1.188 -lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>down_iterate BufAC_Cmt_F n)"
   1.189 -apply (unfold BufAC_Cmt_def)
   1.190 -apply (subst cont_BufAC_Cmt_F [THEN INTER_down_iterate_is_gfp])
   1.191 -apply (fast)
   1.192 -done
   1.193 -
   1.194 -(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
   1.195 -  BufAC_Cmt_2stream_monoP*)
   1.196 -lemma adm_BufAC: "f:BufEq ==> adm (%s. s:BufAC_Asm --> (s, f\<cdot>s):BufAC_Cmt)"
   1.197 -apply (rule flatstream_admI)
   1.198 -apply (subst BufAC_Cmt_iterate_all)
   1.199 -apply (drule BufAC_Cmt_2stream_monoP)
   1.200 -apply safe
   1.201 -apply (drule spec, erule exE)
   1.202 -apply (drule spec, erule impE)
   1.203 -apply  (erule BufAC_Asm_antiton [THEN antitonPD])
   1.204 -apply  (erule is_ub_thelub)
   1.205 -apply (tactic "smp_tac 3 1")
   1.206 -apply (drule is_ub_thelub)
   1.207 -apply (drule (1) mp)
   1.208 -apply (drule (1) mp)
   1.209 -apply (erule mp)
   1.210 -apply (drule BufAC_Cmt_iterate_all [THEN iffD1])
   1.211 -apply (erule spec)
   1.212 -done
   1.213 -
   1.214 -
   1.215 -
   1.216 -(**** Buf_Eq_imp_AC by induction **********************************************)
   1.217 -
   1.218 -(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
   1.219 -  BufAC_Cmt_2stream_monoP,adm_BufAC,BufAC_Cmt_d_req*)
   1.220 -lemma Buf_Eq_imp_AC: "BufEq <= BufAC"
   1.221 -apply (unfold BufAC_def)
   1.222 -apply (rule subsetI)
   1.223 -apply (simp)
   1.224 -apply (rule allI)
   1.225 -apply (rule fstream_ind2)
   1.226 -back
   1.227 -apply (   erule adm_BufAC)
   1.228 -apply (  safe)
   1.229 -apply (   erule BufAC_Cmt_empty)
   1.230 -apply (  erule BufAC_Cmt_d)
   1.231 -apply ( drule BufAC_Asm_prefix2)
   1.232 -apply ( simp)
   1.233 -apply (fast intro: BufAC_Cmt_d_req BufAC_Asm_prefix2)
   1.234 -done
   1.235 -
   1.236 -(**** new approach for admissibility, reduces itself to absurdity *************)
   1.237 -
   1.238 -lemma adm_BufAC_Asm': "adm (\<lambda>x. x\<in>BufAC_Asm)"
   1.239 -apply (rule def_gfp_admI)
   1.240 -apply (rule BufAC_Asm_def [THEN eq_reflection])
   1.241 -apply (safe)
   1.242 -apply (unfold BufAC_Asm_F_def)
   1.243 -apply (safe)
   1.244 -apply (erule contrapos_np)
   1.245 -apply (drule fstream_exhaust_eq [THEN iffD1])
   1.246 -apply (clarsimp)
   1.247 -apply (drule (1) fstream_lub_lemma)
   1.248 -apply (clarify)
   1.249 -apply (erule_tac x="j" in all_dupE)
   1.250 -apply (simp)
   1.251 -apply (drule BufAC_Asm_d2)
   1.252 -apply (clarify)
   1.253 -apply (simp)
   1.254 -apply (rule disjCI)
   1.255 -apply (erule contrapos_np)
   1.256 -apply (drule fstream_exhaust_eq [THEN iffD1])
   1.257 -apply (clarsimp)
   1.258 -apply (drule (1) fstream_lub_lemma)
   1.259 -apply (clarsimp)
   1.260 -apply (tactic "simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1")
   1.261 -apply (rule_tac x="Xa" in exI)
   1.262 -apply (rule allI)
   1.263 -apply (rotate_tac -1)
   1.264 -apply (erule_tac x="i" in allE)
   1.265 -apply (clarsimp)
   1.266 -apply (erule_tac x="jb" in allE)
   1.267 -apply (clarsimp)
   1.268 -apply (erule_tac x="jc" in allE)
   1.269 -apply (clarsimp dest!: BufAC_Asm_d3)
   1.270 -done
   1.271 -
   1.272 -lemma adm_non_BufAC_Asm': "adm (\<lambda>u. u \<notin> BufAC_Asm)" (* uses antitonP *)
   1.273 -apply (rule def_gfp_adm_nonP)
   1.274 -apply (rule BufAC_Asm_def [THEN eq_reflection])
   1.275 -apply (unfold BufAC_Asm_F_def)
   1.276 -apply (safe)
   1.277 -apply (erule contrapos_np)
   1.278 -apply (drule fstream_exhaust_eq [THEN iffD1])
   1.279 -apply (clarsimp)
   1.280 -apply (frule fstream_prefix)
   1.281 -apply (clarsimp)
   1.282 -apply (frule BufAC_Asm_d2)
   1.283 -apply (clarsimp)
   1.284 -apply (rotate_tac -1)
   1.285 -apply (erule contrapos_pp)
   1.286 -apply (drule fstream_exhaust_eq [THEN iffD1])
   1.287 -apply (clarsimp)
   1.288 -apply (frule fstream_prefix)
   1.289 -apply (clarsimp)
   1.290 -apply (frule BufAC_Asm_d3)
   1.291 -apply (force)
   1.292 -done
   1.293 -
   1.294 -lemma adm_BufAC': "f \<in> BufEq \<Longrightarrow> adm (\<lambda>u. u \<in> BufAC_Asm \<longrightarrow> (u, f\<cdot>u) \<in> BufAC_Cmt)"
   1.295 -apply (rule triv_admI)
   1.296 -apply (clarify)
   1.297 -apply (erule (1) Buf_Eq_imp_AC_lemma)
   1.298 -      (* this is what we originally aimed to show, using admissibilty :-( *)
   1.299 -done
   1.300 -
   1.301 -end
   1.302 -
   1.303 -