| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Tutorial/Rules/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle Blast.thySprache: Isabelle |
|||||||||||||||
|
theory Blast imports Main begin lemma "((∃x. ∀y. p(x)=p(y)) = ((∃x. q(x))=(∀y. p(y)))) = ((∃x. ∀y. q(x)=q(y)) = ((∃x. p(x))=(∀y. q(y))))" by blast text‹\noindent Until now, we have proved everything using only induction and simplification. Substantial proofs require more elaborate types of inference.› lemma "(∀x. honest(x) ∧ industrious(x) ⟶ healthy(x)) ∧ ¬ (∃x. grocer(x) ∧ healthy(x)) ∧ (∀x. industrious(x) ∧ grocer(x) ⟶ honest(x)) ∧ (∀x. cyclist(x) ⟶ industrious(x)) ∧ (∀x. ¬healthy(x) ∧ cyclist(x) ⟶ ¬honest(x)) ⟶ (∀x. grocer(x) ⟶ ¬cyclist(x))" by blast lemma "(∪i∈I. A(i)) ∩ (∪j∈J. B(j)) = (∪i∈I. ∪j∈J. A(i) ∩ B(j))" by blast text ‹ @{thm[display] mult_is_0} \rulename{mult_is_0}} @{thm[display] finite_Un} \rulename{finite_Un}} › lemma [iff]: "(xs@ys = []) = (xs=[] & ys=[])" apply (induct_tac xs) by (simp_all) (*ideas for uses of intro, etc.: ex/Primes/is_gcd_unique?*) end
¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet am 2026-04-28) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26