Re: [isabelle] generalize a property


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,

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.