Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] generalize a property

Email Gateway (Aug 18 2022 at 13:26):

From: barzan stefania <stefania_barzan@yahoo.com>
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

Email Gateway (Aug 18 2022 at 13:26):

From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
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

>
>

Email Gateway (Aug 18 2022 at 13:27):

From: Amine Chaieb <ac638@cam.ac.uk>
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:

Last updated: May 03 2024 at 04:19 UTC