277
|
1 |
|
|
2 |
signature QUOTIENT_DEF =
|
774
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
3 |
sig
|
709
|
4 |
val quotient_def: mixfix -> Attrib.binding -> term -> term ->
|
775
|
5 |
local_theory -> (term * thm) * local_theory
|
789
|
6 |
|
705
|
7 |
val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
|
277
|
8 |
local_theory -> local_theory
|
|
9 |
end;
|
|
10 |
|
|
11 |
structure Quotient_Def: QUOTIENT_DEF =
|
|
12 |
struct
|
|
13 |
|
762
|
14 |
open Quotient_Info;
|
774
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
open Quotient_Term;
|
762
|
16 |
|
279
|
17 |
(* wrapper for define *)
|
277
|
18 |
fun define name mx attr rhs lthy =
|
|
19 |
let
|
|
20 |
val ((rhs, (_ , thm)), lthy') =
|
331
|
21 |
Local_Theory.define ((name, mx), (attr, rhs)) lthy
|
277
|
22 |
in
|
|
23 |
((rhs, thm), lthy')
|
|
24 |
end
|
|
25 |
|
|
26 |
|
709
|
27 |
(* interface and syntax setup *)
|
|
28 |
|
804
|
29 |
(* the ML-interface takes a 4-tuple consisting of *)
|
|
30 |
(* *)
|
|
31 |
(* - the mixfix annotation *)
|
|
32 |
(* - name and attributes *)
|
|
33 |
(* - the new constant as term *)
|
|
34 |
(* - the rhs of the definition as term *)
|
|
35 |
(* *)
|
|
36 |
(* it returns the defined constant and its definition *)
|
|
37 |
(* theorem; stores the data in the qconsts slot *)
|
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
|
709
|
39 |
fun quotient_def mx attr lhs rhs lthy =
|
293
|
40 |
let
|
801
|
41 |
val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*)
|
705
|
42 |
val qconst_bname = Binding.name lhs_str;
|
776
d1064fa29424
renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
44 |
val prop = Logic.mk_equals (lhs, absrep_trm)
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
45 |
val (_, prop') = LocalDefs.cert_def lthy prop
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
46 |
val (_, newrhs) = Primitive_Defs.abs_def prop'
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
48 |
val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
|
800
|
50 |
(* data storage *)
|
799
|
51 |
fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
|
319
|
52 |
val lthy'' = Local_Theory.declaration true
|
705
|
53 |
(fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
|
293
|
54 |
in
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
((trm, thm), lthy'')
|
293
|
56 |
end
|
|
57 |
|
804
|
58 |
fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =
|
277
|
59 |
let
|
804
|
60 |
val lhs = Syntax.read_term lthy lhs_str
|
|
61 |
val rhs = Syntax.read_term lthy rhs_str
|
277
|
62 |
in
|
709
|
63 |
quotient_def mx attr lhs rhs lthy |> snd
|
277
|
64 |
end
|
|
65 |
|
705
|
66 |
val _ = OuterKeyword.keyword "as";
|
|
67 |
|
279
|
68 |
val quotdef_parser =
|
705
|
69 |
(SpecParse.opt_thm_name ":" --
|
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
70 |
OuterParse.term) --
|
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
(OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
|
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
OuterParse.term)
|
279
|
73 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
74 |
val _ = OuterSyntax.local_theory "quotient_definition"
|
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
75 |
"definition for constants over the quotient type"
|
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
|
277
|
77 |
|
|
78 |
end; (* structure *)
|