Re: [isabelle] fun, int, nat

Hi Perry,

The problem here the usual Suc/0 vs. numerals representation of things. Function prod is written by pattern matching and its clauses are normally aded to the simplifier. Now these match terms in your subgoals only if they have the 0/Suc _ pattern. Obviously 3 is not such a pattern, since it is internally some binary bit string.

One magic set of simp rules you can use here is "nat_number" which will turn 3 into Suc (Suc (Suc 0)) after which, you can proceed the simplification.

The same problem disturbs the proof of your second goal where you need a subgoal saying that nat i = Suc (nat (i - 1)) since i >0, after this your statement should be proved by simp.

In such cases, and only when I really need this, I derive a lemma saying that prod n ... = (if n = 0 then ... else f (n) * prod (n - 1) ...)

this is better for evaluation by the simplifier.

Furthermore you can see the value of a function using value (just interactive).

There are also methods which basically "prove" by evaluation.

Hope it helps,

Perry James wrote:
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
   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,

========= fact.thy =========
theory fact
imports Main

fun prod :: "nat => int => (int => int) => int"
  "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"
"product lo hi body = prod (nat (hi - lo + 1)) lo body"

lemma test:
  "6 == product 1 3 (%x. x)"
  apply auto

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.