Error analysis of digital filters using HOL theorem proving