simproc_setup less_False ("(x::'a::order) < y") = ‹K (fn ctxt => fn ct =>
let
fun prp t thm = Thm.full_prop_of thm aconv t;
val eq_False_if_not = @{thm eq_False} RS iffD2
fun prove_less_False ((less as Const(_,T)) $ r $ s) =
let val prems = Simplifier.prems_of ctxt;
val le = Const (const_name‹less_eq›, T);
val t = HOLogic.mk_Trueprop(le $ s $ r);
in case find_first (prp t) prems of
NONE =>
let val t = HOLogic.mk_Trueprop(less $ s $ r)
in case find_first (prp t) prems of
NONE => NONE
| SOME thm => SOME(mk_meta_eq((thm RS @{thm less_not_sym}) RS eq_False_if_not))
end
| SOME thm => NONE
end;
in prove_less_False (Thm.term_of ct) end) ›
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-06-30)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
