# Re: [isabelle] parser translation for sets

Is this much better than simply checking for set membership?

`We tried to incorporate the Sequents.thy mechanism into HOL for our
``DOVE environment and
``found that all such rules needed to be augmented with a monotonicity
``check. The trick. as
``I recall, in Sequents.thy is to translate $F, A to something like F
``(A) and allow higher-order
``unification to solve the sequence membership problem. When you
``actually try to model a semantics
``for this, you find the need to check that the higher order function F
``has the property of adding
``A to the sequence membership. Thus you are really just moving the
``semantic problem from one place
`to another.
On 02/02/2007, at 9:13 PM, Paqui Lucio wrote:

`The idea is to allow set expressions like "S1 Un {~A}" (or "S1 Un
``{~A} Un
`S2") for representing

`a set containing "~A" somewhere and, at the same time, naming the
``remaining
`of the set by "S1". This would be

`very useful to implement sequents calculi using de set.thy of
``Isabelle/HOL
``to represent the antecedent (and the consequent in the symmetric
``case). I am
``trying to do it, but I am a beginner Isabelle's user and
``parse_translations
`are a bit hard for me.

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