author  wenzelm 
Thu, 25 Nov 1993 14:43:42 +0100  
changeset 152  37025f8608a6 
parent 150  919a03a587eb 
child 359  b5a2e9503a7a 
permissions  rwrr 
104  1 
\contentsline {chapter}{\numberline {1}Introduction}{1} 
2 
\contentsline {section}{\numberline {1.1}Basic interaction with Isabelle}{1} 

3 
\contentsline {section}{\numberline {1.2}Ending a session}{2} 

4 
\contentsline {section}{\numberline {1.3}Reading files of proofs and theories}{2} 

138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

5 
\contentsline {section}{\numberline {1.4}Printing of terms and theorems}{3} 
104  6 
\contentsline {subsection}{Printing limits}{3} 
7 
\contentsline {subsection}{Printing of metalevel hypotheses}{3} 

141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
138
diff
changeset

8 
\contentsline {subsection}{Printing of types and sorts}{3} 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

9 
\contentsline {subsection}{$\eta $contraction before printing}{4} 
104  10 
\contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{4} 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

11 
\contentsline {section}{\numberline {1.6}Shell scripts}{5} 
104  12 
\contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{6} 
13 
\contentsline {section}{\numberline {2.1}Basic commands}{6} 

14 
\contentsline {subsection}{Starting a backward proof}{6} 

15 
\contentsline {subsection}{Applying a tactic}{7} 

16 
\contentsline {subsection}{Extracting the proved theorem}{8} 

17 
\contentsline {subsection}{Undoing and backtracking}{8} 

18 
\contentsline {subsection}{Printing the proof state}{9} 

19 
\contentsline {subsection}{Timing}{9} 

20 
\contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{9} 

21 
\contentsline {subsection}{Refining a given subgoal}{9} 

22 
\contentsline {subsubsection}{Resolution with a list of theorems}{9} 

23 
\contentsline {subsection}{Scanning shortcuts}{10} 

24 
\contentsline {subsubsection}{Proof by assumption and resolution}{10} 

25 
\contentsline {subsubsection}{Resolution with a list of theorems}{10} 

26 
\contentsline {subsection}{Other shortcuts}{10} 

27 
\contentsline {section}{\numberline {2.3}Advanced features}{11} 

28 
\contentsline {subsection}{Executing batch proofs}{11} 

29 
\contentsline {subsection}{Managing multiple proofs}{11} 

30 
\contentsline {subsubsection}{The stack of proof states}{12} 

31 
\contentsline {subsubsection}{Saving and restoring proof states}{12} 

32 
\contentsline {subsection}{Debugging and inspecting}{12} 

33 
\contentsline {subsubsection}{Reading and printing terms}{13} 

34 
\contentsline {subsubsection}{Inspecting the proof state}{13} 

35 
\contentsline {subsubsection}{Filtering lists of rules}{13} 

36 
\contentsline {chapter}{\numberline {3}Tactics}{14} 

37 
\contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{14} 

38 
\contentsline {subsection}{Resolution tactics}{14} 

39 
\contentsline {subsection}{Assumption tactics}{15} 

40 
\contentsline {subsection}{Matching tactics}{15} 

41 
\contentsline {subsection}{Resolution with instantiation}{15} 

42 
\contentsline {section}{\numberline {3.2}Other basic tactics}{16} 

43 
\contentsline {subsection}{Definitions and metalevel rewriting}{16} 

44 
\contentsline {subsection}{Tactic shortcuts}{17} 

45 
\contentsline {subsection}{Inserting premises and facts}{17} 

46 
\contentsline {subsection}{Theorems useful with tactics}{18} 

47 
\contentsline {section}{\numberline {3.3}Obscure tactics}{18} 

48 
\contentsline {subsection}{Tidying the proof state}{18} 

49 
\contentsline {subsection}{Renaming parameters in a goal}{18} 

50 
\contentsline {subsection}{Composition: resolution without lifting}{19} 

51 
\contentsline {section}{\numberline {3.4}Managing lots of rules}{19} 

52 
\contentsline {subsection}{Combined resolution and elimresolution}{20} 

53 
\contentsline {subsection}{Discrimination nets for fast resolution}{20} 

54 
\contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{21} 

55 
\contentsline {subsection}{Operations on type {\ptt tactic}}{22} 

56 
\contentsline {subsection}{Tracing}{22} 

57 
\contentsline {subsection}{Sequences}{23} 

58 
\contentsline {subsubsection}{Basic operations on sequences}{23} 

59 
\contentsline {subsubsection}{Converting between sequences and lists}{23} 

60 
\contentsline {subsubsection}{Combining sequences}{23} 

61 
\contentsline {chapter}{\numberline {4}Tacticals}{25} 

62 
\contentsline {section}{\numberline {4.1}The basic tacticals}{25} 

63 
\contentsline {subsection}{Joining two tactics}{25} 

64 
\contentsline {subsection}{Joining a list of tactics}{25} 

65 
\contentsline {subsection}{Repetition tacticals}{26} 

66 
\contentsline {subsection}{Identities for tacticals}{26} 

67 
\contentsline {section}{\numberline {4.2}Control and search tacticals}{27} 

