src/HOLCF/FOCUS/Buffer_adm.ML
author wenzelm
Tue Aug 27 11:03:05 2002 +0200 (2002-08-27)
changeset 13524 604d0f3622d6
parent 13454 01e2496dee05
child 14981 e73f8140af78
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title: 	HOLCF/FOCUS/Buffer_adm.ML
     2     ID:         $Id$
     3     Author: 	David von Oheimb, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 infixr 0 y;
     8 fun _ y t = by t;
     9 val b=9999;
    10 
    11 Addsimps [thm "Fin_0"];
    12 
    13 val BufAC_Asm_d2 = prove_forw "a\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d" BufAC_Asm_unfold;
    14 val BufAC_Asm_d3 = prove_forw 
    15     "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\\<bullet> & s:BufAC_Asm" BufAC_Asm_unfold;
    16 
    17 val BufAC_Asm_F_def3 = prove_goalw thy [BufAC_Asm_F_def] 
    18  "(s:BufAC_Asm_F A) = (s=<> | \
    19 \ (? d. ft\\<cdot>s=Def(Md d)) & (rt\\<cdot>s=<> | ft\\<cdot>(rt\\<cdot>s)=Def \\<bullet> & rt\\<cdot>(rt\\<cdot>s):A))" (K [
    20 	Auto_tac]);
    21 
    22 Goal "down_cont BufAC_Asm_F";
    23 by (auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Asm_F_def3]));
    24 qed "cont_BufAC_Asm_F";
    25 
    26 val BufAC_Cmt_F_def3 = prove_goalw thy [BufAC_Cmt_F_def] 
    27  "((s,t):BufAC_Cmt_F C) = (!d x.\
    28 \   (s = <>       --> t = <>                   ) & \
    29 \   (s = Md d\\<leadsto><>  --> t = <>                   ) & \
    30 \   (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C))" (fn _=> [
    31 	subgoal_tac "!d x. (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> (? y. t = d\\<leadsto>y & (x,y):C)) = \
    32 		   \ (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C)"  1,
    33 	Asm_simp_tac 1,
    34 	auto_tac (claset() addIs [surjectiv_scons RS sym], simpset())]);
    35 
    36 val cont_BufAC_Cmt_F = prove_goal thy "down_cont BufAC_Cmt_F" (K [
    37 	auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Cmt_F_def3])]);
    38 
    39 
    40 (**** adm_BufAC_Asm ***********************************************************)
    41 
    42 Goalw [BufAC_Asm_F_def, stream_monoP_def] "stream_monoP BufAC_Asm_F";
    43 by (res_inst_tac [("x","{x. (? d. x = Md d\\<leadsto>\\<bullet>\\<leadsto><>)}")] exI 1);
    44 by (res_inst_tac [("x","Suc (Suc 0)")] exI 1);
    45 by (Clarsimp_tac 1);
    46 qed "BufAC_Asm_F_stream_monoP";
    47 
    48 val adm_BufAC_Asm = prove_goalw thy [BufAC_Asm_def] "adm (%x. x:BufAC_Asm)" (K [
    49 rtac (cont_BufAC_Asm_F RS (BufAC_Asm_F_stream_monoP RS fstream_gfp_admI))1]);
    50 
    51 
    52 (**** adm_non_BufAC_Asm *******************************************************)
    53 
    54 Goalw [stream_antiP_def, BufAC_Asm_F_def] "stream_antiP BufAC_Asm_F";
    55 b y strip_tac 1;
    56 b y res_inst_tac [("x","{x. (? d. x = Md d\\<leadsto>\\<bullet>\\<leadsto><>)}")] exI 1;
    57 b y res_inst_tac [("x","Suc (Suc 0)")] exI 1;
    58 b y rtac conjI 1;
    59 b y  strip_tac 2;
    60 b y  dtac slen_mono 2;
    61 b y  datac (thm "ile_trans") 1 2;
    62 b y ALLGOALS Force_tac;
    63 qed "BufAC_Asm_F_stream_antiP";
    64 
    65 Goalw [BufAC_Asm_def] "adm (%u. u~:BufAC_Asm)";
    66 by (rtac (cont_BufAC_Asm_F RS (BufAC_Asm_F_stream_antiP RS fstream_non_gfp_admI)) 1);
    67 qed "adm_non_BufAC_Asm";
    68 
    69 (**** adm_BufAC ***************************************************************)
    70 
    71 (*adm_non_BufAC_Asm*)
    72 Goal "!f ff. f:BufEq --> ff:BufEq --> s:BufAC_Asm --> f\\<cdot>s = ff\\<cdot>s";
    73 by (rtac fstream_ind2 1);
    74 by (simp_tac (simpset() addsimps [adm_non_BufAC_Asm]) 1);
    75 by   (force_tac (claset() addDs [Buf_f_empty], simpset()) 1);
    76 by  (force_tac (claset() addSDs [BufAC_Asm_d2] 
    77 		addDs [Buf_f_d] addEs [ssubst], simpset()) 1);
    78 by (safe_tac (claset() addSDs [BufAC_Asm_d3]));
    79 by (REPEAT(dtac Buf_f_d_req 1));
    80 by (fast_tac (claset() addEs [ssubst]) 1);
    81 qed_spec_mp "BufAC_Asm_cong";
    82 
    83 (*adm_non_BufAC_Asm,BufAC_Asm_cong*)
    84 val BufAC_Cmt_d_req = prove_goal thy 
    85 "!!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"
    86  (K [
    87 	rtac (BufAC_Cmt_unfold RS iffD2) 1,
    88 	strip_tac 1,
    89 	ftac Buf_f_d_req 1,
    90 	auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
    91 
    92 (*adm_BufAC_Asm*)
    93 Goal "antitonP BufAC_Asm";
    94 b y rtac antitonPI 1;
    95 b y rtac allI 1;
    96 b y rtac fstream_ind2 1;
    97 b y   REPEAT(resolve_tac adm_lemmas 1);
    98 b y    rtac cont_id 1;
    99 b y    rtac adm_BufAC_Asm 1;
   100 b y   safe_tac HOL_cs;
   101 b y   rtac BufAC_Asm_empty 1;
   102 b y  force_tac (claset() addSDs [fstream_prefix]
   103 		addDs [BufAC_Asm_d2] addIs [BufAC_Asm_d],simpset()) 1;
   104 b y  force_tac (claset() addSDs [fstream_prefix]
   105 		addDs [] addIs []
   106 		addDs [BufAC_Asm_d3] addSIs [BufAC_Asm_d_req],simpset()) 1;
   107 qed "BufAC_Asm_antiton";
   108 
   109 (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
   110 Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
   111 		\    (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
   112 		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
   113 by (res_inst_tac [("x","%i. 2*i")] exI 1);
   114 by (rtac allI 1);
   115 by (induct_tac "i" 1);
   116 by ( Simp_tac 1);
   117 by (simp_tac (simpset() addsimps [add_commute]) 1);
   118 by (strip_tac 1);
   119 by (stac BufAC_Cmt_F_def3 1);
   120 by (dres_inst_tac [("P","%x. x")] (BufAC_Cmt_F_def3 RS subst) 1);
   121 by Safe_tac;
   122 by (   etac Buf_f_empty 1);
   123 by (  etac Buf_f_d 1);
   124 by ( dtac Buf_f_d_req 1);
   125 by ( EVERY[safe_tac HOL_cs, etac ssubst 1, Simp_tac 1]);
   126 by (safe_tac (claset() addSDs [slen_fscons_eq RS iffD1] addSss simpset()));
   127 (*
   128  1. \\<And>i d xa ya t.
   129        \\<lbrakk>f \\<in> BufEq;
   130           \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
   131                 x \\<sqsubseteq> s \\<longrightarrow>
   132                 Fin (2 * i) < #x \\<longrightarrow>
   133                 (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
   134                 (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
   135           Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
   136           (ya, t) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa\\<rbrakk>
   137        \\<Longrightarrow> (xa, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>xa))) \\<in> down_iterate BufAC_Cmt_F i
   138 *)
   139 by (rotate_tac 2 1);
   140 by (dtac BufAC_Asm_prefix2 1);
   141 by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1, rotate_tac ~1 1,etac ssubst 1]); 
   142 by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1]);
   143 by (		subgoal_tac "f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya" 1);
   144 by ( atac 2);
   145 by (		rotate_tac ~1 1);
   146 by (		Asm_full_simp_tac 1);
   147 by (hyp_subst_tac 1);
   148 (*
   149  1. \\<And>i d xa ya t ff ffa.
   150        \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (2 * i) < #ya;
   151           (ya, ffa\\<cdot>ya) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa; f \\<in> BufEq;
   152           \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
   153                 x \\<sqsubseteq> s \\<longrightarrow>
   154                 Fin (2 * i) < #x \\<longrightarrow>
   155                 (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
   156                 (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
   157           xa \\<in> BufAC_Asm; ff \\<in> BufEq; ffa \\<in> BufEq\\<rbrakk>
   158        \\<Longrightarrow> (xa, ff\\<cdot>xa) \\<in> down_iterate BufAC_Cmt_F i
   159 *)
   160 by (smp_tac 2 1);
   161 by (mp_tac 1);
   162 by (mp_tac 1);
   163 by (etac impE 1);
   164 by ( EVERY[stac BufAC_Asm_cong 1, atac 1, atac 3, atac 1]);
   165 by ( eatac (BufAC_Asm_antiton RS antitonPD) 1 1);
   166 by (EVERY[stac BufAC_Asm_cong 1, atac 1, atac 3, atac 1, atac 1]);
   167 qed "BufAC_Cmt_2stream_monoP";
   168 
   169 Goalw [BufAC_Cmt_def] "(x\\<in>BufAC_Cmt) = (\\<forall>n. x\\<in>down_iterate BufAC_Cmt_F n)";
   170 by (stac (cont_BufAC_Cmt_F RS INTER_down_iterate_is_gfp) 1);
   171 by (Fast_tac 1);
   172 qed "BufAC_Cmt_iterate_all";
   173 
   174 (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
   175   BufAC_Cmt_2stream_monoP*)
   176 Goal "f:BufEq ==> adm (%s. s:BufAC_Asm --> (s, f\\<cdot>s):BufAC_Cmt)";
   177 by (rtac flatstream_admI 1);
   178 by (stac BufAC_Cmt_iterate_all 1);
   179 by (dtac BufAC_Cmt_2stream_monoP 1);
   180 by Safe_tac;
   181 by (EVERY'[dtac spec, etac exE] 1);
   182 by (EVERY'[dtac spec, etac impE] 1);
   183 by  (etac (BufAC_Asm_antiton RS antitonPD) 1);
   184 by  (etac is_ub_thelub 1);
   185 by (smp_tac 3 1);
   186 by (dtac is_ub_thelub 1);
   187 by (mp_tac 1);
   188 by (mp_tac 1);
   189 by (etac mp 1);
   190 by (dtac (BufAC_Cmt_iterate_all RS iffD1) 1);
   191 by (etac spec 1);
   192 qed "adm_BufAC";
   193 
   194 
   195 
   196 (**** Buf_Eq_imp_AC by induction **********************************************)
   197 
   198 (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
   199   BufAC_Cmt_2stream_monoP,adm_BufAC,BufAC_Cmt_d_req*)
   200 Goalw [BufAC_def] "BufEq <= BufAC";
   201 by (rtac subsetI 1);
   202 by (Simp_tac 1);
   203 by (rtac allI 1);
   204 by (rtac fstream_ind2 1);
   205 back();
   206 by (   etac adm_BufAC 1);
   207 by (  Safe_tac);
   208 by (   etac BufAC_Cmt_empty 1);
   209 by (  etac BufAC_Cmt_d 1);
   210 by ( dtac BufAC_Asm_prefix2 1);
   211 by ( contr_tac 1);
   212 by (fast_tac (claset() addIs [BufAC_Cmt_d_req, BufAC_Asm_prefix2]) 1);
   213 qed "Buf_Eq_imp_AC";
   214 
   215 (**** new approach for admissibility, reduces itself to absurdity *************)
   216 
   217 Goal "adm (\\<lambda>x. x\\<in>BufAC_Asm)";
   218 by (rtac def_gfp_admI 1);
   219 by (rtac BufAC_Asm_def 1);
   220 b y Safe_tac;
   221 b y rewtac BufAC_Asm_F_def;
   222 b y Safe_tac;
   223 b y etac swap 1;
   224 b y dtac (fstream_exhaust_eq RS iffD1) 1;
   225 b y Clarsimp_tac 1;
   226 b y datac fstream_lub_lemma 1 1;
   227 b y Clarify_tac 1;
   228 b y eres_inst_tac [("x","j")] all_dupE 1;
   229 b y Asm_full_simp_tac 1;
   230 b y dtac (BufAC_Asm_d2) 1;
   231 b y Clarify_tac 1;
   232 b y Simp_tac 1;
   233 b y rtac disjCI 1;
   234 b y etac swap 1;
   235 b y dtac (fstream_exhaust_eq RS iffD1) 1;
   236 b y Clarsimp_tac 1;
   237 b y datac fstream_lub_lemma 1 1;
   238 b y Clarsimp_tac 1;
   239 b y simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1;
   240 b y res_inst_tac [("x","Xa")] exI 1;
   241 by (rtac allI 1);
   242 b y rotate_tac ~1 1;
   243 b y eres_inst_tac [("x","i")] allE 1;
   244 b y Clarsimp_tac 1;
   245 b y eres_inst_tac [("x","jb")] allE 1;
   246 b y Clarsimp_tac 1;
   247 b y eres_inst_tac [("x","jc")] allE 1;
   248 by (clarsimp_tac (claset() addSDs [BufAC_Asm_d3], simpset()) 1);
   249 qed "adm_BufAC_Asm";
   250 
   251 Goal "adm (\\<lambda>u. u \\<notin> BufAC_Asm)"; (* uses antitonP *)
   252 by (rtac def_gfp_adm_nonP 1);
   253 by (rtac BufAC_Asm_def 1);
   254 b y rewtac BufAC_Asm_F_def;
   255 b y Safe_tac;
   256 b y etac swap 1;
   257 b y dtac (fstream_exhaust_eq RS iffD1) 1;
   258 b y Clarsimp_tac 1;
   259 b y ftac fstream_prefix 1;
   260 b y Clarsimp_tac 1;
   261 b y ftac BufAC_Asm_d2 1;
   262 b y Clarsimp_tac 1;
   263 b y rotate_tac ~1 1;
   264 b y etac contrapos_pp 1;
   265 b y dtac (fstream_exhaust_eq RS iffD1) 1;
   266 b y Clarsimp_tac 1;
   267 b y ftac fstream_prefix 1;
   268 b y Clarsimp_tac 1;
   269 b y ftac BufAC_Asm_d3 1;
   270 b y Force_tac 1;
   271 qed "adm_non_BufAC_Asm'";
   272 
   273 Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
   274 by (rtac triv_admI 1);
   275 by (Clarify_tac 1);
   276 by (eatac Buf_Eq_imp_AC_lemma 1 1); 
   277       (* this is what we originally aimed to show, using admissibilty :-( *)
   278 qed "adm_BufAC'";