| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Logics_ZF/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle FOL_examples.thySprache: Isabelle |
|||||||||||||||
|
section‹Examples of Classical Reasoning› theory FOL_examples imports FOL begin lemma "EX y. ALL x. P(y)-->P(x)" 🍋 ‹@{subgoals[display,indent=0,margin=65]}› apply (rule exCI) 🍋 ‹@{subgoals[display,indent=0,margin=65]}› apply (rule allI) 🍋 ‹@{subgoals[display,indent=0,margin=65]}› apply (rule impI) 🍋 ‹@{subgoals[display,indent=0,margin=65]}› apply (erule allE) 🍋 ‹@{subgoals[display,indent=0,margin=65]}› txt‹see below for ‹allI› combined with ‹swap›\› apply (erule allI [THEN [2] swap]) 🍋 ‹@{subgoals[display,indent=0,margin=65]}› apply (rule impI) 🍋 ‹@{subgoals[display,indent=0,margin=65]}› apply (erule notE) 🍋 ‹@{subgoals[display,indent=0,margin=65]}› apply assumption done text ‹ @{thm[display] allI [THEN [2] swap]} › lemma "EX y. ALL x. P(y)-->P(x)" by blast end
¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet am 2026-05-01) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26