author  kleing 
Mon, 29 Dec 2003 06:49:26 +0100  
changeset 14333  14f29eb097a3 
parent 14158  15bab630ae31 
child 30099  dde11464969c 
permissions  rwrr 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1 
%% $Id$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

2 
\chapter{FirstOrder Logic} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

3 
\index{firstorder logic(} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

4 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

5 
Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

6 
nk}. Intuitionistic firstorder logic is defined first, as theory 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

7 
\thydx{IFOL}. Classical logic, theory \thydx{FOL}, is 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

8 
obtained by adding the double negation rule. Basic proof procedures are 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

9 
provided. The intuitionistic prover works with derived rules to simplify 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

10 
implications in the assumptions. Classical~\texttt{FOL} employs Isabelle's 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

11 
classical reasoner, which simulates a sequent calculus. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

12 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

13 
\section{Syntax and rules of inference} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

14 
The logic is manysorted, using Isabelle's type classes. The class of 
14154  15 
firstorder terms is called \cldx{term} and is a subclass of \isa{logic}. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

16 
No types of individuals are provided, but extensions can define types such 
14154  17 
as \isa{nat::term} and type constructors such as \isa{list::(term)term} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

18 
(see the examples directory, \texttt{FOL/ex}). Below, the type variable 
14154  19 
$\alpha$ ranges over class \isa{term}; the equality symbol and quantifiers 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

20 
are polymorphic (manysorted). The type of formulae is~\tydx{o}, which 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

21 
belongs to class~\cldx{logic}. Figure~\ref{folsyntax} gives the syntax. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

22 
Note that $a$\verb~=$b$ is translated to $\neg(a=b)$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

23 

14154  24 
Figure~\ref{folrules} shows the inference rules with their names. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

25 
Negation is defined in the usual way for intuitionistic logic; $\neg P$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

26 
abbreviates $P\imp\bot$. The biconditional~($\bimp$) is defined through 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

27 
$\conj$ and~$\imp$; introduction and elimination rules are derived for it. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

28 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

29 
The unique existence quantifier, $\exists!x.P(x)$, is defined in terms 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

30 
of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

31 
quantifications. For instance, $\exists!x\;y.P(x,y)$ abbreviates 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

32 
$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

33 
exists a unique pair $(x,y)$ satisfying~$P(x,y)$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

34 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

35 
Some intuitionistic derived rules are shown in 
14154  36 
Fig.\ts\ref{folintderived}, again with their names. These include 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

37 
rules for the defined symbols $\neg$, $\bimp$ and $\exists!$. Natural 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

38 
deduction typically involves a combination of forward and backward 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

39 
reasoning, particularly with the destruction rules $(\conj E)$, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

40 
$({\imp}E)$, and~$(\forall E)$. Isabelle's backward style handles these 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

41 
rules badly, so sequentstyle rules are derived to eliminate conjunctions, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

42 
implications, and universal quantifiers. Used with elimresolution, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

43 
\tdx{allE} eliminates a universal quantifier while \tdx{all_dupE} 
14154  44 
reinserts the quantified formula for later use. The rules 
45 
\isa{conj\_impE}, etc., support the intuitionistic proof procedure 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

46 
(see~\S\ref{folintprover}). 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

47 

14154  48 
See the online theory library for complete listings of the rules and 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

49 
derived rules. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

50 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

