40   Expressions (Proof Pearl)}

    40   Expressions (Proof Pearl)}

    41 \author{Chunhan Wu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}

    41 \author{Chunhan Wu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}

    42 \institute{PLA University of Science and Technology, China \and TU Munich, Germany}

    42 \institute{PLA University of Science and Technology, China \and TU Munich, Germany}

    43 \maketitle

    43 \maketitle

    44 

    44 

    45 \begin{abstract} 

    46 \begin{abstract} 

    46 There are numerous textbooks on regular languages. Nearly all of them

    47 There are numerous textbooks on regular languages. Nearly all of them

    47 introduce the subject by describing finite automata and only mentioning on the

    48 introduce the subject by describing finite automata and only mentioning on the

    48 side a connection with regular expressions. Unfortunately, automata are difficult

    49 side a connection with regular expressions. Unfortunately, automata are difficult

    49 to formalise in HOL-based theorem provers. The reason is that

    50 to formalise in HOL-based theorem provers. The reason is that