Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014



Thanks for all the hints.
I just tried to translate the first theories. Besides renamed lemmas
which are just annoying I now encountered a serious problem:

(*) clarsimp (more precisely clarify) has changed its default behaviour.
In particular, clarsimp/clarify does not remove (all/any?) useless
assumptions anymore.
In the following example, clarsimp/clarify reduced the goal to "goal (1
subgoal): 1. C" in 2011 but clarsimp/clarify fails at this point in 2014.
Is it possible to change the default clarsimp/clarify behaviour to
remove such assumptions?
lemma "
  A=B
  \<Longrightarrow> C"
apply(clarsimp)

(*) In 2011 warnings were written to the response buffer. in
Isabelle2014/JEdit: is it possible to copy all these responses to a
certain file?

(*) Is it possible to adapt rename_tac s.t. it produces a warning if it
has not altered the state?

(*) Why is "back" considered bad "style" (according to the AFP
submission guidelines)? I removed all occurrences in my code already but
I am still curious.

(*) Has option_case been removed or has it been renamed? In 2014 it is
interpreted as a (blue) variable when it occurs in a lemma statement?

-- Sven Schneider

On 02/14/2015 01:48 PM, Larry Paulson wrote:
> Have you tried doing this port yet, so that you can report specific things that have been causing you problems? I can imagine many proofs that would go through unaltered.
>
> There are no scripts for porting from one version to another.
>
> I find it useful to run both the old and the new copies of Isabelle during porting. Then you can see where a proof goes wrong. Then the simplest thing is to see whether sledgehammer (greatly improved since 2011) can solve the problematical case.
>
> Try to rewrite some of your proofs in the structured style. That gives you control over variable names and makes future porting much easier.
>
> Larry Paulson
>
>
>> On 13 Feb 2015, at 14:56, Sven Schneider <sven.schneider.pub at gmx.de> wrote:
>>
>> Dear experts,
>>
>> are there best practices to transfer Isabelle2011 (apply-style) code to
>> Isabelle2014?
>> For example, a shell-script to execute?
>> What should be done before the transfer?
>>
>> The AFP submission guidelines seem to imply that back and isabelle
>> generated variable names are a source of backwards incompatibilty.
>> Furthermore, I have encountered renamed/removed lemmas.
>>
>> Is there a standard way to remove back? (I guess this is mostly the
>> cases where the *allE* is used in my proofs; so I can image that the
>> best way is to explicitly instantiate the P-variable.)
>>
>> Is there a standard way to remove cases where Isabelle choses variable
>> names? (I could explicitly set the names using rename_tac in all the
>> places, but how do I detect such places?)
>>
>> -- Sven Schneider
>> <0xF0E2AE90.asc>

Attachment: 0xF0E2AE90.asc
Description: application/pgp-keys



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