Calculation by tactic in theorem proving

We illustrate a proof in a theorem proving system can be used not only to show the correctness of a given proposition but also as a calculator to perform symbolic calculation by giving out two case studies under Isabelle/HOL. Through simulating an imperative language, we show this method can be used to realizing various algorithms. Tactics which are designed to construct such proofs can be used to realize automatic theorem proving and fill the gap between the proof in textbook mathematic text and that in a theorem proving system.