CODEWITHSUNDEEP
isabelletheorem-proving
krokodil
krokodil

Reputation: 1366

equivalence of arithmetic expressions using algebra_simps

In Programming and Proving in Isabelle/HOL there is Exercise 2.4 which suggests to use 'algebra_simps' on simple arithmetic expressions, represented as 'datatype exp'. Could somebody give an example how some simple properties of such expressions could be proven using algebra_simps? For example 'Mult a b = Mult b a'?

In general I am trying to prove equivalence of simple arithmetic expressions represented in similar form (with limited set of operators).

Upvotes: 1

Views: 221

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8298

If you have defined your eval function appropriately, you can prove the property you gave in your example like this:

lemma Mult_comm: "eval (Mult a b) x = eval (Mult b a) x"
  by simp

algebra_simps is just a collection of basic simplification rules for groups and rings (such as the integers, in this case). They have nothing to do with this particular example. You can look at the lemmas contained by typing thm algebra_simps.

For this particular proof, you don't actually need algebra_simps, because commutativity of integer multiplication is already a default simplifier rule anyway.

So, to show how to use algebra_simps, consider an example where you actually do need them: right distributivity of multiplication:

lemma Mult_distrib_right: "eval (Mult (Add a b) c) x = eval (Add (Mult a c) (Mult b c)) x"

If you just try apply simp on this, you will get stuck with the goal

(eval a x + eval b x) * eval c x =
  eval a x * eval c x + eval b x * eval c x

Luckily, the rule algebra_simps(4) is a rule that says just that: thm algebra_simps(4) will show you that this rule is (?a + ?b) * ?c = ?a * ?c + ?b * ?c. Isabelle's simplifier will apply it automatically if you tell it to use the algebra_simps rules, by doing:

apply (simp add: algebra_simps)

instead of

apply simp

Upvotes: 2

Related Questions