*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Thu, 03 May 2012 10:57:33 +0200*In-reply-to*: <201205030429.q434TQw9027705@poisson.math.northwestern.edu>*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> <201205030429.q434TQw9027705@poisson.math.northwestern.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:8.0) Gecko/20120104 Icedove/8.0

On 03.05.2012 06:29, Bill Richter wrote:

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.

-- Lars

**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

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

- 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