equal
deleted
inserted
replaced
385 end |
385 end |
386 |
386 |
387 (* the major type of All and Ex quantifiers *) |
387 (* the major type of All and Ex quantifiers *) |
388 fun qnt_typ ty = domain_type (domain_type ty) |
388 fun qnt_typ ty = domain_type (domain_type ty) |
389 |
389 |
|
390 (* Checks that two types match, for example: |
|
391 rty -> rty matches qty -> qty *) |
|
392 fun matches_typ thy T T' = |
|
393 case (T, T') of |
|
394 (TFree _, TFree _) => true |
|
395 | (TVar _, TVar _) => true |
|
396 | (Type (s, tys), Type (s', tys')) => ( |
|
397 if T = T' then true else |
|
398 let |
|
399 val rty = #rtyp (Quotient_Info.quotdata_lookup thy s') |
|
400 in |
|
401 if Sign.typ_instance thy (T, rty) then true else false |
|
402 end |
|
403 handle Not_found => |
|
404 if length tys <> length tys' then false else |
|
405 (* 'andalso' is buildin syntax so it needs to be expanded *) |
|
406 fold (fn x => fn y => x andalso y) (map2 (matches_typ thy) tys tys') (s = s') |
|
407 ) |
|
408 | _ => false |
|
409 |
|
410 |
390 (* produces a regularized version of rtrm |
411 (* produces a regularized version of rtrm |
391 |
412 |
392 - the result might contain dummyTs |
413 - the result might contain dummyTs |
393 |
414 |
394 - for regularisation we do not need any |
415 - for regularisation we do not need any |
435 end |
456 end |
436 |
457 |
437 | (_, Const _) => |
458 | (_, Const _) => |
438 let |
459 let |
439 val thy = ProofContext.theory_of ctxt |
460 val thy = ProofContext.theory_of ctxt |
440 fun matches_typ T T' = |
461 fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T' |
441 case (T, T') of |
|
442 (TFree _, TFree _) => true |
|
443 | (TVar _, TVar _) => true |
|
444 | (Type (s, tys), Type (s', tys')) => ( |
|
445 (s = s' andalso tys = tys') orelse |
|
446 (* 'andalso' is buildin syntax so it needs to be expanded *) |
|
447 (fold (fn x => fn y => x andalso y) (map2 matches_typ tys tys') (s = s') |
|
448 handle UnequalLengths => false |
|
449 ) orelse |
|
450 let |
|
451 val rty = #rtyp (Quotient_Info.quotdata_lookup thy s') |
|
452 in |
|
453 Sign.typ_instance thy (T, rty) |
|
454 end |
|
455 handle Not_found => false (* raised by quotdata_lookup *) |
|
456 ) |
|
457 | _ => false |
|
458 fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ T T' |
|
459 | same_const _ _ = false |
462 | same_const _ _ = false |
460 in |
463 in |
461 if same_const rtrm qtrm then rtrm |
464 if same_const rtrm qtrm then rtrm |
462 else |
465 else |
463 let |
466 let |