Re: [isabelle] parser translation for sets

> This is an interesting idea, but it is non-trivial. The 
> syntactic treatment of sequents is designed to allow 
> expressions like G, ~A, H that represent a sequence of 
> formulas containing ~A somewhere. It relies on an encoding of 
> associative unification in higher-order unification. It 
> allows sequent calculus rules to be written naturally.
> It's not immediately clear to me how this could be added to 
> the current syntax for sets or what examples would benefit from it.

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.

Paqui Lucio                                
Dpto de LSI                    
Facultad de Informática
Paseo Manuel de Lardizabal, 1
20080-San Sebastián
e-mail: paqui.lucio at
Tfn: (+34) (9)43 015049  
Fax: (+34) (9)43 015590

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