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.




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