Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
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
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
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 ------------------------------
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)
" @ 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"
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
theorem rev_rev [simp]: "rev(rev xs) = xs"
(* done *)
This archive was generated by a fusion of
Pipermail (Mailman edition) and