author | krauss |
Tue, 05 Jul 2011 09:54:39 +0200 | |
changeset 43663 | e8c80bbc0c5d |
parent 43608 | 294570668f25 |
child 45279 | 89a17197cb98 |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Tools/Quotient/quotient_def.ML |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Cezary Kaliszyk and Christian Urban |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
|
35788 | 4 |
Definitions for constants on quotient types. |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
signature QUOTIENT_DEF = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
sig |
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
9 |
val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) -> |
37530
70d03844b2f9
export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
36960
diff
changeset
|
10 |
local_theory -> Quotient_Info.qconsts_info * local_theory |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
|
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
12 |
val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) -> |
37530
70d03844b2f9
export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
36960
diff
changeset
|
13 |
local_theory -> Quotient_Info.qconsts_info * local_theory |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
|
37561
19fca77829ea
mixfix can be given for automatically lifted constants
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
15 |
val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory -> |
37530
70d03844b2f9
export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
36960
diff
changeset
|
16 |
Quotient_Info.qconsts_info * local_theory |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
end; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
structure Quotient_Def: QUOTIENT_DEF = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
struct |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
(** Interface and Syntax Setup **) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
(* The ML-interface for a quotient definition takes |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
as argument: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
- an optional binding and mixfix annotation |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
- attributes |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
- the new constant as term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
- the rhs of the definition as term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
|
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
32 |
It stores the qconst_info in the qconsts data slot. |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
|
41444 | 34 |
Restriction: At the moment the left- and right-hand |
35 |
side of the definition must be a constant. |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
*) |
41444 | 37 |
fun error_msg bind str = |
38 |
let |
|
39 |
val name = Binding.name_of bind |
|
40 |
val pos = Position.str_of (Binding.pos_of bind) |
|
41 |
in |
|
42 |
error ("Head of quotient_definition " ^ |
|
43 |
quote str ^ " differs from declaration " ^ name ^ pos) |
|
44 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
|
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
46 |
fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy = |
41444 | 47 |
let |
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
48 |
val (vars, ctxt) = prep_vars (the_list raw_var) lthy |
43663
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
49 |
val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE) |
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
50 |
val lhs = prep_term T_opt ctxt lhs_raw |
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
51 |
val rhs = prep_term NONE ctxt rhs_raw |
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
52 |
|
41444 | 53 |
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
54 |
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
|
55 |
val _ = if is_Const rhs then () else warning "The definiens is not a constant" |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
|
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
57 |
val var = |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
58 |
(case vars of |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
59 |
[] => (Binding.name lhs_str, NoSyn) |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
60 |
| [(binding, _, mx)] => |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
61 |
if Variable.check_name binding = lhs_str then (binding, mx) |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
62 |
else error_msg binding lhs_str |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
63 |
| _ => raise Match) |
41444 | 64 |
|
41451 | 65 |
val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
41444 | 66 |
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
67 |
val (_, prop') = Local_Defs.cert_def lthy prop |
|
68 |
val (_, newrhs) = Local_Defs.abs_def prop' |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
|
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
70 |
val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
71 |
|
41444 | 72 |
(* data storage *) |
73 |
val qconst_data = {qconst = trm, rconst = rhs, def = thm} |
|
37530
70d03844b2f9
export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
36960
diff
changeset
|
74 |
|
41451 | 75 |
fun qcinfo phi = Quotient_Info.transform_qconsts phi qconst_data |
41444 | 76 |
fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) |
41451 | 77 |
val lthy'' = |
78 |
Local_Theory.declaration true |
|
79 |
(fn phi => Quotient_Info.qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' |
|
41444 | 80 |
in |
81 |
(qconst_data, lthy'') |
|
82 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
83 |
|
43663
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
84 |
fun check_term' cnstr ctxt = |
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
85 |
Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I) |
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
86 |
fun read_term' cnstr ctxt = check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt |
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
87 |
|
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
88 |
val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term' |
e8c80bbc0c5d
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents:
43608
diff
changeset
|
89 |
val quotdef_cmd = gen_quotient_def Proof_Context.read_vars read_term' |
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
90 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
91 |
|
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
92 |
(* a wrapper for automatically lifting a raw constant *) |
37561
19fca77829ea
mixfix can be given for automatically lifted constants
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
93 |
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt = |
41444 | 94 |
let |
95 |
val rty = fastype_of rconst |
|
41451 | 96 |
val qty = Quotient_Term.derive_qtyp ctxt qtys rty |
41444 | 97 |
val lhs = Free (qconst_name, qty) |
98 |
in |
|
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
99 |
quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt |
41444 | 100 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
101 |
|
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
102 |
(* parser and command *) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
103 |
val quotdef_parser = |
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
104 |
Scan.option Parse_Spec.constdecl -- |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
105 |
Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term)) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
106 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
107 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
108 |
Outer_Syntax.local_theory "quotient_definition" |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
109 |
"definition for constants over the quotient type" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
110 |
Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd)) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
111 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
112 |
end; (* structure *) |