*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] fun, int, nat*From*: "Perry James" <perry at dsrg.org>*Date*: Mon, 11 Aug 2008 16:25:26 -0400*Cc*: George Karabotsos <g_karab at encs.concordia.ca>, Patrice Chalin <chalin at encs.concordia.ca>*Sender*: perry.dsrg at gmail.com

Hi all, I'm having trouble with functions, integers and nats. In the theory below, a "product" function is defined that takes the bounds as integers and evaluates it using the "prod" function, which is based on the nat that is their difference. In both cases, the "body" parameter is a function to generate each factor from its index. In the examples it is always the identity function. I had hoped that all of the lemmas would go though automatically, but that's not the case for "test" and "lemma_3". test leaves the subgoal 6 = prod 3 1 (%x. x) lemma_3 leaves the subgoal 0 < i ==> i * prod (nat (i - 1)) 1 (%x. x) = prod (nat i) 1 (%x. x) 1) Is there a way to see the value of a function? For example, to see the result of evaluating "prod 3 1 (%x. x)" ? If it is not 6, it would explain why the 2 lemmas don't go through, but I'm also not able to prove "6 ~= prod 3 1 (%x. x)". 2) Is there better form for these functions that would let the proofs go though automatically? 3) If this is the standard way of writing such functions, how can I get the proofs to go through? (hopefully with something similar to simp or auto) 4) Assuming they can be proved, would it be safe to mark these five lemmas as "[simp]" for use in later theories? Thanks for your help, Perry ========= fact.thy ========= theory fact imports Main begin fun prod :: "nat => int => (int => int) => int" where "prod 0 lo body = 1" | "prod (Suc n) lo body = (body (int n + lo)) * (prod n lo body)" fun product :: "int => int => (int => int) => int" where "product lo hi body = prod (nat (hi - lo + 1)) lo body" lemma test: "6 == product 1 3 (%x. x)" apply auto oops lemma lemma_1: "[|(i::int) > 0 ; nat(-1 + i) = n |] ==> (prod (nat(-1 + i)) 1 (%x. x) * i= prod (Suc n) 1 (%x. x))" by auto lemma lemma_2: "[|(i::int) > 0 ; nat(-1 + i) = n |] ==> (i * prod (nat(-1 + i)) 1 (%x. x) = prod (Suc n) 1 (%x. x))" by auto lemma nat_Suc_i_Min_1_eq_i: "0 < i --> (Suc (nat (-1 + i))) = (nat i)" by auto lemma lemma_3: "[| 0 < (i::int) |] ==> (i * prod (nat(i - 1)) 1 (%x. x) = prod (nat i ) 1 (%x. x))" apply auto oops end

**Follow-Ups**:**Re: [isabelle] fun, int, nat***From:*Amine Chaieb

- Previous by Date: Re: [isabelle] Type variable names in inherited locales
- Next by Date: Re: [isabelle] fun, int, nat
- Previous by Thread: Re: [isabelle] Type variable names in inherited locales
- Next by Thread: Re: [isabelle] fun, int, nat
- Cl-isabelle-users August 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list