src/HOLCF/FOCUS/Buffer.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 14171 0cab06e3bbd0
child 15188 9d57263faf9e
permissions -rw-r--r--
Merged in license change from Isabelle2004
     1 (*  Title: 	HOLCF/FOCUS/Buffer.ML
     2     ID:         $Id$
     3     Author: 	David von Oheimb, TU Muenchen
     4 *)
     5 
     6 val set_cong = prove_goal Set.thy "!!X. A = B ==> (x:A) = (x:B)" (K [
     7 	etac subst 1, rtac refl 1]);
     8 
     9 fun B_prover s tac eqs = prove_goal thy s (fn prems => [cut_facts_tac prems 1, 
    10 	tac 1, auto_tac (claset(), simpset() addsimps eqs)]);
    11 
    12 fun prove_forw  s thm     = B_prover s (dtac (thm RS iffD1)) [];
    13 fun prove_backw s thm eqs = B_prover s (rtac (thm RS iffD2)) eqs;
    14 
    15 
    16 (**** BufEq *******************************************************************)
    17 
    18 val mono_BufEq_F = prove_goalw thy [mono_def, BufEq_F_def] 
    19 		"mono BufEq_F" (K [Fast_tac 1]);
    20 
    21 val BufEq_fix = mono_BufEq_F RS (BufEq_def RS def_gfp_unfold);
    22 
    23 val BufEq_unfold = prove_goal thy "(f:BufEq) = (!d. f\\<cdot>(Md d\\<leadsto><>) = <> & \
    24 		\(!x. ? ff:BufEq. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>(ff\\<cdot>x)))" (K [
    25 	stac (BufEq_fix RS set_cong) 1,
    26 	rewtac BufEq_F_def,
    27 	Asm_full_simp_tac 1]);
    28 
    29 val Buf_f_empty = prove_forw "f:BufEq \\<Longrightarrow> f\\<cdot><> = <>" BufEq_unfold;
    30 val Buf_f_d     = prove_forw "f:BufEq \\<Longrightarrow> f\\<cdot>(Md d\\<leadsto><>) = <>" BufEq_unfold;
    31 val Buf_f_d_req = prove_forw 
    32 	"f:BufEq \\<Longrightarrow> \\<exists>ff. ff:BufEq \\<and> f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x" BufEq_unfold;
    33 
    34 
    35 (**** BufAC_Asm ***************************************************************)
    36 
    37 val mono_BufAC_Asm_F = prove_goalw thy [mono_def, BufAC_Asm_F_def]
    38 		"mono BufAC_Asm_F" (K [Fast_tac 1]);
    39 
    40 val BufAC_Asm_fix = mono_BufAC_Asm_F RS (BufAC_Asm_def RS def_gfp_unfold);
    41 
    42 val BufAC_Asm_unfold = prove_goal thy "(s:BufAC_Asm) = (s = <> | (? d x. \
    43 \       s = Md d\\<leadsto>x & (x = <> | (ft\\<cdot>x = Def \\<bullet> & (rt\\<cdot>x):BufAC_Asm))))" (K [
    44 				stac (BufAC_Asm_fix RS set_cong) 1,
    45 				rewtac BufAC_Asm_F_def,
    46 				Asm_full_simp_tac 1]);
    47 
    48 val BufAC_Asm_empty = prove_backw "<>     :BufAC_Asm" BufAC_Asm_unfold [];
    49 val BufAC_Asm_d     = prove_backw "Md d\\<leadsto><>:BufAC_Asm" BufAC_Asm_unfold [];
    50 val BufAC_Asm_d_req = prove_backw "x:BufAC_Asm ==> Md d\\<leadsto>\\<bullet>\\<leadsto>x:BufAC_Asm"
    51 							   BufAC_Asm_unfold [];
    52 val BufAC_Asm_prefix2 = prove_forw "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> s:BufAC_Asm"
    53 							 BufAC_Asm_unfold;
    54 
    55 
    56 (**** BBufAC_Cmt **************************************************************)
    57 
    58 val mono_BufAC_Cmt_F = prove_goalw thy [mono_def, BufAC_Cmt_F_def] 
    59 		"mono BufAC_Cmt_F" (K [Fast_tac 1]);
    60 
    61 val BufAC_Cmt_fix = mono_BufAC_Cmt_F RS (BufAC_Cmt_def RS def_gfp_unfold);
    62 
    63 val BufAC_Cmt_unfold = prove_goal thy "((s,t):BufAC_Cmt) = (!d x. \
    64     \(s = <>       -->      t = <>) & \
    65     \(s = Md d\\<leadsto><>  -->      t = <>) & \
    66     \(s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x, rt\\<cdot>t):BufAC_Cmt))" (K [
    67 	stac (BufAC_Cmt_fix RS set_cong) 1,
    68 	rewtac BufAC_Cmt_F_def,
    69 	Asm_full_simp_tac 1]);
    70 
    71 val BufAC_Cmt_empty = prove_backw "f:BufEq ==> (<>, f\\<cdot><>):BufAC_Cmt"
    72 				BufAC_Cmt_unfold [Buf_f_empty];
    73 
    74 val BufAC_Cmt_d = prove_backw "f:BufEq ==> (a\\<leadsto>\\<bottom>, f\\<cdot>(a\\<leadsto>\\<bottom>)):BufAC_Cmt" 
    75 				BufAC_Cmt_unfold [Buf_f_d];
    76 
    77 val BufAC_Cmt_d2 = prove_forw 
    78  "(Md d\\<leadsto>\\<bottom>, f\\<cdot>(Md d\\<leadsto>\\<bottom>)):BufAC_Cmt ==> f\\<cdot>(Md d\\<leadsto>\\<bottom>) = \\<bottom>" BufAC_Cmt_unfold;
    79 val BufAC_Cmt_d3 = prove_forw 
    80 "(Md d\\<leadsto>\\<bullet>\\<leadsto>x, f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)):BufAC_Cmt ==> (x, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x))):BufAC_Cmt"
    81 							BufAC_Cmt_unfold;
    82 
    83 val BufAC_Cmt_d32 = prove_forw 
    84 "(Md d\\<leadsto>\\<bullet>\\<leadsto>x, f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)):BufAC_Cmt ==> ft\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)) = Def d"
    85 							BufAC_Cmt_unfold;
    86 
    87 (**** BufAC *******************************************************************)
    88 
    89 Goalw [BufAC_def] "f \\<in> BufAC \\<Longrightarrow> f\\<cdot>(Md d\\<leadsto>\\<bottom>) = \\<bottom>";
    90 by (fast_tac (claset() addIs [BufAC_Cmt_d2, BufAC_Asm_d]) 1);
    91 qed "BufAC_f_d";
    92 
    93 Goal "(? ff:B. (!x. f\\<cdot>(a\\<leadsto>b\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x)) = \
    94    \((!x. ft\\<cdot>(f\\<cdot>(a\\<leadsto>b\\<leadsto>x)) = Def d) & (LAM x. rt\\<cdot>(f\\<cdot>(a\\<leadsto>b\\<leadsto>x))):B)";
    95 (*  this is an instance (though unification cannot handle this) of
    96 Goal "(? ff:B. (!x. f\\<cdot>x = d\\<leadsto>ff\\<cdot>x)) = \
    97    \((!x. ft\\<cdot>(f\\<cdot>x) = Def d) & (LAM x. rt\\<cdot>(f\\<cdot>x)):B)";*)
    98 by Safe_tac;
    99 by (  res_inst_tac [("P","(%x. x:B)")] ssubst 2);
   100 by (   atac 3);
   101 by (  rtac ext_cfun 2);
   102 by (  dtac spec 2);
   103 by (  dres_inst_tac [("f","rt")] cfun_arg_cong 2);
   104 by (  Asm_full_simp_tac 2);
   105 by ( Full_simp_tac 2);
   106 by (rtac bexI 2);
   107 by Auto_tac;
   108 by (dtac spec 1);
   109 by (etac exE 1);;
   110 by (etac ssubst 1);
   111 by (Simp_tac 1);
   112 qed "ex_elim_lemma";
   113 
   114 Goalw [BufAC_def] "f\\<in>BufAC \\<Longrightarrow> \\<exists>ff\\<in>BufAC. \\<forall>x. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x";
   115 by (rtac (ex_elim_lemma RS iffD2) 1);
   116 by Safe_tac;
   117 by  (fast_tac (claset() addIs [BufAC_Cmt_d32 RS Def_maximal, 
   118              monofun_cfun_arg,	BufAC_Asm_empty RS BufAC_Asm_d_req]) 1);
   119 by (auto_tac (claset() addIs [BufAC_Cmt_d3, BufAC_Asm_d_req],simpset()));
   120 qed "BufAC_f_d_req";
   121 
   122 
   123 (**** BufSt *******************************************************************)
   124 
   125 val mono_BufSt_F = prove_goalw thy [mono_def, BufSt_F_def] 
   126 		"mono BufSt_F" (K [Fast_tac 1]);
   127 
   128 val BufSt_P_fix = mono_BufSt_F RS (BufSt_P_def RS def_gfp_unfold);
   129 
   130 val BufSt_P_unfold = prove_goal thy "(h:BufSt_P) = (!s. h s\\<cdot><> = <> & \
   131 	 \ (!d x. h \\<currency>     \\<cdot>(Md d\\<leadsto>x)   =    h (Sd d)\\<cdot>x & \
   132   \   (? hh:BufSt_P. h (Sd d)\\<cdot>(\\<bullet>\\<leadsto>x)   = d\\<leadsto>(hh \\<currency>    \\<cdot>x))))" (K [
   133 	stac (BufSt_P_fix RS set_cong) 1,
   134 	rewtac BufSt_F_def,
   135 	Asm_full_simp_tac 1]);
   136 
   137 val BufSt_P_empty = prove_forw "h:BufSt_P ==> h s     \\<cdot> <>       = <>" 
   138 			BufSt_P_unfold;
   139 val BufSt_P_d     = prove_forw "h:BufSt_P ==> h  \\<currency>    \\<cdot>(Md d\\<leadsto>x) = h (Sd d)\\<cdot>x"
   140 			BufSt_P_unfold;
   141 val BufSt_P_d_req = prove_forw "h:BufSt_P ==> \\<exists>hh\\<in>BufSt_P. \
   142 				         \ h (Sd d)\\<cdot>(\\<bullet>   \\<leadsto>x) = d\\<leadsto>(hh \\<currency>    \\<cdot>x)"
   143 			BufSt_P_unfold;
   144 
   145 
   146 (**** Buf_AC_imp_Eq ***********************************************************)
   147 
   148 Goalw [BufEq_def] "BufAC \\<subseteq> BufEq";
   149 by (rtac gfp_upperbound 1);
   150 by (rewtac BufEq_F_def);
   151 by Safe_tac;
   152 by  (etac BufAC_f_d 1);
   153 by (dtac BufAC_f_d_req 1);
   154 by (Fast_tac 1);
   155 qed "Buf_AC_imp_Eq";
   156 
   157 
   158 (**** Buf_Eq_imp_AC by coinduction ********************************************)
   159 
   160 Goal "\\<forall>s f ff. f\\<in>BufEq \\<longrightarrow> ff\\<in>BufEq \\<longrightarrow> \
   161 \ s\\<in>BufAC_Asm \\<longrightarrow> stream_take n\\<cdot>(f\\<cdot>s) = stream_take n\\<cdot>(ff\\<cdot>s)";
   162 by (induct_tac "n" 1);
   163 by  (Simp_tac 1);
   164 by (strip_tac 1);
   165 by (dtac (BufAC_Asm_unfold RS iffD1) 1);
   166 by Safe_tac;
   167 by   (asm_simp_tac (simpset() addsimps [Buf_f_empty]) 1);
   168 by  (asm_simp_tac (simpset() addsimps [Buf_f_d]) 1);
   169 by (dtac (ft_eq RS iffD1) 1);
   170 by (Clarsimp_tac 1);
   171 by (REPEAT(dtac Buf_f_d_req 1));
   172 by Safe_tac;
   173 by (REPEAT(etac ssubst 1));
   174 by (Simp_tac 1);
   175 by (Fast_tac 1);
   176 qed_spec_mp "BufAC_Asm_cong_lemma";
   177 Goal "\\<lbrakk>f \\<in> BufEq; ff \\<in> BufEq; s \\<in> BufAC_Asm\\<rbrakk> \\<Longrightarrow> f\\<cdot>s = ff\\<cdot>s";
   178 by (resolve_tac stream.take_lemmas 1);
   179 by (eatac BufAC_Asm_cong_lemma 2 1);
   180 qed "BufAC_Asm_cong";
   181 
   182 Goalw [BufAC_Cmt_def] "\\<lbrakk>f \\<in> BufEq; x \\<in> BufAC_Asm\\<rbrakk> \\<Longrightarrow> (x, f\\<cdot>x) \\<in> BufAC_Cmt";
   183 by (rotate_tac ~1 1);
   184 by (etac weak_coinduct_image 1);
   185 by (rewtac BufAC_Cmt_F_def);
   186 by Safe_tac;
   187 by    (etac Buf_f_empty 1);
   188 by   (etac Buf_f_d 1);
   189 by  (dtac Buf_f_d_req 1);
   190 by  (Clarsimp_tac 1);
   191 by  (etac exI 1);
   192 by (dtac BufAC_Asm_prefix2 1);
   193 by (ftac Buf_f_d_req 1);
   194 by (Clarsimp_tac 1);
   195 by (etac ssubst 1);
   196 by (Simp_tac 1);
   197 by (datac BufAC_Asm_cong 2 1);
   198 by (etac subst 1);
   199 by (etac imageI 1);
   200 qed "Buf_Eq_imp_AC_lemma";
   201 Goalw [BufAC_def] "BufEq \\<subseteq> BufAC";
   202 by (Clarify_tac 1);
   203 by (eatac Buf_Eq_imp_AC_lemma 1 1);
   204 qed "Buf_Eq_imp_AC";
   205 
   206 (**** Buf_Eq_eq_AC ************************************************************)
   207 
   208 val Buf_Eq_eq_AC = Buf_AC_imp_Eq RS (Buf_Eq_imp_AC RS subset_antisym);
   209 
   210 
   211 (**** alternative (not strictly) stronger version of Buf_Eq *******************)
   212 
   213 val Buf_Eq_alt_imp_Eq = prove_goalw thy [BufEq_def,BufEq_alt_def] 
   214 	"BufEq_alt \\<subseteq> BufEq" (K [
   215 	rtac gfp_mono 1,
   216 	rewtac BufEq_F_def,
   217 	Fast_tac 1]);
   218 
   219 (* direct proof of "BufEq \\<subseteq> BufEq_alt" seems impossible *)
   220 
   221 
   222 Goalw [BufEq_alt_def] "BufAC <= BufEq_alt";
   223 by (rtac gfp_upperbound 1);
   224 by (fast_tac (claset() addEs [BufAC_f_d, BufAC_f_d_req]) 1);
   225 qed "Buf_AC_imp_Eq_alt";
   226 
   227 bind_thm ("Buf_Eq_imp_Eq_alt", 
   228   subset_trans OF [Buf_Eq_imp_AC, Buf_AC_imp_Eq_alt]);
   229 
   230 bind_thm ("Buf_Eq_alt_eq", 
   231  subset_antisym OF [Buf_Eq_alt_imp_Eq, Buf_Eq_imp_Eq_alt]);
   232 
   233 
   234 (**** Buf_Eq_eq_St ************************************************************)
   235 
   236 Goalw [BufSt_def, BufEq_def] "BufSt <= BufEq";
   237 by (rtac gfp_upperbound 1);
   238 by (rewtac BufEq_F_def);
   239 by Safe_tac;
   240 by ( asm_simp_tac (simpset() addsimps [BufSt_P_d, BufSt_P_empty]) 1);
   241 by (asm_simp_tac (simpset() addsimps [BufSt_P_d]) 1);
   242 by (dtac BufSt_P_d_req 1);
   243 by (Force_tac 1);
   244 qed "Buf_St_imp_Eq";
   245 
   246 Goalw [BufSt_def, BufSt_P_def] "BufEq <= BufSt";
   247 by Safe_tac;
   248 by (EVERY'[rename_tac "f", res_inst_tac 
   249         [("x","\\<lambda>s. case s of Sd d => \\<Lambda> x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1);
   250 by ( Simp_tac 1);
   251 by (etac weak_coinduct_image 1);
   252 by (rewtac BufSt_F_def); 
   253 by (Simp_tac 1);
   254 by Safe_tac;
   255 by (  EVERY'[rename_tac "s", induct_tac "s"] 1);
   256 by (   asm_simp_tac (simpset() addsimps [Buf_f_d]) 1);
   257 by (  asm_simp_tac (simpset() addsimps [Buf_f_empty]) 1);
   258 by ( Simp_tac 1);
   259 by (Simp_tac 1);
   260 by (EVERY'[rename_tac"f d x",dres_inst_tac[("d","d"),("x","x")] Buf_f_d_req] 1);
   261 by Auto_tac;
   262 qed "Buf_Eq_imp_St";
   263 
   264 bind_thm ("Buf_Eq_eq_St", Buf_St_imp_Eq RS (Buf_Eq_imp_St RS subset_antisym));
   265 
   266 
   267