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:47]
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".
-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 =====
@@ Line 166: / Line 185: @@
 ==== Structural Induction =====
+Consider a language $L$ of function symbols.  Let $ar(f)$ denote the number of arguments (arity) of a function symbol $f \in L$.  Let ${\it Terms}(L)$ denote the set of all terms in this language.  To prove a property for all terms, we show that if the property holds for subterms, then it holds for the term built from these subterms.
+\[
+\frac{\bigwedge_{f \in L} \forall t_1,\ldots,t_{ar(f)}.\ (\bigwedge_{i=1}^{ar(f)} P(t_i)) \rightarrow P(f(t_1,\ldots,t_n))}
+     {\forall t \in {\it Terms}(L). P(t)}
+\]
   * [[Calculus of Computation Textbook]], Chapter 4 (some example refer to previous chapters, if you do not understand them, ignore them for now)