Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals (Q7361305)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Nested_Multisets_Ordinals
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals |
AFP entry Nested_Multisets_Ordinals |
Statements
12 November 2016
0 references
Jasmin Christian Blanchette
0 references
Mathias Fleury
0 references
Dmitriy Traytel
0 references
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals (English)
0 references
This Isabelle/HOL formalization introduces a nested multiset datatype and defines Dershowitz and Manna's nested multiset order. The order is proved well founded and linear. By removing one constructor, we transform the nested multisets into hereditary multisets. These are isomorphic to the syntactic ordinals—the ordinals can be recursively expressed in Cantor normal form. Addition, subtraction, multiplication, and linear orders are provided on this type.
0 references
