Email Gateway (Aug 18 2022 at 18:58): Email Gateway (Aug 18 2022 at 18:58):From: Björn Bartels <bbartels@cs.tu-berlin.de>
Hi all,
we just came across the following problem when using the datatype command. The following datatype definition works when using Jedit but does not work when using Emacs as interface. In the previous distribution the example used to work with Emacs as well.
theory test
imports Main
begin
datatype 'a tree =
leaf "'a"
| node "nat \<Rightarrow> 'a tree"
datatype 'a dtype = constr "'a tree"
end
When using Emacs, we get the following error message:
*** Proof failed.
*** dtype_size fa (constr tree) = 0
*** 1. Suc 0 = 0
*** 1 unsolved goal(s)!
*** The error(s) above occurred for the goal statement:
*** dtype_size fa (constr tree) = 0
Thanks for any suggestions!
Email Gateway (Aug 18 2022 at 18:58):From: Tobias Nipkow <nipkow@in.tum.de>
Just as another data point: I tried the development version with emacs
and it works.
Tobias
Email Gateway (Aug 18 2022 at 18:58):From: Lukas Bulwahn <bulwahn@in.tum.de>
I tried it myself as well on the development version (changeset
693d8d7bc3cd - the current tip):
It works if you switch on quick_and_dirty, but it fails if you switch it
off.
This succeeds:
ML {* quick_and_dirty := true *}
datatype 'a dtype = constr "'a tree"
But this fails:
ML {* quick_and_dirty := false *}
datatype 'a dtype = constr "'a tree"
Just a short explanation, why this differs:
In quick-and-dirty mode, we actually skip proofs, which are
automatically generated by packages, and just provide the theorems
without proof.
Switching it off, the package will actually perform the proof, but in
the case mentioned here, this proof method fails.
It seems that your default settings actually differ on the two
interfaces, JEdit and Emacs.
We will have to investigate why the proof method actually breaks down in
this case.
Lukas
Email Gateway (Aug 18 2022 at 18:58):From: Brian Huffman <huffman@in.tum.de>
Congratulations Björn, you've found a soundness bug in the datatype
package! At least in quick and dirty mode, the datatype package
generates some unproven "theorems" that are contradictory. Here's a
proof of False that works if you are in quick and dirty mode:
datatype 'a tree = leaf "'a" | node "nat => 'a tree"
datatype 'a dtype = constr "'a tree"
lemma "False"
proof -
have "dtype_size fa (constr tree) = Suc 0"
unfolding dtype_size_def by simp
also have "dtype_size fa (constr tree) = 0"
by (rule dtype.size(1))
finally show "False"
by simp
qed
This is a good reminder why quick and dirty mode is a bad idea. We
should definitely make sure that the default is set to "off" in all
future releases, for both ProofGeneral and jEdit.
Email Gateway (Aug 18 2022 at 18:58):From: Lukas Bulwahn <bulwahn@in.tum.de>
On changeset 693d8d7bc3cd, the issue is somehow hidden in the different
conditions (if null ts ...) of these two source code positions below.
Maybe, one of two authors of this file could take a closer look at this
point.
Lukas
diff -r 693d8d7bc3cd src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML Fri Jan 20 09:28:54 2012 +0100
+++ b/src/HOL/Tools/Function/size.ML Fri Jan 20 17:47:23 2012 +0100
@@ -105,7 +105,7 @@
else us, i, j + 1))
(cargs cargs' Ts) ([], 0, k);
val t =
if null ts andalso (not b orelse not (exists (is_poly thy)
cargs'))
if null ts andalso (not b orelse not (exists (is_poly thy)
cargs'))
then HOLogic.zero
else foldl1 plus (ts @ [HOLogic.Suc_zero])
in
@@ -182,7 +182,7 @@
HOLogic.mk_Trueprop (HOLogic.mk_eq
(size_const $ list_comb (Const (cname, Ts ---> T),
map2 (curry Free) tnames Ts),
if null ts then HOLogic.zero
Email Gateway (Aug 18 2022 at 18:58):From: Peter Gammie <peteg42@gmail.com>
"sorry" only works if quick and dirty is switched on. I use that a lot when developing a proof interactively, as I expect everyone does.
cheers
peter
Email Gateway (Aug 18 2022 at 18:58):From: Brian Huffman <huffman@in.tum.de>
Actually, you can use "sorry" in ProofGeneral even with
quick-and-dirty mode switched off, if you manually step through the
file(s) containing "sorry".
You only get the "Cheating requires quick_and_dirty mode!" error if an
import statement causes Isabelle to load a theory file containing
"sorry". The workaround is to pre-load any offending files
individually.
Of course, if you have a large collection of interconnected theories,
and you use "sorry" in many different files, this might be a pain. But
in that case, you are always free to turn quick-and-dirty mode back
on, at your own risk!
Email Gateway (Aug 18 2022 at 18:59):From: Stefan Berghofer <berghofe@in.tum.de>
Björn Bartels wrote:
Hi all,
we just came across the following problem when using the datatype command. The following datatype definition works when using Jedit but does not work when using Emacs as interface. In the previous distribution the example used to work with Emacs as well.
Hi Björn,
thanks for reporting this. The problem has now been fixed in the current
repository version of Isabelle, see
http://isabelle.in.tum.de/repos/isabelle/rev/fd21bbcbe61b
Greetings,
Stefan
Last updated: Apr 30 2024 at 08:19 UTC