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



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.



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