Re: [isabelle] Isabelle2015-RC2 available for testing



This is more an indication of the flexibility of Isabelleâs inference mechanisms that you can solve the goal

	x = x

in one single step by applying the rule

	?f (Basic_BNF_LFPs.xtor ?x) = ?f ?x

or

 	?R (Basic_BNF_LFPs.xtor ?x) (Basic_BNF_LFPs.xtor ?y) = ?R ?x ?y .

Iâm sure that these theorems, in the form given, serve some useful purpose.

Larry Paulson


> On 1 May 2015, at 15:32, C. Diekmann <diekmann at in.tum.de> wrote:
> 
> Hi,
> 
> I guess there are some superfluous lemmas in 2015-RC2 in Main:
> 
> theory Scratch
> imports Main
> begin
> 
> lemma "x = x"
> Auto solve_direct: The current goal can be solved directly with
>  BNF_Composition.DEADID.map_ident: ?t = ?t
>  BNF_Composition.DEADID.rel_refl: ?x = ?x
>  Basic_BNF_LFPs.xtor_rel: ?R (Basic_BNF_LFPs.xtor ?x)
> (Basic_BNF_LFPs.xtor ?y) = ?R ?x ?y
>  Basic_BNF_LFPs.xtor_set: ?f (Basic_BNF_LFPs.xtor ?x) = ?f ?x
>  HOL.refl: ?t = ?t
> 
> Cheers,
>  Cornelius
> 





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