Re: [isabelle] Different behavior in Jedit and Emacs



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





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