On 01/11/2019 18:38, David Topham wrote:
Adapting to the idea of using only whole numbers for a geometric
progression that sums over powers I am trying this approach:
It works up until trying to instantiate into induction_thm where it
breaks down since conjecture needs 2 variables: r and e (summing over
terms r^e)
If you want to prove a theorem by induction, you need to chose carefully
the property which you are using, which must be a property of a single
number, this has an impact on the complexity of the proof.
Where the theorem you are trying to prove quantifies over more than one
number, you might find that you have to do a double induction, but could
possibly avoid this if you formulate the proposition optimally (you will
then be able to prove the theorem you really want from the one that is
easier for the induction).
So, for example, if your theorem involves two natural numbers you might
do induction over the sum of the two numbers.
I attached screenshot (but I know the mailing list won't take that)
force_delete_theory "cs113" handle Fail _ => ();
new_theory "cs113";
¹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))
°
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;
That's not so easy to read!
However, I can see first that you have done your inductive definitions
in a style similar to what would work well for SML rather than the
slightly different style you need for ProofPower to automatically prove
the consistency of the definition, which will make things awkward later.
sum (n + 1) = (n + 1) + (sum n)
is preferable, and the definition of power will work better if the
second clause is:
pow b (e+1) = b*(pow b e)
To include the ProofPower script in your email try saving in a .doc file
and running conv_ascii to get
an ascii version using keywords.
I can't see how Div(1-r) is going to work for you!
Roger
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
