equal
deleted
inserted
replaced
158 |
158 |
159 (**** Buf_Eq_imp_AC by coinduction ********************************************) |
159 (**** Buf_Eq_imp_AC by coinduction ********************************************) |
160 |
160 |
161 Goal "\\<forall>s f ff. f\\<in>BufEq \\<longrightarrow> ff\\<in>BufEq \\<longrightarrow> \ |
161 Goal "\\<forall>s f ff. f\\<in>BufEq \\<longrightarrow> ff\\<in>BufEq \\<longrightarrow> \ |
162 \ s\\<in>BufAC_Asm \\<longrightarrow> stream_take n\\<cdot>(f\\<cdot>s) = stream_take n\\<cdot>(ff\\<cdot>s)"; |
162 \ s\\<in>BufAC_Asm \\<longrightarrow> stream_take n\\<cdot>(f\\<cdot>s) = stream_take n\\<cdot>(ff\\<cdot>s)"; |
163 by (nat_ind_tac "n" 1); |
163 by (induct_tac "n" 1); |
164 by (Simp_tac 1); |
164 by (Simp_tac 1); |
165 by (strip_tac 1); |
165 by (strip_tac 1); |
166 by (dtac (BufAC_Asm_unfold RS iffD1) 1); |
166 by (dtac (BufAC_Asm_unfold RS iffD1) 1); |
167 by Safe_tac; |
167 by Safe_tac; |
168 by (asm_simp_tac (simpset() addsimps [Buf_f_empty]) 1); |
168 by (asm_simp_tac (simpset() addsimps [Buf_f_empty]) 1); |