# Re: [isabelle] generalize a property

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

`
`

Barzan,
To express something like
(g1 (^) a1') times (g2 (^) a2') times... times (g87(^) (a87'))
in a general way, you want to use foldl or foldr,
> read "foldl";

`val it = Const ("List.foldl", "('a => 'b => 'a) => 'a => 'b List.list =>
``'a")
`: Term.term
> read "foldr";

`val it = Const ("List.foldr", "('a => 'b => 'b) => 'a List.list => 'b =>
``'b")
`: Term.term
Jeremy

`
``
`

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