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





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