Re: [isabelle] Parameterized Types?



Title: RE: [isabelle] Parameterized Types?

On Wed 3/29/2006 2:04 PM, Brian Huffman wrote:
|
| As a simpler alternative, you can give coset_def as an argument to simp or
| unfold, which avoids the problems with instantiating type variables:
|
| lemma "EX s. S = coset I s ==> EX s. S = {i + s | i. i \<in> I}"
|   proof -
|     assume "EX s. S = coset I s"
|     then show "EX s. S = {i + s | i. i \<in> I}"
|     by (unfold coset_def)
|   qed
|
| - Brian
|

Brian,

Thanks for your patient and speedy reply.  I do not know why I didn't think of unfold, but it solved the problem immediately.  It has been useful in other situations. 

Robert Lamar



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