Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:proofs_and_induction [2008/02/21 16:49] vkuncak |
sav08:proofs_and_induction [2008/02/21 17:25] vkuncak |
||
|---|---|---|---|
| Line 137: | Line 137: | ||
| More information: [[http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf|Isabelle tutorial]], Chapter 5 "The Rules of the Game". | More information: [[http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf|Isabelle tutorial]], Chapter 5 "The Rules of the Game". | ||
| - | Demo: Proving above example in Isabelle. | + | Demo: Proving above example in Isabelle. A working Isabelle script: |
| + | <code> | ||
| + | theory ForallExists imports Main | ||
| + | begin | ||
| + | |||
| + | lemma fe1: "(EX x. ALL y. F x y) --> (ALL u. EX v. F v u)" | ||
| + | apply (rule "impI") | ||
| + | apply (rule "allI") | ||
| + | apply (erule "exE") | ||
| + | apply (erule "allE") | ||
| + | apply (rule "exI") | ||
| + | apply assumption | ||
| + | done | ||
| + | |||
| + | lemma fe2: "(EX x. ALL y. F x y) --> (ALL u. EX v. F v u)" | ||
| + | apply auto | ||
| + | done | ||
| + | |||
| + | end | ||
| + | </code> | ||
| ===== Completeness for First-Order Logic ===== | ===== Completeness for First-Order Logic ===== | ||