[isabelle] Simple question about theory parameter

Dear all,

Here is a simplified version of my problem, which should have a simple answer.

I wish to prove a bunch of theorems about an arbitrary set S of numbers that contains a designated element, say 1. For example, S intersect S and S union S will both contain 1, etc.

Thereafter, I wish to get theorems for free about particular sets that contain 1. For example, {1,2,3} intersect {1,2,3} contains 1, etc.

What is the recommended way to do this in Isabelle?


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