Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:proofs_and_induction [2008/02/21 11:21] vkuncak |
sav08:proofs_and_induction [2008/02/21 17:25] vkuncak |
||
---|---|---|---|
Line 77: | Line 77: | ||
Instead of proving a goal, you can assume its negation and prove any remaining goals (this generalizes proof by contradiction). | Instead of proving a goal, you can assume its negation and prove any remaining goals (this generalizes proof by contradiction). | ||
\[ | \[ | ||
- | \frac{\lnot P \vdash\} | + | \frac{\lnot P \vdash} |
{\vdash P} | {\vdash P} | ||
\] | \] | ||
Line 93: | Line 93: | ||
If you have a universally quantified assumption, you can instantiate universal quantifier with any value, denoted by term //t// (this is what "for all" means). You keep the original quantified assumption in case you need to instantiate it multiple times. | If you have a universally quantified assumption, you can instantiate universal quantifier with any value, denoted by term //t// (this is what "for all" means). You keep the original quantified assumption in case you need to instantiate it multiple times. | ||
\[ | \[ | ||
- | \frac{P(t), \forall x.P(x)} | + | \frac{P(t), \forall x.P(x) \vdash} |
{\forall x.P(x) \vdash} | {\forall x.P(x) \vdash} | ||
\] | \] | ||
Line 109: | Line 109: | ||
When you have an existentially quantified assumption, you can pick a witness for existential statement and denote it by fresh variable "x_0". Informally we would say "let $x_0$ be such $x$". | When you have an existentially quantified assumption, you can pick a witness for existential statement and denote it by fresh variable "x_0". Informally we would say "let $x_0$ be such $x$". | ||
\[ | \[ | ||
- | \frac{P(x_0)} | + | \frac{P(x_0) \vdash} |
{\exists x. P(x) \vdash} | {\exists x. P(x) \vdash} | ||
\] | \] | ||
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 ===== |