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_term.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
Constructs terms corresponding to goals from lifting theorems to
61671de8a545
synchronised with main hg-repository; used add_typedef_global in nominal_atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 5
quotient types.
952
+ − 6
*)
+ − 7
758
+ − 8
signature QUOTIENT_TERM =
+ − 9
sig
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 10
datatype flag = AbsF | RepF
853
+ − 11
+ − 12
val absrep_fun: flag -> Proof.context -> typ * typ -> term
+ − 13
val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
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
+ − 14
974
+ − 15
(* Allows Nitpick to represent quotient types as single elements from raw type *)
+ − 16
val absrep_const_chk: flag -> Proof.context -> string -> term
+ − 17
853
+ − 18
val equiv_relation: Proof.context -> typ * typ -> term
+ − 19
val equiv_relation_chk: Proof.context -> typ * typ -> term
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 20
853
+ − 21
val regularize_trm: Proof.context -> term * term -> term
+ − 22
val regularize_trm_chk: Proof.context -> term * term -> term
+ − 23
+ − 24
val inj_repabs_trm: Proof.context -> term * term -> term
+ − 25
val inj_repabs_trm_chk: Proof.context -> term * term -> term
1065
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 26
1188
+ − 27
val quotient_lift_const: string * term -> local_theory -> term
1065
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 28
val quotient_lift_all: Proof.context -> term -> term
758
+ − 29
end;
+ − 30
+ − 31
structure Quotient_Term: QUOTIENT_TERM =
+ − 32
struct
+ − 33
762
+ − 34
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
+ − 35
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 36
exception LIFT_MATCH of string
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37
849
+ − 38
+ − 39
+ − 40
(*** Aggregate Rep/Abs Function ***)
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 41
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 42
1128
+ − 43
(* The flag RepF is for types in negative position; AbsF is for types
+ − 44
in positive position. Because of this, function types need to be
+ − 45
treated specially, since there the polarity changes.
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
+ − 46
*)
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
+ − 47
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 48
datatype flag = AbsF | RepF
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
+ − 49
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 50
fun negF AbsF = RepF
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 51
| negF RepF = AbsF
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
+ − 52
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
+ − 53
fun is_identity (Const (@{const_name "id"}, _)) = true
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
+ − 54
| is_identity _ = false
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
+ − 55
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
+ − 56
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 57
1128
+ − 58
fun mk_fun_compose flag (trm1, trm2) =
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
+ − 59
case flag of
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 60
AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 61
| RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
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
+ − 62
790
+ − 63
fun get_mapfun ctxt s =
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
+ − 64
let
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 65
val thy = ProofContext.theory_of ctxt
1450
+ − 66
val exn = error ("No map function for type " ^ quote s ^ " found.")
1100
+ − 67
val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
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
+ − 68
in
784
+ − 69
Const (mapfun, dummyT)
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
+ − 70
end
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 71
800
+ − 72
(* makes a Free out of a TVar *)
+ − 73
fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
+ − 74
1128
+ − 75
(* produces an aggregate map function for the
+ − 76
rty-part of a quotient definition; abstracts
+ − 77
over all variables listed in vs (these variables
+ − 78
correspond to the type variables in rty)
+ − 79
+ − 80
for example for: (?'a list * ?'b)
+ − 81
it produces: %a b. prod_map (map a) b
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
+ − 82
*)
803
+ − 83
fun mk_mapfun ctxt vs rty =
790
+ − 84
let
+ − 85
val vs' = map (mk_Free) vs
+ − 86
803
+ − 87
fun mk_mapfun_aux rty =
+ − 88
case rty of
+ − 89
TVar _ => mk_Free rty
+ − 90
| Type (_, []) => mk_identity rty
790
+ − 91
| Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
1450
+ − 92
| _ => raise (error "mk_mapfun (default)")
790
+ − 93
in
803
+ − 94
fold_rev Term.lambda vs' (mk_mapfun_aux rty)
790
+ − 95
end
+ − 96
1128
+ − 97
(* looks up the (varified) rty and qty for
+ − 98
a quotient definition
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
+ − 99
*)
790
+ − 100
fun get_rty_qty ctxt s =
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
+ − 101
let
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 102
val thy = ProofContext.theory_of ctxt
1450
+ − 103
val exn = error ("No quotient type " ^ quote s ^ " found.")
1100
+ − 104
val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
790
+ − 105
in
+ − 106
(#rtyp qdata, #qtyp qdata)
+ − 107
end
+ − 108
1128
+ − 109
(* takes two type-environments and looks
+ − 110
up in both of them the variable v, which
+ − 111
must be listed in the environment
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
+ − 112
*)
790
+ − 113
fun double_lookup rtyenv qtyenv v =
+ − 114
let
+ − 115
val v' = fst (dest_TVar v)
+ − 116
in
+ − 117
(snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
+ − 118
end
+ − 119
832
+ − 120
(* matches a type pattern with a type *)
+ − 121
fun match ctxt err ty_pat ty =
+ − 122
let
+ − 123
val thy = ProofContext.theory_of ctxt
+ − 124
in
+ − 125
Sign.typ_match thy (ty_pat, ty) Vartab.empty
+ − 126
handle MATCH_TYPE => err ctxt ty_pat ty
+ − 127
end
+ − 128
800
+ − 129
(* produces the rep or abs constant for a qty *)
790
+ − 130
fun absrep_const flag ctxt qty_str =
+ − 131
let
+ − 132
val thy = ProofContext.theory_of ctxt
+ − 133
val qty_name = Long_Name.base_name qty_str
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
+ − 134
in
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 135
case flag of
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 136
AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 137
| RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
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
+ − 138
end
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 139
974
+ − 140
(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
+ − 141
fun absrep_const_chk flag ctxt qty_str =
+ − 142
Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
+ − 143
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 144
fun absrep_match_err ctxt ty_pat ty =
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 145
let
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 146
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
1128
+ − 147
val ty_str = Syntax.string_of_typ ctxt ty
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 148
in
1450
+ − 149
raise error (cat_lines
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 150
["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 151
end
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 152
849
+ − 153
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
+ − 154
(** generation of an aggregate absrep function **)
791
+ − 155
1128
+ − 156
(* - In case of equal types we just return the identity.
+ − 157
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
+ − 158
- In case of TFrees we also return the identity.
1128
+ − 159
+ − 160
- In case of function types we recurse taking
+ − 161
the polarity change into account.
+ − 162
+ − 163
- If the type constructors are equal, we recurse for the
+ − 164
arguments and build the appropriate map function.
+ − 165
+ − 166
- If the type constructors are unequal, there must be an
+ − 167
instance of quotient types:
+ − 168
+ − 169
- we first look up the corresponding rty_pat and qty_pat
+ − 170
from the quotient definition; the arguments of qty_pat
+ − 171
must be some distinct TVars
+ − 172
- we then match the rty_pat with rty and qty_pat with qty;
+ − 173
if matching fails the types do not correspond -> error
+ − 174
- the matching produces two environments; we look up the
+ − 175
assignments for the qty_pat variables and recurse on the
+ − 176
assignments
+ − 177
- we prefix the aggregate map function for the rty_pat,
+ − 178
which is an abstraction over all type variables
+ − 179
- finally we compose the result with the appropriate
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
+ − 180
absrep function in case at least one argument produced
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
+ − 181
a non-identity function /
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
+ − 182
otherwise we just return the appropriate absrep
1128
+ − 183
function
+ − 184
+ − 185
The composition is necessary for types like
+ − 186
+ − 187
('a list) list / ('a foo) foo
+ − 188
+ − 189
The matching is necessary for types like
+ − 190
+ − 191
('a * 'a) list / 'a bar
849
+ − 192
858
+ − 193
The test is necessary in order to eliminate superfluous
1128
+ − 194
identity maps.
+ − 195
*)
849
+ − 196
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 197
fun absrep_fun flag ctxt (rty, qty) =
1128
+ − 198
if rty = qty
803
+ − 199
then mk_identity rty
790
+ − 200
else
+ − 201
case (rty, qty) of
+ − 202
(Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
+ − 203
let
+ − 204
val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
+ − 205
val arg2 = absrep_fun flag ctxt (ty2, ty2')
+ − 206
in
+ − 207
list_comb (get_mapfun ctxt "fun", [arg1, arg2])
+ − 208
end
+ − 209
| (Type (s, tys), Type (s', tys')) =>
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
+ − 210
if s = s'
1128
+ − 211
then
790
+ − 212
let
+ − 213
val args = map (absrep_fun flag ctxt) (tys ~~ tys')
+ − 214
in
+ − 215
list_comb (get_mapfun ctxt s, args)
1128
+ − 216
end
790
+ − 217
else
+ − 218
let
+ − 219
val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
832
+ − 220
val rtyenv = match ctxt absrep_match_err rty_pat rty
+ − 221
val qtyenv = match ctxt absrep_match_err qty_pat qty
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
+ − 222
val args_aux = map (double_lookup rtyenv qtyenv) vs
790
+ − 223
val args = map (absrep_fun flag ctxt) args_aux
1128
+ − 224
val map_fun = mk_mapfun ctxt vs rty_pat
+ − 225
val result = list_comb (map_fun, args)
790
+ − 226
in
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
+ − 227
if forall is_identity args
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
+ − 228
then absrep_const flag ctxt s'
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
+ − 229
else mk_fun_compose flag (absrep_const flag ctxt s', result)
830
+ − 230
end
790
+ − 231
| (TFree x, TFree x') =>
+ − 232
if x = x'
803
+ − 233
then mk_identity rty
1450
+ − 234
else raise (error "absrep_fun (frees)")
790
+ − 235
| (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
1450
+ − 236
| _ => raise (error "absrep_fun (default)")
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
+ − 237
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 238
fun absrep_fun_chk flag ctxt (rty, qty) =
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 239
absrep_fun flag ctxt (rty, qty)
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 240
|> Syntax.check_term ctxt
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
+ − 241
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 242
849
+ − 243
+ − 244
+ − 245
(*** Aggregate Equivalence Relation ***)
758
+ − 246
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
+ − 247
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
+ − 248
(* works very similar to the absrep generation,
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
+ − 249
except there is no need for polarities
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
+ − 250
*)
758
+ − 251
783
06e17083e90b
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 252
(* instantiates TVars so that the term is of type ty *)
792
+ − 253
fun force_typ ctxt trm ty =
783
06e17083e90b
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 254
let
1128
+ − 255
val thy = ProofContext.theory_of ctxt
783
06e17083e90b
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 256
val trm_ty = fastype_of trm
06e17083e90b
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 257
val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
06e17083e90b
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 258
in
06e17083e90b
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 259
map_types (Envir.subst_type ty_inst) trm
06e17083e90b
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 260
end
06e17083e90b
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 261
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
+ − 262
fun is_eq (Const (@{const_name "op ="}, _)) = true
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
+ − 263
| is_eq _ = false
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
+ − 264
825
+ − 265
fun mk_rel_compose (trm1, trm2) =
1438
61671de8a545
synchronised with main hg-repository; used add_typedef_global in nominal_atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 266
Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
807
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 267
792
+ − 268
fun get_relmap ctxt s =
+ − 269
let
+ − 270
val thy = ProofContext.theory_of ctxt
1450
+ − 271
val exn = error ("get_relmap (no relation map function found for type " ^ s ^ ")")
1100
+ − 272
val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
792
+ − 273
in
+ − 274
Const (relmap, dummyT)
+ − 275
end
+ − 276
807
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 277
fun mk_relmap ctxt vs rty =
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 278
let
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 279
val vs' = map (mk_Free) vs
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 280
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 281
fun mk_relmap_aux rty =
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 282
case rty of
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 283
TVar _ => mk_Free rty
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 284
| Type (_, []) => HOLogic.eq_const rty
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 285
| Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
1450
+ − 286
| _ => raise (error "mk_relmap (default)")
807
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 287
in
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 288
fold_rev Term.lambda vs' (mk_relmap_aux rty)
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 289
end
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 290
792
+ − 291
fun get_equiv_rel ctxt s =
+ − 292
let
+ − 293
val thy = ProofContext.theory_of ctxt
1450
+ − 294
val exn = error ("get_quotdata (no quotient found for type " ^ s ^ ")")
792
+ − 295
in
1100
+ − 296
#equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
792
+ − 297
end
+ − 298
808
90bde96f5dd1
proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 299
fun equiv_match_err ctxt ty_pat ty =
90bde96f5dd1
proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 300
let
90bde96f5dd1
proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 301
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
1128
+ − 302
val ty_str = Syntax.string_of_typ ctxt ty
808
90bde96f5dd1
proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 303
in
1450
+ − 304
raise error (space_implode " "
808
90bde96f5dd1
proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 305
["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
90bde96f5dd1
proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 306
end
90bde96f5dd1
proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 307
1128
+ − 308
(* builds the aggregate equivalence relation
+ − 309
that will be the argument of Respects
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
+ − 310
*)
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 311
fun equiv_relation ctxt (rty, qty) =
758
+ − 312
if rty = qty
+ − 313
then HOLogic.eq_const rty
+ − 314
else
+ − 315
case (rty, qty) of
+ − 316
(Type (s, tys), Type (s', tys')) =>
1128
+ − 317
if s = s'
+ − 318
then
761
+ − 319
let
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 320
val args = map (equiv_relation ctxt) (tys ~~ tys')
761
+ − 321
in
1128
+ − 322
list_comb (get_relmap ctxt s, args)
+ − 323
end
+ − 324
else
784
+ − 325
let
831
+ − 326
val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
832
+ − 327
val rtyenv = match ctxt equiv_match_err rty_pat rty
+ − 328
val qtyenv = match ctxt equiv_match_err qty_pat qty
1128
+ − 329
val args_aux = map (double_lookup rtyenv qtyenv) vs
831
+ − 330
val args = map (equiv_relation ctxt) args_aux
1128
+ − 331
val rel_map = mk_relmap ctxt vs rty_pat
831
+ − 332
val result = list_comb (rel_map, args)
792
+ − 333
val eqv_rel = get_equiv_rel ctxt s'
831
+ − 334
val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
761
+ − 335
in
1128
+ − 336
if forall is_eq args
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
+ − 337
then eqv_rel'
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
+ − 338
else mk_rel_compose (result, eqv_rel')
761
+ − 339
end
783
06e17083e90b
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 340
| _ => HOLogic.eq_const rty
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 341
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 342
fun equiv_relation_chk ctxt (rty, qty) =
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 343
equiv_relation ctxt (rty, qty)
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 344
|> Syntax.check_term ctxt
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 345
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 346
849
+ − 347
+ − 348
(*** Regularization ***)
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 349
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 350
(* Regularizing an rtrm means:
1128
+ − 351
+ − 352
- Quantifiers over types that need lifting are replaced
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 353
by bounded quantifiers, for example:
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 354
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 355
All P ----> All (Respects R) P
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 356
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 357
where the aggregate relation R is given by the rty and qty;
1128
+ − 358
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 359
- Abstractions over types that need lifting are replaced
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 360
by bounded abstractions, for example:
1128
+ − 361
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 362
%x. P ----> Ball (Respects R) %x. P
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 363
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 364
- Equalities over types that need lifting are replaced by
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 365
corresponding equivalence relations, for example:
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 366
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 367
A = B ----> R A B
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 368
853
+ − 369
or
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 370
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 371
A = B ----> (R ===> R) A B
853
+ − 372
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 373
for more complicated types of A and B
955
+ − 374
+ − 375
+ − 376
The regularize_trm accepts raw theorems in which equalities
+ − 377
and quantifiers match exactly the ones in the lifted theorem
+ − 378
but also accepts partially regularized terms.
+ − 379
+ − 380
This means that the raw theorems can have:
982
+ − 381
Ball (Respects R), Bex (Respects R), Bex1_rel (Respects R), Babs, R
955
+ − 382
in the places where:
959
1786aa86e52b
When commenting discovered a missing case of Babs->Abs regularization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 383
All, Ex, Ex1, %, (op =)
955
+ − 384
is required the lifted theorem.
+ − 385
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 386
*)
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 387
758
+ − 388
val mk_babs = Const (@{const_name Babs}, dummyT)
+ − 389
val mk_ball = Const (@{const_name Ball}, dummyT)
+ − 390
val mk_bex = Const (@{const_name Bex}, dummyT)
999
+ − 391
val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
758
+ − 392
val mk_resp = Const (@{const_name Respects}, dummyT)
+ − 393
1128
+ − 394
(* - applies f to the subterm of an abstraction,
+ − 395
otherwise to the given term,
+ − 396
- used by regularize, therefore abstracted
+ − 397
variables do not have to be treated specially
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
+ − 398
*)
775
+ − 399
fun apply_subt f (trm1, trm2) =
758
+ − 400
case (trm1, trm2) of
775
+ − 401
(Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
+ − 402
| _ => f (trm1, trm2)
758
+ − 403
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 404
fun term_mismatch str ctxt t1 t2 =
865
+ − 405
let
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 406
val t1_str = Syntax.string_of_term ctxt t1
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 407
val t2_str = Syntax.string_of_term ctxt t2
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 408
val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 409
val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
865
+ − 410
in
1450
+ − 411
raise error (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
865
+ − 412
end
+ − 413
758
+ − 414
(* the major type of All and Ex quantifiers *)
853
+ − 415
fun qnt_typ ty = domain_type (domain_type ty)
758
+ − 416
867
+ − 417
(* Checks that two types match, for example:
+ − 418
rty -> rty matches qty -> qty *)
875
+ − 419
fun matches_typ thy rT qT =
+ − 420
if rT = qT then true else
+ − 421
case (rT, qT) of
+ − 422
(Type (rs, rtys), Type (qs, qtys)) =>
+ − 423
if rs = qs then
+ − 424
if length rtys <> length qtys then false else
+ − 425
forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
+ − 426
else
+ − 427
(case Quotient_Info.quotdata_lookup_raw thy qs of
+ − 428
SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
+ − 429
| NONE => false)
867
+ − 430
| _ => false
+ − 431
+ − 432
856
+ − 433
(* produces a regularized version of rtrm
758
+ − 434
1128
+ − 435
- the result might contain dummyTs
758
+ − 436
1128
+ − 437
- for regularisation we do not need any
+ − 438
special treatment of bound variables
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
+ − 439
*)
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 440
fun regularize_trm ctxt (rtrm, qtrm) =
758
+ − 441
case (rtrm, qtrm) of
+ − 442
(Abs (x, ty, t), Abs (_, ty', t')) =>
+ − 443
let
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 444
val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
758
+ − 445
in
+ − 446
if ty = ty' then subtrm
831
+ − 447
else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
758
+ − 448
end
1000
+ − 449
| (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
959
1786aa86e52b
When commenting discovered a missing case of Babs->Abs regularization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 450
let
1786aa86e52b
When commenting discovered a missing case of Babs->Abs regularization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 451
val subtrm = regularize_trm ctxt (t, t')
1786aa86e52b
When commenting discovered a missing case of Babs->Abs regularization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 452
val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
1786aa86e52b
When commenting discovered a missing case of Babs->Abs regularization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 453
in
1000
+ − 454
if resrel <> needres
+ − 455
then term_mismatch "regularize (Babs)" ctxt resrel needres
+ − 456
else mk_babs $ resrel $ subtrm
959
1786aa86e52b
When commenting discovered a missing case of Babs->Abs regularization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 457
end
758
+ − 458
+ − 459
| (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
+ − 460
let
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 461
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
758
+ − 462
in
+ − 463
if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
831
+ − 464
else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
758
+ − 465
end
+ − 466
953
+ − 467
| (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+ − 468
let
+ − 469
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+ − 470
in
+ − 471
if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
+ − 472
else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+ − 473
end
+ − 474
1077
+ − 475
| (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
1128
+ − 476
(Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
+ − 477
(Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
1077
+ − 478
Const (@{const_name "Ex1"}, ty') $ t') =>
1074
+ − 479
let
1077
+ − 480
val t_ = incr_boundvars (~1) t
+ − 481
val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
1074
+ − 482
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
+ − 483
in
+ − 484
if resrel <> needrel
+ − 485
then term_mismatch "regularize (Bex1)" ctxt resrel needrel
+ − 486
else mk_bex1_rel $ resrel $ subtrm
+ − 487
end
+ − 488
953
+ − 489
| (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+ − 490
let
+ − 491
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+ − 492
in
+ − 493
if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
999
+ − 494
else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
953
+ − 495
end
+ − 496
1128
+ − 497
| (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
952
+ − 498
Const (@{const_name "All"}, ty') $ t') =>
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 499
let
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 500
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
952
+ − 501
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 502
in
904
+ − 503
if resrel <> needrel
952
+ − 504
then term_mismatch "regularize (Ball)" ctxt resrel needrel
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 505
else mk_ball $ (mk_resp $ resrel) $ subtrm
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 506
end
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 507
1128
+ − 508
| (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
952
+ − 509
Const (@{const_name "Ex"}, ty') $ t') =>
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 510
let
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 511
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
952
+ − 512
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 513
in
904
+ − 514
if resrel <> needrel
952
+ − 515
then term_mismatch "regularize (Bex)" ctxt resrel needrel
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 516
else mk_bex $ (mk_resp $ resrel) $ subtrm
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 517
end
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 518
982
+ − 519
| (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
906
+ − 520
let
+ − 521
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
952
+ − 522
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
906
+ − 523
in
+ − 524
if resrel <> needrel
952
+ − 525
then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
999
+ − 526
else mk_bex1_rel $ resrel $ subtrm
946
+ − 527
end
+ − 528
1128
+ − 529
| (* equalities need to be replaced by appropriate equivalence relations *)
758
+ − 530
(Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
+ − 531
if ty = ty' then rtrm
1128
+ − 532
else equiv_relation ctxt (domain_type ty, domain_type ty')
758
+ − 533
1128
+ − 534
| (* in this case we just check whether the given equivalence relation is correct *)
758
+ − 535
(rel, Const (@{const_name "op ="}, ty')) =>
865
+ − 536
let
785
+ − 537
val rel_ty = fastype_of rel
1128
+ − 538
val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
865
+ − 539
in
1128
+ − 540
if rel' aconv rel then rtrm
952
+ − 541
else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
865
+ − 542
end
758
+ − 543
+ − 544
| (_, Const _) =>
835
+ − 545
let
+ − 546
val thy = ProofContext.theory_of ctxt
867
+ − 547
fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
835
+ − 548
| same_const _ _ = false
758
+ − 549
in
835
+ − 550
if same_const rtrm qtrm then rtrm
+ − 551
else
+ − 552
let
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 553
val rtrm' = #rconst (qconsts_lookup thy qtrm)
1099
+ − 554
handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 555
in
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 556
if Pattern.matches thy (rtrm', rtrm)
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 557
then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
758
+ − 558
end
1128
+ − 559
end
758
+ − 560
1000
+ − 561
| (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
+ − 562
((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
+ − 563
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
944
6267ad688ea8
2 cases for regularize with split, lemmas with split now lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 564
1000
+ − 565
| (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)),
+ − 566
((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) =>
+ − 567
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
944
6267ad688ea8
2 cases for regularize with split, lemmas with split now lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 568
758
+ − 569
| (t1 $ t2, t1' $ t2') =>
1000
+ − 570
regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
758
+ − 571
+ − 572
| (Bound i, Bound i') =>
1128
+ − 573
if i = i' then rtrm
1450
+ − 574
else raise (error "regularize (bounds mismatch)")
758
+ − 575
+ − 576
| _ =>
1128
+ − 577
let
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 578
val rtrm_str = Syntax.string_of_term ctxt rtrm
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 579
val qtrm_str = Syntax.string_of_term ctxt qtrm
758
+ − 580
in
1450
+ − 581
raise (error ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
758
+ − 582
end
+ − 583
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 584
fun regularize_trm_chk ctxt (rtrm, qtrm) =
1128
+ − 585
regularize_trm ctxt (rtrm, qtrm)
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 586
|> Syntax.check_term ctxt
758
+ − 587
797
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 588
849
+ − 589
+ − 590
(*** Rep/Abs Injection ***)
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 591
758
+ − 592
(*
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 593
Injection of Rep/Abs means:
758
+ − 594
849
+ − 595
For abstractions:
+ − 596
1128
+ − 597
* If the type of the abstraction needs lifting, then we add Rep/Abs
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 598
around the abstraction; otherwise we leave it unchanged.
1128
+ − 599
758
+ − 600
For applications:
1128
+ − 601
+ − 602
* If the application involves a bounded quantifier, we recurse on
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 603
the second argument. If the application is a bounded abstraction,
782
+ − 604
we always put an Rep/Abs around it (since bounded abstractions
1128
+ − 605
are assumed to always need lifting). Otherwise we recurse on both
782
+ − 606
arguments.
758
+ − 607
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 608
For constants:
758
+ − 609
1128
+ − 610
* If the constant is (op =), we leave it always unchanged.
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 611
Otherwise the type of the constant needs lifting, we put
1128
+ − 612
and Rep/Abs around it.
758
+ − 613
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 614
For free variables:
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 615
797
35436401f00d
added a functor that allows checking what is added to the theorem lists
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 616
* We put a Rep/Abs around it if the type needs lifting.
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 617
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 618
Vars case cannot occur.
758
+ − 619
*)
+ − 620
1128
+ − 621
fun mk_repabs ctxt (T, T') trm =
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 622
absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
758
+ − 623
833
129caba33c03
the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 624
fun inj_repabs_err ctxt msg rtrm qtrm =
129caba33c03
the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 625
let
129caba33c03
the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 626
val rtrm_str = Syntax.string_of_term ctxt rtrm
1128
+ − 627
val qtrm_str = Syntax.string_of_term ctxt qtrm
833
129caba33c03
the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 628
in
1450
+ − 629
raise error (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
833
129caba33c03
the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 630
end
129caba33c03
the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 631
758
+ − 632
849
+ − 633
(* bound variables need to be treated properly,
+ − 634
as the type of subterms needs to be calculated *)
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 635
fun inj_repabs_trm ctxt (rtrm, qtrm) =
758
+ − 636
case (rtrm, qtrm) of
+ − 637
(Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 638
Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
758
+ − 639
+ − 640
| (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 641
Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
758
+ − 642
+ − 643
| (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
+ − 644
let
+ − 645
val rty = fastype_of rtrm
+ − 646
val qty = fastype_of qtrm
+ − 647
in
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 648
mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
758
+ − 649
end
+ − 650
+ − 651
| (Abs (x, T, t), Abs (x', T', t')) =>
+ − 652
let
+ − 653
val rty = fastype_of rtrm
+ − 654
val qty = fastype_of qtrm
+ − 655
val (y, s) = Term.dest_abs (x, T, t)
+ − 656
val (_, s') = Term.dest_abs (x', T', t')
+ − 657
val yvar = Free (y, T)
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 658
val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
758
+ − 659
in
+ − 660
if rty = qty then result
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 661
else mk_repabs ctxt (rty, qty) result
758
+ − 662
end
+ − 663
1128
+ − 664
| (t $ s, t' $ s') =>
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 665
(inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
758
+ − 666
1128
+ − 667
| (Free (_, T), Free (_, T')) =>
+ − 668
if T = T' then rtrm
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 669
else mk_repabs ctxt (T, T') rtrm
758
+ − 670
+ − 671
| (_, Const (@{const_name "op ="}, _)) => rtrm
+ − 672
+ − 673
| (_, Const (_, T')) =>
+ − 674
let
+ − 675
val rty = fastype_of rtrm
1128
+ − 676
in
758
+ − 677
if rty = T' then rtrm
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 678
else mk_repabs ctxt (rty, T') rtrm
1128
+ − 679
end
+ − 680
833
129caba33c03
the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 681
| _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
758
+ − 682
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 683
fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
1128
+ − 684
inj_repabs_trm ctxt (rtrm, qtrm)
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 685
|> Syntax.check_term ctxt
776
d1064fa29424
renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 686
1077
+ − 687
+ − 688
1094
+ − 689
(*** Wrapper for automatically transforming an rthm into a qthm ***)
1072
+ − 690
1094
+ − 691
(* subst_tys takes a list of (rty, qty) substitution pairs
1085
+ − 692
and replaces all occurences of rty in the given type
+ − 693
by appropriate qty, with substitution *)
1070
+ − 694
fun subst_ty thy ty (rty, qty) r =
+ − 695
if r <> NONE then r else
1090
de2d1929899f
Fixed pattern matching, now the test in Abs works correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 696
case try (Sign.typ_match thy (rty, ty)) Vartab.empty of
1070
+ − 697
SOME inst => SOME (Envir.subst_type inst qty)
+ − 698
| NONE => NONE
+ − 699
fun subst_tys thy substs ty =
+ − 700
case fold (subst_ty thy ty) substs NONE of
+ − 701
SOME ty => ty
+ − 702
| NONE =>
+ − 703
(case ty of
+ − 704
Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
+ − 705
| x => x)
+ − 706
1094
+ − 707
(* subst_trms takes a list of (rtrm, qtrm) substitution pairs
1113
+ − 708
and if the given term matches any of the raw terms it
1085
+ − 709
returns the appropriate qtrm instantiated. If none of
+ − 710
them matched it returns NONE. *)
1078
+ − 711
fun subst_trm thy t (rtrm, qtrm) s =
1071
+ − 712
if s <> NONE then s else
1090
de2d1929899f
Fixed pattern matching, now the test in Abs works correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 713
case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of
1078
+ − 714
SOME inst => SOME (Envir.subst_term inst qtrm)
1071
+ − 715
| NONE => NONE;
+ − 716
fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
+ − 717
1085
+ − 718
(* prepares type and term substitution pairs to be used by above
+ − 719
functions that let replace all raw constructs by appropriate
+ − 720
lifted counterparts. *)
1070
+ − 721
fun get_ty_trm_substs ctxt =
+ − 722
let
+ − 723
val thy = ProofContext.theory_of ctxt
1094
+ − 724
val quot_infos = Quotient_Info.quotdata_dest ctxt
+ − 725
val const_infos = Quotient_Info.qconsts_dest ctxt
1070
+ − 726
val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
+ − 727
val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
+ − 728
fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
+ − 729
val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
+ − 730
in
1077
+ − 731
(ty_substs, const_substs @ rel_substs)
1070
+ − 732
end
+ − 733
1188
+ − 734
fun quotient_lift_const (b, t) ctxt =
+ − 735
let
+ − 736
val thy = ProofContext.theory_of ctxt
+ − 737
val (ty_substs, _) = get_ty_trm_substs ctxt;
+ − 738
val (_, ty) = dest_Const t;
+ − 739
val nty = subst_tys thy ty_substs ty;
+ − 740
in
+ − 741
Free(b, nty)
+ − 742
end
1085
+ − 743
+ − 744
(*
1094
+ − 745
Takes a term and
1085
+ − 746
1094
+ − 747
* replaces raw constants by the quotient constants
1085
+ − 748
+ − 749
* replaces equivalence relations by equalities
+ − 750
1094
+ − 751
* replaces raw types by the quotient types
+ − 752
1085
+ − 753
*)
+ − 754
1065
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 755
fun quotient_lift_all ctxt t =
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 756
let
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 757
val thy = ProofContext.theory_of ctxt
1070
+ − 758
val (ty_substs, substs) = get_ty_trm_substs ctxt
1065
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 759
fun lift_aux t =
1071
+ − 760
case subst_trms thy substs t of
1065
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 761
SOME x => x
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 762
| NONE =>
1070
+ − 763
(case t of
+ − 764
a $ b => lift_aux a $ lift_aux b
1072
+ − 765
| Abs(a, ty, s) =>
+ − 766
let
+ − 767
val (y, s') = Term.dest_abs (a, ty, s)
+ − 768
val nty = subst_tys thy ty_substs ty
+ − 769
in
1077
+ − 770
Abs(y, nty, abstract_over (Free (y, nty), lift_aux s'))
1070
+ − 771
end
1072
+ − 772
| Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
+ − 773
| Var(n, ty) => Var(n, subst_tys thy ty_substs ty)
1070
+ − 774
| Bound i => Bound i
1072
+ − 775
| Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
1065
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 776
in
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 777
lift_aux t
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 778
end
3664eafcad09
The automatic lifting translation function, still with dummy types,
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 779
758
+ − 780
end; (* structure *)