SSL Less_False.thy
Interaktion und PortierbarkeitIsabelle
(* Author: Tobias Nipkow *)
section \<open>Improved Simproc for $<$\<close>
theory Less_False imports Main begin
simproc_setup less_False ("(x::'a::order) < y") = \<open>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>\<open>less_eq\<close>, T);
val t = HOLogic.mk_Trueprop(le $ s $ r); incase find_first (prp t) prems of
NONE => let val t = HOLogic.mk_Trueprop(less $ s $ r) incase 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) \<close>
end
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.26Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
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 ist noch experimentell.
