Email Gateway (Aug 18 2022 at 12:17): Email Gateway (Aug 18 2022 at 12:17):From: Perry James <perry@dsrg.org>
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
Last updated: May 03 2024 at 08:18 UTC