Re: [isabelle] Untyped formalized systems are wrong (blog post)



> I will explain what "\cap" should do:
> 
> Before investing my time into learning HOL, I want to ask whether the following is possible at all to implement in HOL:
> 
> Let "sets" and "filters" are unique tags.
> 
> Let "(sets, X)" denotes a ZF set X understood a plain set.
> Let "(filters, F)" denotes a filter whose ZF value is F. Let filters are ordered REVERSE to set-theoretic inclusion, that is I want:
> "(filters, F1) \subseteq (filters, F2) <-> F1 \supseteq F2".
> 
> Can we define the following with pattern matching (not with enumerating all possible cases, to be extensible without rewriting existing matching code)?
> 
> "(sets, X1) \cap (sets, X2)" to be different than "(filters, X1) \cap (filters, X2)" where X1 and X2 are filters (in the sense as filters are defined in ZF).
> 
> I want "(sets, X1) \cap (sets, X2) = (sets, X1\cap X2)" and "(filters, X1) \cap (filters, X2)" to mean "(filters, Y)" where Y is the coarsest filter which is finer than both X1 and X2.


Instead of using tags/tuples you would probably rather use something like

datatype myuniverse = Sets of ZF | Filters of ZF   

you can then define your operation "\cap", but you would need to also say what Sets (A) \cap Filters (B) should mean (for example, "arbitrary", if there is no good definition for this)

If you don't want both to live in the same universe, then also

datatype sets = Sets of ZF
datatype filters = Filters of ZF

could work. Due to overloading, you could still define "\cap" to operate on sets*filters if you should need that. 

I think you should definitely go for it and try to formalize your stuff using HOLZF to see if that works. I think it is definitely worth the time anyway as you will learn more about both HOL and your stuff.

- Steven




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