Re: [isabelle] universal quantifiers vs. schematic variables



On 05.10.2015 04:51, Alfio Martini wrote:
> lemma nat_induct0:
>   fixes n
>   assumes "P 0" and "ân. P n â P (Suc n)"
>   shows "P n"
> 
> If I would formulate this rule, I would (unnecessarily I see), write the
> conclusion as "!n. P n", since this is what the rule allows me
> to infer if the premises are satisfied. From the logical point of view, it
> would have a clearer and more natural reading.

Indeed, Isabelle normalizes all rules by (a) moving universal
quantifiers as far outside as possible and (b) replacing outermost
universal quantifiers by schematic variables. This canonical format (I
believe it is called Hereditarily Harrop Formula in the sources) allows
a consistent handling of such formulas in the implementation.





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