*To*: "'Dr. Brendan Patrick Mahony'" <brendan.mahony at dsto.defence.gov.au>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] parser translation for sets*From*: "Paqui Lucio" <paqui.lucio at ehu.es>*Date*: Mon, 5 Feb 2007 11:28:48 +0100*In-reply-to*: <A31FC35F-3A52-4448-8015-EF6C01DA69C1@dsto.defence.gov.au>*Thread-index*: AcdIsUxO1jL6N0x5TEesaci2w4OQIgAWuhwg

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

**References**:**Re: [isabelle] parser translation for sets***From:*Dr. Brendan Patrick Mahony

- Previous by Date: Re: [isabelle] parser translation for sets
- Next by Date: [isabelle] Properties on intervals
- Previous by Thread: Re: [isabelle] parser translation for sets
- Next by Thread: Re: [isabelle] Pure and CPure non-compatible
- Cl-isabelle-users February 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list