[Logiweb] Induction example

[Klaus Ebbe Grue]

Hi Logiweb at diku.dk,

An example of a proof by induction has been placed at
http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano

A new base page is available at
http://www.diku.dk/~grue/logiweb/20050502/home/grue/base
(the old base pages are still where they used to be, so there is no need 
to move to the new one).

The new base page has an updated version of unification which allows e.g.
Aa:Ab:a=>b=>a to be instantiated to b=>b=>b without variable clashes. The 
new unification tactic first renames bound meta-variables to fresh 
variables and then does what it used to do.

The peano page corrects some errors and, furthermore, gives examples of 
hypoothetical reasoning. It also gives examples of facilities that I have 
not mentioned at lectures: Macro definitions, local macro defintions, and 
proof of theorems with side conditions.

Finally, the page 'cheats': All lemmas I have been too lazy to prove are 
stated as rules. That is quite convenient during development. You can do 
the same provided (1) that you final delivery does not cheat (2) you copy 
the source of the peano page and work on that. You cannot just refer to 
the peano page since you cannot add more rules to a theory on another 
page.

Have fun

Klaus