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



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