There's a chunk of stuff in examples/set-theory/hol_sets/cardinalTheory,
including, for example, the fact that k x k = k.
Michael
On 09/08/2013, at 17:15, "Ramana Kumar" <[email protected]> wrote:
> HOL Light has a decent body of theory about cardinality inequalities and
> arithmetic for sets-as-predicates.
> For example, see
> https://code.google.com/p/hol-light/source/browse/trunk/sets.ml#2774 and
> https://code.google.com/p/hol-light/source/browse/trunk/Library/card.ml#171
> onwards.
>
> As far as I know, HOL4 only has a bit of theory about cardinality of finite
> sets.
> But before I start on porting many of the results above, I'd love to find out
> that I'm wrong...
>
> Anybody know of any theory about cardinality in HOL4, or of its certain
> absence?
> ------------------------------------------------------------------------------
> Get 100% visibility into Java/.NET code with AppDynamics Lite!
> It's a free troubleshooting tool designed for production.
> Get down to code-level detail for bottlenecks, with <2% overhead.
> Download for free and get started troubleshooting in minutes.
> http://pubads.g.doubleclick.net/gampad/clk?id=48897031&iu=/4140/ostg.clktrk
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Get 100% visibility into Java/.NET code with AppDynamics Lite!
It's a free troubleshooting tool designed for production.
Get down to code-level detail for bottlenecks, with <2% overhead.
Download for free and get started troubleshooting in minutes.
http://pubads.g.doubleclick.net/gampad/clk?id=48897031&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
