[isabelle] fun, int, nat



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




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