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

```Hi José,

here is an Eisbach version to generate 16 cases. I changed the
definition of preSumPythTwo to manual case splitting isntead of pattern
matching,
in order to split all products in a first step ... may be this can be
modified to the original definition.

--
Peter

p.s.
apply (auto split!: if_splits)
yields 32 subgoals, i.e., is still somewhat redundant.

---------------------------

theory Scratch
imports Main "HOL-Eisbach.Eisbach"
begin

definition 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) )"

method repeat_all_new methods m =
(m; repeat_all_new ‹m›)?

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)"
unfolding preSumPythTwo_def
apply (clarsimp simp only: split: prod.split)
apply (repeat_all_new ‹(split if_splits, (intro impI conjI)?)›)

16 subgoals here.

On Do, 2018-06-28 at 09:37 +0200, Peter Lammich wrote:
> 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.

```

• References:

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