equal
deleted
inserted
replaced
354 (case Quotient_Info.lookup_quotmaps ctxt s of |
354 (case Quotient_Info.lookup_quotmaps ctxt s of |
355 SOME map_data => Thm.transfer thy (#quot_thm map_data) |
355 SOME map_data => Thm.transfer thy (#quot_thm map_data) |
356 | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")")) |
356 | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")")) |
357 end |
357 end |
358 |
358 |
359 fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient}) |
359 fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient3}) |
360 |
360 |
361 infix 0 MRSL |
361 infix 0 MRSL |
362 |
362 |
363 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm |
363 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm |
364 |
364 |
373 |
373 |
374 fun mk_quot_thm_compose (rel_quot_thm, quot_thm) = |
374 fun mk_quot_thm_compose (rel_quot_thm, quot_thm) = |
375 let |
375 let |
376 val quot_thm_rel = get_rel_from_quot_thm quot_thm |
376 val quot_thm_rel = get_rel_from_quot_thm quot_thm |
377 in |
377 in |
378 if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient} |
378 if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient3} |
379 else raise NOT_IMPL "nested quotients: not implemented yet" |
379 else raise NOT_IMPL "nested quotients: not implemented yet" |
380 end |
380 end |
381 |
381 |
382 fun prove_quot_theorem ctxt (rty, qty) = |
382 fun prove_quot_theorem ctxt (rty, qty) = |
383 if rty = qty |
383 if rty = qty |
384 then @{thm identity_quotient} |
384 then @{thm identity_quotient3} |
385 else |
385 else |
386 case (rty, qty) of |
386 case (rty, qty) of |
387 (Type (s, tys), Type (s', tys')) => |
387 (Type (s, tys), Type (s', tys')) => |
388 if s = s' |
388 if s = s' |
389 then |
389 then |
408 val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s) |
408 val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s) |
409 in |
409 in |
410 mk_quot_thm_compose (rel_quot_thm, quot_thm) |
410 mk_quot_thm_compose (rel_quot_thm, quot_thm) |
411 end |
411 end |
412 end |
412 end |
413 | _ => @{thm identity_quotient} |
413 | _ => @{thm identity_quotient3} |
414 |
414 |
415 |
415 |
416 |
416 |
417 (*** Regularization ***) |
417 (*** Regularization ***) |
418 |
418 |