*To*: Victor Porton <porton at yandex.ru>*Subject*: Re: [isabelle] Untyped formalized systems are wrong (blog post)*From*: Steven Obua <steven.obua at googlemail.com>*Date*: Sat, 9 Jul 2011 15:22:21 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <526071310216452@web75.yandex.ru>*References*: <1319931310144510@web97.yandex.ru> <8B1DEAC2-0593-4F73-9B2B-636B4575408A@googlemail.com> <655171310154225@web136.yandex.ru> <D12FBAAB-9ADD-481F-9AEF-70CAD48E2E6D@googlemail.com> <226801310157524@web45.yandex.ru> <C8AF9434-D5AF-423B-83B3-804902BFBFCA@googlemail.com> <168591310214618@web11.yandex.ru> <571FE939-B8D8-442F-9D44-6C8148489CC4@googlemail.com> <526071310216452@web75.yandex.ru>

> 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

**References**:**[isabelle] Untyped formalized systems are wrong (blog post)***From:*Victor Porton

**Re: [isabelle] Untyped formalized systems are wrong (blog post)***From:*Steven Obua

**Re: [isabelle] Untyped formalized systems are wrong (blog post)***From:*Victor Porton

**Re: [isabelle] Untyped formalized systems are wrong (blog post)***From:*Steven Obua

**Re: [isabelle] Untyped formalized systems are wrong (blog post)***From:*Victor Porton

**Re: [isabelle] Untyped formalized systems are wrong (blog post)***From:*Steven Obua

**Re: [isabelle] Untyped formalized systems are wrong (blog post)***From:*Victor Porton

**Re: [isabelle] Untyped formalized systems are wrong (blog post)***From:*Steven Obua

**Re: [isabelle] Untyped formalized systems are wrong (blog post)***From:*Victor Porton

- Previous by Date: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Next by Date: [isabelle] Surprisingly this verifies
- Previous by Thread: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Next by Thread: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Cl-isabelle-users July 2011 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