equal
deleted
inserted
replaced
414 section {* REGULARIZE *} |
414 section {* REGULARIZE *} |
415 |
415 |
416 text {* tyRel takes a type and builds a relation that a quantifier over this |
416 text {* tyRel takes a type and builds a relation that a quantifier over this |
417 type needs to respect. *} |
417 type needs to respect. *} |
418 ML {* |
418 ML {* |
|
419 fun matches (ty1, ty2) = |
|
420 Type.raw_instance (ty1, Logic.varifyT ty2); |
|
421 |
419 fun tyRel ty rty rel lthy = |
422 fun tyRel ty rty rel lthy = |
420 if ty = rty |
423 if matches (rty, ty) |
421 then rel |
424 then rel |
422 else (case ty of |
425 else (case ty of |
423 Type (s, tys) => |
426 Type (s, tys) => |
424 let |
427 let |
425 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
428 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
890 *} |
893 *} |
891 |
894 |
892 ML {* |
895 ML {* |
893 fun lookup_quot_data lthy qty = |
896 fun lookup_quot_data lthy qty = |
894 let |
897 let |
895 val SOME quotdata = find_first (fn x => #qtyp x = qty) (quotdata_lookup lthy) |
898 val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy) |
896 val rty = #rtyp quotdata |
899 val rty = Logic.unvarifyT (#rtyp quotdata) |
897 val rel = #rel quotdata |
900 val rel = #rel quotdata |
898 val rel_eqv = #equiv_thm quotdata |
901 val rel_eqv = #equiv_thm quotdata |
899 val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv] |
902 val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv] |
900 val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre] |
903 val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre] |
901 in |
904 in |