Re: [isabelle] lemmas-command normalizes theorems



Addition: Local_Theory.notes already performs this normalization,
so I am unable to give another name to this theorem at all!

On Fr, 2014-07-11 at 18:31 +0200, Peter Lammich wrote:
> Hi,
> 
> I stumbled over the following (unexpected, undocumented) behaviour of
> the lemmas command:
> 
> thm norm_hhf_eq
> (* (PROP ?phi ==> (!!x. PROP ?psi x)) 
>   == (!!x. PROP ?phi ==> PROP ?psi x) *)
> lemmas foo = norm_hhf_eq
> (* lemma foo: (!!x. PROP ?phi ==> PROP ?psi x) 
>   == (!!x. PROP ?phi ==> PROP ?psi x) *)
> 
> So, obviously, there is some normalization going on. What normalization
> is exactly applied? 
> The isar-ref manual says:
>   "Results are standardized before being stored, i.e. schematic
>    variables are renamed to enforce index 0 uniformly."
> 
> but nothing about other normalizations.
> 
> 
> Is there a way, other than raw isabelle-ML declaration, to avoid this
> normalization and just give a name to a list of theorems?
> 
> --
>   Peter
> 
> 






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