277
|
1 |
|
|
2 |
signature QUOTIENT_DEF =
|
|
3 |
sig
|
|
4 |
datatype flag = absF | repF
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
val get_fun: flag -> Proof.context -> typ * typ -> term
|
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
|
6 |
val make_def: binding -> mixfix -> Attrib.binding -> term -> term ->
|
277
|
7 |
Proof.context -> (term * thm) * local_theory
|
|
8 |
|
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
|
9 |
val quotdef: (binding * term * mixfix) * (Attrib.binding * term) ->
|
277
|
10 |
local_theory -> (term * thm) * local_theory
|
|
11 |
val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->
|
|
12 |
local_theory -> local_theory
|
|
13 |
end;
|
|
14 |
|
|
15 |
structure Quotient_Def: QUOTIENT_DEF =
|
|
16 |
struct
|
|
17 |
|
279
|
18 |
(* wrapper for define *)
|
277
|
19 |
fun define name mx attr rhs lthy =
|
|
20 |
let
|
|
21 |
val ((rhs, (_ , thm)), lthy') =
|
331
|
22 |
Local_Theory.define ((name, mx), (attr, rhs)) lthy
|
277
|
23 |
in
|
|
24 |
((rhs, thm), lthy')
|
|
25 |
end
|
|
26 |
|
|
27 |
datatype flag = absF | repF
|
|
28 |
|
|
29 |
fun negF absF = repF
|
|
30 |
| negF repF = absF
|
|
31 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
|
277
|
33 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
fun get_fun_aux lthy s fs =
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
case (maps_lookup (ProofContext.theory_of lthy) s) of
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
36 |
SOME info => list_comb (Const (#mapfun info, dummyT), fs)
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
| NONE => raise
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
(LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]))
|
277
|
39 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
fun get_const flag lthy _ qty =
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
(* FIXME: check here that _ and qty are related *)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
let
|
279
|
43 |
val thy = ProofContext.theory_of lthy
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
44 |
val qty_name = Long_Name.base_name (fst (dest_Type qty))
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
45 |
in
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
case flag of
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
| repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
end
|
277
|
50 |
|
329
|
51 |
|
|
52 |
(* calculates the aggregate abs and rep functions for a given type;
|
|
53 |
repF is for constants' arguments; absF is for constants;
|
|
54 |
function types need to be treated specially, since repF and absF
|
|
55 |
change *)
|
|
56 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
57 |
fun get_fun flag lthy (rty, qty) =
|
389
|
58 |
if rty = qty then mk_identity qty else
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
case (rty, qty) of
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
60 |
(Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
61 |
let
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
62 |
val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
63 |
val fs_ty2 = get_fun flag lthy (ty2, ty2')
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
64 |
in
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
end
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
| (Type (s, []), Type (s', [])) =>
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
68 |
if s = s'
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
69 |
then mk_identity qty
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
70 |
else get_const flag lthy rty qty
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
| (Type (s, tys), Type (s', tys')) =>
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
if s = s'
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys'))
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
74 |
else get_const flag lthy rty qty
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
75 |
| (TFree x, TFree x') =>
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
if x = x'
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
77 |
then mk_identity qty
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
78 |
else raise (LIFT_MATCH "get_fun")
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
79 |
| (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
80 |
| _ => raise (LIFT_MATCH "get_fun")
|
277
|
81 |
|
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
|
82 |
fun make_def qconst_bname mx attr lhs rhs lthy =
|
293
|
83 |
let
|
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
|
84 |
val absrep_trm = get_fun absF lthy (fastype_of rhs, fastype_of lhs) $ rhs
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
85 |
|> Syntax.check_term lthy
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
86 |
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
|
87 |
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
|
88 |
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
|
89 |
|
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
|
90 |
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
|
91 |
|
496
|
92 |
fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
|
319
|
93 |
val lthy'' = Local_Theory.declaration true
|
549
|
94 |
(fn phi =>
|
|
95 |
let
|
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
|
96 |
val qconst_str = Binding.name_of qconst_bname
|
549
|
97 |
in
|
|
98 |
qconsts_update_gen qconst_str (qcinfo phi)
|
|
99 |
end) lthy'
|
293
|
100 |
in
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
101 |
((trm, thm), lthy'')
|
293
|
102 |
end
|
|
103 |
|
|
104 |
(* interface and syntax setup *)
|
|
105 |
|
|
106 |
(* the ML-interface takes a 5-tuple consisting of *)
|
|
107 |
(* *)
|
|
108 |
(* - the name of the constant to be lifted *)
|
|
109 |
(* - its type *)
|
|
110 |
(* - its mixfix annotation *)
|
|
111 |
(* - a meta-equation defining the constant, *)
|
|
112 |
(* and the attributes of for this meta-equality *)
|
277
|
113 |
|
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
|
114 |
fun quotdef ((bind, lhs, mx), (attr, rhs)) lthy =
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
115 |
make_def bind mx attr lhs rhs lthy
|
277
|
116 |
|
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
|
117 |
fun quotdef_cmd ((bind, lhsstr, mx), (attr, rhsstr)) lthy =
|
277
|
118 |
let
|
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
|
119 |
val lhs = Syntax.read_term lthy lhsstr
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
120 |
val rhs = Syntax.read_term lthy rhsstr
|
277
|
121 |
in
|
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
|
122 |
quotdef ((bind, lhs, mx), (attr, rhs)) lthy |> snd
|
277
|
123 |
end
|
|
124 |
|
279
|
125 |
val quotdef_parser =
|
|
126 |
(OuterParse.binding --
|
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
|
127 |
(OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.term --
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
128 |
OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
|
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
129 |
(SpecParse.opt_thm_name ":" -- OuterParse.term)
|
279
|
130 |
|
277
|
131 |
val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
|
|
132 |
OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
|
|
133 |
|
|
134 |
end; (* structure *)
|
|
135 |
|
307
|
136 |
open Quotient_Def;
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
137 |
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
138 |
|