68 
\contentsline {subsection}{Filtering a tactic's results}{27} 

69 
\contentsline {subsection}{Depthfirst search}{28} 

70 
\contentsline {subsection}{Other search strategies}{28} 

71 
\contentsline {subsection}{Auxiliary tacticals for searching}{29} 

72 
\contentsline {subsection}{Predicates and functions useful for searching}{29} 

73 
\contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{29} 

74 
\contentsline {subsection}{Restricting a tactic to one subgoal}{30} 

75 
\contentsline {subsection}{Scanning for a subgoal by number}{31} 

76 
\contentsline {subsection}{Joining tactic functions}{32} 

77 
\contentsline {subsection}{Applying a list of tactics to 1}{32} 

78 
\contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{33} 

79 
\contentsline {section}{\numberline {5.1}Basic operations on theorems}{33} 

80 
\contentsline {subsection}{Prettyprinting a theorem}{33} 

81 
\contentsline {subsubsection}{Toplevel commands}{33} 

82 
\contentsline {subsubsection}{Operations for programming}{34} 

83 
\contentsline {subsection}{Forwards proof: joining rules by resolution}{34} 

84 
\contentsline {subsection}{Expanding definitions in theorems}{35} 

85 
\contentsline {subsection}{Instantiating a theorem}{35} 

86 
\contentsline {subsection}{Miscellaneous forward rules}{35} 

87 
\contentsline {subsection}{Taking a theorem apart}{36} 

88 
\contentsline {subsection}{Tracing flags for unification}{36} 

89 
\contentsline {section}{\numberline {5.2}Primitive metalevel inference rules}{37} 

90 
\contentsline {subsection}{Propositional rules}{38} 

91 
\contentsline {subsubsection}{Assumption}{38} 

92 
\contentsline {subsubsection}{Implication}{38} 

93 
\contentsline {subsubsection}{Logical equivalence (equality)}{39} 

94 
\contentsline {subsection}{Equality rules}{39} 

95 
\contentsline {subsection}{The $\lambda $conversion rules}{39} 

96 
\contentsline {subsection}{Universal quantifier rules}{40} 

97 
\contentsline {subsubsection}{Forall introduction}{40} 

98 
\contentsline {subsubsection}{Forall elimination}{40} 

99 
\contentsline {subsubsection}{Instantiation of unknowns}{41} 

100 
\contentsline {subsection}{Freezing/thawing type variables}{41} 

101 
\contentsline {section}{\numberline {5.3}Derived rules for goaldirected proof}{41} 

102 
\contentsline {subsection}{Proof by assumption}{41} 

103 
\contentsline {subsection}{Resolution}{41} 

104 
\contentsline {subsection}{Composition: resolution without lifting}{42} 

105 
\contentsline {subsection}{Other metarules}{42} 

106 
\contentsline {chapter}{\numberline {6}Theories, Terms and Types}{44} 

107 
\contentsline {section}{\numberline {6.1}Defining Theories}{44} 

150
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

108 
\contentsline {subsection}{Classes and types}{47} 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

109 
\contentsline {section}{\numberline {6.2}Loading Theories}{47} 
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

110 
\contentsline {subsection}{Reading a new theory}{47} 
150
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

111 
\contentsline {subsection}{Filenames and paths}{48} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

112 
\contentsline {subsection}{Reloading a theory}{48} 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

113 
\contentsline {subsection}{Pseudo theories}{48} 
150
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

114 
\contentsline {subsection}{Removing a theory}{49} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

115 
\contentsline {subsection}{Using Poly/{\psc ml}}{49} 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

116 
\contentsline {section}{\numberline {6.3}Basic operations on theories}{49} 
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

117 
\contentsline {subsection}{Extracting an axiom from a theory}{49} 
150
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

118 
\contentsline {subsection}{Building a theory}{50} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

119 
\contentsline {subsection}{Inspecting a theory}{51} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

120 
\contentsline {section}{\numberline {6.4}Terms}{52} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

121 
\contentsline {section}{\numberline {6.5}Certified terms}{53} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

122 
\contentsline {subsection}{Printing terms}{53} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

123 
\contentsline {subsection}{Making and inspecting certified terms}{53} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

124 
\contentsline {section}{\numberline {6.6}Types}{54} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

125 
\contentsline {section}{\numberline {6.7}Certified types}{54} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

126 
\contentsline {subsection}{Printing types}{54} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

127 
\contentsline {subsection}{Making and inspecting certified types}{54} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

128 
\contentsline {chapter}{\numberline {7}Substitution Tactics}{56} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

129 
\contentsline {section}{\numberline {7.1}Simple substitution}{56} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

130 
\contentsline {section}{\numberline {7.2}Substitution in the hypotheses}{57} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

131 
\contentsline {section}{\numberline {7.3}Setting up {\ptt hyp_subst_tac}}{57} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

132 
\contentsline {chapter}{\numberline {8}Simplification}{60} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

133 
\contentsline {section}{\numberline {8.1}Simplification sets}{60} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

134 
\contentsline {subsection}{Rewrite rules}{60} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

135 
\contentsline {subsection}{Congruence rules}{61} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

136 
\contentsline {subsection}{The subgoaler}{61} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

137 
\contentsline {subsection}{The solver}{62} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

138 
\contentsline {subsection}{The looper}{62} 
152  139 
\contentsline {section}{\numberline {8.2}The simplification tactics}{62} 
140 
\contentsline {section}{\numberline {8.3}Example: using the simplifier}{63} 

150
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

141 
\contentsline {chapter}{\numberline {9}The classical theorem prover}{67} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

142 
\contentsline {section}{\numberline {9.1}The sequent calculus}{67} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

143 
\contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{68} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

144 
\contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{69} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

145 
\contentsline {section}{\numberline {9.4}Classical rule sets}{70} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

146 
\contentsline {section}{\numberline {9.5}The classical tactics}{71} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

147 
\contentsline {subsection}{Singlestep tactics}{72} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

148 
\contentsline {subsection}{The automatic tactics}{72} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

149 
\contentsline {subsection}{Other useful tactics}{72} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

150 
\contentsline {subsection}{Creating swapped rules}{73} 
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
141
diff
changeset

151 
\contentsline {section}{\numberline {9.6}Setting up the classical prover}{73} 