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#171onwards.
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
