319 in |
319 in |
320 map (find_assoc qenv) qtys |
320 map (find_assoc qenv) qtys |
321 end |
321 end |
322 *} |
322 *} |
323 |
323 |
324 ML {* |
324 |
325 val qd_parser = |
325 ML {* |
326 (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- |
326 fun quotdef_cmd qenv ((bind, qty_, mx), (attr, prop)) lthy = |
327 (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) |
327 let |
328 *} |
328 val (lhs_, rhs) = Logic.dest_equals prop |
329 |
329 in |
330 ML {* |
330 make_const_def bind rhs mx qenv lthy |
331 fun parse_qd_spec (qtystrs, ((bind, tystr, mx), (attr__, propstr))) lthy = |
331 end |
|
332 *} |
|
333 |
|
334 ML {* |
|
335 val quotdef_parser = |
|
336 Scan.option (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- |
|
337 (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- |
|
338 OuterParse.prop)) >> OuterParse.triple2 |
|
339 *} |
|
340 |
|
341 ML {* |
|
342 fun quotdef (qtystrs, (bind, tystr, mx), (attr, propstr)) lthy = |
332 let |
343 let |
333 val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs |
344 val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) (the qtystrs) |
334 val qenv = build_qenv lthy qtys |
345 val qenv = build_qenv lthy qtys |
335 val qty = Syntax.parse_typ lthy (the tystr) |> Syntax.check_typ lthy |
346 val qty = Option.map (Syntax.check_typ lthy o Syntax.parse_typ lthy) tystr |
336 val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy |
347 val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy |
337 val (lhs, rhs) = Logic.dest_equals prop |
348 in |
338 in |
349 quotdef_cmd qenv ((bind, qty, mx), (attr, prop)) lthy |> snd |
339 make_const_def bind rhs mx qenv lthy |> snd |
|
340 end |
350 end |
341 *} |
351 *} |
342 |
352 |
343 ML {* |
353 ML {* |
344 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
354 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
345 OuterKeyword.thy_decl (qd_parser >> parse_qd_spec) |
355 OuterKeyword.thy_decl (quotdef_parser >> quotdef) |
346 *} |
356 *} |
347 |
|
348 |
357 |
349 section {* ATOMIZE *} |
358 section {* ATOMIZE *} |
350 |
359 |
351 text {* |
360 text {* |
352 Unabs_def converts a definition given as |
361 Unabs_def converts a definition given as |