author  paulson 
Mon, 30 May 2011 16:10:12 +0100  
changeset 43077  7d69154d824b 
parent 30099  dde11464969c 
permissions  rwrr 
30099
dde11464969c
Updated the theory syntax. Corrected an error in a command.
paulson
parents:
14158
diff
changeset

1 
%!TEX root = logicsZF.tex 
6121
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} 
43077
7d69154d824b
Workaround for bug involving makeindex, hyperref and the  symbol
paulson
parents:
30099
diff
changeset

80 
\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because  stopped working 
6121
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} 
30099
dde11464969c
Updated the theory syntax. Corrected an error in a command.
paulson
parents:
14158
diff
changeset

363 
\isacommand{theory}\ IFOL\_examples\ \isacommand{imports}\ IFOL\isanewline 
dde11464969c
Updated the theory syntax. Corrected an error in a command.
paulson
parents:
14158
diff
changeset

364 
\isacommand{begin} 
14154  365 
\end{isabelle} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

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

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

371 
\isanewline 

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

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

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

375 
\end{isabelle} 

376 
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

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

380 
\(\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

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

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

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

386 
\end{isabelle} 

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

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

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

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

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

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

393 
\begin{isabelle} 

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

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

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

397 
\end{isabelle} 

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

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

400 
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

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

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

405 
\end{isabelle} 

406 
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

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

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

411 
\begin{isabelle} 

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

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

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

415 
\end{isabelle} 

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

416 
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

417 
$({\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

418 
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

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

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

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

424 
\isanewline 

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

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

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

428 
\end{isabelle} 

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

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

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

432 
\begin{isabelle} 

433 
\isacommand{apply}\ assumption\isanewline 

434 
No\ subgoals!\isanewline 

435 
\isacommand{done} 

436 
\end{isabelle} 

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

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

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

440 
\begin{isabelle} 

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

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

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

444 
\isanewline 

30099
dde11464969c
Updated the theory syntax. Corrected an error in a command.
paulson
parents:
14158
diff
changeset

445 
\isacommand{by} (tactic \ttlbrace*IntPr.fast_tac 1*\ttrbrace)\isanewline 
14154  446 
No\ subgoals! 
447 
\end{isabelle} 

6121
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 

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

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

451 
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

452 
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

453 
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

454 

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

455 
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

456 
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

457 
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

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

461 
% 

462 
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

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

464 

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

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

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

469 
and allows use of the special implication rules. 

470 
\begin{isabelle} 

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

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

473 
\isanewline 

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

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

476 
\end{isabelle} 

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

478 
\begin{isabelle} 

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

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

481 
\end{isabelle} 

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

482 
By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but 
14154  483 
that formula is not a theorem of intuitionistic logic. Instead, we 
484 
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

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

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

489 
False 

490 
\end{isabelle} 

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

491 
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

492 
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

493 
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

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

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

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

499 
False 

500 
\end{isabelle} 

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

501 
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

502 
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

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

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

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

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

509 
\end{isabelle} 

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

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

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

514 
False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline 

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

516 
\isasymlongrightarrow \ False;\ False\isasymrbrakk \ 

517 
\isasymLongrightarrow \ False% 

518 
\isanewline 

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

520 
No\ subgoals!\isanewline 

521 
\isacommand{done} 

522 
\end{isabelle} 

523 
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

524 

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

525 

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

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

527 
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

528 
$\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

529 
follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise 
14154  530 
$\all{x}P(x)$ is true. Either way the theorem holds. First, we must 
14158  531 
work in a theory based on classical logic, the theory \isa{FOL}: 
14154  532 
\begin{isabelle} 
30099
dde11464969c
Updated the theory syntax. Corrected an error in a command.
paulson
parents:
14158
diff
changeset

533 
\isacommand{theory}\ FOL\_examples\ \isacommand{imports}\ FOL\isanewline 
dde11464969c
Updated the theory syntax. Corrected an error in a command.
paulson
parents:
14158
diff
changeset

534 
\isacommand{begin} 
14154  535 
\end{isabelle} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

536 

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

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

540 
quantifier. 

541 
\begin{isabelle} 

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

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

544 
\isanewline 

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

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

547 
\end{isabelle} 

548 
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

549 
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

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

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

554 
\isanewline 

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

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

557 
\end{isabelle} 

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

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

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

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

563 
\end{isabelle} 

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

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

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

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

570 
\end{isabelle} 

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

572 
\begin{isabelle} 

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

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

575 
?P1(x)\isasymrbrakk \ 

576 
\isasymLongrightarrow \ ?P% 

577 
\end{isabelle} 

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

579 
\begin{isabelle} 

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

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

582 
\end{isabelle} 

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

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

586 
unknown~\isa{?a}. 

587 
\begin{isabelle} 

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

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

590 
\isanewline 

591 
\isacommand{apply}\ assumption\isanewline 

592 
No\ subgoals!\isanewline 

593 
\isacommand{done} 

594 
\end{isabelle} 

595 
The civilised way to prove this theorem is using the 

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

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

598 
\begin{isabelle} 

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

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

601 
\isanewline 

602 
\isacommand{by}\ blast\isanewline 

603 
No\ subgoals! 

604 
\end{isabelle} 

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

605 
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

606 
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

607 
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

608 
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

609 

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

610 

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

611 
\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

612 
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

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

614 
$$ 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

615 
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

616 
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

617 
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

618 
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

619 

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

620 
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

621 
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

622 
\[ 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

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

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

625 
\[ \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

626 
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

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

628 
\[ \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

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

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

631 
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

632 
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

633 
$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

634 
equation~$(if)$. 
14154  635 
\begin{isabelle} 
30099
dde11464969c
Updated the theory syntax. Corrected an error in a command.
paulson
parents:
14158
diff
changeset

636 
\isacommand{theory}\ If\ \isacommand{imports}\ FOL\isanewline 
dde11464969c
Updated the theory syntax. Corrected an error in a command.
paulson
parents:
14158
diff
changeset

637 
\isacommand{begin}\isanewline 
14154  638 
\isacommand{constdefs}\isanewline 
639 
\ \ if\ ::\ "[o,o,o]=>o"\isanewline 

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

641 
\end{isabelle} 

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

642 
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

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

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

647 
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

648 

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

649 

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

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

651 

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

652 
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

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

655 

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

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

659 
subgoal. 

660 
\begin{isabelle} 

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

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

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

664 
\isanewline 

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

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

667 
R 

668 
\end{isabelle} 

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

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

671 
\methdx{blast}. 

672 
\begin{isabelle} 

673 
\isacommand{apply}\ blast\isanewline 

674 
No\ subgoals!\isanewline 

675 
\isacommand{done} 

676 
\end{isabelle} 

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

677 

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

678 

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

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

680 
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

681 
The conclusion is simply $S$. 
14154  682 
\begin{isabelle} 
683 
\isacommand{lemma}\ ifE:\isanewline 

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

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

686 
\isanewline 

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

688 
\ 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% 

689 
\end{isabelle} 

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

691 
\isa{blast}: 

692 
\begin{isabelle} 

693 
\isacommand{apply}\ blast\isanewline 

694 
No\ subgoals!\isanewline 

695 
\isacommand{done} 

696 
\end{isabelle} 

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

697 

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

698 

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

699 
\subsection{Using the derived rules} 
14154  700 
Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural 
701 
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

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

703 
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

704 
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

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

706 
Proofs also require the classical reasoning rules and the $\bimp$ 
14154  707 
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

708 

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

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

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

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

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

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

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

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

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

719 
\end{isabelle} 

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

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

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

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

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

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

727 
\isanewline 

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

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

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

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

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

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

734 
\end{isabelle} 

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

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

736 
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

737 
$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

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

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

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

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

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

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

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

747 
\isanewline 

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

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

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

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

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

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

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

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

756 
\end{isabelle} 

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

757 
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

758 
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

759 
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

760 
for~$if$. 
14154  761 
\begin{isabelle} 
762 
\isacommand{declare}\ ifI\ [intro!]\isanewline 

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

764 
\end{isabelle} 

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

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

767 
\begin{isabelle} 

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

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

770 
\isanewline 

771 
\isacommand{by}\ blast 

772 
\end{isabelle} 

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

773 

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

774 

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

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

776 
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

777 
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

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

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

782 
\end{isabelle} 

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

784 
\begin{isabelle} 

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

786 
\ 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 

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

788 
\end{isabelle} 

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

790 
\isa{blast}: 

791 
\begin{isabelle} 

792 
\isacommand{apply}\ blast\isanewline 

793 
No\ subgoals! 

794 
\end{isabelle} 

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

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

798 
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

799 

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

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

803 
diagnosing the problem. 

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

804 

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

805 
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

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

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

810 
A)) 

811 
\end{isabelle} 

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

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

814 
\begin{isabelle} 

815 
\isacommand{apply}\ auto\isanewline 

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

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

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

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

820 
False 

821 
\end{isabelle} 

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

822 
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

823 
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

824 
$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

825 

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

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

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

831 
A)) 

832 
\isanewline 

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

834 
\ 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 

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

836 
\end{isabelle} 

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

838 
\begin{isabelle} 

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

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

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

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

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

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

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

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

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

848 
\end{isabelle} 

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

849 
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

850 
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

851 

14154  852 
Expanding your definitions usually makes proofs more difficult. This is 
853 
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

854 

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

855 
\index{firstorder logic)} 