QuotMain.thy
changeset 257 68bd5c2a1b96
parent 255 264c7b9d19f4
child 259 22c199522bef
equal deleted inserted replaced
256:53d7477a1f94 257:68bd5c2a1b96
   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