equal
deleted
inserted
replaced
1 theory QuotMain |
1 theory QuotMain |
2 imports QuotScript QuotList Prove |
2 imports QuotScript QuotList Prove |
3 uses ("quotient.ML") |
3 uses ("quotient.ML") |
4 begin |
4 begin |
|
5 |
|
6 ML {* Attrib.empty_binding *} |
5 |
7 |
6 locale QUOT_TYPE = |
8 locale QUOT_TYPE = |
7 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
9 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
8 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
10 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
9 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
11 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
298 |
300 |
299 ML {* |
301 ML {* |
300 fun build_qenv lthy qtys = |
302 fun build_qenv lthy qtys = |
301 let |
303 let |
302 val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy) |
304 val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy) |
303 val tsig = Sign.tsig_of (ProofContext.theory_of lthy) |
305 val thy = ProofContext.theory_of lthy |
304 |
306 |
305 fun find_assoc ((qty', rty')::rest) qty = |
307 fun find_assoc ((qty', rty')::rest) qty = |
306 let |
308 let |
307 val inst = Type.typ_match tsig (qty', qty) Vartab.empty |
309 val inst = Sign.typ_match thy (qty', qty) Vartab.empty |
308 in |
310 in |
309 (Envir.norm_type inst qty, Envir.norm_type inst rty') |
311 (Envir.norm_type inst qty, Envir.norm_type inst rty') |
310 end |
312 end |
311 | find_assoc [] qty = |
313 | find_assoc [] qty = |
312 let |
314 let |
341 ML {* |
343 ML {* |
342 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
344 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
343 OuterKeyword.thy_decl (qd_parser >> parse_qd_spec) |
345 OuterKeyword.thy_decl (qd_parser >> parse_qd_spec) |
344 *} |
346 *} |
345 |
347 |
346 (* ML {* show_all_types := true *} *) |
|
347 |
348 |
348 section {* ATOMIZE *} |
349 section {* ATOMIZE *} |
349 |
350 |
350 text {* |
351 text {* |
351 Unabs_def converts a definition given as |
352 Unabs_def converts a definition given as |