David
The ascii may not be readable, but it can be converted back to ext, or
to utf8:
ⓈHOLCONST
│ sum:ℕ→ℕ
├──
│ ∀n⦁ sum 0 = 0 ∧ sum (n) = n + (sum n-1)
■
ⓈHOLCONST
│ pow:ℕ→ℕ→ℕ
├──
│ ∀b e⦁ (pow b 0) = 1 ∧ (pow b e) = b * (pow b (e - 1))
■
=SML
val ex92 = ⌜λ n r⦁ sum (pow r n) = (1 - (pow r (n - 1)) Div (1 - r))⌝;
val UI = ∀_elim ex92 induction_thm;
val lemma1 = rewrite_rule [] UI;
putting in utf8 would be better, but you probably wouldn't find that easy.
(the next release of ProofPower will make it easier)
To understand why your definitions don't work, consider what they say
when you instantiate n or e to 0.
You get conflicting and nonsensical assertions about sum 0 and pow b 0.
When you use similar definitions in SML its OK because execution is
sequential and the second reading is never reached (for the zero
argument), but in logic you can reach the second clause and you can
derive a contradiction.
Also, it is now clear (even though you don't actually state your goal),
that you are trying to reason about the sum of a segment of series, but
the function "sum" you have (almost) defined gives the sum of an initial
segment of the natural numbers, not of an arbitrary series.
The "sum" you want takes a function as well as a number, so it has type:
sum:(ℕ→ℕ) → ℕ → ℕ
When it comes to doing induction, apart from the need to chose the
proposition carefully which I mentioned earlier, you obtain the required
property by eliminating only the outermost universal, so you would have:
val ex92 = ⌜λ n⦁ ∀r⦁ sum (pow r n) = (1 - (pow r (n - 1)) Div (1 - r))⌝;
Then you would have a term of the right type to instantiate induction thm.
Roger
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
