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

```Hi Peter

Thanks for your help, it was my first time with Eisbach. I feel that it is
really practical for mathematicians.

José M.

2018-06-28 10:46 GMT+02:00 Peter Lammich <lammich at in.tum.de>:

> 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.