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.