Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014



Dear Sven,

I (or more precisely the NEWS file) can answer some of your questions.

On 20.02.2015 14:59, Sven Schneider wrote:
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)
From the NEWS file:

* Standard tactics and proof methods such as "clarsimp", "auto" and
"safe" now preserve equality hypotheses "x = expr" where x is a free
variable.  Locale assumptions and chained facts containing "x"
continue to be useful.  The new method "hypsubst_thin" and the
configuration option "hypsubst_thin" (within the attribute name space)
restore the previous behavior.  INCOMPATIBILITY, especially where
induction is done after these methods or when the names of free and
bound variables clash.  As first approximation, old proofs may be
repaired by "using [[hypsubst_thin = true]]" in the critical spot.

If you have many occurrences, you could also

declare [[hypsubst_thin = true]]

globally.

(*) 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.
Because it makes your proof rely on the order in which the HO-unifier produces its results.
(*) 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?
From the NEWS file:
  - The generated constants "xxx_case" and "xxx_rec" have been renamed
    "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
    INCOMPATIBILITY.

Dmitriy








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