Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



   > Bad filename "Toylist.thy" for theory ToyList.
   Well this error message is actually very informative. The file name and 
   the name of the theory differ (in case) and that is against conventions, 
   it's rather a bug of ProofGeneral to accept your file.

You're a good teacher, Chris!  You made me think: I was supposed to
write `theory toylist', and not `theory ToyList' in my Isabelle file.

   The induct/induction/induct_tac methods just set up an induction
   proof (i.e., base cases + inductive cases) according to the
   variable you want to induct over. It's the same with pen'n'paper
   actually. What you do to solve the base case and inductive case is
   not induction, but mostly different techniques like equational
   reasoning etc.

I need to understand what you mean in order to understand how to write
Isabelle or HOL Light proofs, but what I did is certainly what
mathematicians call an inductive proof.  I showed the results were
true for lists of length 0 (just []), and then assumed the results
were true for all lists of length n, and used that to prove the
results were true for all lists length n+1.  I've heard Schemers call
that tree induction.  

-- 
Thanks again!
Bill 





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