*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 22:38:44 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FA0BBE7.4060302@jaist.ac.jp> (message from Christian Sternagel on Wed, 02 May 2012 13:45:27 +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>

Thanks for the example, Chris! I'll have to study it. Your links https://isabelle.in.tum.de/community/Course_Material seemed more about learning Isabelle (and so relevant to me) than teaching undergraduate math courses. But I know Julien Narboux and others are thinking that way. I took your advice to read the tutorial, and have a bug report: 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. So I can't do any of the sec 2.3 tests in jedit! I think I got some red wiggly lines of yours, and definitely a red-and-white do not enter sign on the left of the first line theory ToyList. So instead I opened it in Proof Generaland everything works. (localhost)Isabelle2011-1> bin/isabelle emacs Toylist.thy & I get the message proof (prove): step 2 goal: No subgoals! By commenting things out and looking at the Proof General output, I can understand the proof, which I'll explain. It's about Scheme-type lists, built with cons (although no car & cdr), and the two simple list functions append (@) and reverse. They inductively prove xs @ [] = xs (xs @ ys) @ zs = xs @ (ys @ zs) rev(xs @ ys) = (rev ys) @ (rev xs) rev(rev xs) = xs with each proof using the previous results. We prove each statements is true for xs = [], and then we prove that the statement for xs implies the statement for x # xs. Let's just do the last one: The base case is easy: rev(rev []) = rev([]) = [] Now note that rev([x]) = rev(x # []) = rev([]) @ (x # []) = [] @ (x # []) = x # [] 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 *) ------------------------------ Toylist.thy ------------------------------ theory ToyList imports Datatype begin datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) (* This is the append function: *) primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where "[] @ ys = ys" | "(x # xs) @ ys = x # (xs @ ys)" primrec rev :: "'a list \<Rightarrow> 'a list" where "rev [] = []" | "rev (x # xs) = (rev xs) @ (x # [])" lemma app_Nil2 [simp]: "xs @ [] = xs" apply(induct_tac xs) apply(auto) done lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" apply(induct_tac xs) apply(auto) done lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" apply(induct_tac xs) apply(auto) done theorem rev_rev [simp]: "rev(rev xs) = xs" apply(induct_tac xs) apply(auto) (* done *) -- Best, Bill

**Follow-Ups**:**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:*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

- 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