# Re: [isabelle] to automatically generate all the 16 lemmas corresponding to all the possible cases just from the definition of the function

Hi,

Could you simply split on the ifs in your definition of presum? Isabelles simplifier will do this with split: if_splits, or, to get more control, you might call the split method.

As first attempt, you might try to make presum a definition, ie do the pattern matching in the pairs in the rhs, then unfold presum_def, and then auto split: if_splits prod.splits

Hope that helps
Peter

-------- Original Message --------
Subject: [isabelle] to automatically generate all the 16 lemmas corresponding to all the possible cases just from the definition of the function
From: José Manuel Rodriguez Caballero
To: cl-isabelle-users at lists.cam.ac.uk
CC:

Dear Eisbach/Isabelle/ML experts,

In his paper

Eckert, Ernest J. "The group of primitive Pythagorean triangles." *Mathematics
> Magazine* 57.1 (1984): 22-27.

Eckert defined the function

fun preSumPythTwo :: "(nat * nat) ⇒ (nat * nat) ⇒ (nat * nat)" where
"preSumPythTwo (a, b) (A, B) = (if a*A > b*B
then (a*A - b*B, b*A + a*B)
else (b*A + a*B, b*B - a*A) )"

and claimed that it is associative, i.e.,

lemma SumPythIsAssocLemTwo :
fixes a b u v x y :: nat
shows "preSumPythTwo (a, b) ( preSumPythTwo (u, v) (x, y) ) =
preSumPythTwo ( preSumPythTwo (a, b) (u, v) ) (x, y)"

In order to verify his claim, I divided the problem into 16 lemmas with
relatively easy proofs, corresponding to all the possible cases, e.g.,

lemma SumPythIsAssocLemTwoId0000:
fixes a b u v x y :: nat
assumes "a*u > b*v"
and "( fst ( preSumPythTwo (a, b) (u, v) ) ) * x > ( snd (
preSumPythTwo (a, b) (u, v) ) ) * y"
and "u*x > v*y"
and "a * (fst ( preSumPythTwo (u, v) (x, y) )) > b * (snd ( preSumPythTwo
(u, v) (x, y) ))"
shows "preSumPythTwo (a, b) ( preSumPythTwo (u, v) (x, y) ) =
preSumPythTwo ( preSumPythTwo (a, b) (u, v) ) (x, y)"

I wonder if there is a tactic in Isabelle HOL in order to automatically
generate all the 16 lemmas corresponding to all the possible cases just
from the definition of the function. I ask this question because I want to
generalize Eckert's result from dimension 2 (complex numbers) to dimension
8 (octonions) and this goal can not be done without a good automation.

Sincerely yours,
José M.

• Follow-Ups:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.