Re: [isabelle] Legacy feature?



On Fri, 17 Aug 2007, Randy Pollack wrote:

> I frequently use the forms:
> 
>   case (constr v1 v2 ...)
>   hence j1:"..." and j2:"..." ... by auto
> 
> or 
> 
>   case (constr v1 v2 ...)
>   have j1:"..." and j2:"..." ... by fact
> 
> Both of these now give a warning:
> 
>   ### Legacy feature: implicit use of prems in assumption proof
> 
> I would not like to see these forms eliminated.  It seems natural to
> set out the known facts before working on the proof.  

This warning indicates that the above 'by' steps are actually "deceptive", 
meaning that both auto and fact failed to solve the atomic sub-proofs 
completely.

In the second case you just need to say "fact+" to produce multiple facts.  

The first case needs to be debugged by looking at the internal goal state, 
after turning ``by auto'' into ``apply auto'' temporarily.  You will then 
see that some subgoals are left over, which happen to be solvable by 
referring to prems that are not indicated explicitly in the text.  I.e. 
``by auto'' was actually wrong as a description of how the proof works.


> This naming scheme, constr.hyps and constr.prems, could be improved.

Yes, this will happen at some later stage.  At the moment we are glad 
enough to have gotten rid of alphabetically sorted bound variables.


	Makarius





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