(* Title: HOL/HOLCF/IOA/NTP/Lemmas.thy
Author: Tobias Nipkow & Konrad Slind
*)
theory Lemmas
imports Main
begin
subsubsection \<open>Logic\<close>
lemma neg_flip: "(X = (\ Y)) = ((\X) = Y)"
by blast
subsection \<open>Sets\<close>
lemma set_lemmas:
"f(x) \ (\x. {f(x)})"
"f x y \ (\x y. {f x y})"
"\a. (\x. a \ f(x)) \ a \ (\x. {f(x)})"
"\a. (\x y. a \ f x y) \ a \ (\x y. {f x y})"
by auto
subsection \<open>Arithmetic\<close>
lemma pred_suc: "0 (x - 1 = y) = (x = Suc(y))"
by (simp add: diff_Suc split: nat.split)
lemmas [simp] = hd_append set_lemmas
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
