161 end |
161 end |
162 |
162 |
163 (* syntax setup *) |
163 (* syntax setup *) |
164 local structure P = OuterParse in |
164 local structure P = OuterParse in |
165 |
165 |
166 fun mk_typedef (qty, mx, rty, rel_trm) lthy = |
166 fun mk_typedef (qty_name, mx, rty, rel_trm) lthy = |
167 let |
167 let |
168 val (qty_name, _) = Term.dest_Type qty |
|
169 |
|
170 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
168 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
171 val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm) |
169 val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm) |
172 |
170 |
173 fun after_qed thms lthy = |
171 fun after_qed thms lthy = |
174 let |
172 let |
179 in |
177 in |
180 Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy |
178 Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy |
181 end |
179 end |
182 |
180 |
183 val quottype_parser = |
181 val quottype_parser = |
184 P.typ -- P.opt_infix -- |
182 P.short_ident -- P.opt_infix -- |
185 (P.$$$ "=" |-- P.typ) -- |
183 (P.$$$ "=" |-- P.typ) -- |
186 (P.$$$ "/" |-- P.term) |
184 (P.$$$ "/" |-- P.term) |
187 |
185 |
188 fun mk_typedef_cmd (((qstr, mx), rstr), rel_str) lthy = |
186 fun mk_typedef_cmd (((qstr, mx), rstr), rel_str) lthy = |
189 let |
187 let |
190 val qty = Syntax.parse_typ lthy qstr |
|
191 val rty = Syntax.parse_typ lthy rstr |
188 val rty = Syntax.parse_typ lthy rstr |
192 val rel_trm = Syntax.parse_term lthy rel_str |
189 val rel_trm = Syntax.parse_term lthy rel_str |
193 |> Syntax.check_term lthy |
190 |> Syntax.check_term lthy |
194 in |
191 in |
195 mk_typedef (qty, mx, rty, rel_trm) lthy |
192 mk_typedef (qstr, mx, rty, rel_trm) lthy |
196 end |
193 end |
197 |
194 |
198 val _ = OuterKeyword.keyword "/" |
195 val _ = OuterKeyword.keyword "/" |
199 |
196 |
200 val _ = |
197 val _ = |