Re: [isabelle] Why no HOL set type in 2008?



Brendan, you are certainly right that in some situations proofs are less
automatic. We were aware of this but found that in the theories we have
access to it was not too bad, only a few times per theory on average.
However we concede that depending on your application this could be
worse. I'm very sorry if you were particularly affected.

Concerning boolean algebras (and lattices), we do intend to develop this
connection further.

Regards
Tobias

Dr. Brendan Patrick Mahony schrieb:
> 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.
> 
> 





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