author | wenzelm |
Wed, 27 Apr 2011 20:58:40 +0200 | |
changeset 42494 | eef1a23c9077 |
parent 42357 | 3305f573294e |
child 43608 | 294570668f25 |
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 |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
val quotient_def: (binding option * mixfix) * (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 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
val quotdef_cmd: (binding option * mixfix) * (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 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy = |
41444 | 47 |
let |
48 |
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
|
49 |
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
|
50 |
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
|
51 |
|
41444 | 52 |
fun sanity_test NONE _ = true |
53 |
| sanity_test (SOME bind) str = |
|
42494 | 54 |
if Variable.check_name bind = str then true |
41444 | 55 |
else error_msg bind str |
56 |
||
57 |
val _ = sanity_test optbind lhs_str |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
58 |
|
41444 | 59 |
val qconst_bname = Binding.name lhs_str |
41451 | 60 |
val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
41444 | 61 |
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
62 |
val (_, prop') = Local_Defs.cert_def lthy prop |
|
63 |
val (_, newrhs) = Local_Defs.abs_def prop' |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
64 |
|
41444 | 65 |
val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
66 |
|
41444 | 67 |
(* data storage *) |
68 |
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
|
69 |
|
41451 | 70 |
fun qcinfo phi = Quotient_Info.transform_qconsts phi qconst_data |
41444 | 71 |
fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) |
41451 | 72 |
val lthy'' = |
73 |
Local_Theory.declaration true |
|
74 |
(fn phi => Quotient_Info.qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' |
|
41444 | 75 |
in |
76 |
(qconst_data, lthy'') |
|
77 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
78 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |
fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy = |
41444 | 80 |
let |
81 |
val lhs = Syntax.read_term lthy lhs_str |
|
82 |
val rhs = Syntax.read_term lthy rhs_str |
|
83 |
val lthy' = Variable.declare_term lhs lthy |
|
84 |
val lthy'' = Variable.declare_term rhs lthy' |
|
85 |
in |
|
86 |
quotient_def (decl, (attr, (lhs, rhs))) lthy'' |
|
87 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
88 |
|
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
89 |
(* 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
|
90 |
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt = |
41444 | 91 |
let |
92 |
val rty = fastype_of rconst |
|
41451 | 93 |
val qty = Quotient_Term.derive_qtyp ctxt qtys rty |
41444 | 94 |
val lhs = Free (qconst_name, qty) |
95 |
in |
|
96 |
quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt |
|
97 |
end |
|
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 |
(* parser and command *) |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
100 |
val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where" |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
101 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
102 |
val quotdef_parser = |
41444 | 103 |
Scan.optional quotdef_decl (NONE, NoSyn) -- |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
104 |
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
|
105 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
106 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
107 |
Outer_Syntax.local_theory "quotient_definition" |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
108 |
"definition for constants over the quotient type" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
109 |
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
|
110 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
111 |
end; (* structure *) |