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.