*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Thu, 03 May 2012 12:51:26 +0900*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201205030338.q433ciL9026861@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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:12.0) Gecko/20120424 Thunderbird/12.0

Dear Bill, On 05/03/2012 12:38 PM, Bill Richter wrote:

I learned interesting Isabelle from Proof General, but not jedit. I learned the main thing that I wanted to know: we you can use fancy symbols Mizar disallows, like ⇒, in isabelle proofs. I pasted in the tutorial.pdf file Toylist.thy below of sec 2.3, with the last `done' commented out. I opened it in jedit: (localhost)Isabelle2011-1> bin/isabelle jedit Toylist.thy& and get only the error message Bad filename "Toylist.thy" for theory ToyList.

Now assume theorem rev_rev is true xs. Then using lemma rev_app, the induction assumption and the above, we prove the induction equation: rev(rev (x # xs)) = rev(rev(xs) @ [x]) = rev([x]) @ rev(rev(xs)) = (x # []) @ xs = x # ([] @ xs) = x # xs That's a nice proof. I don't know why we have to use strategy auto as well as induct_tac, because it sure looks like just induction to me.

But if we comment out just the apply(auto) in the proof of theorem rev_rev, we get the output proof (prove): step 1 goal (2 subgoals): 1. rev (rev []) = [] 2. \<And>a list. rev (rev list) = list \<Longrightarrow> rev (rev (a # list)) = a # list Well, isabelle did nothing put state the inductive case. It didn't even prove the base case. Page 12 of tutorial.pdf says apply(induct_tac xs) This tells Isabelle to perform induction on variable xs. Apparently that's not true: to perform induction we need also auto. If we instead comment out app_assoc and rev_app, we get message goal (1 subgoal): 1. \<And>a list. rev (rev list) = list \<Longrightarrow> rev (rev list @ a # []) = a # list *)

cheers chris

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

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

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

- 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