Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
On 05/03/2012 12:38 PM, Bill Richter wrote:
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.
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.
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.
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 *)
This archive was generated by a fusion of
Pipermail (Mailman edition) and