1438
61671de8a545
synchronised with main hg-repository; used add_typedef_global in nominal_atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1
(* Title: HOL/Tools/Quotient/quotient_def.thy
952
+ − 2
Author: Cezary Kaliszyk and Christian Urban
+ − 3
1438
61671de8a545
synchronised with main hg-repository; used add_typedef_global in nominal_atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 4
Definitions for constants on quotient types.
952
+ − 5
*)
277
+ − 6
+ − 7
signature QUOTIENT_DEF =
1128
+ − 8
sig
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 9
val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->
775
+ − 10
local_theory -> (term * thm) * local_theory
789
+ − 11
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 12
val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
1146
+ − 13
local_theory -> (term * thm) * local_theory
1188
+ − 14
+ − 15
val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory
277
+ − 16
end;
+ − 17
+ − 18
structure Quotient_Def: QUOTIENT_DEF =
+ − 19
struct
+ − 20
762
+ − 21
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
+ − 22
open Quotient_Term;
762
+ − 23
884
+ − 24
(** Interface and Syntax Setup **)
850
+ − 25
1128
+ − 26
(* The ML-interface for a quotient definition takes
884
+ − 27
as argument:
709
+ − 28
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 29
- an optional binding and mixfix annotation
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 30
- attributes
884
+ − 31
- the new constant as term
+ − 32
- the rhs of the definition as term
850
+ − 33
884
+ − 34
It returns the defined constant and its definition
1128
+ − 35
theorem; stores the data in the qconsts data slot.
884
+ − 36
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37
Restriction: At the moment the right-hand side of the
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 38
definition must be a constant. Similarly the left-hand
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39
side must be a constant.
858
+ − 40
*)
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 41
fun error_msg bind str =
1151
+ − 42
let
+ − 43
val name = Binding.name_of bind
+ − 44
val pos = Position.str_of (Binding.pos_of bind)
+ − 45
in
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 46
error ("Head of quotient_definition " ^
1151
+ − 47
(quote str) ^ " differs from declaration " ^ name ^ pos)
+ − 48
end
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 49
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 50
fun quotient_def ((optbind, 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"
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 54
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
fun sanity_test NONE _ = true
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 56
| sanity_test (SOME bind) str =
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 57
if Name.of_binding bind = str then true
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 58
else error_msg bind str
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 59
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 60
val _ = sanity_test optbind lhs_str
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 61
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 62
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
+ − 63
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
+ − 64
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
1354
+ − 65
val (_, prop') = Local_Defs.cert_def lthy prop
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
+ − 66
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
+ − 67
1142
+ − 68
val ((trm, (_ , thm)), lthy') = Local_Theory.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
+ − 69
800
+ − 70
(* data storage *)
799
+ − 71
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
+ − 72
fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
319
+ − 73
val lthy'' = Local_Theory.declaration true
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 74
(fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
293
+ − 75
in
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 76
((trm, thm), lthy'')
293
+ − 77
end
+ − 78
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 79
fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
277
+ − 80
let
1141
+ − 81
val lhs = Syntax.read_term lthy lhs_str
+ − 82
val rhs = Syntax.read_term lthy rhs_str
1114
+ − 83
val lthy' = Variable.declare_term lhs lthy
+ − 84
val lthy'' = Variable.declare_term rhs lthy'
277
+ − 85
in
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 86
quotient_def (decl, (attr, (lhs, rhs))) lthy''
277
+ − 87
end
+ − 88
1188
+ − 89
fun quotient_lift_const (b, t) ctxt =
+ − 90
quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
+ − 91
(Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt
+ − 92
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 93
local
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 94
structure P = OuterParse;
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 95
in
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 96
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 97
val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where"
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 98
279
+ − 99
val quotdef_parser =
1150
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 100
Scan.optional quotdef_decl (NONE, NoSyn) --
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 101
P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
689a18f9484c
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 102
end
279
+ − 103
1144
+ − 104
val _ =
+ − 105
OuterSyntax.local_theory "quotient_definition"
+ − 106
"definition for constants over the quotient type"
1146
+ − 107
OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
277
+ − 108
+ − 109
end; (* structure *)