Re: [isabelle] parser translation for sets



> Is this much better than simply checking for set membership?

I think that it allows an easier and more natural way of reasoning 
with sequent than the membersphip and subseteq checks, but 
maybe I miss something about how using sets better than I do it.

> 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.

I see, thanks for the advice, I had imagine that semantics issues
should be more complicate than in the set case because the higher-order
unification. However, once you have proved the meta-logical properties
of your calculus (if possible) using a this more intrincate semantics, 
the resulting calculus is, in my opinion, more suitable for users that
are accustomed to sequents. 

Please, could you tell me how to have access to more information 
(public .thy files and so on, if possible)
about your attempt for incorporating the Sequents.thy mechanism into HOL.
In particular, how do you solve the incompatibility between Pure and CPure.
Thanks in advance,
Paqui

> 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.