[isabelle] generalize a property



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.