Re: [isabelle] case rule and OF



Le 21/09/2016 Ã 09:10, Andreas Lochbihler a Ãcrit :

When you instantiate some premises of a rule with OF, all the case name
information gets erased (because it is not trivial to determine how they
would have to be shifted). However, you normally do not instantiate
premises manually in case distinctions, but appropriately declare the
first n premises to be unified with the facts chained in using the
"consumes n" attribute. "lemma assumes ... obtains ..." implicitly sets
"consumes" appropriately. Hence, you merely have to chain in the
necessary assumptions, as I had shown in my example.

This is perfectly clear, thanks a lot for the explanations.





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