1 theory QuotMain |
1 theory QuotMain |
2 imports QuotScript QuotList Prove |
2 imports QuotScript QuotList Prove |
3 uses ("quotient.ML") |
3 uses ("quotient_info.ML") |
|
4 ("quotient.ML") |
4 begin |
5 begin |
|
6 |
|
7 ML {* Attrib.empty_binding *} |
5 |
8 |
6 locale QUOT_TYPE = |
9 locale QUOT_TYPE = |
7 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
10 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
8 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
11 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
9 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
12 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
135 end |
138 end |
136 |
139 |
137 |
140 |
138 section {* type definition for the quotient type *} |
141 section {* type definition for the quotient type *} |
139 |
142 |
|
143 use "quotient_info.ML" |
140 use "quotient.ML" |
144 use "quotient.ML" |
141 |
145 |
142 declare [[map list = (map, LIST_REL)]] |
146 declare [[map list = (map, LIST_REL)]] |
143 declare [[map * = (prod_fun, prod_rel)]] |
147 declare [[map * = (prod_fun, prod_rel)]] |
144 declare [[map "fun" = (fun_map, FUN_REL)]] |
148 declare [[map "fun" = (fun_map, FUN_REL)]] |
298 |
302 |
299 ML {* |
303 ML {* |
300 fun build_qenv lthy qtys = |
304 fun build_qenv lthy qtys = |
301 let |
305 let |
302 val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy) |
306 val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy) |
303 val tsig = Sign.tsig_of (ProofContext.theory_of lthy) |
307 val thy = ProofContext.theory_of lthy |
304 |
308 |
305 fun find_assoc ((qty', rty')::rest) qty = |
309 fun find_assoc ((qty', rty')::rest) qty = |
306 let |
310 let |
307 val inst = Type.typ_match tsig (qty', qty) Vartab.empty |
311 val inst = Sign.typ_match thy (qty', qty) Vartab.empty |
308 in |
312 in |
309 (Envir.norm_type inst qty, Envir.norm_type inst rty') |
313 (Envir.norm_type inst qty, Envir.norm_type inst rty') |
310 end |
314 end |
311 | find_assoc [] qty = |
315 | find_assoc [] qty = |
312 let |
316 let |
317 in |
321 in |
318 map (find_assoc qenv) qtys |
322 map (find_assoc qenv) qtys |
319 end |
323 end |
320 *} |
324 *} |
321 |
325 |
322 ML {* |
326 |
323 val qd_parser = |
327 ML {* |
324 (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- |
328 fun quotdef_cmd qenv ((bind, qty_, mx), (attr, prop)) lthy = |
325 (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) |
329 let |
326 *} |
330 val (lhs_, rhs) = Logic.dest_equals prop |
327 |
331 in |
328 ML {* |
332 make_const_def bind rhs mx qenv lthy |
329 fun parse_qd_spec (qtystrs, ((bind, tystr, mx), (attr__, propstr))) lthy = |
333 end |
|
334 *} |
|
335 |
|
336 ML {* |
|
337 val quotdef_parser = |
|
338 Scan.option (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- |
|
339 (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- |
|
340 OuterParse.prop)) >> OuterParse.triple2 |
|
341 *} |
|
342 |
|
343 ML {* |
|
344 fun quotdef (qtystrs, (bind, tystr, mx), (attr, propstr)) lthy = |
330 let |
345 let |
331 val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs |
346 val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) (the qtystrs) |
332 val qenv = build_qenv lthy qtys |
347 val qenv = build_qenv lthy qtys |
333 val qty = Syntax.parse_typ lthy (the tystr) |> Syntax.check_typ lthy |
348 val qty = Option.map (Syntax.check_typ lthy o Syntax.parse_typ lthy) tystr |
334 val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy |
349 val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy |
335 val (lhs, rhs) = Logic.dest_equals prop |
350 in |
336 in |
351 quotdef_cmd qenv ((bind, qty, mx), (attr, prop)) lthy |> snd |
337 make_const_def bind rhs mx qenv lthy |> snd |
|
338 end |
352 end |
339 *} |
353 *} |
340 |
354 |
341 ML {* |
355 ML {* |
342 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
356 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
343 OuterKeyword.thy_decl (qd_parser >> parse_qd_spec) |
357 OuterKeyword.thy_decl (quotdef_parser >> quotdef) |
344 *} |
358 *} |
345 |
|
346 (* ML {* show_all_types := true *} *) |
|
347 |
359 |
348 section {* ATOMIZE *} |
360 section {* ATOMIZE *} |
349 |
361 |
350 text {* |
362 text {* |
351 Unabs_def converts a definition given as |
363 Unabs_def converts a definition given as |