Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



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.
Well this error message is actually very informative. The file name and the name of the theory differ (in case) and that is against conventions, it's rather a bug of ProofGeneral to accept your file.

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.
The induct/induction/induct_tac methods just set up an induction proof (i.e., base cases + inductive cases) according to the variable you want to induct over. It's the same with pen'n'paper actually. What you do to solve the base case and inductive case is not induction, but mostly different techniques like equational reasoning etc.

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





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