Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

Thanks for the example, Chris!  I'll have to study it.  Your links 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
       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
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"
apply(induct_tac xs)

lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
apply(induct_tac xs)

lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
apply(induct_tac xs)

theorem rev_rev [simp]: "rev(rev xs) = xs"
apply(induct_tac xs)
(* done *)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.