185 val args_aux = map (double_lookup rtyenv qtyenv) vs |
185 val args_aux = map (double_lookup rtyenv qtyenv) vs |
186 val args = map (absrep_fun flag ctxt) args_aux |
186 val args = map (absrep_fun flag ctxt) args_aux |
187 val map_fun = mk_mapfun ctxt vs rty_pat |
187 val map_fun = mk_mapfun ctxt vs rty_pat |
188 val result = list_comb (map_fun, args) |
188 val result = list_comb (map_fun, args) |
189 in |
189 in |
190 mk_fun_compose flag (absrep_const flag ctxt s', result) |
190 if tys' = [] orelse tys' = tys then absrep_const flag ctxt s' |
191 end |
191 else mk_fun_compose flag (absrep_const flag ctxt s', result) |
|
192 end |
192 | (TFree x, TFree x') => |
193 | (TFree x, TFree x') => |
193 if x = x' |
194 if x = x' |
194 then mk_identity rty |
195 then mk_identity rty |
195 else raise (LIFT_MATCH "absrep_fun (frees)") |
196 else raise (LIFT_MATCH "absrep_fun (frees)") |
196 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
197 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
287 val rel_map = mk_relmap ctxt vs rty_pat |
288 val rel_map = mk_relmap ctxt vs rty_pat |
288 val result = list_comb (rel_map, args) |
289 val result = list_comb (rel_map, args) |
289 val eqv_rel = get_equiv_rel ctxt s' |
290 val eqv_rel = get_equiv_rel ctxt s' |
290 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
291 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
291 in |
292 in |
292 mk_rel_compose (result, eqv_rel') |
293 if tys' = [] orelse tys' = tys then eqv_rel' |
293 end |
294 else mk_rel_compose (result, eqv_rel') |
|
295 end |
294 | _ => HOLogic.eq_const rty |
296 | _ => HOLogic.eq_const rty |
295 |
297 |
296 fun new_equiv_relation_chk ctxt (rty, qty) = |
298 fun new_equiv_relation_chk ctxt (rty, qty) = |
297 new_equiv_relation ctxt (rty, qty) |
299 new_equiv_relation ctxt (rty, qty) |
298 |> Syntax.check_term ctxt |
300 |> Syntax.check_term ctxt |
384 (Abs (x, ty, t), Abs (_, ty', t')) => |
386 (Abs (x, ty, t), Abs (_, ty', t')) => |
385 let |
387 let |
386 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
388 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
387 in |
389 in |
388 if ty = ty' then subtrm |
390 if ty = ty' then subtrm |
389 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
391 else mk_babs $ (mk_resp $ new_equiv_relation ctxt (ty, ty')) $ subtrm |
390 end |
392 end |
391 |
393 |
392 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
394 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
393 let |
395 let |
394 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
396 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
395 in |
397 in |
396 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
398 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
397 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
399 else mk_ball $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
398 end |
400 end |
399 |
401 |
400 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
402 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
401 let |
403 let |
402 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
404 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
403 in |
405 in |
404 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
406 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
405 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
407 else mk_bex $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
406 end |
408 end |
407 |
409 |
408 | (* equalities need to be replaced by appropriate equivalence relations *) |
410 | (* equalities need to be replaced by appropriate equivalence relations *) |
409 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
411 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
410 if ty = ty' then rtrm |
412 if ty = ty' then rtrm |
411 else equiv_relation ctxt (domain_type ty, domain_type ty') |
413 else new_equiv_relation ctxt (domain_type ty, domain_type ty') |
412 |
414 |
413 | (* in this case we just check whether the given equivalence relation is correct *) |
415 | (* in this case we just check whether the given equivalence relation is correct *) |
414 (rel, Const (@{const_name "op ="}, ty')) => |
416 (rel, Const (@{const_name "op ="}, ty')) => |
415 let |
417 let |
416 val exc = LIFT_MATCH "regularise (relation mismatch)" |
418 fun exc rel rel' = LIFT_MATCH ("regularise (relation mismatch)\n[" ^ |
|
419 Syntax.string_of_term ctxt rel ^ " :: " ^ |
|
420 Syntax.string_of_typ ctxt (fastype_of rel) ^ "]\n[" ^ |
|
421 Syntax.string_of_term ctxt rel' ^ " :: " ^ |
|
422 Syntax.string_of_typ ctxt (fastype_of rel') ^ "]") |
417 val rel_ty = fastype_of rel |
423 val rel_ty = fastype_of rel |
418 val rel' = equiv_relation ctxt (domain_type rel_ty, domain_type ty') |
424 val rel' = new_equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
419 in |
425 in |
420 if rel' aconv rel then rtrm else raise exc |
426 if rel' aconv rel then rtrm else raise (exc rel rel') |
421 end |
427 end |
422 |
428 |
423 | (_, Const _) => |
429 | (_, Const _) => |
424 let |
430 let |
425 fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*) |
431 fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*) |