# Re: [isabelle] generalize a property

Hi,

`It seems like you need a version of setprod that works in set-based
``locales and not just on classes. This kind of problems starts showing up
``more often.
`

`If you had classes (i.e. no carrier set G --- I hope I am interpreting
``your formalization right) then
`
you could write e.g. "setprod (%i. g i (^) a i) {1..n}
for (g1 (^) an) times (gn (^) an) times... times (gn (^) (an))
where times is also denoted by *.

`Within a set-based locale, you might need to use the fold or fold_image
``iterator to "re"define setprod. Have a look at HOL/FiniteSet.thy to see
``how setprod is defined in terms of fold_image.
`

`A "hack" here is also to use foldl or foldr (proofs with foldr are
``easier in general) over lists --- the length of the list will give you
``the n above, but you have to "artificially" enforce that you have the
``same number of g's and a's either by enforcing the two list to have the
``same length or by just using a list of pairs (gi,ai).
`
Hope I am understanding your message right and that this helps,
Amine.
barzan stefania wrote:

Dear all,

`In Isabelle i always deal with simple algebra properties.
``I
``proved that having g,h,y,t in (G,times), (a, b, a1, b1, c, c1 :: int) and this two equations:
`` (g (^) a) times (h (^) b)= t times (y
``(^) c)
`` and (g (^) a1) times (h (^) b1)= t times (y (^) c1)
`` ==>(g (^) (a-a1)) times (h (^) (b-b1))= y (^) (c-c1) is true.
``
``How can
``i generalize this for finitely many base elements?
``(for example to prove that
`having (g1 (^) a1) times (g2 (^) a2) times... times (g87 (^) (a87))= t

`times (y (^) c)
`` and (g1 (^) a1') times (g2 (^) a2') times... times (g87
``(^) (a87'))= t times (y (^) c1)
`` to get true (g1 (^) (a1-a1')) times (g2
``(^) (a2-a2')) times... times (g87 (^) (a87-a87')))= y (^) (c-c1)).
``Is
``there a way at all? Is is not right the way i look at the problem?
``
``
`Thank you very much!
Stefania Barzan

`
`

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