952
+ − 1
(* Title: quotient_def.thy
+ − 2
Author: Cezary Kaliszyk and Christian Urban
+ − 3
+ − 4
Definitions for constants on quotient types.
+ − 5
+ − 6
*)
277
+ − 7
+ − 8
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
+ − 9
sig
709
+ − 10
val quotient_def: mixfix -> Attrib.binding -> term -> term ->
775
+ − 11
local_theory -> (term * thm) * local_theory
789
+ − 12
705
+ − 13
val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
277
+ − 14
local_theory -> local_theory
+ − 15
end;
+ − 16
+ − 17
structure Quotient_Def: QUOTIENT_DEF =
+ − 18
struct
+ − 19
762
+ − 20
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
+ − 21
open Quotient_Term;
762
+ − 22
279
+ − 23
(* wrapper for define *)
277
+ − 24
fun define name mx attr rhs lthy =
+ − 25
let
+ − 26
val ((rhs, (_ , thm)), lthy') =
331
+ − 27
Local_Theory.define ((name, mx), (attr, rhs)) lthy
277
+ − 28
in
+ − 29
((rhs, thm), lthy')
+ − 30
end
+ − 31
+ − 32
884
+ − 33
(** Interface and Syntax Setup **)
850
+ − 34
884
+ − 35
(* The ML-interface for a quotient definition takes
+ − 36
as argument:
709
+ − 37
884
+ − 38
- the mixfix annotation
+ − 39
- name and attributes
+ − 40
- the new constant as term
+ − 41
- the rhs of the definition as term
850
+ − 42
884
+ − 43
It returns the defined constant and its definition
+ − 44
theorem; stores the data in the qconsts data slot.
+ − 45
+ − 46
Restriction: At the moment the right-hand side must
+ − 47
be a terms composed of constant. Similarly the
+ − 48
left-hand side must be a single constant.
858
+ − 49
*)
709
+ − 50
fun quotient_def mx attr lhs rhs lthy =
293
+ − 51
let
884
+ − 52
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
+ − 53
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+ − 54
+ − 55
val qconst_bname = Binding.name lhs_str
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 56
val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
854
5961edda27d7
absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 57
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
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
+ − 58
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
+ − 59
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
+ − 60
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
+ − 61
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
+ − 62
800
+ − 63
(* data storage *)
799
+ − 64
fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 65
fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
319
+ − 66
val lthy'' = Local_Theory.declaration true
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 67
(fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
293
+ − 68
in
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 69
((trm, thm), lthy'')
293
+ − 70
end
+ − 71
804
+ − 72
fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =
277
+ − 73
let
804
+ − 74
val lhs = Syntax.read_term lthy lhs_str
+ − 75
val rhs = Syntax.read_term lthy rhs_str
884
+ − 76
(* FIXME: Relating the reads will cause errors. *)
277
+ − 77
in
709
+ − 78
quotient_def mx attr lhs rhs lthy |> snd
277
+ − 79
end
+ − 80
705
+ − 81
val _ = OuterKeyword.keyword "as";
+ − 82
279
+ − 83
val quotdef_parser =
705
+ − 84
(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
+ − 85
OuterParse.term) --
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 86
(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
+ − 87
OuterParse.term)
279
+ − 88
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 89
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
+ − 90
"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
+ − 91
OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
277
+ − 92
+ − 93
end; (* structure *)