5 datatype flag = absF | repF |
5 datatype flag = absF | repF |
6 |
6 |
7 val absrep_fun: flag -> Proof.context -> (typ * typ) -> term |
7 val absrep_fun: flag -> Proof.context -> (typ * typ) -> term |
8 val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term |
8 val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term |
9 |
9 |
|
10 val new_equiv_relation: Proof.context -> (typ * typ) -> term |
|
11 val new_equiv_relation_chk: Proof.context -> (typ * typ) -> term |
|
12 |
10 val equiv_relation: Proof.context -> (typ * typ) -> term |
13 val equiv_relation: Proof.context -> (typ * typ) -> term |
11 val equiv_relation_chk: Proof.context -> (typ * typ) -> term |
14 val equiv_relation_chk: Proof.context -> (typ * typ) -> term |
12 |
15 |
13 val regularize_trm: Proof.context -> (term * term) -> term |
16 val regularize_trm: Proof.context -> (term * term) -> term |
14 val regularize_trm_chk: Proof.context -> (term * term) -> term |
17 val regularize_trm_chk: Proof.context -> (term * term) -> term |
37 fun negF absF = repF |
40 fun negF absF = repF |
38 | negF repF = absF |
41 | negF repF = absF |
39 |
42 |
40 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
43 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
41 |
44 |
42 fun mk_compose flag (trm1, trm2) = |
45 fun mk_fun_compose flag (trm1, trm2) = |
43 case flag of |
46 case flag of |
44 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
47 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
45 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
48 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
46 |
49 |
47 fun get_mapfun ctxt s = |
50 fun get_mapfun ctxt s = |
182 val args_aux = map (double_lookup rtyenv qtyenv) vs |
185 val args_aux = map (double_lookup rtyenv qtyenv) vs |
183 val args = map (absrep_fun flag ctxt) args_aux |
186 val args = map (absrep_fun flag ctxt) args_aux |
184 val map_fun = mk_mapfun ctxt vs rty_pat |
187 val map_fun = mk_mapfun ctxt vs rty_pat |
185 val result = list_comb (map_fun, args) |
188 val result = list_comb (map_fun, args) |
186 in |
189 in |
187 mk_compose flag (absrep_const flag ctxt s', result) |
190 mk_fun_compose flag (absrep_const flag ctxt s', result) |
188 end |
191 end |
189 | (TFree x, TFree x') => |
192 | (TFree x, TFree x') => |
190 if x = x' |
193 if x = x' |
191 then mk_identity rty |
194 then mk_identity rty |
192 else raise (LIFT_MATCH "absrep_fun (frees)") |
195 else raise (LIFT_MATCH "absrep_fun (frees)") |
210 val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty |
213 val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty |
211 in |
214 in |
212 map_types (Envir.subst_type ty_inst) trm |
215 map_types (Envir.subst_type ty_inst) trm |
213 end |
216 end |
214 |
217 |
|
218 fun mk_rel_compose (trm1, trm2) = |
|
219 Const (@{const_name "pred_comp"}, dummyT) $ trm1 $ trm2 |
|
220 |
215 fun get_relmap ctxt s = |
221 fun get_relmap ctxt s = |
216 let |
222 let |
217 val thy = ProofContext.theory_of ctxt |
223 val thy = ProofContext.theory_of ctxt |
218 val exc = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
224 val exc = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
219 val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc |
225 val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc |
220 in |
226 in |
221 Const (relmap, dummyT) |
227 Const (relmap, dummyT) |
222 end |
228 end |
223 |
229 |
|
230 fun mk_relmap ctxt vs rty = |
|
231 let |
|
232 val vs' = map (mk_Free) vs |
|
233 |
|
234 fun mk_relmap_aux rty = |
|
235 case rty of |
|
236 TVar _ => mk_Free rty |
|
237 | Type (_, []) => HOLogic.eq_const rty |
|
238 | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys) |
|
239 | _ => raise LIFT_MATCH ("mk_relmap (default)") |
|
240 in |
|
241 fold_rev Term.lambda vs' (mk_relmap_aux rty) |
|
242 end |
|
243 |
224 fun get_equiv_rel ctxt s = |
244 fun get_equiv_rel ctxt s = |
225 let |
245 let |
226 val thy = ProofContext.theory_of ctxt |
246 val thy = ProofContext.theory_of ctxt |
227 val exc = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
247 val exc = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
228 in |
248 in |
231 |
251 |
232 (* builds the aggregate equivalence relation *) |
252 (* builds the aggregate equivalence relation *) |
233 (* that will be the argument of Respects *) |
253 (* that will be the argument of Respects *) |
234 |
254 |
235 (* FIXME: check that the types correspond to each other *) |
255 (* FIXME: check that the types correspond to each other *) |
|
256 fun new_equiv_relation ctxt (rty, qty) = |
|
257 if rty = qty |
|
258 then HOLogic.eq_const rty |
|
259 else |
|
260 case (rty, qty) of |
|
261 (Type (s, tys), Type (s', tys')) => |
|
262 if s = s' |
|
263 then |
|
264 let |
|
265 val args = map (new_equiv_relation ctxt) (tys ~~ tys') |
|
266 in |
|
267 list_comb (get_relmap ctxt s, args) |
|
268 end |
|
269 else |
|
270 let |
|
271 val thy = ProofContext.theory_of ctxt |
|
272 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
|
273 val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty |
|
274 handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty |
|
275 val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty |
|
276 handle MATCH_TYPE => absrep_match_err ctxt qty_pat qty |
|
277 val args_aux = map (double_lookup rtyenv qtyenv) vs |
|
278 val args = map (new_equiv_relation ctxt) args_aux |
|
279 val rel_map = mk_relmap ctxt vs rty_pat |
|
280 val result = list_comb (rel_map, args) |
|
281 val eqv_rel = get_equiv_rel ctxt s' |
|
282 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
|
283 in |
|
284 mk_rel_compose (eqv_rel', result) |
|
285 end |
|
286 | _ => HOLogic.eq_const rty |
|
287 |
|
288 fun new_equiv_relation_chk ctxt (rty, qty) = |
|
289 new_equiv_relation ctxt (rty, qty) |
|
290 |> Syntax.check_term ctxt |
|
291 |
236 fun equiv_relation ctxt (rty, qty) = |
292 fun equiv_relation ctxt (rty, qty) = |
237 if rty = qty |
293 if rty = qty |
238 then HOLogic.eq_const rty |
294 then HOLogic.eq_const rty |
239 else |
295 else |
240 case (rty, qty) of |
296 case (rty, qty) of |