author | wenzelm |
Fri, 16 Mar 2012 18:20:12 +0100 | |
changeset 46961 | 5c6955f487e5 |
parent 46949 | 94aa7b81bcf6 |
child 47091 | d5cd13aca90b |
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 |
45598 | 9 |
val quotient_def: |
10 |
(binding * typ option * mixfix) option * (Attrib.binding * (term * term)) -> |
|
45279 | 11 |
local_theory -> Quotient_Info.quotconsts * local_theory |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
|
45598 | 13 |
val quotient_def_cmd: |
14 |
(binding * string option * mixfix) option * (Attrib.binding * (string * string)) -> |
|
45279 | 15 |
local_theory -> Quotient_Info.quotconsts * local_theory |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
|
37561
19fca77829ea
mixfix can be given for automatically lifted constants
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
17 |
val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory -> |
45279 | 18 |
Quotient_Info.quotconsts * local_theory |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
end; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
structure Quotient_Def: QUOTIENT_DEF = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
struct |
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 |
(** Interface and Syntax Setup **) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
(* The ML-interface for a quotient definition takes |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
as argument: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
- an optional binding and mixfix annotation |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
- attributes |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
- the new constant as term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
- the rhs of the definition as term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
|
45279 | 34 |
It stores the qconst_info in the quotconsts data slot. |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
|
41444 | 36 |
Restriction: At the moment the left- and right-hand |
37 |
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
|
38 |
*) |
41444 | 39 |
fun error_msg bind str = |
40 |
let |
|
41 |
val name = Binding.name_of bind |
|
42 |
val pos = Position.str_of (Binding.pos_of bind) |
|
43 |
in |
|
44 |
error ("Head of quotient_definition " ^ |
|
45 |
quote str ^ " differs from declaration " ^ name ^ pos) |
|
46 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
|
46909 | 48 |
fun gen_quotient_def prep_vars prep_term (raw_var, ((name, atts), (lhs_raw, rhs_raw))) lthy = |
41444 | 49 |
let |
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
50 |
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
|
51 |
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
|
52 |
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
|
53 |
val rhs = prep_term NONE ctxt rhs_raw |
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
54 |
|
41444 | 55 |
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
56 |
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
|
57 |
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
|
58 |
|
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
59 |
val var = |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
60 |
(case vars of |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
61 |
[] => (Binding.name lhs_str, NoSyn) |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
62 |
| [(binding, _, mx)] => |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
63 |
if Variable.check_name binding = lhs_str then (binding, mx) |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
64 |
else error_msg binding lhs_str |
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
65 |
| _ => raise Match) |
41444 | 66 |
|
45797 | 67 |
val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs |
45826 | 68 |
val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm)) |
41444 | 69 |
val (_, prop') = Local_Defs.cert_def lthy prop |
70 |
val (_, newrhs) = Local_Defs.abs_def prop' |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
71 |
|
46909 | 72 |
val ((trm, (_ , thm)), lthy') = |
73 |
Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
74 |
|
41444 | 75 |
(* data storage *) |
76 |
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
|
77 |
|
45292
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset
|
78 |
val lthy'' = lthy' |
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset
|
79 |
|> Local_Theory.declaration {syntax = false, pervasive = true} |
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset
|
80 |
(fn phi => |
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset
|
81 |
(case Quotient_Info.transform_quotconsts phi qconst_data of |
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset
|
82 |
qcinfo as {qconst = Const (c, _), ...} => |
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset
|
83 |
Quotient_Info.update_quotconsts c qcinfo |
90106a351a11
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents:
45291
diff
changeset
|
84 |
| _ => I)); |
41444 | 85 |
in |
86 |
(qconst_data, lthy'') |
|
87 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
88 |
|
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
|
89 |
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
|
90 |
Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I) |
45598 | 91 |
|
92 |
fun read_term' cnstr ctxt = |
|
45929
d7d6c8cfb6f6
removing some debug output in quotient_definition
bulwahn
parents:
45826
diff
changeset
|
93 |
check_term' cnstr ctxt o Syntax.parse_term ctxt |
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
|
94 |
|
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
|
95 |
val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term' |
45598 | 96 |
val quotient_def_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
|
97 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
98 |
|
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
99 |
(* 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
|
100 |
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt = |
41444 | 101 |
let |
102 |
val rty = fastype_of rconst |
|
41451 | 103 |
val qty = Quotient_Term.derive_qtyp ctxt qtys rty |
41444 | 104 |
val lhs = Free (qconst_name, qty) |
105 |
in |
|
43608
294570668f25
parse term in auxiliary context augmented with variable;
krauss
parents:
42494
diff
changeset
|
106 |
quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt |
41444 | 107 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
108 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
109 |
(* command *) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
110 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
111 |
val _ = |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
112 |
Outer_Syntax.local_theory @{command_spec "quotient_definition"} |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
113 |
"definition for constants over the quotient type" |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
114 |
(Scan.option Parse_Spec.constdecl -- |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
115 |
Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term)) |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
116 |
>> (snd oo quotient_def_cmd)) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
117 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
118 |
end; (* structure *) |