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
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 6
709
+ − 7
val quotient_def: mixfix -> Attrib.binding -> term -> term ->
277
+ − 8
Proof.context -> (term * thm) * local_theory
705
+ − 9
val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
277
+ − 10
local_theory -> local_theory
+ − 11
end;
+ − 12
+ − 13
structure Quotient_Def: QUOTIENT_DEF =
+ − 14
struct
+ − 15
762
+ − 16
open Quotient_Info;
+ − 17
open Quotient_Type;
+ − 18
279
+ − 19
(* wrapper for define *)
277
+ − 20
fun define name mx attr rhs lthy =
+ − 21
let
+ − 22
val ((rhs, (_ , thm)), lthy') =
331
+ − 23
Local_Theory.define ((name, mx), (attr, rhs)) lthy
277
+ − 24
in
+ − 25
((rhs, thm), lthy')
+ − 26
end
+ − 27
+ − 28
datatype flag = absF | repF
+ − 29
+ − 30
fun negF absF = repF
+ − 31
| negF repF = absF
+ − 32
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
277
+ − 34
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 35
fun mk_compose flag (trm1, trm2) =
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 36
case flag of
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37
absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 38
| repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 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_fun_aux lthy s fs =
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 41
let
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 42
val thy = ProofContext.theory_of lthy
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 43
val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
val info = maps_lookup thy s handle NotFound => raise exc
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 45
in
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 46
list_comb (Const (#mapfun info, dummyT), fs)
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 47
end
277
+ − 48
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 49
fun get_const flag lthy _ qty =
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 50
(* FIXME: check here that the type-constructors of _ and qty are related *)
719
+ − 51
let
279
+ − 52
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
+ − 53
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
+ − 54
in
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
case flag of
719
+ − 56
absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
+ − 57
| repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 58
end
277
+ − 59
329
+ − 60
+ − 61
(* calculates the aggregate abs and rep functions for a given type;
+ − 62
repF is for constants' arguments; absF is for constants;
+ − 63
function types need to be treated specially, since repF and absF
+ − 64
change *)
+ − 65
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 66
fun get_fun flag lthy (rty, qty) =
389
+ − 67
if rty = qty then mk_identity qty else
719
+ − 68
case (rty, qty) of
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 69
(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
+ − 70
let
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 71
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
+ − 72
val fs_ty2 = get_fun flag lthy (ty2, ty2')
719
+ − 73
in
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 74
get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
719
+ − 75
end
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 76
| (Type (s, _), Type (s', [])) =>
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 77
if s = s'
719
+ − 78
then mk_identity qty
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 79
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
+ − 80
| (Type (s, tys), Type (s', tys')) =>
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 81
let
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 82
val args = map (get_fun flag lthy) (tys ~~ tys')
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 83
in
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 84
if s = s'
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 85
then get_fun_aux lthy s args
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 86
else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args)
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 87
end
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 88
| (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
+ − 89
if x = x'
719
+ − 90
then mk_identity qty
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 91
else raise (LIFT_MATCH "get_fun (frees)")
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 92
| (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)")
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 93
| _ => raise (LIFT_MATCH "get_fun (default)")
277
+ − 94
709
+ − 95
(* interface and syntax setup *)
+ − 96
+ − 97
(* the ML-interface takes a 4-tuple consisting of *)
+ − 98
(* *)
+ − 99
(* - the mixfix annotation *)
+ − 100
(* - name and attributes of the meta eq *)
+ − 101
(* - the new constant including its type *)
+ − 102
(* - the rhs of the definition *)
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 103
709
+ − 104
fun quotient_def mx attr lhs rhs lthy =
293
+ − 105
let
705
+ − 106
val Free (lhs_str, lhs_ty) = lhs;
+ − 107
val qconst_bname = Binding.name lhs_str;
+ − 108
val absrep_trm = get_fun 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
+ − 109
|> 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
+ − 110
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
+ − 111
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
+ − 112
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
+ − 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
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
+ − 115
496
+ − 116
fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
319
+ − 117
val lthy'' = Local_Theory.declaration true
705
+ − 118
(fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
293
+ − 119
in
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 120
((trm, thm), lthy'')
293
+ − 121
end
+ − 122
709
+ − 123
fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy =
277
+ − 124
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
+ − 125
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
+ − 126
val rhs = Syntax.read_term lthy rhsstr
277
+ − 127
in
709
+ − 128
quotient_def mx attr lhs rhs lthy |> snd
277
+ − 129
end
+ − 130
705
+ − 131
val _ = OuterKeyword.keyword "as";
+ − 132
279
+ − 133
val quotdef_parser =
705
+ − 134
(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
+ − 135
OuterParse.term) --
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 136
(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
+ − 137
OuterParse.term)
279
+ − 138
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 139
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
+ − 140
"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
+ − 141
OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
277
+ − 142
+ − 143
end; (* structure *)
+ − 144
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 145
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 146
762
+ − 147