equal
deleted
inserted
replaced
245 qed "Buf_St_imp_Eq"; |
245 qed "Buf_St_imp_Eq"; |
246 |
246 |
247 Goalw [BufSt_def, BufSt_P_def] "BufEq <= BufSt"; |
247 Goalw [BufSt_def, BufSt_P_def] "BufEq <= BufSt"; |
248 by Safe_tac; |
248 by Safe_tac; |
249 by (EVERY'[rename_tac "f", res_inst_tac |
249 by (EVERY'[rename_tac "f", res_inst_tac |
250 [("x","\\<lambda>s. case s of Sd d => \\<Lambda>x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1); |
250 [("x","\\<lambda>s. case s of Sd d => \\<Lambda> x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1); |
251 by ( Simp_tac 1); |
251 by ( Simp_tac 1); |
252 by (etac weak_coinduct_image 1); |
252 by (etac weak_coinduct_image 1); |
253 by (rewtac BufSt_F_def); |
253 by (rewtac BufSt_F_def); |
254 by (Simp_tac 1); |
254 by (Simp_tac 1); |
255 by Safe_tac; |
255 by Safe_tac; |