doc-src/Intro/advanced.tex
changeset 459 03b445551763
parent 348 1f5a94209c97
child 841 14b96e3bd4ab
equal deleted inserted replaced
458:877704b91847 459:03b445551763
   862 use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good
   862 use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good
   863 instantiation for~$\Var{P}$.
   863 instantiation for~$\Var{P}$.
   864 \begin{ttbox}
   864 \begin{ttbox}
   865 goal Nat.thy "~ (Suc(k) = k)";
   865 goal Nat.thy "~ (Suc(k) = k)";
   866 {\out Level 0}
   866 {\out Level 0}
   867 {\out ~Suc(k) = k}
   867 {\out Suc(k) ~= k}
   868 {\out  1. ~Suc(k) = k}
   868 {\out  1. Suc(k) ~= k}
   869 \ttbreak
   869 \ttbreak
   870 by (res_inst_tac [("n","k")] induct 1);
   870 by (res_inst_tac [("n","k")] induct 1);
   871 {\out Level 1}
   871 {\out Level 1}
   872 {\out ~Suc(k) = k}
   872 {\out Suc(k) ~= k}
   873 {\out  1. ~Suc(0) = 0}
   873 {\out  1. Suc(0) ~= 0}
   874 {\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
   874 {\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
   875 \end{ttbox}
   875 \end{ttbox}
   876 We should check that Isabelle has correctly applied induction.  Subgoal~1
   876 We should check that Isabelle has correctly applied induction.  Subgoal~1
   877 is the base case, with $k$ replaced by~0.  Subgoal~2 is the inductive step,
   877 is the base case, with $k$ replaced by~0.  Subgoal~2 is the inductive step,
   878 with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.
   878 with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.
   879 The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the
   879 The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the
   880 other rules of theory {\tt Nat}.  The base case holds by~\ttindex{Suc_neq_0}:
   880 other rules of theory {\tt Nat}.  The base case holds by~\ttindex{Suc_neq_0}:
   881 \begin{ttbox}
   881 \begin{ttbox}
   882 by (resolve_tac [notI] 1);
   882 by (resolve_tac [notI] 1);
   883 {\out Level 2}
   883 {\out Level 2}
   884 {\out ~Suc(k) = k}
   884 {\out Suc(k) ~= k}
   885 {\out  1. Suc(0) = 0 ==> False}
   885 {\out  1. Suc(0) = 0 ==> False}
   886 {\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
   886 {\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
   887 \ttbreak
   887 \ttbreak
   888 by (eresolve_tac [Suc_neq_0] 1);
   888 by (eresolve_tac [Suc_neq_0] 1);
   889 {\out Level 3}
   889 {\out Level 3}
   890 {\out ~Suc(k) = k}
   890 {\out Suc(k) ~= k}
   891 {\out  1. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
   891 {\out  1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
   892 \end{ttbox}
   892 \end{ttbox}
   893 The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
   893 The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
   894 Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
   894 Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
   895 $Suc(Suc(x)) = Suc(x)$:
   895 $Suc(Suc(x)) = Suc(x)$:
   896 \begin{ttbox}
   896 \begin{ttbox}
   897 by (resolve_tac [notI] 1);
   897 by (resolve_tac [notI] 1);
   898 {\out Level 4}
   898 {\out Level 4}
   899 {\out ~Suc(k) = k}
   899 {\out Suc(k) ~= k}
   900 {\out  1. !!x. [| ~Suc(x) = x; Suc(Suc(x)) = Suc(x) |] ==> False}
   900 {\out  1. !!x. [| Suc(x) ~= x; Suc(Suc(x)) = Suc(x) |] ==> False}
   901 \ttbreak
   901 \ttbreak
   902 by (eresolve_tac [notE] 1);
   902 by (eresolve_tac [notE] 1);
   903 {\out Level 5}
   903 {\out Level 5}
   904 {\out ~Suc(k) = k}
   904 {\out Suc(k) ~= k}
   905 {\out  1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
   905 {\out  1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
   906 \ttbreak
   906 \ttbreak
   907 by (eresolve_tac [Suc_inject] 1);
   907 by (eresolve_tac [Suc_inject] 1);
   908 {\out Level 6}
   908 {\out Level 6}
   909 {\out ~Suc(k) = k}
   909 {\out Suc(k) ~= k}
   910 {\out No subgoals!}
   910 {\out No subgoals!}
   911 \end{ttbox}
   911 \end{ttbox}
   912 
   912 
   913 
   913 
   914 \subsection{An example of ambiguity in {\tt resolve_tac}}
   914 \subsection{An example of ambiguity in {\tt resolve_tac}}
   981 packaged into a {\bf simplification set},\index{simplification sets} 
   981 packaged into a {\bf simplification set},\index{simplification sets} 
   982 or {\bf simpset}.  We take the standard simpset for first-order logic and
   982 or {\bf simpset}.  We take the standard simpset for first-order logic and
   983 insert the equations proved in the previous section, namely
   983 insert the equations proved in the previous section, namely
   984 $0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
   984 $0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
   985 \begin{ttbox}
   985 \begin{ttbox}
   986 val add_ss = FOL_ss addrews [add_0, add_Suc];
   986 val add_ss = FOL_ss addsimps [add_0, add_Suc];
   987 \end{ttbox}
   987 \end{ttbox}
   988 We state the goal for associativity of addition, and
   988 We state the goal for associativity of addition, and
   989 use \ttindex{res_inst_tac} to invoke induction on~$k$:
   989 use \ttindex{res_inst_tac} to invoke induction on~$k$:
   990 \begin{ttbox}
   990 \begin{ttbox}
   991 goal Nat.thy "(k+m)+n = k+(m+n)";
   991 goal Nat.thy "(k+m)+n = k+(m+n)";