section ‹Miscellaneous Nonuniform Codatatype Definitions›
theory Misc_Types
imports "../code/BNF_Nonuniform_Fixpoint" "~~/src/HOL/Library/FSet"
begin
nonuniform_datatype 'a plist = PNil | PCons (phd: 'a) (ptl: "('a × 'a) plist")
nonuniform_datatype 'a ptree = Node 'a "'a pforest"
and 'a pforest = Nil | Cons "'a ptree" "('a × 'a) pforest"
nonuniform_datatype 'a plist' = PNil |
PCons1 (phd: 'a) (ptl1: "'a plist'") |
PCons2 (phd: 'a) (ptl2: "('a × 'a) plist'")
nonuniform_datatype ('a, 'b) tplist = PNil 'b | PCons 'a "('a × 'a, unit + 'b) tplist"
nonuniform_datatype 'a stree = Node 'a "'a fset stree fset"
nonuniform_codatatype 'a pstream = Cons (pshd: 'a) (pstl: "('a × 'a) pstream")
nonuniform_codatatype ('a, 'b) alter = C 'a "('b, 'a) alter" | D 'a "('b, 'a) alter"
nonuniform_datatype 'a lam = Var 'a | App "'a lam" "'a lam" | Abs "'a option lam"
datatype 'a node = Node2 'a 'a | Node3 'a 'a 'a
datatype 'a digit = One 'a | Two 'a 'a | Three 'a 'a 'a | Four 'a 'a 'a 'a
nonuniform_datatype 'a finger_tree =
Empty
| Single 'a
| Depth "'a digit" "'a node finger_tree" "'a digit"
nonuniform_datatype 'a bootstrapped_queue =
Empty
| Queue (front: "'a list") (middle: "(unit ⇒ 'a list) bootstrapped_queue")
(len_front_middle: "nat") (rear: "'a list") (len_rear: "nat")
datatype 'a zero_one = Zero | One 'a
datatype 'a one_two = One 'a | Two 'a 'a
nonuniform_datatype 'a implicit_queue =
Shallow "'a zero_one"
| Deep (front: "'a one_two") (middle: "unit ⇒ ('a × 'a) implicit_queue") (rear: "'a zero_one")
datatype 'a D = Zero | One 'a | Two 'a 'a | Three 'a 'a 'a
nonuniform_datatype 'a implicit_dequeue =
Shallow "'a D"
| Deep (front: "'a D") (middle: "unit ⇒ ('a × 'a) implicit_dequeue") (rear: "'a D")
nonuniform_datatype 'a simple_catenable_dequeue =
Shallow "'a implicit_dequeue"
| Deep (front: "'a implicit_dequeue") (middle: "unit ⇒ 'a implicit_dequeue simple_catenable_dequeue") (rear: "'a implicit_dequeue")
nonuniform_datatype ('a, 'b) cyclist = CNil | CCons (chd: 'a) (ctl: "('a, 'b option) cyclist") | Cycle 'b
nonuniform_codatatype 'a pllist = PLNil | PLCons (plhd: 'a) (pltl: "('a × 'a) pllist")
end