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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and