*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] Different behavior in Jedit and Emacs*From*: Lukas Bulwahn <bulwahn at in.tum.de>*Date*: Fri, 20 Jan 2012 17:52:50 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, bbartels at cs.tu-berlin.de*In-reply-to*: <CAAMXsiavNf2b4OqfT0w5ubg9ZAjHxCY--8_mkqXpXBUSZvVriA@mail.gmail.com>*References*: <52922E34-3B64-4933-8EE9-E333885266E0@cs.tu-berlin.de> <4F198879.6040701@in.tum.de> <4F198C66.3000206@in.tum.de> <CAAMXsiavNf2b4OqfT0w5ubg9ZAjHxCY--8_mkqXpXBUSZvVriA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:8.0) Gecko/20111124 Thunderbird/8.0

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 =

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 + if null ts then HOLogic.zero else foldl1 plus (ts @ [HOLogic.Suc_zero]))) end; On 01/20/2012 05:16 PM, Brian Huffman wrote:

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. - Brian On Fri, Jan 20, 2012 at 4:46 PM, Lukas Bulwahn<bulwahn at in.tum.de> wrote: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 On 01/20/2012 04:30 PM, Tobias Nipkow wrote:Just as another data point: I tried the development version with emacs and it works. Tobias Am 20/01/2012 16:09, schrieb Björn Bartels: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!

**References**:**[isabelle] Different behavior in Jedit and Emacs***From:*Björn Bartels

**Re: [isabelle] Different behavior in Jedit and Emacs***From:*Tobias Nipkow

**Re: [isabelle] Different behavior in Jedit and Emacs***From:*Lukas Bulwahn

**Re: [isabelle] Different behavior in Jedit and Emacs***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Different behavior in Jedit and Emacs
- Next by Date: Re: [isabelle] Different behavior in Jedit and Emacs
- Previous by Thread: Re: [isabelle] Different behavior in Jedit and Emacs
- Next by Thread: Re: [isabelle] Different behavior in Jedit and Emacs
- Cl-isabelle-users January 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list