117 |
117 |
118 use "Tools/typedef_package.ML" setup TypedefPackage.setup |
118 use "Tools/typedef_package.ML" setup TypedefPackage.setup |
119 use "Tools/typecopy_package.ML" setup TypecopyPackage.setup |
119 use "Tools/typecopy_package.ML" setup TypecopyPackage.setup |
120 use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup |
120 use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup |
121 |
121 |
122 |
|
123 text {* This class is just a workaround for classes without parameters; |
|
124 it shall disappear as soon as possible. *} |
|
125 |
|
126 class itself = |
|
127 fixes itself :: "'a itself" |
|
128 |
|
129 setup {* |
|
130 let fun add_itself tyco thy = |
|
131 let |
|
132 val vs = Name.names Name.context "'a" |
|
133 (replicate (Sign.arity_number thy tyco) @{sort type}); |
|
134 val ty = Type (tyco, map TFree vs); |
|
135 val lhs = Const (@{const_name itself}, Term.itselfT ty); |
|
136 val rhs = Logic.mk_type ty; |
|
137 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
|
138 in |
|
139 thy |
|
140 |> TheoryTarget.instantiation ([tyco], vs, @{sort itself}) |
|
141 |> `(fn lthy => Syntax.check_term lthy eq) |
|
142 |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) |
|
143 |> snd |
|
144 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
|
145 |> LocalTheory.exit_global |
|
146 end |
|
147 in TypedefPackage.interpretation add_itself end |
|
148 *} |
|
149 |
|
150 instantiation bool :: itself |
|
151 begin |
|
152 |
|
153 definition "itself = TYPE(bool)" |
|
154 |
|
155 instance .. |
|
156 |
|
157 end |
122 end |
158 |
|
159 instantiation "fun" :: ("type", "type") itself |
|
160 begin |
|
161 |
|
162 definition "itself = TYPE('a \<Rightarrow> 'b)" |
|
163 |
|
164 instance .. |
|
165 |
|
166 end |
|
167 |
|
168 hide (open) const itself |
|
169 |
|
170 end |
|