| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Tutorial/Misc/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 761 B |
|
Quelle prime_def.thySprache: Isabelle |
|||||||||||||||
|
(*<*) theory prime_def imports Main begin consts prime :: "nat ==> bool" (*>*) text‹ \begin{warn} A common mistake when writing definitions is to introduce extra free variables on the right-hand side. Consider the following, flawed definition (where ‹dvd› m @{term[display,quotes]"prime(p) ≡ 1 < p ∧ (m dvd p ⟶ (m=1 ∨ m=p))"} \par\noindent\hangindent=0pt Isabelle rejects this ``definition'' because of the extra 🍋‹m› on the right-hand side, which would introduce an inconsistency (why?). The correct version is @{term[display,quotes]"prime(p) ≡ 1 < p ∧ (∀m. m dvd p ⟶ (m=1 ∨ m=p))"} \end{warn} › (*<*) end (*>*)
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26