doc-src/Logics/FOL.tex
 changeset 874 2432820efbfe parent 706 31b1e4f9af30 child 1388 7705e6211865
equal inserted replaced
873:0cfc734e3dbd 874:2432820efbfe
   612 by (assume_tac 1);
   612 by (assume_tac 1);
   613 {\out Level 8}
   613 {\out Level 8}
   614 {\out EX y. ALL x. P(y) --> P(x)}
   614 {\out EX y. ALL x. P(y) --> P(x)}
   615 {\out No subgoals!}
   615 {\out No subgoals!}
   616 \end{ttbox}
   616 \end{ttbox}
   617 The civilised way to prove this theorem is through \ttindex{best_tac},
   617 The civilised way to prove this theorem is through \ttindex{deepen_tac},
   618 supplying the classical version of~$(\exists I)$:
   618 which automatically uses the classical version of~$(\exists I)$:
   619 \begin{ttbox}
   619 \begin{ttbox}
   620 goal FOL.thy "EX y. ALL x. P(y)-->P(x)";
   620 goal FOL.thy "EX y. ALL x. P(y)-->P(x)";
   621 {\out Level 0}
   621 {\out Level 0}
   622 {\out EX y. ALL x. P(y) --> P(x)}
   622 {\out EX y. ALL x. P(y) --> P(x)}
   623 {\out  1. EX y. ALL x. P(y) --> P(x)}
   623 {\out  1. EX y. ALL x. P(y) --> P(x)}
   624 by (best_tac FOL_dup_cs 1);
   624 by (deepen_tac FOL_cs 0 1);

   625 {\out Depth = 0}

   626 {\out Depth = 2}
   625 {\out Level 1}
   627 {\out Level 1}
   626 {\out EX y. ALL x. P(y) --> P(x)}
   628 {\out EX y. ALL x. P(y) --> P(x)}
   627 {\out No subgoals!}
   629 {\out No subgoals!}
   628 \end{ttbox}
   630 \end{ttbox}
   629 If this theorem seems counterintuitive, then perhaps you are an
   631 If this theorem seems counterintuitive, then perhaps you are an