*To*: Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Wed, 2 May 2012 23:29:26 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FA200BE.10006@jaist.ac.jp> (message from Christian Sternagel on Thu, 03 May 2012 12:51:26 +0900)*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.7030904@jaist.ac.jp> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.4060302@jaist.ac.jp> <201205030338.q433ciL9026861@poisson.math.northwestern.edu> <4FA200BE.10006@jaist.ac.jp>

> 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

**Follow-Ups**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Lars Noschinski

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list