409 in |
409 in |
410 if rel' aconv rel then rtrm else raise (exc rel rel') |
410 if rel' aconv rel then rtrm else raise (exc rel rel') |
411 end |
411 end |
412 |
412 |
413 | (_, Const _) => |
413 | (_, Const _) => |
414 let |
414 let |
415 fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*) |
415 val thy = ProofContext.theory_of ctxt |
416 | same_name _ _ = false |
416 fun matches_typ T T' = ( |
417 (* TODO/FIXME: This test is not enough. *) |
417 let |
418 (* Why? *) |
418 val rty = #rtyp (quotdata_lookup_type thy T') |
419 (* Because constants can have the same name but not be the same |
419 in |
420 constant. All overloaded constants have the same name but because |
420 if Sign.typ_instance thy (T, rty) then true else T = T' |
421 of different types they do differ. |
421 end |
422 |
422 handle Not_found => (* raised by quotdata_lookup_type *) |
423 This code will let one write a theorem where plus on nat is |
423 case (T, T') of |
424 matched to plus on int, even if the latter is defined differently. |
424 (TFree _, TFree _) => true |
425 |
425 | (TVar _, TVar _) => true |
426 This would result in hard to understand failures in injection and |
426 | (Type (s, tys), Type (s', tys')) => |
427 cleaning. *) |
427 (* 'andalso' is buildin syntax so it needs to be expanded *) |
428 (* cu: if I also test the type, then something else breaks *) |
428 fold (fn x => fn y => x andalso y) (map2 matches_typ tys tys') (s = s') |
|
429 handle UnequalLengths => false |
|
430 ) |
|
431 fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ T T' |
|
432 | same_const _ _ = false |
429 in |
433 in |
430 if same_name rtrm qtrm then rtrm |
434 if same_const rtrm qtrm then rtrm |
431 else |
435 else |
432 let |
436 let |
433 val thy = ProofContext.theory_of ctxt |
|
434 val qtrm_str = Syntax.string_of_term ctxt qtrm |
437 val qtrm_str = Syntax.string_of_term ctxt qtrm |
435 val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") |
438 val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") |
436 val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") |
439 val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") |
437 val rtrm' = #rconst (qconsts_lookup thy qtrm) handle NotFound => raise exc1 |
440 val rtrm' = #rconst (qconsts_lookup thy qtrm) handle NotFound => raise exc1 |
438 in |
441 in |