author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Mon, 28 Jun 2010 07:32:51 +0200 | |
changeset 37562 | 21ab339715cd |
parent 37561 | 19fca77829ea |
child 37563 | 6cf28a1dfd75 |
permissions | -rw-r--r-- |
35788 | 1 |
(* Title: HOL/Tools/Quotient/quotient_def.thy |
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 |
open Quotient_Info; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
open Quotient_Term; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
(** Interface and Syntax Setup **) |
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 |
(* The ML-interface for a quotient definition takes |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
as argument: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
- an optional binding and mixfix annotation |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
- attributes |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
- the new constant as term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
- the rhs of the definition as term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
|
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
35 |
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
|
36 |
|
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
37 |
Restriction: At the moment the left- and right-hand |
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
38 |
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
|
39 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
fun error_msg bind str = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
val name = Binding.name_of bind |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
val pos = Position.str_of (Binding.pos_of bind) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
in |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
error ("Head of quotient_definition " ^ |
37530
70d03844b2f9
export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
36960
diff
changeset
|
46 |
quote str ^ " differs from declaration " ^ name ^ pos) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
49 |
fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
51 |
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
37562
21ab339715cd
Restrict quotient definitions to constants
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37561
diff
changeset
|
52 |
val _ = if is_Const rhs then () else error "The definiens should be a constant" |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
53 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
54 |
fun sanity_test NONE _ = true |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
55 |
| sanity_test (SOME bind) str = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
if Name.of_binding bind = str then true |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
else error_msg bind str |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
58 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
59 |
val _ = sanity_test optbind lhs_str |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
60 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
61 |
val qconst_bname = Binding.name lhs_str |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
62 |
val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
63 |
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
35624 | 64 |
val (_, prop') = Local_Defs.cert_def lthy prop |
36108 | 65 |
val (_, newrhs) = Local_Defs.abs_def prop' |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
66 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
67 |
val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
68 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
(* data storage *) |
37530
70d03844b2f9
export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
36960
diff
changeset
|
70 |
val qconst_data = {qconst = trm, rconst = rhs, def = thm} |
70d03844b2f9
export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
36960
diff
changeset
|
71 |
|
70d03844b2f9
export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
36960
diff
changeset
|
72 |
fun qcinfo phi = transform_qconsts phi qconst_data |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
74 |
val lthy'' = Local_Theory.declaration true |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
75 |
(fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
76 |
in |
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 |
(qconst_data, lthy'') |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
78 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
80 |
fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
81 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
82 |
val lhs = Syntax.read_term lthy lhs_str |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
83 |
val rhs = Syntax.read_term lthy rhs_str |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
84 |
val lthy' = Variable.declare_term lhs lthy |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
85 |
val lthy'' = Variable.declare_term rhs lthy' |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
86 |
in |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
87 |
quotient_def (decl, (attr, (lhs, rhs))) lthy'' |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
88 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
89 |
|
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
90 |
(* 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
|
91 |
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt = |
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
92 |
let |
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
93 |
val rty = fastype_of rconst |
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
94 |
val qty = derive_qtyp qtys rty ctxt |
37561
19fca77829ea
mixfix can be given for automatically lifted constants
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
95 |
val lhs = Free (qconst_name, qty) |
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
96 |
in |
37561
19fca77829ea
mixfix can be given for automatically lifted constants
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
97 |
quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt |
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
98 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
99 |
|
37532
8a9a34be09e0
slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents:
37530
diff
changeset
|
100 |
(* parser and command *) |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
101 |
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
|
102 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
103 |
val quotdef_parser = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
104 |
Scan.optional quotdef_decl (NONE, NoSyn) -- |
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 *) |