src/HOLCF/FOCUS/Buffer_adm.ML
changeset 11350 4c55b020d6ee
child 11355 778c369559d9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Thu May 31 16:53:00 2001 +0200
     1.3 @@ -0,0 +1,278 @@
     1.4 +(*  Title: 	HOLCF/FOCUS/Buffer_adm.ML
     1.5 +    ID:         $ $
     1.6 +    Author: 	David von Oheimb, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +*)
     1.9 +
    1.10 +infixr 0 y;
    1.11 +fun _ y t = by t;
    1.12 +val b=9999;
    1.13 +
    1.14 +Addsimps [Fin_0];
    1.15 +
    1.16 +val BufAC_Asm_d2 = prove_forw "a\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d" BufAC_Asm_unfold;
    1.17 +val BufAC_Asm_d3 = prove_forw 
    1.18 +    "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\\<bullet> & s:BufAC_Asm" BufAC_Asm_unfold;
    1.19 +
    1.20 +val BufAC_Asm_F_def3 = prove_goalw thy [BufAC_Asm_F_def] 
    1.21 + "s:BufAC_Asm_F A = (s=<> | \
    1.22 +\ (? d. ft\\<cdot>s=Def(Md d)) & (rt\\<cdot>s=<> | ft\\<cdot>(rt\\<cdot>s)=Def \\<bullet> & rt\\<cdot>(rt\\<cdot>s):A))" (K [
    1.23 +	Auto_tac]);
    1.24 +
    1.25 +Goal "down_cont BufAC_Asm_F";
    1.26 +by (auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Asm_F_def3]));
    1.27 +qed "cont_BufAC_Asm_F";
    1.28 +
    1.29 +val BufAC_Cmt_F_def3 = prove_goalw thy [BufAC_Cmt_F_def] 
    1.30 + "(s,t):BufAC_Cmt_F C = (!d x.\
    1.31 +\   (s = <>       --> t = <>                   ) & \
    1.32 +\   (s = Md d\\<leadsto><>  --> t = <>                   ) & \
    1.33 +\   (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C))" (fn _=> [
    1.34 +	subgoal_tac "!d x. (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> (? y. t = d\\<leadsto>y & (x,y):C)) = \
    1.35 +		   \ (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C)"  1,
    1.36 +	Asm_simp_tac 1,
    1.37 +	auto_tac (claset() addIs [surjectiv_scons RS sym], simpset())]);
    1.38 +
    1.39 +val cont_BufAC_Cmt_F = prove_goal thy "down_cont BufAC_Cmt_F" (K [
    1.40 +	auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Cmt_F_def3])]);
    1.41 +
    1.42 +
    1.43 +(**** adm_BufAC_Asm ***********************************************************)
    1.44 +
    1.45 +Goalw [BufAC_Asm_F_def, stream_monoP_def] "stream_monoP BufAC_Asm_F";
    1.46 +by (res_inst_tac [("x","{x. (? d. x = Md d\\<leadsto>\\<bullet>\\<leadsto><>)}")] exI 1);
    1.47 +by (res_inst_tac [("x","2")] exI 1);
    1.48 +by (Clarsimp_tac 1);
    1.49 +qed "BufAC_Asm_F_stream_monoP";
    1.50 +
    1.51 +val adm_BufAC_Asm = prove_goalw thy [BufAC_Asm_def] "adm (%x. x:BufAC_Asm)" (K [
    1.52 +rtac (cont_BufAC_Asm_F RS (BufAC_Asm_F_stream_monoP RS fstream_gfp_admI))1]);
    1.53 +
    1.54 +
    1.55 +(**** adm_non_BufAC_Asm *******************************************************)
    1.56 +
    1.57 +Goalw [stream_antiP_def, BufAC_Asm_F_def] "stream_antiP BufAC_Asm_F";
    1.58 +b y strip_tac 1;
    1.59 +b y res_inst_tac [("x","{x. (? d. x = Md d\\<leadsto>\\<bullet>\\<leadsto><>)}")] exI 1;
    1.60 +b y res_inst_tac [("x","2")] exI 1;
    1.61 +b y rtac conjI 1;
    1.62 +b y  strip_tac 2;
    1.63 +b y  dtac slen_mono 2;
    1.64 +b y  datac ile_trans 1 2;
    1.65 +b y ALLGOALS Force_tac;
    1.66 +qed "BufAC_Asm_F_stream_antiP";
    1.67 +
    1.68 +Goalw [BufAC_Asm_def] "adm (%u. u~:BufAC_Asm)";
    1.69 +by (rtac (cont_BufAC_Asm_F RS (BufAC_Asm_F_stream_antiP RS fstream_non_gfp_admI)) 1);
    1.70 +qed "adm_non_BufAC_Asm";
    1.71 +
    1.72 +(**** adm_BufAC ***************************************************************)
    1.73 +
    1.74 +(*adm_non_BufAC_Asm*)
    1.75 +Goal "!f ff. f:BufEq --> ff:BufEq --> s:BufAC_Asm --> f\\<cdot>s = ff\\<cdot>s";
    1.76 +by (rtac fstream_ind2 1);
    1.77 +by (simp_tac (simpset() addsimps [adm_non_BufAC_Asm]) 1);
    1.78 +by   (force_tac (claset() addDs [Buf_f_empty], simpset()) 1);
    1.79 +by  (force_tac (claset() addSDs [BufAC_Asm_d2] 
    1.80 +		addDs [Buf_f_d] addEs [ssubst], simpset()) 1);
    1.81 +by (safe_tac (claset() addSDs [BufAC_Asm_d3]));
    1.82 +by (REPEAT(dtac Buf_f_d_req 1));
    1.83 +by (fast_tac (claset() addEs [ssubst]) 1);
    1.84 +qed_spec_mp "BufAC_Asm_cong";
    1.85 +
    1.86 +(*adm_non_BufAC_Asm,BufAC_Asm_cong*)
    1.87 +val BufAC_Cmt_d_req = prove_goal thy 
    1.88 +"!!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.89 + (K [
    1.90 +	rtac (BufAC_Cmt_unfold RS iffD2) 1,
    1.91 +	strip_tac 1,
    1.92 +	forward_tac [Buf_f_d_req] 1,
    1.93 +	auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
    1.94 +
    1.95 +(*adm_BufAC_Asm*)
    1.96 +Goal "antitonP BufAC_Asm";
    1.97 +b y rtac antitonPI 1;
    1.98 +b y rtac allI 1;
    1.99 +b y rtac fstream_ind2 1;
   1.100 +b y   REPEAT(resolve_tac adm_lemmas 1);
   1.101 +b y    rtac cont_id 1;
   1.102 +b y    rtac adm_BufAC_Asm 1;
   1.103 +b y   safe_tac HOL_cs;
   1.104 +b y   rtac BufAC_Asm_empty 1;
   1.105 +b y  force_tac (claset() addSDs [fstream_prefix]
   1.106 +		addDs [BufAC_Asm_d2] addIs [BufAC_Asm_d],simpset()) 1;
   1.107 +b y  force_tac (claset() addSDs [fstream_prefix]
   1.108 +		addDs [] addIs []
   1.109 +		addDs [BufAC_Asm_d3] addSIs [BufAC_Asm_d_req],simpset()) 1;
   1.110 +qed "BufAC_Asm_antiton";
   1.111 +
   1.112 +(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
   1.113 +Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
   1.114 +		\    (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
   1.115 +		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
   1.116 +by (res_inst_tac [("x","%i. i+i")] exI 1);
   1.117 +by (rtac allI 1);
   1.118 +by (nat_ind_tac "i" 1);
   1.119 +by ( Simp_tac 1);
   1.120 +by (simp_tac (simpset() addsimps [add_commute]) 1);
   1.121 +by (strip_tac 1);
   1.122 +by (stac BufAC_Cmt_F_def3 1);
   1.123 +by (dres_inst_tac [("P","%x. x")] (BufAC_Cmt_F_def3 RS subst) 1);
   1.124 +by (Safe_tac);
   1.125 +by (   etac Buf_f_empty 1);
   1.126 +by (  etac Buf_f_d 1);
   1.127 +by ( dtac Buf_f_d_req 1);
   1.128 +by ( EVERY[safe_tac HOL_cs, etac ssubst 1, Simp_tac 1]);
   1.129 +by (safe_tac (claset() addSDs [slen_fscons_eq RS iffD1] addSss simpset()));
   1.130 +(*
   1.131 + 1. \\<And>i d xa ya t.
   1.132 +       \\<lbrakk>f \\<in> BufEq;
   1.133 +          \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
   1.134 +                x \\<sqsubseteq> s \\<longrightarrow>
   1.135 +                Fin (#2 * i) < #x \\<longrightarrow>
   1.136 +                (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
   1.137 +                (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
   1.138 +          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.139 +          (ya, t) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa\\<rbrakk>
   1.140 +       \\<Longrightarrow> (xa, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>xa))) \\<in> down_iterate BufAC_Cmt_F i
   1.141 +*)
   1.142 +by (rotate_tac 2 1);
   1.143 +by (dtac BufAC_Asm_prefix2 1);
   1.144 +by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1, rotate_tac ~1 1,etac ssubst 1]); 
   1.145 +by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1]);
   1.146 +by (		subgoal_tac "f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya" 1);
   1.147 +by ( atac 2);
   1.148 +by (		rotate_tac ~1 1);
   1.149 +by (		Asm_full_simp_tac 1);
   1.150 +by (hyp_subst_tac 1);
   1.151 +(*
   1.152 + 1. \\<And>i d xa ya t ff ffa.
   1.153 +       \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (#2 * i) < #ya;
   1.154 +          (ya, ffa\\<cdot>ya) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa; f \\<in> BufEq;
   1.155 +          \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
   1.156 +                x \\<sqsubseteq> s \\<longrightarrow>
   1.157 +                Fin (#2 * i) < #x \\<longrightarrow>
   1.158 +                (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
   1.159 +                (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
   1.160 +          xa \\<in> BufAC_Asm; ff \\<in> BufEq; ffa \\<in> BufEq\\<rbrakk>
   1.161 +       \\<Longrightarrow> (xa, ff\\<cdot>xa) \\<in> down_iterate BufAC_Cmt_F i
   1.162 +*)
   1.163 +by (smp_tac 2 1);
   1.164 +by (mp_tac 1);
   1.165 +by (mp_tac 1);
   1.166 +by (etac impE 1);
   1.167 +by ( EVERY[stac BufAC_Asm_cong 1, atac 1, atac 3, atac 1]);
   1.168 +by ( eatac (BufAC_Asm_antiton RS antitonPD) 1 1);
   1.169 +by (EVERY[stac BufAC_Asm_cong 1, atac 1, atac 3, atac 1, atac 1]);
   1.170 +qed "BufAC_Cmt_2stream_monoP";
   1.171 +
   1.172 +Goalw [BufAC_Cmt_def] "x\\<in>BufAC_Cmt = (\\<forall>n. x\\<in>down_iterate BufAC_Cmt_F n)";
   1.173 +by (stac (cont_BufAC_Cmt_F RS INTER_down_iterate_is_gfp) 1);
   1.174 +by (Fast_tac 1);
   1.175 +qed "BufAC_Cmt_iterate_all";
   1.176 +
   1.177 +(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
   1.178 +  BufAC_Cmt_2stream_monoP*)
   1.179 +Goal "f:BufEq ==> adm (%s. s:BufAC_Asm --> (s, f\\<cdot>s):BufAC_Cmt)";
   1.180 +by (rtac flatstream_admI 1);
   1.181 +by (stac BufAC_Cmt_iterate_all 1);
   1.182 +by (dtac BufAC_Cmt_2stream_monoP 1);
   1.183 +by Safe_tac;
   1.184 +by (EVERY'[dtac spec, etac exE] 1);
   1.185 +by (EVERY'[dtac spec, etac impE] 1);
   1.186 +by  (etac (BufAC_Asm_antiton RS antitonPD) 1);
   1.187 +by  (etac is_ub_thelub 1);
   1.188 +by (smp_tac 3 1);
   1.189 +by (dtac is_ub_thelub 1);
   1.190 +by (mp_tac 1);
   1.191 +by (mp_tac 1);
   1.192 +by (etac mp 1);
   1.193 +by (dtac (BufAC_Cmt_iterate_all RS iffD1) 1);
   1.194 +by (etac spec 1);
   1.195 +qed "adm_BufAC";
   1.196 +
   1.197 +
   1.198 +
   1.199 +(**** Buf_Eq_imp_AC by induction **********************************************)
   1.200 +
   1.201 +(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
   1.202 +  BufAC_Cmt_2stream_monoP,adm_BufAC,BufAC_Cmt_d_req*)
   1.203 +Goalw [BufAC_def] "BufEq <= BufAC";
   1.204 +by (rtac subsetI 1);
   1.205 +by (Simp_tac 1);
   1.206 +by (rtac allI 1);
   1.207 +by (rtac fstream_ind2 1);
   1.208 +back();
   1.209 +by (   etac adm_BufAC 1);
   1.210 +by (  Safe_tac);
   1.211 +by (   etac BufAC_Cmt_empty 1);
   1.212 +by (  etac BufAC_Cmt_d 1);
   1.213 +by ( dtac BufAC_Asm_prefix2 1);
   1.214 +by ( contr_tac 1);
   1.215 +by (fast_tac (claset() addIs [BufAC_Cmt_d_req, BufAC_Asm_prefix2]) 1);
   1.216 +qed "Buf_Eq_imp_AC";
   1.217 +
   1.218 +(**** new approach for admissibility, reduces itself to absurdity *************)
   1.219 +
   1.220 +Goal "adm (\\<lambda>x. x\\<in>BufAC_Asm)";
   1.221 +by(rtac def_gfp_admI 1);
   1.222 +by(rtac BufAC_Asm_def 1);
   1.223 +b y Safe_tac;
   1.224 +b y rewtac BufAC_Asm_F_def;
   1.225 +b y Safe_tac;
   1.226 +b y etac swap 1;
   1.227 +b y dtac (fstream_exhaust_eq RS iffD1) 1;
   1.228 +b y Clarsimp_tac 1;
   1.229 +b y datac fstream_lub_lemma 1 1;
   1.230 +b y Clarify_tac 1;
   1.231 +b y eres_inst_tac [("x","j")] all_dupE 1;
   1.232 +b y Asm_full_simp_tac 1;
   1.233 +b y dtac (BufAC_Asm_d2) 1;
   1.234 +b y Clarify_tac 1;
   1.235 +b y Simp_tac 1;
   1.236 +b y rtac disjCI 1;
   1.237 +b y etac swap 1;
   1.238 +b y dtac (fstream_exhaust_eq RS iffD1) 1;
   1.239 +b y Clarsimp_tac 1;
   1.240 +b y datac fstream_lub_lemma 1 1;
   1.241 +b y Clarsimp_tac 1;
   1.242 +b y simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1;
   1.243 +b y res_inst_tac [("x","Xa")] exI 1;
   1.244 +br allI 1;
   1.245 +b y rotate_tac ~1 1;
   1.246 +b y eres_inst_tac [("x","i")] allE 1;
   1.247 +b y Clarsimp_tac 1;
   1.248 +b y eres_inst_tac [("x","jb")] allE 1;
   1.249 +b y Clarsimp_tac 1;
   1.250 +b y eres_inst_tac [("x","jc")] allE 1;
   1.251 +by (clarsimp_tac (claset() addSDs [BufAC_Asm_d3], simpset()) 1);
   1.252 +qed "adm_BufAC_Asm";
   1.253 +
   1.254 +Goal "adm (\\<lambda>u. u \\<notin> BufAC_Asm)"; (* uses antitonP *)
   1.255 +by (rtac def_gfp_adm_nonP 1);
   1.256 +by (rtac BufAC_Asm_def 1);
   1.257 +b y rewtac BufAC_Asm_F_def;
   1.258 +b y Safe_tac;
   1.259 +b y etac swap 1;
   1.260 +b y dtac (fstream_exhaust_eq RS iffD1) 1;
   1.261 +b y Clarsimp_tac 1;
   1.262 +b y ftac fstream_prefix 1;
   1.263 +b y Clarsimp_tac 1;
   1.264 +b y ftac BufAC_Asm_d2 1;
   1.265 +b y Clarsimp_tac 1;
   1.266 +b y rotate_tac ~1 1;
   1.267 +b y etac contrapos_pp 1;
   1.268 +b y dtac (fstream_exhaust_eq RS iffD1) 1;
   1.269 +b y Clarsimp_tac 1;
   1.270 +b y ftac fstream_prefix 1;
   1.271 +b y Clarsimp_tac 1;
   1.272 +b y ftac BufAC_Asm_d3 1;
   1.273 +b y Force_tac 1;
   1.274 +qed "adm_non_BufAC_Asm";
   1.275 +
   1.276 +Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
   1.277 +by(rtac triv_admI 1);
   1.278 +by(Clarify_tac 1);
   1.279 +by(eatac Buf_Eq_imp_AC_lemma 1 1); 
   1.280 +      (* this is what we originally aimed to show, using admissibilty :-( *)
   1.281 +qed "adm_BufAC";