equal
deleted
inserted
replaced
78 |
78 |
79 subsection {* Step 2: Define types, prove class instances *} |
79 subsection {* Step 2: Define types, prove class instances *} |
80 |
80 |
81 text {* Use @{text pcpodef} with the appropriate type combinator. *} |
81 text {* Use @{text pcpodef} with the appropriate type combinator. *} |
82 |
82 |
83 pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))" |
83 pcpodef 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))" |
84 by (rule defl_set_bottom, rule adm_defl_set) |
84 by (rule defl_set_bottom, rule adm_defl_set) |
85 |
85 |
86 pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))" |
86 pcpodef 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))" |
87 by (rule defl_set_bottom, rule adm_defl_set) |
87 by (rule defl_set_bottom, rule adm_defl_set) |
88 |
88 |
89 pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))" |
89 pcpodef 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))" |
90 by (rule defl_set_bottom, rule adm_defl_set) |
90 by (rule defl_set_bottom, rule adm_defl_set) |
91 |
91 |
92 text {* Prove rep instance using lemma @{text typedef_rep_class}. *} |
92 text {* Prove rep instance using lemma @{text typedef_rep_class}. *} |
93 |
93 |
94 instantiation foo :: ("domain") "domain" |
94 instantiation foo :: ("domain") "domain" |