185 val args_aux = map (double_lookup rtyenv qtyenv) vs |
182 val args_aux = map (double_lookup rtyenv qtyenv) vs |
186 val args = map (absrep_fun flag ctxt) args_aux |
183 val args = map (absrep_fun flag ctxt) args_aux |
187 val map_fun = mk_mapfun ctxt vs rty_pat |
184 val map_fun = mk_mapfun ctxt vs rty_pat |
188 val result = list_comb (map_fun, args) |
185 val result = list_comb (map_fun, args) |
189 in |
186 in |
190 if tys' = [] orelse tys' = tys then absrep_const flag ctxt s' |
187 if tys' = [] orelse tys' = tys |
|
188 then absrep_const flag ctxt s' |
191 else mk_fun_compose flag (absrep_const flag ctxt s', result) |
189 else mk_fun_compose flag (absrep_const flag ctxt s', result) |
192 end |
190 end |
193 | (TFree x, TFree x') => |
191 | (TFree x, TFree x') => |
194 if x = x' |
192 if x = x' |
195 then mk_identity rty |
193 then mk_identity rty |
260 ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
258 ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
261 end |
259 end |
262 |
260 |
263 (* builds the aggregate equivalence relation *) |
261 (* builds the aggregate equivalence relation *) |
264 (* that will be the argument of Respects *) |
262 (* that will be the argument of Respects *) |
265 fun new_equiv_relation ctxt (rty, qty) = |
|
266 if rty = qty |
|
267 then HOLogic.eq_const rty |
|
268 else |
|
269 case (rty, qty) of |
|
270 (Type (s, tys), Type (s', tys')) => |
|
271 if s = s' |
|
272 then |
|
273 let |
|
274 val args = map (new_equiv_relation ctxt) (tys ~~ tys') |
|
275 in |
|
276 list_comb (get_relmap ctxt s, args) |
|
277 end |
|
278 else |
|
279 let |
|
280 val thy = ProofContext.theory_of ctxt |
|
281 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
|
282 val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty |
|
283 handle MATCH_TYPE => equiv_match_err ctxt rty_pat rty |
|
284 val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty |
|
285 handle MATCH_TYPE => equiv_match_err ctxt qty_pat qty |
|
286 val args_aux = map (double_lookup rtyenv qtyenv) vs |
|
287 val args = map (new_equiv_relation ctxt) args_aux |
|
288 val rel_map = mk_relmap ctxt vs rty_pat |
|
289 val result = list_comb (rel_map, args) |
|
290 val eqv_rel = get_equiv_rel ctxt s' |
|
291 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
|
292 in |
|
293 if tys' = [] orelse tys' = tys then eqv_rel' |
|
294 else mk_rel_compose (result, eqv_rel') |
|
295 end |
|
296 | _ => HOLogic.eq_const rty |
|
297 |
|
298 fun new_equiv_relation_chk ctxt (rty, qty) = |
|
299 new_equiv_relation ctxt (rty, qty) |
|
300 |> Syntax.check_term ctxt |
|
301 |
|
302 fun equiv_relation ctxt (rty, qty) = |
263 fun equiv_relation ctxt (rty, qty) = |
303 if rty = qty |
264 if rty = qty |
304 then HOLogic.eq_const rty |
265 then HOLogic.eq_const rty |
305 else |
266 else |
306 case (rty, qty) of |
267 case (rty, qty) of |
312 in |
273 in |
313 list_comb (get_relmap ctxt s, args) |
274 list_comb (get_relmap ctxt s, args) |
314 end |
275 end |
315 else |
276 else |
316 let |
277 let |
|
278 val thy = ProofContext.theory_of ctxt |
|
279 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
|
280 val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty |
|
281 handle MATCH_TYPE => equiv_match_err ctxt rty_pat rty |
|
282 val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty |
|
283 handle MATCH_TYPE => equiv_match_err ctxt qty_pat qty |
|
284 val args_aux = map (double_lookup rtyenv qtyenv) vs |
|
285 val args = map (equiv_relation ctxt) args_aux |
|
286 val rel_map = mk_relmap ctxt vs rty_pat |
|
287 val result = list_comb (rel_map, args) |
317 val eqv_rel = get_equiv_rel ctxt s' |
288 val eqv_rel = get_equiv_rel ctxt s' |
|
289 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
318 in |
290 in |
319 force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
291 if tys' = [] orelse tys' = tys |
|
292 then eqv_rel' |
|
293 else mk_rel_compose (result, eqv_rel') |
320 end |
294 end |
321 | _ => HOLogic.eq_const rty |
295 | _ => HOLogic.eq_const rty |
322 |
296 |
323 fun equiv_relation_chk ctxt (rty, qty) = |
297 fun equiv_relation_chk ctxt (rty, qty) = |
324 equiv_relation ctxt (rty, qty) |
298 equiv_relation ctxt (rty, qty) |
386 (Abs (x, ty, t), Abs (_, ty', t')) => |
360 (Abs (x, ty, t), Abs (_, ty', t')) => |
387 let |
361 let |
388 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
362 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
389 in |
363 in |
390 if ty = ty' then subtrm |
364 if ty = ty' then subtrm |
391 else mk_babs $ (mk_resp $ new_equiv_relation ctxt (ty, ty')) $ subtrm |
365 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
392 end |
366 end |
393 |
367 |
394 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
368 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
395 let |
369 let |
396 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
370 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
397 in |
371 in |
398 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
372 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
399 else mk_ball $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
373 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
400 end |
374 end |
401 |
375 |
402 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
376 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
403 let |
377 let |
404 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
378 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
405 in |
379 in |
406 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
380 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
407 else mk_bex $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
381 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
408 end |
382 end |
409 |
383 |
410 | (* equalities need to be replaced by appropriate equivalence relations *) |
384 | (* equalities need to be replaced by appropriate equivalence relations *) |
411 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
385 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
412 if ty = ty' then rtrm |
386 if ty = ty' then rtrm |
413 else new_equiv_relation ctxt (domain_type ty, domain_type ty') |
387 else equiv_relation ctxt (domain_type ty, domain_type ty') |
414 |
388 |
415 | (* in this case we just check whether the given equivalence relation is correct *) |
389 | (* in this case we just check whether the given equivalence relation is correct *) |
416 (rel, Const (@{const_name "op ="}, ty')) => |
390 (rel, Const (@{const_name "op ="}, ty')) => |
417 let |
391 let |
418 fun exc rel rel' = LIFT_MATCH ("regularise (relation mismatch)\n[" ^ |
392 fun exc rel rel' = LIFT_MATCH ("regularise (relation mismatch)\n[" ^ |
419 Syntax.string_of_term ctxt rel ^ " :: " ^ |
393 Syntax.string_of_term ctxt rel ^ " :: " ^ |
420 Syntax.string_of_typ ctxt (fastype_of rel) ^ "]\n[" ^ |
394 Syntax.string_of_typ ctxt (fastype_of rel) ^ "]\n[" ^ |
421 Syntax.string_of_term ctxt rel' ^ " :: " ^ |
395 Syntax.string_of_term ctxt rel' ^ " :: " ^ |
422 Syntax.string_of_typ ctxt (fastype_of rel') ^ "]") |
396 Syntax.string_of_typ ctxt (fastype_of rel') ^ "]") |
423 val rel_ty = fastype_of rel |
397 val rel_ty = fastype_of rel |
424 val rel' = new_equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
398 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
425 in |
399 in |
426 if rel' aconv rel then rtrm else raise (exc rel rel') |
400 if rel' aconv rel then rtrm else raise (exc rel rel') |
427 end |
401 end |
428 |
402 |
429 | (_, Const _) => |
403 | (_, Const _) => |