Differences

This shows you the differences between two versions of the page.

--- sav08:proofs_and_induction [2008/02/21 16:49]
vkuncak
+++ sav08:proofs_and_induction [2008/02/21 17:25]
vkuncak
@@ 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.
 \[
-\frac{P(t), \forall x.P(x)}
+\frac{P(t), \forall x.P(x) \vdash}
      {\forall 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".
-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 =====