51 
\begin{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

52 
\begin{center} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

53 
\begin{tabular}{rrr} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

54 
\it name &\it metatype & \it description \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

55 
\cdx{Trueprop}& $o\To prop$ & coercion to $prop$\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

56 
\cdx{Not} & $o\To o$ & negation ($\neg$) \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

57 
\cdx{True} & $o$ & tautology ($\top$) \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

58 
\cdx{False} & $o$ & absurdity ($\bot$) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

59 
\end{tabular} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

60 
\end{center} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

61 
\subcaption{Constants} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

62 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

63 
\begin{center} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

64 
\begin{tabular}{llrrr} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

65 
\it symbol &\it name &\it metatype & \it priority & \it description \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

66 
\sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

67 
universal quantifier ($\forall$) \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

68 
\sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

69 
existential quantifier ($\exists$) \\ 
14154  70 
\isa{EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 & 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

71 
unique existence ($\exists!$) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

72 
\end{tabular} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

73 
\index{*"E"X"! symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

74 
\end{center} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

75 
\subcaption{Binders} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

76 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

77 
\begin{center} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

78 
\index{*"= symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

79 
\index{&@{\tt\&} symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

80 
\index{*" symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

81 
\index{*"""> symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

82 
\index{*"<""> symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

83 
\begin{tabular}{rrrr} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

84 
\it symbol & \it metatype & \it priority & \it description \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

85 
\tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

86 
\tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

87 
\tt  & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

88 
\tt > & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

89 
\tt <> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

90 
\end{tabular} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

91 
\end{center} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

92 
\subcaption{Infixes} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

93 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

94 
\dquotes 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

95 
\[\begin{array}{rcl} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

96 
formula & = & \hbox{expression of type~$o$} \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

97 
&  & term " = " term \quad \quad term " \ttilde= " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

98 
&  & "\ttilde\ " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

99 
&  & formula " \& " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

100 
&  & formula "  " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

101 
&  & formula " > " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

102 
&  & formula " <> " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

103 
&  & "ALL~" id~id^* " . " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

104 
&  & "EX~~" id~id^* " . " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

105 
&  & "EX!~" id~id^* " . " formula 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

106 
\end{array} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

107 
\] 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

108 
\subcaption{Grammar} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

109 
\caption{Syntax of \texttt{FOL}} \label{folsyntax} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

110 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

111 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

112 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

113 
\begin{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

114 
\begin{ttbox} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

115 
\tdx{refl} a=a 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

116 
\tdx{subst} [ a=b; P(a) ] ==> P(b) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

117 
\subcaption{Equality rules} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

118 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

119 
\tdx{conjI} [ P; Q ] ==> P&Q 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

120 
\tdx{conjunct1} P&Q ==> P 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

121 
\tdx{conjunct2} P&Q ==> Q 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

122 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

123 
\tdx{disjI1} P ==> PQ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

124 
\tdx{disjI2} Q ==> PQ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

125 
\tdx{disjE} [ PQ; P ==> R; Q ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

126 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

127 
\tdx{impI} (P ==> Q) ==> P>Q 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

128 
\tdx{mp} [ P>Q; P ] ==> Q 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

129 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

130 
\tdx{FalseE} False ==> P 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

131 
\subcaption{Propositional rules} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

132 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

133 
\tdx{allI} (!!x. P(x)) ==> (ALL x.P(x)) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

134 
\tdx{spec} (ALL x.P(x)) ==> P(x) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

135 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

136 
\tdx{exI} P(x) ==> (EX x.P(x)) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

137 
\tdx{exE} [ EX x.P(x); !!x. P(x) ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

138 
\subcaption{Quantifier rules} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

139 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

140 
\tdx{True_def} True == False>False 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

141 
\tdx{not_def} ~P == P>False 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

142 
\tdx{iff_def} P<>Q == (P>Q) & (Q>P) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

143 
\tdx{ex1_def} EX! x. P(x) == EX x. P(x) & (ALL y. P(y) > y=x) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

144 
\subcaption{Definitions} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

145 
\end{ttbox} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

146 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

147 
\caption{Rules of intuitionistic logic} \label{folrules} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

148 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

149 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

150 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

151 
\begin{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

152 
\begin{ttbox} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

153 
\tdx{sym} a=b ==> b=a 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

154 
\tdx{trans} [ a=b; b=c ] ==> a=c 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

155 
\tdx{ssubst} [ b=a; P(a) ] ==> P(b) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

156 
\subcaption{Derived equality rules} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

157 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

158 
\tdx{TrueI} True 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

159 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

160 
\tdx{notI} (P ==> False) ==> ~P 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

161 
\tdx{notE} [ ~P; P ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

162 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

163 
\tdx{iffI} [ P ==> Q; Q ==> P ] ==> P<>Q 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

164 
\tdx{iffE} [ P <> Q; [ P>Q; Q>P ] ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

165 
\tdx{iffD1} [ P <> Q; P ] ==> Q 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

166 
\tdx{iffD2} [ P <> Q; Q ] ==> P 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

167 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

168 
\tdx{ex1I} [ P(a); !!x. P(x) ==> x=a ] ==> EX! x. P(x) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

169 
\tdx{ex1E} [ EX! x.P(x); !!x.[ P(x); ALL y. P(y) > y=x ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

170 
] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

171 
\subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

172 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

173 
\tdx{conjE} [ P&Q; [ P; Q ] ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

174 
\tdx{impE} [ P>Q; P; Q ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

175 
\tdx{allE} [ ALL x.P(x); P(x) ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

176 
\tdx{all_dupE} [ ALL x.P(x); [ P(x); ALL x.P(x) ] ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

177 
\subcaption{Sequentstyle elimination rules} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

178 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

179 
\tdx{conj_impE} [ (P&Q)>S; P>(Q>S) ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

180 
\tdx{disj_impE} [ (PQ)>S; [ P>S; Q>S ] ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

181 
\tdx{imp_impE} [ (P>Q)>S; [ P; Q>S ] ==> Q; S ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

182 
\tdx{not_impE} [ ~P > S; P ==> False; S ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

183 
\tdx{iff_impE} [ (P<>Q)>S; [ P; Q>S ] ==> Q; [ Q; P>S ] ==> P; 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

184 
S ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

185 
\tdx{all_impE} [ (ALL x.P(x))>S; !!x.P(x); S ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

186 
\tdx{ex_impE} [ (EX x.P(x))>S; P(a)>S ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

187 
\end{ttbox} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

188 
\subcaption{Intuitionistic simplification of implication} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

189 
\caption{Derived rules for intuitionistic logic} \label{folintderived} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

190 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

191 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

192 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

193 
\section{Generic packages} 
9695  194 
FOL instantiates most of Isabelle's generic packages. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

195 
\begin{itemize} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

196 
\item 
14154  197 
It instantiates the simplifier, which is invoked through the method 
198 
\isa{simp}. Both equality ($=$) and the biconditional 

199 
($\bimp$) may be used for rewriting. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

200 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

201 
\item 
14154  202 
It instantiates the classical reasoner, which is invoked mainly through the 
203 
methods \isa{blast} and \isa{auto}. See~\S\ref{folclaprover} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

204 
for details. 
14154  205 
% 
206 
%\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for 

207 
% an equality throughout a subgoal and its hypotheses. This tactic uses FOL's 

208 
% general substitution rule. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

209 
\end{itemize} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

210 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

211 
\begin{warn}\index{simplification!of conjunctions}% 
14154  212 
Simplifying $a=b\conj P(a)$ to $a=b\conj P(b)$ is often advantageous. The 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

213 
left part of a conjunction helps in simplifying the right part. This effect 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

214 
is not available by default: it can be slow. It can be obtained by 
14154  215 
including the theorem \isa{conj_cong}\index{*conj_cong (rule)}% 
216 
as a congruence rule in 

217 
simplification, \isa{simp cong:\ conj\_cong}. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

218 
\end{warn} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

219 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

220 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

221 
\section{Intuitionistic proof procedures} \label{folintprover} 
14154  222 
Implication elimination (the rules~\isa{mp} and~\isa{impE}) pose 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

223 
difficulties for automated proof. In intuitionistic logic, the assumption 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

224 
$P\imp Q$ cannot be treated like $\neg P\disj Q$. Given $P\imp Q$, we may 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

225 
use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

226 
use of $P\imp Q$. If the proof of~$P$ fails then the whole branch of the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

227 
proof must be abandoned. Thus intuitionistic propositional logic requires 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

228 
backtracking. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

229 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

230 
For an elementary example, consider the intuitionistic proof of $Q$ from 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

231 
$P\imp Q$ and $(P\imp Q)\imp P$. The implication $P\imp Q$ is needed 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

232 
twice: 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

233 
\[ \infer[({\imp}E)]{Q}{P\imp Q & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

234 
\infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

235 
\] 
14154  236 
The theorem prover for intuitionistic logic does not use~\isa{impE}.\@ 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

237 
Instead, it simplifies implications using derived rules 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

238 
(Fig.\ts\ref{folintderived}). It reduces the antecedents of implications 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

239 
to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

240 
The rules \tdx{conj_impE} and \tdx{disj_impE} are 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

241 
straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

242 
$(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp 
14154  243 
S$. The other \ldots\isa{\_impE} rules are unsafe; the method requires 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

244 
backtracking. All the rules are derived in the same simple manner. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

245 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

246 
Dyckhoff has independently discovered similar rules, and (more importantly) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

247 
has demonstrated their completeness for propositional 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

248 
logic~\cite{dyckhoff}. However, the tactics given below are not complete 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

249 
for firstorder logic because they discard universally quantified 
14154  250 
assumptions after a single use. These are \ML{} functions, and are listed 
251 
below with their \ML{} type: 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

252 
\begin{ttbox} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

253 
mp_tac : int > tactic 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

254 
eq_mp_tac : int > tactic 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

255 
IntPr.safe_step_tac : int > tactic 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

256 
IntPr.safe_tac : tactic 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

257 
IntPr.inst_step_tac : int > tactic 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

258 
IntPr.step_tac : int > tactic 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

259 
IntPr.fast_tac : int > tactic 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

260 
IntPr.best_tac : int > tactic 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

261 
\end{ttbox} 
14158  262 
Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the 
263 
tactics of Isabelle's classical reasoner. There are no corresponding 

264 
Isar methods, but you can use the 

14154  265 
\isa{tactic} method to call \ML{} tactics in an Isar script: 
266 
\begin{isabelle} 

267 
\isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*}) 

268 
\end{isabelle} 

269 
Here is a description of each tactic: 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

270 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

271 
\begin{ttdescription} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

272 
\item[\ttindexbold{mp_tac} {\it i}] 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

273 
attempts to use \tdx{notE} or \tdx{impE} within the assumptions in 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

274 
subgoal $i$. For each assumption of the form $\neg P$ or $P\imp Q$, it 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

275 
searches for another assumption unifiable with~$P$. By 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

276 
contradiction with $\neg P$ it can solve the subgoal completely; by Modus 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

277 
Ponens it can replace the assumption $P\imp Q$ by $Q$. The tactic can 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

278 
produce multiple outcomes, enumerating all suitable pairs of assumptions. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

279 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

280 
\item[\ttindexbold{eq_mp_tac} {\it i}] 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

281 
is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns  thus, it 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

282 
is safe. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

283 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

284 
\item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

285 
subgoal~$i$. This may include proof by assumption or Modus Ponens (taking 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

286 
care not to instantiate unknowns), or \texttt{hyp_subst_tac}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

287 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

288 
\item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

289 
subgoals. It is deterministic, with at most one outcome. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

290 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

291 
\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac}, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

292 
but allows unknowns to be instantiated. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

293 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

294 
\item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

295 
inst_step_tac}, or applies an unsafe rule. This is the basic step of 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

296 
the intuitionistic proof procedure. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

297 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

298 
\item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

299 
depthfirst search, to solve subgoal~$i$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

300 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

301 
\item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

302 
bestfirst search (guided by the size of the proof state) to solve subgoal~$i$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

303 
\end{ttdescription} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

304 
Here are some of the theorems that \texttt{IntPr.fast_tac} proves 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

305 
automatically. The latter three date from {\it Principia Mathematica} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

306 
(*11.53, *11.55, *11.61)~\cite{principia}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

307 
\begin{ttbox} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

308 
~~P & ~~(P > Q) > ~~Q 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

309 
(ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y))) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

310 
(EX x y. P(x) & Q(x,y)) <> (EX x. P(x) & (EX y. Q(x,y))) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

311 
(EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y))) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

312 
\end{ttbox} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

313 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

314 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

315 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

316 
\begin{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

317 
\begin{ttbox} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

318 
\tdx{excluded_middle} ~P  P 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

319 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

320 
\tdx{disjCI} (~Q ==> P) ==> PQ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

321 
\tdx{exCI} (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

322 
\tdx{impCE} [ P>Q; ~P ==> R; Q ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

323 
\tdx{iffCE} [ P<>Q; [ P; Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

324 
\tdx{notnotD} ~~P ==> P 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

325 
\tdx{swap} ~P ==> (~Q ==> P) ==> Q 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

326 
\end{ttbox} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

327 
\caption{Derived rules for classical logic} \label{folcladerived} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

328 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

329 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

330 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

331 
\section{Classical proof procedures} \label{folclaprover} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

332 
The classical theory, \thydx{FOL}, consists of intuitionistic logic plus 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

333 
the rule 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

334 
$$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

335 
\noindent 
9695  336 
Natural deduction in classical logic is not really all that natural. FOL 
337 
derives classical introduction rules for $\disj$ and~$\exists$, as well as 

338 
classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see 

339 
Fig.\ts\ref{folcladerived}). 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

340 

14154  341 
The classical reasoner is installed. The most useful methods are 
342 
\isa{blast} (pure classical reasoning) and \isa{auto} (classical reasoning 

343 
combined with simplification), but the full range of 

344 
methods is available, including \isa{clarify}, 

345 
\isa{fast}, \isa{best} and \isa{force}. 

346 
See the 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

347 
\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

348 
{Chap.\ts\ref{chap:classical}} 
14154  349 
and the \emph{Tutorial}~\cite{isatutorial} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

350 
for more discussion of classical proof methods. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

351 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

352 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

353 
\section{An intuitionistic example} 
14158  354 
Here is a session similar to one in the book {\em Logic and Computation} 
355 
\cite[pages~2223]{paulson87}. It illustrates the treatment of 

356 
quantifier reasoning, which is different in Isabelle than it is in 

357 
{\sc lcf}based theorem provers such as {\sc hol}. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

358 

14158  359 
The theory header specifies that we are working in intuitionistic 
360 
logic by designating \isa{IFOL} rather than \isa{FOL} as the parent 

361 
theory: 

14154  362 
\begin{isabelle} 
363 
\isacommand{theory}\ IFOL\_examples\ =\ IFOL: 

364 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

365 
The proof begins by entering the goal, then applying the rule $({\imp}I)$. 
14154  366 
\begin{isabelle} 
367 
\isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ >\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline 

368 
\ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\ 

369 
\isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y)) 

370 
\isanewline 

371 
\isacommand{apply}\ (rule\ impI)\isanewline 

372 
\ 1.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\ 

373 
\isasymLongrightarrow \ \isasymforall x.\ \isasymexists y.\ Q(x,\ y) 

374 
\end{isabelle} 

375 
Isabelle's output is shown as it would appear using Proof General. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

376 
In this example, we shall never have more than one subgoal. Applying 
14154  377 
$({\imp}I)$ replaces~\isa{\isasymlongrightarrow} 
378 
by~\isa{\isasymLongrightarrow}, so that 

379 
\(\ex{y}\all{x}Q(x,y)\) becomes an assumption. We have the choice of 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

380 
$({\exists}E)$ and $({\forall}I)$; let us try the latter. 
14154  381 
\begin{isabelle} 
382 
\isacommand{apply}\ (rule\ allI)\isanewline 

383 
\ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\ 

384 
\isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)\hfill\((*)\) 

385 
\end{isabelle} 

386 
Applying $({\forall}I)$ replaces the \isa{\isasymforall 

387 
x} (in ASCII, \isa{ALL~x}) by \isa{\isasymAnd x} 

388 
(or \isa{!!x}), replacing FOL's universal quantifier by Isabelle's 

389 
meta universal quantifier. The bound variable is a {\bf parameter} of 

390 
the subgoal. We now must choose between $({\exists}I)$ and 

391 
$({\exists}E)$. What happens if the wrong rule is chosen? 

392 
\begin{isabelle} 

393 
\isacommand{apply}\ (rule\ exI)\isanewline 

394 
\ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\ 

395 
\isasymLongrightarrow \ Q(x,\ ?y2(x)) 

396 
\end{isabelle} 

397 
The new subgoal~1 contains the function variable \isa{?y2}. Instantiating 

398 
\isa{?y2} can replace~\isa{?y2(x)} by a term containing~\isa{x}, even 

399 
though~\isa{x} is a bound variable. Now we analyse the assumption 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

400 
\(\exists y.\forall x. Q(x,y)\) using elimination rules: 
14154  401 
\begin{isabelle} 
402 
\isacommand{apply}\ (erule\ exE)\isanewline 

403 
\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ \isasymLongrightarrow \ Q(x,\ ?y2(x)) 

404 
\end{isabelle} 

405 
Applying $(\exists E)$ has produced the parameter \isa{y} and stripped the 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

406 
existential quantifier from the assumption. But the subgoal is unprovable: 
14154  407 
there is no way to unify \isa{?y2(x)} with the bound variable~\isa{y}. 
408 
Using Proof General, we can return to the critical point, marked 

409 
$(*)$ above. This time we apply $({\exists}E)$: 

410 
\begin{isabelle} 

411 
\isacommand{apply}\ (erule\ exE)\isanewline 

412 
\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ 

413 
\isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y) 

414 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

415 
We now have two parameters and no scheme variables. Applying 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

416 
$({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

417 
applied to those parameters. Parameters should be produced early, as this 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

418 
example demonstrates. 
14154  419 
\begin{isabelle} 
420 
\isacommand{apply}\ (rule\ exI)\isanewline 

421 
\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ 

422 
\isasymLongrightarrow \ Q(x,\ ?y3(x,\ y)) 

423 
\isanewline 

424 
\isacommand{apply}\ (erule\ allE)\isanewline 

425 
\ 1.\ \isasymAnd x\ y.\ Q(?x4(x,\ y),\ y)\ \isasymLongrightarrow \ 

426 
Q(x,\ ?y3(x,\ y)) 

427 
\end{isabelle} 

428 
The subgoal has variables \isa{?y3} and \isa{?x4} applied to both 

429 
parameters. The obvious projection functions unify \isa{?x4(x,y)} with~\isa{ 

430 
x} and \isa{?y3(x,y)} with~\isa{y}. 

431 
\begin{isabelle} 

432 
\isacommand{apply}\ assumption\isanewline 

433 
No\ subgoals!\isanewline 

434 
\isacommand{done} 

435 
\end{isabelle} 

436 
The theorem was proved in six method invocations, not counting the 

437 
abandoned ones. But proof checking is tedious, and the \ML{} tactic 

438 
\ttindex{IntPr.fast_tac} can prove the theorem in one step. 

439 
\begin{isabelle} 

440 
\isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ >\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline 

441 
\ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\ 

442 
\isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y)) 

443 
\isanewline 

444 
\isacommand{by} (tactic {*IntPr.fast_tac 1*})\isanewline 

445 
No\ subgoals! 

446 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

447 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

448 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

449 
\section{An example of intuitionistic negation} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

450 
The following example demonstrates the specialized forms of implication 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

451 
elimination. Even propositional formulae can be difficult to prove from 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

452 
the basic rules; the specialized rules help considerably. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

453 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

454 
Propositional examples are easy to invent. As Dummett notes~\cite[page 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

455 
28]{dummett}, $\neg P$ is classically provable if and only if it is 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

456 
intuitionistically provable; therefore, $P$ is classically provable if and 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

457 
only if $\neg\neg P$ is intuitionistically provable.% 
14154  458 
\footnote{This remark holds only for propositional logic, not if $P$ is 
459 
allowed to contain quantifiers.} 

460 
% 

461 
Proving $\neg\neg P$ intuitionistically is 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

462 
much harder than proving~$P$ classically. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

463 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

464 
Our example is the double negation of the classical tautology $(P\imp 
14154  465 
Q)\disj (Q\imp P)$. The first step is apply the 
466 
\isa{unfold} method, which expands 

467 
negations to implications using the definition $\neg P\equiv P\imp\bot$ 

468 
and allows use of the special implication rules. 

469 
\begin{isabelle} 

470 
\isacommand{lemma}\ "\isachartilde \ \isachartilde \ ((P>Q)\ \ (Q>P))"\isanewline 

471 
\ 1.\ \isasymnot \ \isasymnot \ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)) 

472 
\isanewline 

473 
\isacommand{apply}\ (unfold\ not\_def)\isanewline 

474 
\ 1.\ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False)\ \isasymlongrightarrow \ False% 

475 
\end{isabelle} 

476 
The next step is a trivial use of $(\imp I)$. 

477 
\begin{isabelle} 

478 
\isacommand{apply}\ (rule\ impI)\isanewline 

479 
\ 1.\ (P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\ \isasymLongrightarrow \ False% 

480 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

481 
By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but 
14154  482 
that formula is not a theorem of intuitionistic logic. Instead, we 
483 
apply the specialized implication rule \tdx{disj_impE}. It splits the 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

484 
assumption into two assumptions, one for each disjunct. 
14154  485 
\begin{isabelle} 
486 
\isacommand{apply}\ (erule\ disj\_impE)\isanewline 

487 
\ 1.\ \isasymlbrakk (P\ \isasymlongrightarrow \ Q)\ \isasymlongrightarrow \ False;\ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ 

488 
False 

489 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

490 
We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

491 
their negations are inconsistent. Applying \tdx{imp_impE} breaks down 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

492 
the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

493 
assumptions~$P$ and~$\neg Q$. 
14154  494 
\begin{isabelle} 
495 
\isacommand{apply}\ (erule\ imp\_impE)\isanewline 

496 
\ 1.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ P;\ Q\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline 

497 
\ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ 

498 
False 

499 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

500 
Subgoal~2 holds trivially; let us ignore it and continue working on 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

501 
subgoal~1. Thanks to the assumption~$P$, we could prove $Q\imp P$; 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

502 
applying \tdx{imp_impE} is simpler. 
14154  503 
\begin{isabelle} 
504 
\ \isacommand{apply}\ (erule\ imp\_impE)\isanewline 

505 
\ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ Q;\ P\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ P\isanewline 

506 
\ 2.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline 

507 
\ 3.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ False% 

508 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

509 
The three subgoals are all trivial. 
14154  510 
\begin{isabelle} 
511 
\isacommand{apply}\ assumption\ \isanewline 

512 
\ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ 

513 
False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline 

514 
\ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ 

515 
\isasymlongrightarrow \ False;\ False\isasymrbrakk \ 

516 
\isasymLongrightarrow \ False% 

517 
\isanewline 

518 
\isacommand{apply}\ (erule\ FalseE)+\isanewline 

519 
No\ subgoals!\isanewline 

520 
\isacommand{done} 

521 
\end{isabelle} 

522 
This proof is also trivial for the \ML{} tactic \isa{IntPr.fast_tac}. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

523 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

524 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

525 
\section{A classical example} \label{folclaexample} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

526 
To illustrate classical logic, we shall prove the theorem 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

527 
$\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

528 
follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise 
14154  529 
$\all{x}P(x)$ is true. Either way the theorem holds. First, we must 
14158  530 
work in a theory based on classical logic, the theory \isa{FOL}: 
14154  531 
\begin{isabelle} 
532 
\isacommand{theory}\ FOL\_examples\ =\ FOL: 

533 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

534 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

535 
The formal proof does not conform in any obvious way to the sketch given 
14154  536 
above. Its key step is its first rule, \tdx{exCI}, a classical 
537 
version of~$(\exists I)$ that allows multiple instantiation of the 

538 
quantifier. 

539 
\begin{isabelle} 

540 
\isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)>P(x)"\isanewline 

541 
\ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x) 

542 
\isanewline 

543 
\isacommand{apply}\ (rule\ exCI)\isanewline 

544 
\ 1.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ \isasymforall x.\ P(?a)\ \isasymlongrightarrow \ P(x) 

545 
\end{isabelle} 

546 
We can either exhibit a term \isa{?a} to satisfy the conclusion of 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

547 
subgoal~1, or produce a contradiction from the assumption. The next 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

548 
steps are routine. 
14154  549 
\begin{isabelle} 
550 
\isacommand{apply}\ (rule\ allI)\isanewline 

551 
\ 1.\ \isasymAnd x.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ P(?a)\ \isasymlongrightarrow \ P(x) 

552 
\isanewline 

553 
\isacommand{apply}\ (rule\ impI)\isanewline 

554 
\ 1.\ \isasymAnd x.\ \isasymlbrakk \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x));\ P(?a)\isasymrbrakk \ \isasymLongrightarrow \ P(x) 

555 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

556 
By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$ 
14154  557 
is equivalent to applying~$(\exists I)$ again. 
558 
\begin{isabelle} 

559 
\isacommand{apply}\ (erule\ allE)\isanewline 

560 
\ 1.\ \isasymAnd x.\ \isasymlbrakk P(?a);\ \isasymnot \ (\isasymforall xa.\ P(?y3(x))\ \isasymlongrightarrow \ P(xa))\isasymrbrakk \ \isasymLongrightarrow \ P(x) 

561 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

562 
In classical logic, a negated assumption is equivalent to a conclusion. To 
8249  563 
get this effect, we create a swapped version of $(\forall I)$ and apply it 
14154  564 
using \ttindex{erule}. 
565 
\begin{isabelle} 

566 
\isacommand{apply}\ (erule\ allI\ [THEN\ [2]\ swap])\isanewline 

567 
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x)\isasymrbrakk \ \isasymLongrightarrow \ P(?y3(x))\ \isasymlongrightarrow \ P(xa) 

568 
\end{isabelle} 

569 
The operand of \isa{erule} above denotes the following theorem: 

570 
\begin{isabelle} 

571 
\ \ \ \ \isasymlbrakk \isasymnot \ (\isasymforall x.\ ?P1(x));\ 

572 
\isasymAnd x.\ \isasymnot \ ?P\ \isasymLongrightarrow \ 

573 
?P1(x)\isasymrbrakk \ 

574 
\isasymLongrightarrow \ ?P% 

575 
\end{isabelle} 

576 
The previous conclusion, \isa{P(x)}, has become a negated assumption. 

577 
\begin{isabelle} 

578 
\isacommand{apply}\ (rule\ impI)\isanewline 

579 
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(xa) 

580 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

581 
The subgoal has three assumptions. We produce a contradiction between the 
14154  582 
\index{assumptions!contradictory} assumptions~\isa{\isasymnot P(x)} 
583 
and~\isa{P(?y3(x))}. The proof never instantiates the 

584 
unknown~\isa{?a}. 

585 
\begin{isabelle} 

586 
\isacommand{apply}\ (erule\ notE)\isanewline 

587 
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(x) 

588 
\isanewline 

589 
\isacommand{apply}\ assumption\isanewline 

590 
No\ subgoals!\isanewline 

591 
\isacommand{done} 

592 
\end{isabelle} 

593 
The civilised way to prove this theorem is using the 

594 
\methdx{blast} method, which automatically uses the classical form 

595 
of the rule~$(\exists I)$: 

596 
\begin{isabelle} 

597 
\isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)>P(x)"\isanewline 

598 
\ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x) 

599 
\isanewline 

600 
\isacommand{by}\ blast\isanewline 

601 
No\ subgoals! 

602 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

603 
If this theorem seems counterintuitive, then perhaps you are an 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

604 
intuitionist. In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

605 
requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

606 
which we cannot do without further knowledge about~$P$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

607 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

608 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

609 
\section{Derived rules and the classical tactics} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

610 
Classical firstorder logic can be extended with the propositional 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

611 
connective $if(P,Q,R)$, where 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

612 
$$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

613 
Theorems about $if$ can be proved by treating this as an abbreviation, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

614 
replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals. But 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

615 
this duplicates~$P$, causing an exponential blowup and an unreadable 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

616 
formula. Introducing further abbreviations makes the problem worse. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

617 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

618 
Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

619 
directly, without reference to its definition. The simple identity 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

620 
\[ if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R) \] 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

621 
suggests that the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

622 
$if$introduction rule should be 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

623 
\[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}} \] 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

624 
The $if$elimination rule reflects the definition of $if(P,Q,R)$ and the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

625 
elimination rules for~$\disj$ and~$\conj$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

626 
\[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

627 
& \infer*{S}{[\neg P,R]}} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

628 
\] 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

629 
Having made these plans, we get down to work with Isabelle. The theory of 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

630 
classical logic, \texttt{FOL}, is extended with the constant 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

631 
$if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

632 
equation~$(if)$. 
14154  633 
\begin{isabelle} 
634 
\isacommand{theory}\ If\ =\ FOL:\isanewline 

635 
\isacommand{constdefs}\isanewline 

636 
\ \ if\ ::\ "[o,o,o]=>o"\isanewline 

637 
\ \ \ "if(P,Q,R)\ ==\ P\&Q\ \ \isachartilde P\&R" 

638 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

639 
We create the file \texttt{If.thy} containing these declarations. (This file 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

640 
is on directory \texttt{FOL/ex} in the Isabelle distribution.) Typing 
14154  641 
\begin{isabelle} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

642 
use_thy "If"; 
14154  643 
\end{isabelle} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

644 
loads that theory and sets it to be the current context. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

645 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

646 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

647 
\subsection{Deriving the introduction rule} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

648 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

649 
The derivations of the introduction and elimination rules demonstrate the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

650 
methods for rewriting with definitions. Classical reasoning is required, 
14154  651 
so we use \isa{blast}. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

652 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

653 
The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$, 
14154  654 
concludes $if(P,Q,R)$. We propose this lemma and immediately simplify 
655 
using \isa{if\_def} to expand the definition of \isa{if} in the 

656 
subgoal. 

657 
\begin{isabelle} 

658 
\isacommand{lemma}\ ifI: "[\ P\ ==>\ Q;\ \isachartilde P\ ==>\ R\ 

659 
]\ ==>\ if(P,Q,R)"\isanewline 

660 
\ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ Q,\ R) 

661 
\isanewline 

662 
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline 

663 
\ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ 

664 
R 

665 
\end{isabelle} 

666 
The rule's premises, although expressed using metalevel implication 

667 
(\isa{\isasymLongrightarrow}) are passed as ordinary implications to 

668 
\methdx{blast}. 

669 
\begin{isabelle} 

670 
\isacommand{apply}\ blast\isanewline 

671 
No\ subgoals!\isanewline 

672 
\isacommand{done} 

673 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

674 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

675 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

676 
\subsection{Deriving the elimination rule} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

677 
The elimination rule has three premises, two of which are themselves rules. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

678 
The conclusion is simply $S$. 
14154  679 
\begin{isabelle} 
680 
\isacommand{lemma}\ ifE:\isanewline 

681 
\ \ \ "[\ if(P,Q,R);\ \ [P;\ Q]\ ==>\ S;\ [\isachartilde P;\ R]\ ==>\ S\ ]\ ==>\ S"\isanewline 

682 
\ 1.\ \isasymlbrakk if(P,\ Q,\ R);\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S% 

683 
\isanewline 

684 
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline 

685 
\ 1.\ \isasymlbrakk P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R;\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S% 

686 
\end{isabelle} 

687 
The proof script is the same as before: \isa{simp} followed by 

688 
\isa{blast}: 

689 
\begin{isabelle} 

690 
\isacommand{apply}\ blast\isanewline 

691 
No\ subgoals!\isanewline 

692 
\isacommand{done} 

693 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

694 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

695 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

696 
\subsection{Using the derived rules} 
14154  697 
Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural 
698 
proofs of theorems such as the following: 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

699 
\begin{eqnarray*} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

700 
if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

701 
if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B)) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

702 
\end{eqnarray*} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

703 
Proofs also require the classical reasoning rules and the $\bimp$ 
14154  704 
introduction rule (called~\tdx{iffI}: do not confuse with~\isa{ifI}). 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

705 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

706 
To display the $if$rules in action, let us analyse a proof step by step. 
14154  707 
\begin{isabelle} 
708 
\isacommand{lemma}\ if\_commute:\isanewline 

709 
\ \ \ \ \ "if(P,\ if(Q,A,B),\ 

710 
if(Q,C,D))\ <>\ if(Q,\ if(P,A,C),\ if(P,B,D))"\isanewline 

711 
\isacommand{apply}\ (rule\ iffI)\isanewline 

712 
\ 1.\ if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))\ \isasymLongrightarrow \isanewline 

713 
\isaindent{\ 1.\ }if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 

714 
\ 2.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline 

715 
\isaindent{\ 2.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) 

716 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

717 
The $if$elimination rule can be applied twice in succession. 
14154  718 
\begin{isabelle} 
719 
\isacommand{apply}\ (erule\ ifE)\isanewline 

720 
\ 1.\ \isasymlbrakk P;\ if(Q,\ A,\ B)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 

721 
\ 2.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 

722 
\ 3.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline 

723 
\isaindent{\ 3.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) 

724 
\isanewline 

725 
\isacommand{apply}\ (erule\ ifE)\isanewline 

726 
\ 1.\ \isasymlbrakk P;\ Q;\ A\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 

727 
\ 2.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 

728 
\ 3.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 

729 
\ 4.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline 

730 
\isaindent{\ 4.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) 

731 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

732 
% 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

733 
In the first two subgoals, all assumptions have been reduced to atoms. Now 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

734 
$if$introduction can be applied. Observe how the $if$rules break down 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

735 
occurrences of $if$ when they become the outermost connective. 
14154  736 
\begin{isabelle} 
737 
\isacommand{apply}\ (rule\ ifI)\isanewline 

738 
\ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ A,\ C)\isanewline 

739 
\ 2.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline 

740 
\ 3.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 

741 
\ 4.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 

742 
\ 5.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline 

743 
\isaindent{\ 5.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) 

744 
\isanewline 

745 
\isacommand{apply}\ (rule\ ifI)\isanewline 

746 
\ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline 

747 
\ 2.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ C\isanewline 

748 
\ 3.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline 

749 
\ 4.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 

750 
\ 5.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 

751 
\ 6.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline 

752 
\isaindent{\ 6.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) 

753 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

754 
Where do we stand? The first subgoal holds by assumption; the second and 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

755 
third, by contradiction. This is getting tedious. We could use the classical 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

756 
reasoner, but first let us extend the default claset with the derived rules 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

757 
for~$if$. 
14154  758 
\begin{isabelle} 
759 
\isacommand{declare}\ ifI\ [intro!]\isanewline 

760 
\isacommand{declare}\ ifE\ [elim!] 

761 
\end{isabelle} 

762 
With these declarations, we could have proved this theorem with a single 

763 
call to \isa{blast}. Here is another example: 

764 
\begin{isabelle} 

765 
\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <>\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline 

766 
\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B)) 

767 
\isanewline 

768 
\isacommand{by}\ blast 

769 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

770 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

771 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

772 
\subsection{Derived rules versus definitions} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

773 
Dispensing with the derived rules, we can treat $if$ as an 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

774 
abbreviation, and let \ttindex{blast_tac} prove the expanded formula. Let 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

775 
us redo the previous proof: 
14154  776 
\begin{isabelle} 
777 
\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <>\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline 

778 
\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B)) 

779 
\end{isabelle} 

780 
This time, we simply unfold using the definition of $if$: 

781 
\begin{isabelle} 

782 
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline 

783 
\ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline 

784 
\isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ A\ \isasymor \ \isasymnot \ R\ \isasymand \ B) 

785 
\end{isabelle} 

786 
We are left with a subgoal in pure firstorder logic, and it falls to 

787 
\isa{blast}: 

788 
\begin{isabelle} 

789 
\isacommand{apply}\ blast\isanewline 

790 
No\ subgoals! 

791 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

792 
Expanding definitions reduces the extended logic to the base logic. This 
14154  793 
approach has its merits, but it can be slow. In these examples, proofs 
794 
using the derived rules for~\isa{if} run about six 

795 
times faster than proofs using just the rules of firstorder logic. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

796 

14154  797 
Expanding definitions can also make it harder to diagnose errors. 
798 
Suppose we are having difficulties in proving some goal. If by expanding 

799 
definitions we have made it unreadable, then we have little hope of 

800 
diagnosing the problem. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

801 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

802 
Attempts at program verification often yield invalid assertions. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

803 
Let us try to prove one: 
14154  804 
\begin{isabelle} 
805 
\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <>\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline 

806 
\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\ 

807 
A)) 

808 
\end{isabelle} 

809 
Calling \isa{blast} yields an uninformative failure message. We can 

810 
get a closer look at the situation by applying \methdx{auto}. 

811 
\begin{isabelle} 

812 
\isacommand{apply}\ auto\isanewline 

813 
\ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline 

814 
\ 2.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline 

815 
\ 3.\ \isasymlbrakk B;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline 

816 
\ 4.\ \isasymlbrakk \isasymnot \ R;\ A;\ \isasymnot \ B;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ 

817 
False 

818 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

819 
Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

820 
while~$R$ and~$A$ are true. This truth assignment reduces the main goal to 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

821 
$true\bimp false$, which is of course invalid. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

822 

9695  823 
We can repeat this analysis by expanding definitions, using just the rules of 
14154  824 
firstorder logic: 
825 
\begin{isabelle} 

826 
\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <>\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline 

827 
\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\ 

828 
A)) 

829 
\isanewline 

830 
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline 

831 
\ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline 

832 
\isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ B\ \isasymor \ \isasymnot \ R\ \isasymand \ A) 

833 
\end{isabelle} 

834 
Again \isa{blast} would fail, so we try \methdx{auto}: 

835 
\begin{isabelle} 

836 
\isacommand{apply}\ (auto)\ \isanewline 

837 
\ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline 

838 
\ 2.\ \isasymlbrakk A;\ \isasymnot \ P;\ R;\ \isasymnot \ B\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline 

839 
\ 3.\ \isasymlbrakk B;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline 

840 
\ 4.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ A;\ \isasymnot \ R;\ Q\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline 

841 
\ 5.\ \isasymlbrakk B;\ \isasymnot \ Q;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline 

842 
\ 6.\ \isasymlbrakk B;\ \isasymnot \ A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline 

843 
\ 7.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline 

844 
\ 8.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ Q% 

845 
\end{isabelle} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

846 
Subgoal~1 yields the same countermodel as before. But each proof step has 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

847 
taken six times as long, and the final result contains twice as many subgoals. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

848 

14154  849 
Expanding your definitions usually makes proofs more difficult. This is 
850 
why the classical prover has been designed to accept derived rules. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

851 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

852 
\index{firstorder logic)} 