| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/LibreOffice/vcl/source/edit/ (LibreOffice Version 25.8.3.2©) Datei vom 5.10.2025 mit Größe 17 kB |
|
Quellcode-Bibliothek Lemmas.thy Sprache: Isabelle |
|||||||||||||||
|
(* Title: HOL/HOLCF/IOA/NTP/Lemmas.thy Author: Tobias Nipkow & Konrad Slind *) theory Lemmas imports Main begin subsubsection ‹Logic› lemma neg_flip: "(X = (¬ Y)) = ((¬X) = Y)" by blast subsection ‹Sets› 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 ‹Arithmetic› lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))" by (simp add: diff_Suc split: nat.split) lemmas [simp] = hd_append set_lemmas end
¤ 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.0.0Bemerkung: (vorverarbeitet am 2026-09-29) ¤*Bot Zugriff |
|
||||||||||||||
2026-10-10