*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Why no HOL set type in 2008?*From*: "Dr. Brendan Patrick Mahony" <brendan.mahony at dsto.defence.gov.au>*Date*: Mon, 15 Dec 2008 10:03:25 +1030*In-reply-to*: <49422735.4010900@in.tum.de>*References*: <540EA156-C864-4B6C-8A6D-DE24F46DE0B2@dsto.defence.gov.au> <49422735.4010900@in.tum.de>

One of those times when I regret my wasted education as a Z weenie, but my amateur viewpoint really sees this as concerning. Some points of debate follow. On 12/12/2008, at 7:26 PM, Tobias Nipkow wrote: > There were two main motivations: > > 1. Avoiding pointless coercions between the two worlds. In > particular, given a predicate P you had to write {x. P(x)} to turn > it into a set. Now you have to worry less as to whether 'a set or 'a > => bool is more appropriate. Isn't this an argument for using ZF over HOL? Surely there are benefits to strong typing? Probably the people who actually worry about this question, want to worry about it. More likely, people who always chose 'a => bool, occasionally realise that {f x | x y. t x y} is a way more convenient (and disciplined) way of writing (% z. (! x y. z = f x & t x y)) and get annoyed they need a coercion to make use it. In any case, they won't use set notations very often, I guarantee that the predicate oriented user will not write { (x, y) | x y. t x y} instead of (% x y. t x y). A proper theory of predicates would be more to their liking, with a (generalised) predicate comprehension and predicate conjunction, disjunction, and negation operators. This would pretty much need little more than the introduction of a boolean_algebra class and the generalisation of the boolean operators to this class. Biggest irony of all, the Collect coercion operator hasn't gone away as it is needed to support print translations. Only the strong typing on sets has gone! Why does this cause problems (other than the problems always caused by weak typing)? In effect, this equates sets with meta-abstraction, as there is already effectively no object-level "function" type in HOL. Thus set instances suffer from the same "higher-order unification" problems that make arg_cong and fun_cong a pain to work with in Isar. It is now necessary to instantiate set reasoning rules far more often than previously. Isar only allows a single reasoning set. With a distinguished set type, this could be worked around to a degree. Now there is no way to say, "just do set-style reasoning here." Auto fails to terminate in many more situations now. I'll continue evaluating the situation, but the chances are that I'll be investigating the feasibility making a copy of Set.thy with datatype 'a set = Collect "'a => bool" replacing types 'a set = "'a => bool". Brendan IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.

**Follow-Ups**:**Re: [isabelle] Why no HOL set type in 2008?***From:*Tobias Nipkow

**References**:**[isabelle] Why no HOL set type in 2008?***From:*Dr. Brendan Patrick Mahony

**Re: [isabelle] Why no HOL set type in 2008?***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Integer Division
- Next by Date: [isabelle] CfP: ICTAC'09
- Previous by Thread: Re: [isabelle] Why no HOL set type in 2008?
- Next by Thread: Re: [isabelle] Why no HOL set type in 2008?
- Cl-isabelle-users December 2008 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