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:50]
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 163: / Line 182: @@
      {\forall n \in \mathbb{N}. P(n)}
 \]
 ==== Structural Induction =====
+Stepwise induction allows us to prove properties of natural numbers by proving that it holds for 0 and that it extends with each successor.  Structural induction similarly allows us to prove that if property holds for basic structures and that if it holds for smaller structures then it also holds for larger structures.  Examples of such structures are terms or expression trees.
+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)}
+\]
+Note that if $c$ is a constant we assume $ar(c)=0$.  Therefore, structural induction requires us to prove $P(c)$ for all constants $c \in L$.
   * [[Calculus of Computation Textbook]], Chapter 4 (some example refer to previous chapters, if you do not understand them, ignore them for now)