Home

The IMPS User's Manual - Interactive Mathematical Proof System

1. Description of String Syntax2 Description of Atoms 0 20220000048 Operator Binding Powers 204 Search Order for prove by logic and simplification 10 List of Figures 3 1 5 1 5 2 5 3 5 4 5 9 5 6 5 7 5 8 5 9 5 10 5 11 5 12 5 13 6 1 6 2 12 1 17 1 17 2 17 3 An Inference Node 0 000 00000 eee The Combinatorial Identity The Combinatorial Identity with One Occurrence Unfolded The left denominator removal for equalities Theorem Rewriting Done by Left Denominator Removal Result of the Second Unfolding All Occurrences have been Eliminated The Form of fractional expression manipulation The Result of fractional expression manipulation The Simpler Definedness Subgoal The factorial reduction Macete Commands to Delete 2 2 a E a E R a a e a The Sum of the First n Natural Numbers Result of Applying the little integer induction Macete Generalized Power Rule aoaaa aa Telescoping Product Formula 04 An IMPS Proof Script oaoa 222220004 Axioms for Nat as Introduced by BNF BNF Syntax for a Small Programming Language IMPS def bnf Form for Programming Language Syntax 11 Part I Introductory Material Chapter 1 Introduction IMPS is an Interactive Mathematical Proo
2. 8 If O is if form or if V O A B C 80 10 11 12 13 14 16 T if V A1 V An T F otherwise T if V A T for some i with 1 lt i lt n F otherwise T if Vopr 2011901 nian Gn A T for all a1 an Do Za X Dan F otherwise Vo V 1 01 Zn Qn A T if Voica aiai 0n Gn A AL for some a7 an Vo 311 07 Tn QAn A e S e104 Dag ese X Dan F otherwise _ _ T ifV A V B Vo A i F otherwise Assume F is of kind Then VA F A AS An Vo F Vo A1 gt Vo An if V P V A1 V An are each defined otherwise VAF A1 An is undefined Assume F is of sort a 0 1 of kind Then Va F A ES An Vo F Vo A1 gt Vo An if V A1 V An are each defined otherwise V F A Daey An F lany Assume A is of sort amp n 1 of kind Then V A 21 01 Un Qn A is the partial function f Da X X Da Da such that f a gt an A tog tA if Voto 01 gt a1 0n anr gt an A is defined otherwise f a1 n is un defined 81 17 Assume A is of sort an 41 of kind Then V A 21 01 Un Qn A is the total function f Dy q X X Dean gt Pony Such that f a gt an Voa asan on iin A if a1 n Da X X Dan otherwise f a an Fr an4i 18 V vx a A is the unique element a Da such that Voto ar a LA T otherwise V
3. aooaa ee ee 244 force substitution a 246 generalize using sequent a a 247 incorporate antecedent 2 2 e 247 MUCHO Mala Se ihe OR ts he RA els 248 insistent direct inference e 250 insistent direct inference strategy o 250 instantiate existential ee 251 instantiate theorem a 251 instantiate transported theorem a 252 instantiate universal antecedent o ooo a 253 instantiate universal antecedent multiply 254 prove by logic and simplification 0 0 00084 255 raise conditional 10230 ioe ey Boke a ected Bo doe ee aoe 256 SIMP hyd rl ats eee ts es ove AA A ON ae hes 258 simplify antecedent e 259 simplify insistently o o e 260 simplify with minor premises 2 2 0004 260 SOrt defined ness ass mhur alk BT a ee Ee Ge ee oe a Se 261 sort definedness and conditionals 04 262 unfold defined constants e 262 unfold defined constants Tepeatedly o o o 262 unfold directly defined constants 263 unfold directly defined constants repeatedly 264 unfold recursively defined constaMtS 264 unfold recursively defined constants repeatedly 265 unfold single defined constant 265 unfold single defined constant globally 266 unordered d
4. expression categories depend on parts of the state of the IMPS system which are likely to change from user to user We also want to stress that these tables say nothing about how strings are parsed into nested lists and much less about what the strings mean mathematically For example one cannot say how argument associations are disambiguated from these tables alone The table of operator prece dences in the next section specifies this information The syntax tables are thus of limited value and should only be consulted to get a very rough idea of what expressions look like 16 4 Parsing The process of building an s expression from an input string itself breaks up into two parts e Tokenization of the input string This can be thought of as dividing the input string into a list of substrings called tokens e Parsing of the list of tokens This can be thought of as transforming a linear structure of tokens into a tree structure of tokens The table below gives some examples of how a string s is translated into an s expression s according to the string syntax String Reads pi and and pn and pi P pn p Or Or Pn or p1 pn if zx y z if E x O y z if x y z w v if B x P y if O z P w O w t s defined in t s t is defined t ay apply x y Ty apply x y Gite Eg apply f D x1 Dl z T
5. from T to Ta is an interpretation if each of its obligations is a theorem of Tz See 5 7 for a more detailed discussion of theory interpretations in LUTINS 9 3 Building Theory Interpretations The most direct way for you to build an interpretation is with the def translation form However there are also several ways interpretations can be built automatically by IMPS with little or no assistance from you 95 Building an interpretation with def translation is generally a two step process The first step is to build a translation by evaluating a def translation form which contains a specified name source theory target theory sort association list and constant association list These latter lists composed of pairs specify respectively the two functions y and y discussed in the previous section Each pair in the sort association list consists of an atomic sort of the source theory and a specification of a sort unary predi cate or indicator of the target theory Each pair in the constant association list consists of a constant of the source theory and a specification of an ex pression of the target theory There does not need to be a pair in the sort association list for each atomic sort in the source theory missing primitive atomic sorts are paired with themselves and missing defined atomic sorts are handled in the special way described in the next section A similar statement is true about the constant association list W
6. with f ind ind forall x_0 ind f x_0 without quasi constructor abbreviations That is the two internal expressions are the same except for the name of the single bound variable One of the most devastating forms of quasi constructor explosion can occur when a nonnormal translation which maps some atomic sorts to unary predicates is applied to an expression containing quasi constructors The quasi constructor explosion happens because the binding expressions in the internal representation of a quasi constructor will be rewritten when the translation is applied if the variables being bound involve a atomic sort which is mapped to a unary predicate Often two different internal expressions containing quasi constructors will be printed in exactly the same way Usually this is due to the fact that some of the bound variables in the internal representation of some of the quasi constructors have different names i e the two expressions are a equivalent In this case there is no problem for the most part IMPS will treat the expressions as if they were identical However the two expressions may differ in other ways e g some of the corresponding bound variables may have different sorts Hence in rare occasions it may happen that there are two internal expressions printed the same which are not known by IMPS to be equal or quasi equal This situation can be very hard to deal with It is often best to backup and try a differen
7. Qn An 1 The range sort of a function sort a written ran a is defined as follows if a a1 Qn Qn 1 then ran a a 1 otherwise ran a ran 8 where 3 is the enclosing sort of a Sorts are divided into two kinds as follows A sort is of kind x if either it is or it isa compound sort aj n41 where 0 1 is of kind x otherwise it is of kind We shall see later the purpose behind this division All atomic sorts except are of kind v 7 2 2 Expressions contains a set C of names called constants Each constant is assigned a sort in S An expression of L of sort a is a sequence of symbols defined inductively by 1 If x is a name and a S then z a is an expression of sort a 2 If A C is of sort a then A is an expression of sort a 3 If A B C Ai An are expressions of sort with n gt 0 then T F 4 A D B A B ifform A B C 41 A A An and A V V An are expressions of sort 4 If x1 7 are distinct names Q7 Qn S A is an expression of sort 6 and n gt 1 then V 11 01 Tn QGn A and 3 11 01 Tn Qn A are expressions of sort TT 5 If A and B are expressions of sort a and respectively with Tr a T 6 then A B is an expression of sort x 6 If F is an expression of sort a and type a1 n Q n41 A1 An are expressions of sort a4 a and a T a4 Qn T a then F A1 An is an expression of sort
8. e is a sentence when e is a sentence When u maps an atomic sort a to a unary predicate U the variable binding constructors A V 3 and are relativized when they bind a 94 variable of sort a For example Va a Vx B U x gt y Something very similar happens when y maps an atomic sort to an indicator The constructor defined in is also relativized when its second argument is a A translation is normal if it maps each atomic sort of the source theory to a sort of the target theory Normal translations do not relativize constructors Let be a translation from 71 to T is an interpretation of T in Ta if P p is a theorem of Ta for each theorem y of 71 In other words an interpretation is a translation that maps theorems to theorems An obligation of is a formula y where y is either 1 a primitive axiom of 71 axiom obligation 2 a definition axiom of 71 definition obligation 3 a formula asserting that a particular primitive atomic sort of 71 is nonempty sort nonemptiness obligation 4 a formula asserting that a particular primitive constant of 71 is defined in its sort constant sort obligation or 5 a formula asserting that a particular primitive atomic sort of 71 is a subset of its enclosing sort sort inclusion obligation The following theorem gives a sufficient condition for a translation to be an interpretation Theorem 9 2 1 Interpretation Theorem A translation
9. repeatedly is called after all the unfoldings are performed Related commands unfold defined constants repeatedly unfold directly defined constants repeatedly unfold recursively defined constants unfold single defined constant Remarks This command may run forever unfold single defined constant Script usage unfold single defined constant occurrences constant occurrences is a list of integers and constant is denoted by the constant name Interactive argument retrieval e Constant name c 265 e Occurrences to unfold 0 based A list l given in the form Hessie Notice that the order in which arguments are requested is different than the order for script usage Command kind Multi inference Description This command replaces each specified occurrence of the de fined constant c by its unfolding e Conclusion gt p Premise T gt ple cl The command beta reduce repeatedly is called after all the unfoldings are performed Related commands unfold defined constants unfold defined constants repeatedly unfold directly defined constants unfold directly defined constants repeatedly unfold recursively defined constants unfold recursively defined constants repeatedly unfold single defined constant globally Remarks The related commands are all elaborations of this command Key binding u unfold single defined constant globally Script usage unfold single defined constant globa
10. vx a A is undefined 19 Vo tpz a A is the unique element a Da such that Voto a a LA T otherwise V tpx a A Fr a T if V A is defined F otherwise 20 V AL _ J T if V A is defined and V A Da 21 VAG F otherwise 22 Vo La is undefined Clearly for each variable assignment y into M and each expression A of L 1 V A Da if V A is defined and 2 V A is defined if A is of kind V A is called the value or denotation of A in M with respect to p provided it is defined When V A is not defined A is said to be nondenoting in M with respect to y 7 4 Extensions of the Logic The logic can be effectively extended by introducing quasi constructors They are the subject of Chapter 10 7 5 Hints and Cautions 1 In most cases the novice IMPS user is better off relying on his intuition instead of trying to fully comprehend the formal semantics of LUTINS 82 2 3 Although IMPS can handle expressions containing two variables with the same name such as x a and 2 3 with a 4 3 they tend to be confusing and should be avoided if possible LUTINS is a logic of two worlds the world and the world Expres sions of kind are part of the world and expressions of kind x are part of the world Although both worlds can be used for encoding math ematics the world is much preferred for this purpose As a general rule expressions of kind should no
11. Key binding C c b beta reduce with minor premises Script usage beta reduce with minor premises Interactive argument retrieval None 233 Command kind Single inference Description This command is the same as beta reduce except that instead of failing when convergence requirements are not verified it posts the unverified convergence requirements as additional subgoals to be proved Related commands beta reduce simplify with minor premises Remarks This command is useful for determining why a lambda application does not beta reduce case split Script usage case split list of formulas Interactive argument retrieval e First formula y e Next formula lt RET gt if done j e Next formula lt RET gt if done Yn n gt 1 Description This command considers all the different possible cases for Pl Pn Conclusion T gt 0w Premises A C 1 n TU Y A Aptf gt y Notes e For each A C 1 n vf is y if i A and p otherwise 234 case split on conditionals Script usage case split on conditionals occurrences occurrences is a list of integers Interactive argument retrieval e Occurrences of conditionals to be raised O based A list given in the form li In Command kind Multi inference Description This command applies case split to the first components of the conditional expressions in the given sequent specified by l The command s
12. Step 4 Find the macete domain of inverse using either Macete de scription or the macete menu Step 5 Find the macete non zero product using either Macete de scription or the macete menu 53 Step 5 Find the macete factorial non zero using either Macete de scription or the macete menu Step 6 Under the Command menu item find simplify usually about half way down the list Result You will see that IMPS has marked this subgoal as Grounded in the black stripe under the sequent node buffer This means that IMPS has now ascertained that it is true In the xdg window you will see that Sequent 7 is marked as grounded and the sequents supporting it are no longer displayed To move to the next subgoal either click left on it in the xdg window or else look under the Nodes menubar item for the First unsupported relative The resulting sequent is a more complicated definedness assertion Step 7 Rather than using the individual lemmas we will use the com pound macete definedness manipulations To see how the macete is built use the Xview macete item under the TeX menubar item Invoke it via the macete menu or through the Macete description item It will ground the subgoal after about 30 seconds of computation Step 8 To move to the last remaining subgoal either click left on it in the xdg window or else look under the Nodes menubar item for the First unsupported relative Apply the compound macete factorial reduction F
13. Vp a 21 01 2niAn PS Yo AY with none of the sorts Q1 Q being of kind x wo is referred to as the base case and Y is the induction step 183 Description This form builds an inductor from the formula y represented by induction principle or if the translation keyword is present from the translation of p under the translation named by name The base case and induction step hooks are macetes or commands that provide additional handling for the base and induction cases Examples def inductor TRIVIAL INTEGER INDUCTOR forall s zz prop m zz forall t zz m lt t implies s t iff s m and forall t zz m lt t implies s t implies s t 1 theory h o real arithmetic def inductor NATURAL NUMBER INDUCTOR foral1 s nn prop forall t nn s t iff s 0 and forall t nn s t implies s t 1 theory h o real arithmetic def inductor INTEGER INDUCTOR induct theory h o real arithmetic base case hook unfold defined constants repeatedly def inductor SM INDUCT forall p state prop forall s state accessible s implies p s iff forall s state initial s implies p s and forall s_1 s_2 state a action accessible s_1 and p s_1 and tr s_1 a s_2 implies p s_2 theory h o real arithmetic 184 base case hook eliminate nonrecursive definitions and simplify def inductor SEQUENCE INDUCTOR foral1l p mn ind_1 prop forall s nn ind_1 f_seq_q s implies
14. e By adding definitions to an existing theory e By building a new theory altogether with new primitive constants sorts and axioms For example in the theory of h o real arithmetic evaluation of the fol lowing s expression adds the definition of convergence to oo of a real valued sequence def constant CONVERGENTYTO INFINITY lambda s zz rr forall m rr forsome x zz forall j zz x lt j implies m lt s j theory h o real arithmetic 37 As an exercise try defining the concept of limit of real valued sequences Next we illustrate how new theories are built by building a theory of monoids Building a theory is a two step process First we build a lan guage with the required sorts and constants def language MONOID LANGUAGE embedded languages h o real arithmetic base types uu constants e uu uu uu uul The next step builds the theory itself by listing the axioms def theory MONOID THEORY component theories h o real arithmetic language monoid language axioms associative law for multiplication for monoids forall z y x uu x y z x y z rewrite right multiplicative identity for monoids forall x uu x e x rewrite left multiplicative identity for monoids forall x uu e x x rewrite total_q uu uu uu d r convergence There are numerous other ways IMPS can be extended These are dis cussed in detail in Chapter 17 In addition there are a number of
15. e One can prove uniqueness of the multiplicative identity Va U W U rey yex x x e e A sequential product operator for sequences can be defined as the least solution of II Am n Z f Z U i m lt n I m n 1 f F n e e One can easily prove II satisfies Vf Z U m n Z n lt m gt IK n m f T n m 1 f e f m e An monoid endomorphism i e a self homomorphism can be defined by the predicate Ap U U p e e A Yz y U p x e y p x e p y However there is no way to talk about monoid homomorphisms between different monoids Nevertheless it is possible to produce a suitable theory in IMPS in which a general notion of monoid homomorphism can be defined To do so requires at the very least a theory with two possibly distinct monoids In general multiple instances of structures can be dealt with in IMPS in two ways e In one approach we first formalize set theory as an IMPS theory This can be done by treating Set as a primitive sort and the membership relation as a primitive function symbol It is then possible to define a structure of a particular kind by a predicate on Set For instance a monoid is any object in Set of the form U e e where e is a binary associative operation on U for which e is a right and left identity e The other approach is to create a new theory which is the union of embedded replicas of a theory of a single structure A replica of a theory T is a theory 7 whic
16. equal S expression The external representation of the basic data structure of Lisp like languages including T S expressions are usually represented as nested lists such as fuba abacaxi farofa alface Sequent node A node in a deduction graph that represents a sequent a formula composed of a set of assumptions and an assertion Sort A sort denotes a nonempty set of mathematical entities Every ex pression has a sort which restricts the value of that expression Syntax Rules for parsing and printing expressions The syntaxes that are currently used in IMPS are the string syntax which allows for infix and postfix notation the s expression syntax which provides a uniform prefix syntax for all constructors and operators and the tex syntax for displaying but not parsing in T X 296 T A dialect of Lisp developed at the Yale University Computer Science Department in which the core machinery of IMPS is implemented T is very similar to the Scheme programming language familiar to readers of Abelson and Sussman s book 1 Tea An alias for the T programming language Theory The term theory as used in this manual consists of a language and a set of closed formulas in the language called axioms A theory is implemented as a record structure having slots for the language the list of axioms and other relevant information There is also a slot for a table of procedures which the simplifier uses to apply the axioms This is me
17. gt 0 Premises TU Ay gt 0 TU y gt 0 Conclusion TU i A Apn gt Y Premise DU Gal gt Y Conclusion TU pV Veo Sy Premises 1 lt i lt n TU pj gt Y Conclusion TU p v gt 0 Premises TU pvj gt PU 7 ay 0 Conclusion T U if form y Y 0 gt Premises TU p py gt E ru Lp 0 gt E Conclusion T U 321 01 En On P gt Y Premise TU p sy Notes e Each sequent in the preceding table is of the form TU 4 gt Y where y is the parameter to the primitive inference procedure e is obtained from y by renaming the variables among 71 2n which are free in both y and the original sequent backchain inference Parameters A sequent node assumption Description This primitive inference procedure attempts to use the as sumption given as argument to replace the assertion to be proved In the simplest case if the given assumption is y gt Y and the assertion is 4 then backchain inference replaces the assertion with y Similarly if the assertion is it is replaced with y The command extends this simplest case in four ways 270 e If the assumption is universally quantified then matching is used to select a relevant instance e If the assumption is a disjunction V Pi iEI then for any j I it may be treated as A mw gt ej iL iAj e If the assumption is of one of the forms s t s gt t s t ifa subexpression of the assertion matches s
18. many theorems about groups are more conveniently proved about groups actions because several group theorems may be just different instantiations of a particular group action theorem The following def forms show how group actions is an extension of groups def language GROUP ACTION LANGUAGE embedded language groups language base types uu constants act uu gg uul def theory GROUP ACTIONS language group action language component theories groups axioms act id forall alpha uu g 8g8 act alpha e alpha rewrite transportable macete act associativity forall alpha uu g h g88 act alpha g mul h act act alpha g h transportable macete There are many natural interpretations of group actions in groups such as def translation ACT gt CONJUGATE source group actions target groups fixed theories h o real arithmetic sort pairs uu gg constant pairs act lambda g h gg inv h mul g mul h theory interpretation check using simplification Suppose T is an extension of 71 that is obtained by adding to 71 new constants and axioms relating the new constants of T 2 to the old constants of T Then each theorem of T has a analogue in 71 obtained by generalizing over the new constants of 71 This notion of generalization is performed automatically in IMPS with an appropriate interpretation of To in 73 103 For example the def forms def language LCT LANGUAGE embedded language gr
19. operation alist is a list of entries operation type operator where operation type is one of lt lt operator is the name of a constant in the language of the associated algebraic processor e discrete sorts sort spec sort spec Description This form builds an object called an order processor for simplification of formulas involving order relations Processors are used by IMPS to generate 187 algebraic and order simplification procedures used by the simplifier for the following purposes e To utilize theory specific information of an algebraic nature in per forming simplification For example the expression x x x should simplify to x or x lt x 1 should simplify to true e To reduce any formula built from formal constants whose value can be algebraically computed from the values of the components Thus the expression 2 lt 3 should reduce to true Examples def order processor RR ORDER algebraic processor rr algebraic processor operations lt lt lt lt discrete sorts zz def primitive recursive constant Positional Arguments e constant name The name of the function or predicate constant to be introduced by the def form e bnf The BNF object furnishing the primitive recursive schema for the definition see def bnf The base type of this BNF will also be the domain of the constant Keyword Arguments e theory theory name Required The theory to which th
20. s 0 a a 189 def record theory a 190 def recursive constant a 191 def renaimnmer ive vee oe A AA AA A 192 def schematic macete 2 0 ee ee 193 d t seript 250 ak ok es Mas ok Ges Eo AE 194 def section sos ia ase ba Ee OA ee ow eS 195 def sublanguage 0000 2 eee ee eee 196 def theoretit As mhen y cee we oe be te ee lee de es 197 def theory oi se ue me bce ee Ae Bag eee ale Bh ee 199 def theory ensemble e 201 def theory ensemble instances 202 def theory ensemble multiple 205 def theory ensemble overloadings 205 def theory instance e o 206 def theory processors 207 def translation ee 208 def transported symbols 2 002 0004 211 172 Changing Syntace paei a ees PUE p pee Bt OAS Se iia 212 def overloading 2 000022 eens 212 def parse syntax 2 a 212 def print syntax 2 ee eee 214 17 3 Loading Sections and Files 2 08 215 load section a 215 imclud files a sars anor a a 215 17 4 Presenting Expressions o e 216 VICW OX DI Sor A A AAA AA 216 18 The Proof Commands 217 antecedent inference 2 ee 221 antecedent inference strategy 0000 0222 e 222 apply macet 24 ack Dah ae EEE Sw a 223 apply macete locally 2 0 ee 224 apply macete locally with minor premises 224 appl
21. the parity of l must be 1 otherwise no condition is imposed on the path e The source pattern s matches e Thus there is a substitution p x1 t1 n tn such that p applied to s gives ej e The validity of all the convergence requirements of the substitution p and all the formulas c in the context T localized at the path l are called the minor premises generated by the macete application These formulas may or may not generate applicability conditions If the macete is being applied with the accumulation of minor premises then these formulas are posted as new sequents and must be proven separately No new applicability conditions are generated in this case Otherwise the minor premises must be recognized as valid by the simplifier e No smaller path 1 lx satisfies the preceding conditions The replacement formula is obtained by replacing each subexpression e by pi e1 Macetes obtained in this way are called elementary macetes Whenever you enter a theorem into a theory the associated schematic macete is automatically installed so that you can use it in deductions by hitting the key m The case of translation matching is similar but instead of consider ing only convergence requirements we need to insure that the translation component of the translation match is a theory interpretation Macetes ob tained in this way are called transportable macetes The use of a theorem as a transportable ma
22. then it is replaced by the corresponding instance of t e If the assumption is a conjunction each conjunct is tried separately in turn e These rules are used iteratively to descend through the structure of the assumption as deeply as necessary If IMPS cannot recognize that the terms returned by a match are defined in the appropriate sorts then these assertions are returned as additional minor premises that must later be grounded to complete the derivation backchain backwards inference Parameters A sequent node assumption Description This primitive inference procedure works the same way as backchain except that subformulas of the assumption of the forms s t s t s t are used from right to left backchain through formula inference Parameters A sequent node assumption Description Similar to backchain except that it does not backchain through equivalences i e formulas of the form s t s t or s t 271 choice Parameters None Description This primitive inference procedure implements a version of the axiom of choice Conclusion I gt af slo ias T V 1 0 O Premise T gt Y1 En On US is a la Notes e c and o have the same type for all i with 1 lt i lt n e The command fails if there is any occurrence of f in py which is not in an application of the form f 71 2n contraposition Parameters A sequent node assumption y Description This pri
23. 259 Description This command tries to ground a sequent by applying a list inference procedures some of which have a sequent assumption as an addi tional argument to the goal node and recursively to the generated subgoal nodes See Table 18 1 When an inference procedure is applied to the goal sequent or to a subgoal sequent two possibilities can occur 1 The inference procedure fails In this case prove by logic and simplification tries the same inference procedure with the next as sumption as argument if this makes sense the next inference proce dure on the list if one exists or otherwise backtracks 2 The inference procedure succeeds either grounding the node or gen erating one or more new subgoals to prove In this case we attempt to prove each new subgoal by applying the primitive inferences in order Remarks This command is an example of an ending strategy that is a proof construction procedure to be used when all that remains to be done is completely straightforward reasoning It should be used with great caution since in the cases in which it fails to ground a node it may generate a large number of irrelevant subgoals Key binding None lest you accidently hit it raise conditional Script usage raise conditional occurrences occurrences is given by a list of integers Interactive argument retrieval e Occurrences of conditionals to be raised O based A list l given in the form J ln Comman
24. 4 b Moreover a ran co e No Junk Everything in 7 apart from the atoms is generated by the constructor functions This is in fact a form of induction It allows us to infer that a property holds of all members of the data type on two assumptions 1 The property holds true of each atom 2 The property holds true of a value returned by any constructor function c assuming that it holds true of those arguments that belong to 7 rather than to some sort 8 of the underlying theory The implementation ensures that the resulting theory will be a model con servative extension of the underlying theory That is given any model M of the underlying theory we can augment M with a new domain to interpret 7 and provide interpretations of the new vocabulary so that the resulting M is a model of extended theory In the case where 7 contains no subtype it is clear that to ensure con servatism it is enough to establish that 7 will be non empty The syntax of the declaration suffices to determine whether this condition is met either there must be an atom or else at least one constructor function must take all of its arguments from types 5 of the underlying theory If 7 does have subtypes the implementation must establish that each subtype is non empty That will hold if there is an ordering of the new sorts o such that for each a at least one of the following conditions holds 1 There is an atom declared to be of sort a or 2 Th
25. IMPS can deal with You will probably want to use a parser which supports infix and prefix operators and settable precedence relations between different operators You can also use a Lisp like syntax if you prefer The syntax we will use by way of illustration is quite straightforward and you should have no difficulty in building expressions after seeing a few examples We now describe the string syntax for IMPS First some preliminary considerations A language in IMPS has two kinds of objects sorts and expressions Sorts are intended to denote classes of elements they are used to help specify the value of an expression and to restrict quantification They are especially useful for reasoning with respect to overlapping domains For example suppose zz and rr are sorts denoting the integers and the real numbers respectively Then the Archimedean principle for the real numbers can be expressed quite naturally as forall a rr forsome n zz a lt n Sorts are of two kinds atomic sorts and compound sorts An atomic sort is just a name A compound sort is a list s0 sn where each si is itself a compound sort or an atomic sort Compound sorts are intended to denote the set of all n ary partial functions from the domain sorts s0 s n 1 31 Sort Type of Sort Expressions of given sort nn ind iota k nn k 2 9 ZZ ind 1 0 1 qq ind 3 2 rr ind iota x rr x 2 2 ind ind with x ind x prop prop
26. IMPS to translate all the defined sorts and constants in metric spaces 2 tuples to normed linear spaces This can be accomplished by evaluating the form def theory ensemble instances METRIC SPACES target theories normed linear spaces h o real arithmetic multiples 1 2 sorts pp uu rr constants dist lambda x y uu norm x y lambda x y rr abs x y This does two things First it builds an interpretation from metric spaces 2 tuples into normed linear spaces in which e pp_0 goes to uu e pp_1 goes to rr e dist_0 goes to lambda x y uu norm x y e dist_1 goes to lambda x y rr abs x y Secondly it translates all the natively defined constants in metric spaces and metric spaces 2 tuples into normed linear spaces 11 7 Def theory ensemble overloadings This form takes the following arguments e The name of the theory ensemble e Any number of integers M1 Nk Evaluation of the def form causes IMPS to overload those constants natively defined in the theory multiples N Ng For example 121 def theory ensemble overloadings metric spaces 1 2 This form makes the theory ensemble mechanism manageable to the user When the system transports a natively defined constant c from a theory multiple it will often give the new constant an unappealing name For instance the name might be very long with several indices as suffixes Ideally one would like to use the same name for all instances of c and thi
27. J i po y n g z1 nn pl So in this direction extensionality is nothing new Key binding 245 force substitution Script usage force substitution expression replacement occurrences expression and replacement are denoted by strings and occurrences is a list of integers Interactive argument retrieval e Expression to replace The subexpression e of the sequent node assertion you want to replace e Replace it with The new expression r you want to replace it with e O based indices of occurrences to change A list l given in the form l dn Command kind Single inference Description This command allows you to change part of the sequent assertion It yields two or more new subgoals One subgoal is obtained from the original sequent assertion by making the requested replacements The other subgoals assert that the replacements are sound Conclusion Tso Major Premise T y r eli Minor Premises 1 lt i lt n T gt yi Notes e T is the local context of IT y at the location of the l th occurrence of ein y e Yi is e r if e is a formula and the parity of the path l is 0 r De if eis a formula and the parity of the path l is 1 eDr if e is a formula and the parity of the path l is 1 e r in all other cases 246 Key binding f generalize using sequent Script usage generalize using sequent major premise major premise can be given as an int
28. LUTINS including the string syntax introduced in Chapter 3 and the s expression syntax presented in 16 Expressions are formed by applying constructors to variables constants and compound expressions The constructors are given in Table 7 1 they serve as logical constants that are available in every language Variables and constants belong to specific languages In the mathematical syntax the symbols for the constructors the com mon punctuation symbols and the symbol with are reserved By a name we mean any unreserved symbol 7 2 1 Sorts The sorts of are generated from a finite set A of names called atomic sorts More precisely a sort of is a sequence of symbols defined inductively by 1 Each a A is a sort of 2 If a1 Qn 1 are sorts of L with n gt 1 then a1 Qm 1 is a sort of Sorts of the form ay Q n41 are called compound sorts In the next section we shall show that a compound sort denotes a domain of functions Let S denote the set of sorts of L assigns each a Aa member of S called the enclosing sort of a The atomic enclosing sort relation determines a partial order lt on S with the following properties 1 Ifa A and is the enclosing sort of a then a lt Tn 16 LUTINS is called PF 79 Constructor String syntax Mathematical syntax the true truth T
29. Section 9 2 can be normalized i e 92 transformed into a normal translation by defining new atomic sorts in the target theory of the translation 93 Chapter 9 Theory Interpretations 9 1 Introduction Theory Interpretations are translations which map the expressions from one theory to the expressions of another with the property that theorems are mapped to theorems They serve as conduits to pass results from one theory to another As such they are an essential ingredient in the little theories version of the axiomatic method which IMPS supports see Section 3 7 The IMPS notion of theory interpretation 5 7 is modeled on the standard approach to theory interpretation in first order logic e g see 2 19 24 Most of the various ways that interpretations are used in IMPS are de scribed in the penultimate section of this chapter 9 2 Translations Let 71 and 72 be LUTINS theories A translation from T to Ta is a pair u v where u is a mapping from the atomic sorts of T to the sorts unary predicates quasi sorts and indicators sets of Ta and v is a mapping from the constants of 7 to the expressions of T 2 satisfying certain syntactic conditions 71 and T are called the source theory and target theory of O respectively Given an expression e of 71 the translation of e via written e is an expression of 72 defined from p and v in a manner that preserves expression structure In particular
30. They can thus all be used in one step wherever they apply syntactically A compound macete may be constructed so as to apply the lemmas repeatedly until there are no more opportunities for applying any of them 5 4 Taking Larger Steps Under the IMPS Help menu please select the next micro exercise You will again see the combinatorial identity displayed as the goal of a new deduction This time we will start by eliminating all the occurrences of comb in favor of the defining expression Step 1 Under the Extend DG menu please again select the item Com mands Move your mouse to the item unfold single defined constant globally and click on it this function may also be invoked without menus 49 Sequent 3 for every k m Z_ implication e conjunction ol lt k ok lt m e 14 m k 1 m k m k 1 m k 1 m k m k Figure 5 6 All Occurrences have been Eliminated by typing U IMPS does not need to prompt for a numerical index of the occurrence to unfold as it will operate on all of the occurrences Result The resulting sequent shown in Figure 5 6 will need a good deal of algebraic manipulation A large part of it can be carried out by a single compound macete named fractional expression manipulation Step 2 Under the TeX menubar item click on Xview Macete IMPS will prompt you at the bottom of the screen for a name Type the first few letters of fractional expression manip
31. about polymorphic operators The great majority of the theory interpretations needed by the IMPS user are built by software without user assistance For example when a theorem is applied outside of its home theory via a transportable macete IMPS automatically builds the required theory interpretation if needed 1 3 2 Supporting Machinery We have built an extension of the core machinery with the following goals in mind e To facilitate building and printing of expressions by providing various parsing and printing procedures e To make the inference mechanism more flexible and more autonomous In particular the set of commands available to users includes an ex tensible set of inference procedures called strategies Strategies affect the deduction graph only by using the primitive inference procedures of the core machinery but are otherwise unrestricted e To facilitate construction of theories and interpretations between them 1 3 3 User Interface The user interface which is a completely detachable component of IMPS is mainly designed to provide users with facilities to easily direct and moni tor proofs Specifically it controls three critical elements of an interactive system 18 e The display of the state of the proof This includes graphical displays of the deduction graph as a tree TREX typesetting of the proof history and proof scripts composed of the commands used to build the proof The graphical display of the dedu
32. and its value for an integer j is the difference in the sense of minus between f j 1 and f j We can then prove the telescoping product formula shown in Figure 6 2 This in turn can serve as the basis of an alternative proof for formulas such as the ones for the sum of the first n natural numbers or of their squares To do so we introduce an interpretation mapping U to R and the monoid operator to real addition As a consequence the operator within the monoid is carried to the real valued finite summation operator gt gt 64 Purpose This exercise illustrates how to develop little theories and how to apply them via interpretation It also illustrates a simple recursive defi nition 6 2 4 Some Theorems on Limits Contents This exercise defines the limit of a sequence of real numbers A sequence of reals is represented in IMPS as a partial function mapping integers to real numbers The limit is defined using the iota constructor L where z o p x has as its value the unique value of x such that y x holds true The iota expression is undefined if y is satisfied by more than one value or if it is not satisfied for any value In this case the instance of y is the familiar property that for every positive real e there is an integer n such that for indices p greater than n x s p lt e Theorems include a variant of the definition in which iota does not occur as well as the familiar condition for the existence
33. and thereby the translation is forced to be a theory in terpretation Similarly if the modifier argument force under quick load is present and the switch quick load is set to true the obligations of the translation are not generated The former lets you build a theory interpre tation when the obligations are very hard to prove and the latter is useful for processing the def form faster when it has been previously determined that the translation is indeed a theory interpretation If the modifier argument dont enrich is present the translation will not be enriched A translation is enriched at various times to take into account new definitions in the source and target theories If one expects there to be many untranslated definitions after enrichment it may be computationally beneficial to use this modifier argument Examples def translation MONOID THEORY TO ADDITIVE RR source monoid theory target h o real arithmetic fixed theories h o real arithmetic sort pairs uu rr constant pairs e 0 xx theory interpretation check using simplification def translation MUL REVERSE source groups target groups fixed theories h o real arithmetic constant pairs mul lambda x y gg y mul x theory interpretation check using simplification def translation GROUPS gt SUBGROUP force source groups target groups 210 assumptions vith a sets ggl nonempty_indic_q a with a sets gg forall g h
34. annotated files which show you how theories are built and theorems proved in them These are described in the chapters of this manual 5 and 6 on the micro exercises and the exercises 3 7 The Little Theories Style The IMPS methodology for formalizing mathematics is based on a particular version of the axiomatic method The axiomatic method is commonly used both for encoding existing mathematics and for creating new mathematics A chunk of mathematics is represented as an axiomatic theory consisting of a formal language plus a set of sentences in the language called axioms The axioms specify the mathematical objects to be studied and facts about 38 the objects are obtained by reasoning logically from the axioms that is by proving theorems The axiomatic method comes in two styles both well established in modern mathematical practice We refer to them as the big theory version and the little theories version In the big theory version all reasoning is performed within a single powerful and highly expressive axiomatic theory such as Zermelo Fraenkel set theory The basic idea is that the theory we work in is expressive enough so that any model of it contains all the objects that will be of interest to us and powerful enough so that theorems about these objects can be proved entirely within this single theory In the little theories version a number of theories are used in the course of developing a portion of mathemat
35. applied to the given sequent with argument i beta reduce repeatedly applied to the sequent yielded by the previous command and direct inference applied to the sequent yielded by the previous command The commands halts if beta reduce repeatedly grounds the first produced sequent Related commands beta reduce repeatedly simplify antecedent Remarks The implementation of this command has the side effect that the assertion is beta reduced as well as the antecedent formula beta reduce insistently Script usage beta reduce insistently Interactive argument retrieval None Command kind Single inference 232 Description This command is equivalent to disabling all quasi construc tors and then calling beta reduce Related commands beta reduce insistent direct inference simplify insistently Remarks There is rarely any need to use this command It has the disagreeable effect of exploding quasi constructors beta reduce repeatedly Script usage beta reduce repeatedly Interactive argument retrieval None Command kind Single inference Description This command attempts to beta reduce each lambda application in the assertion of the given sequent repeatedly until there are no longer any lambda applications that beta reduce Related commands beta reduce beta reduce antecedent Remarks Since beta reduction can often be applied several times in a row this command is usually preferable to the command beta reduce
36. as well as the completeness axiom which states that any predicate which is nonvacuous and bounded above has a least upper bound This theory also contains the full second order induction principle for the integers as an axiom At any given time there is a theory that IMPS regards as the current theory For example as we mentioned above the current theory is h o real arithmetic when IMPS finishes loading The current theory affects the behavior of IMPS in two very significant ways 30 e Any expression that is read in by IMPS belongs to the language of the current theory unless another language is explicitly specified e In any proof that you begin you may avail yourself of all the axioms of the current theory and all the theorems previously proved and entered in the current theory You can change the current theory by selecting the Set current theory option of the pane General When you are finished playing around with changing theories set the current theory back to h o real arithmetic which is needed for the tutorial 3 4 Syntax Mathematicians and logicians usually think of a formula as a syntactic object represented by some text such as x y y For IMPS on the other hand a formula is a complex data structure essentially a record with numerous fields To build a formula in a convenient way you need to have a parser A parser takes a formula represented as a string and produces a formula represented as a data structure that
37. axioms of the theory h o real arithmetic Consequently reasoning is performed in generic theories using only the purely logical apparatus of LUTINS and possibly h o real arithmetic Moreover theorems about generic objects are easy to apply in other theories since the operators as quasi constructors are polymorphic and since the theory interpretations involved usually have no obligations to check 10 4 Hints and Cautions 1 Reasoning with quasi constructors can be tricky because the internal representation of the quasi constructor the structure it abbreviates 111 is hidden from view The view expr form see Chapter 17 can be used to print an expression without quasi constructor abbreviations For example when view expr 1 0 zz language name h o real arithmetic no quasi constructors is evaluated the expression 1 0 Lz is printed as 1 0 or zz implies 1 0 zz It is often easy to confuse quasi constructors with constants For in stance a common mistake is to try to unfold a quasi constructor To help you avoid such confusion curly brackets can be used to surround the operands of a quasi constructor instead of parentheses That is a string qfe1 en where q is a quasi constructor is parsed ex actly like q e1 en In addition the internal expression is always printed like qf e1 en unless you have defined a special print syn tax for q It should always be remembered that the interna
38. defining the command is a list of forms each of which is a command 194 form or a keyword form See a description of the proof script language in Chapter 12 Examples def script EPSILON N ARGUMENT 1 instantiate universal antecedent with p prop forall eps rr O lt eps implies p 1 def section Positional Arguments e section name Keyword Arguments e component sections section name section name e files file spec file spec Description This form builds a section which when loaded loads the sections with names section name section name and then loads the files with spec ifications file spec file spec A section can be loaded with the form load section Examples def section BASIC REAL ARITHMETIC component sections reals files imps theories reals some lemmas imps theories reals arithmetic macetes imps theories reals number theory def section FUNDAMENTAL COUNTING THEOREM component sections basic cardinality basic group theory 195 files imps theories groups group cardinality imps theories groups counting theorem def sublanguage Positional Arguments e sublanguage name Keyword Arguments e superlanguage superlanguage name Required The name of the language containing the sublanguage e languages language name language name e sorts sort name sort name e constants constant name constant name D
39. definitions theorems and macetes in this theory It also adds a number of definitions and theorems in the generic theories named generic theory 1 generic theory 2 generic theory 3 and generic theory 4 and the theory indicators Definitions The following constants in h o real arithmetic are among those included in the section foundation e sum denoted gt gt in the mathematical syntax is the least fixed point of the functional ar m n Z f Z R if m lt n o m n 1 f f n 0 284 e prod denoted in the mathematical syntax is the least fixed point of the functional TH Am n Z f Z R if m lt n n m n 1 f f n 1 e abs denoted in the mathematical notation is Ar R if 0 lt r r r e floor Aw R 12z Z 2z lt a2Aan lt 1 z groups as monoids This section interprets monoid theory in groups and then proves the telescoping product formula knaster fixed point theorem The main interest of this section is the statement and proof of the Knaster fixed point theorem which states that on a complete partial order with a least element and a greatest element any monotone mapping has a fixed point One important application of this result included in this section is a proof of the Schr der Bernstein theorem metric spaces metric spaces is the only new theory included in this section Y metric spaces Contains h o real arithmetic as a component theory Language e Sorts
40. employing any of the aforementioned tools for eliminating iota As an example consider the limit operator lim rr on sequences of reals defined by def constant LIMZRR lambda s zz rr iota x rr forall eps rr O lt eps implies forsome n zz forall p zz n lt p implies abs x s p lt eps theory h o real arithmetic Since a sequence always has at most one limit point there is an iota free characterization of lim rr def theorem CHARACTERIZATION OF REAL LIMIT forall s zz rr x rr Limfrr s x iff forall eps rr O lt eps implies forsome n zz forall p zz n lt p implies abs x s p lt eps theory h o real arithmetic 3 It is rarely a good idea to unfold a constant defined as an iota expression if it has an iota free characterization Instead the following steps are suggested For concreteness let us assume the constant we 154 are unfolding is a function constant f as in the previous item Our aim is to reduce all occurrences of f to occurrences of the form f a b e If all occurrences in the formula are of the form f a b then apply the iota free characterization of f as a macete Otherwise for every occurrence f a where a is a free variable cut with the formula Jy P f a y Each application of cut adds two new sequent nodes to the de duction graph The cut major premise which is the original sequent plus the cut formula as another assumption The cut min
41. equalities Theorem 5 2 A First Step If you have not started the first micro exercise by means of the Next micro exercise item on the IMPS Help menu do so now You will find that IMPS starts a derivation with the formula shown in Figure 5 2 This is simply the identity with the left most occurrence of comb unfolded using its definition To proceed you would like to eliminate the denominator on the left side of the equality by multiplying both sides This manipulation is justified by the theorem shown in Figure 5 3 be sure to read the lt gt as the following are equivalent The downward arrow in z asserts that 27 is well defined in effect it requires that the denominator was nonzero In the ASCII display used in Emacs buffers this is written in the form z 1 This theorem has been proved from the axioms of real arithmetic and it has been made available for a kind of rewriting in the form of a macete Its behavior as a rewrite is to replace the equation by a 2A macete meaning a clever trick in Portuguese slang is a lemma or group of lemmas 46 Replace with z z y R y z x By withy r z R z Ax 2 4 Figure 5 4 Rewriting Done by Left Denominator Removal conjunction as indicated in Figure 5 4 Step 1 You want to extend the deduction graph i e the partial proof that you have just begun Thus hold down a mouse button while pointing to the Extend DG menubar item and select the option Macete
42. facts about sets their unions and the inclusion relation It applies them to intervals of integers Purpose The purpose of this exercise is to provide experience reasoning with quasi constructors 6 3 2 Temporal Logic Contents Temporal logic is a kind of modal logic for reasoning about dynamic phenomenon In recent years temporal logic has won favor as a logic for reasoning about programs particularly concurrent programs The following is an exercise to develop a version of propositional temporal logic PTL in IMPS In this exercise we view time as discrete and linear that is we identify time with the integers The goal of the exercise is to build machinery for reasoning about time predicates which are simply expressions of sort Z gt prop In traditional PTL the time argument is suppressed and objects which 68 are syntactically formulas are manipulated instead of syntactic predicates In IMPS we will deal directly with the predicates This is a very open ended exercise which should be done after the user is fairly familiar with IMPS and its modus operandi 6 4 Exercises related to Computer Science IMPS also provides some facilities for reasoning about computing applica tions although these are still less extensive than those for mathematics The exercises illustrate a facility for defining recursive data types as well as an application of a theory of state machines 6 4 1 The World s Smallest Compiler Cont
43. is carried out within one theory usually some highly expressive theory such as Zermelo Fraenkel set theory In the little theories approach reasoning is distributed over a network of theories Results are typically proved in com pact abstract theories and then transported as needed to more concrete theories or indeed to other equally abstract theories Theory interpreta tions provide the mechanism for transporting theorems The little theories style of the axiomatic method is employed extensively in mathematical prac tice in 10 we discuss its benefits for mechanical theorem provers and how the approach is used in IMPS 1 2 2 Logic Standard mathematical reasoning in many areas focuses on functions and their properties together with operations on functions For this reason IMPS is based on a version of simple type theory However we have adopted a version called LUTINS containing partial functions because they are ubiquitous in both mathematics and computer science Although terms such as 2 0 may be nondenoting the logic is bivalent and formulas always have a truth value In particular an atomic formula is false if any of its constituents is nondenoting This convention follows an approach common in traditional rigorous mathematics and it entails only small changes in the axioms and rules of classical simple type theory 4 This version is many sorted in that there may be several types of basic individuals Moreover
44. it is multivariate in that a function may take more than one argument Cur rying is not required However taking possibly n ary functions is the only type forming operation Pronounced as in French See 4 5 7 for studies of logical issues associated with LUTINS see 16 for a detailed description of its syntax and semantics 15 Moreover LUTINS allows subtypes to be included within types Thus for instance the natural numbers form a subtype of the reals and the con tinuous real functions a subtype of the functions from reals to reals The subtyping mechanism facilitates machine deduction because the subtype of an expression gives some immediate information about the expression s value if it is defined at all Moreover many theorems have restrictions that can be stated in terms of the subtype of a value and the theorem prover can be programmed to handle these assertions using special algorithms This subtyping mechanism interacts well with the type theory only be cause functions may be partial If op is a subtype of T while 01 is a subtype of 71 then dy oj is a subtype of 7 71 In particular it contains just those partial functions that are never defined for arguments outside oo and which never yield values outside 01 1 2 3 Computation and Proof One problem in understanding and controlling the behavior of theorem provers is that a derivation in predicate logic contains too much information The mathema
45. last conjunct C of a ternary conjunction AA BAC A and B may be assumed in the local context On the other hand when a variable binding operator is traversed and there are context assumptions in which the bound variable occurs free then the simplifier must either rename the bound variable or discard the offending assumptions The strategy of exploiting local contexts is discussed in 20 At any stage in this recursive descent certain theory specific procedures may be applied to a subexpression of the original expression or to a se mantically equivalent form of the original expression These procedures are called transforms A transform T takes two arguments a context I and an expression e and returns two values an expression T T e and a set of formulas c T e cn T e called convergence requirements To apply a transform T to a context I and an expression e means to do one of three things e If the simplifier can determine that all the convergence requirements are met in L replace e with T T e e If the simplifier can determine that one of the convergence require ments fails in I replace e with an undefined expression of the same sort as e e Otherwise leave e as it is 137 This process is sound provided for every context I and expression e the following conditions hold e If all the convergence requirements c1 T e cn T e are true in T then T T e gt e e If any of the convergence requirements is f
46. node compound for nodes unsupported descendents if matches with t rr t 1 apply macete with minor premises definedness manipulations block apply macete with minor premises factorial reduction simplify Figure 12 1 An IMPs Proof Script In interactive mode the current node is the one which is displayed in the sequent node buffer 1 Expand the definition of comb which in IMPS is given in terms of the factorial function The resulting sequent consists of a context containing the formulas k lt m and 1 lt k and the assertion 1 m m m Fem Pa e on Apply the macete fractional expression manipulation to the sequent above Moreover attach to the label compound to the resulting node but otherwise leave the deduction graph intact This will allow us to subsequently return to this node Apply the command direct and antecedent inference strategy to the result of the previous step This adds three new sequents to the de duction graphs two concerning definedness and one whose assertion is an equation 129 4 We will process these nodes in step by iterating through them with the for nodes keyword form as follows a For the sequents concerning definedness use the macete definedness manipulations This combines a number of facts about the definedness of the arithmetic operations and the facto rial function b For the remaining sequent use the macete factorial reduction 12 4 1
47. occurrence of s in y is the b th occurrence of w in y and the a th occurrence of s in y is the c th occurrence of s in w If every free occurrence of a variable in s is also a free occurrence in 4 the primitive inference procedure reduces the sequent to T gt glif form 6 plti s Ylt2 sle Ylo and otherwise the primitive inference procedure fails Now assume n gt 1 The primitive inference procedure will then simul taneously raise each specified occurrence of a conditional expression in y in the manner of the previous paragraph if there are no conflicts between the occurrences The kinds of conflicts that can arise and how they are resolved are listed below e If two or more specified occurrences of a conditional expression s in y are contained in same smallest formula they are raised together e If two or more specified occurrences of distinct conditional expressions in y are contained in same smallest formula at most one of the occur rences is raised e If y and Ys are the smallest formulas respectively containing two specified occurrences of a conditional expression in y and 41 is a proper subexpression of Y then the first specified conditional expression is not raised simplification Parameters None Description This primitive inference procedure simplifies the assertion of the given sequent with respect to the context of the sequent It uses both theory specific and general logical methods to reduce the seque
48. of the limit The homogeneity of limit is also proved Purpose The main purpose of this exercise is to illustrate how to reason with iota In particular it illustrates the importance of deriving an iota free characterization for a notion defined in terms of iota 6 2 5 Banach s Fixed Point Theorem Contents This extensive file contraction t contains a complete proof of Banach s contractive mapping fixed point theorem An alternative proof using a little more general machinery is contained in the theory library in file IMPS theories metric spaces fixed point theorem t The theorem states that in a complete metric space P d any contrac tive function has a unique fixed point A function f is contractive if there exists a real value k lt 1 such that for all points x and y in P Uf x F y lt k d a y The heart of the proof is to show that under this condition the sequence s of iterates of f starting from an arbitrary point x s x f x fr f a 65 will converge It is then easy to show that the limit of s is a fixed point Finally if any two distinct points x and y were both fixed then we would have This theorem serves as a very good illustration of IMPS s little theories approach It combines e Concrete theorems about the reals such as the geometric series for mula which are needed to bound the differences between points in e A few abstract facts about the sequence of
49. pp P in the mathematical syntax denotes the underlying set of points of the metric space e Constants dist denotes a real valued two place function on pp 285 Axioms 1 Positivity Vx y P 0 lt dist x y 3 Symmetry Vax y P dist x y dist y x 1 2 Separation Yx y P x y dist x y 0 3 4 Triangle Inequality Yx y z P dist x z lt dist x y dist y z metric space pairs This section introduces the theory metric space pairs metric space pairs This theory is defined by the theory ensemble mechanism Alternatively it can be described as follows Language The language contains two copies of the language for metric spaces Notice however that it does not contain two copies of the reals e Sorts pp_O Po in the mathematical syntax pp 1 P in the mathematical syntax e Constants dist_0 disto in the mathematical syntax dist_1 dist in the mathematical syntax Axioms The axioms are the positivity separation symmetry and triangle inequality axioms for both functions dist_0 and dist_1 See 13 for some example proofs metric space continuity This section develops continuity and related notions in the context of metric spaces 286 number theory This section develops the rudiments of number theory The fundamental theorem of arithmetic and the infinity of primes are proved pairs A pair of elements a b of sort a 6 is rep
50. pred pred are constant names denoting two place predicates We will say that the predicates pred are within the scope of the specified order processor algebraic term comparator spec spec specis just the name of an algebraic or order processor We will say that the equality con structor is within the scope of the specified processor 207 Description This form causes the simplifier of the theory named theory name to simplify certain terms using the specified algebraic and order processors as follows e All applications of an operator or predicate within the scope of a pro cessor are handled by that processor An operation or predicate may be within the scope of more than one processor e All equalities are handled by processors which contain the equality constructor within its scope Examples def theory processors H 0 REAL ARITHMETIC algebraic simplifier rr algebraic processor sub algebraic order simplifier rr order lt lt algebraic term comparator rr order def theory processors VECTOR SPACES OVER RR algebraic simplifier vector space algebraic processor algebraic term comparator vector space algebraic processor def translation Positional Arguments e name The name of the translation Modifier Arguments e force e force under quick load e dont enrich 208 Keyword Arguments e source source theory name Required e target target theory na
51. premise moreover in some cases we distinguish one particular premise as a major premise In so doing we regard the remaining premises as minor premises 218 Related commands These are other commands you might consider ap plying because for example they are quicker or more effective for your task at hand Remarks Hints or observations that we think you should find useful Key binding A single key to invoke the command Command Application in Interactive Mode To apply a command in interactive mode to the current sequent node that is the one visible in the sequent node buffer hit You can also apply a command by selecting it from the command menu as follows e For Emacs version 19 click on the entry Extend DG in the menubar and select the option Commands e For Emacs version 18 click right on the Command menu item in the Extending the Deduction Graph pane You can also invoke the command menu directly by pressing the key F3 You will be presented with a well pruned menu of those commands which are applicable to the given sequent node Once you select a command the system will request the additional arguments it needs to apply the command You will notice that for a given command the system will sometimes request additional arguments and at other times not do so In the cases where the system fails to make a request for arguments the system determines what these additional arguments should be on its own Command Ap
52. ran a 7 If x1 are distinct names Q7 0 S A is an expression of sort and n gt 1 then A 21 01 Tn An A is an expression of sort a1 An Pl 8 If x and y are names a and are sorts are of kind and x respectively and A is an expression of sort x then 4 x 0 A and tp y B A are expressions of sort a and 6 respectively 9 If A B C are expressions of sort x 5 y respectively with 7 8 T y then if A B C is an expression of sort BU y 10 If A is an expression and a S then AJ and A a are expressions of sort 11 If a is a sort of kind v then La is an expression of sort a A variable is an expression of the form x a A formula is an expression of sort x A sentence is a closed formula A predicate is an expression with a sort of the form a1 Qn An expression is said to be of type a if the type of its sort is a and it is said to be of kind 1 respectively if its type is of kind respectively x Notice that the well formedness of an expression depends only on the types and not directly on the sorts of its components Expressions of kind are used to refer to mathematical objects they may be nondenoting Expres sions of kind are primarily used in making assertions about mathematical objects they always have a denotation 7 2 3 Alternate Notation Expressions will usually be written in an abbreviated form as follows Sup pose A is an expre
53. simplification Script usage direct and antecedent inference strategy with simplification Interactive argument retrieval None Command kind Multi inference Description This command first applies direct and antecedent inference strategy to the given sequent and then applies simplify to all resulting sequents Related commands antecedent inference strategy direct and antecedent inference strategy direct inference strategy 239 direct inference Script usage direct inference Interactive argument retrieval None Command kind Single inference Description This command applies an analogue of an introduction rule of Gentzen s sequent calculus in reverse based on the leading constructor of the assertion of the given sequent Conclusion TSy Dy Premise TU p gt Y Conclusion TS p1A AOn Premises 1 lt i lt n TU qgi yi 1 gt Yi Conclusion T gt yV Ven Premise TU 7y1 Pn 1 gt Pn Conclusion T gt 0 V Premises TU p gt Y PU y gt e Conclusion T if form y y 0 Premises TU p gt Y FU w 0 Conclusion T gt V21 01 Tn 0n P Premise r y Notes e is obtained from y by renaming the variables among 71 p which are free in both y and the context T Related commands antecedent inference direct inference strategy unordered direct inference 240 Remarks Keep in mind that any direct infere
54. sort pairs uu rr constant pairs e 0 theory interpretation check using simplification The purpose of the line fixed theories h o real arithmetic is to speed up the construction of the interpretation by telling IMPS ahead of time that the theory h o real arithmetic which is a subtheory of monoid theory is fixed by the translation i e each expression of h o real arithmetic is mapped to itself 9 4 Translation of Defined Sorts and Constants Let be a translation from 71 to 72 Translations have been implemented in IMPS so that the defined sorts and constants of J are handled in an effec tive manner even when they are defined after is constructed There are three possible ways that a defined sort or constant of 71 can be translated First if the defined sort or constant is a member of one of the fixed theories of it is translated to itself Second if the defined sort or constant is mentioned i e is the first component of a pair in the sort or constant association list of it is translated to the second component of the pair In practice most defined sorts and constants are not mentioned in the sort and constant association lists And third if the defined sort or constant is not mentioned in the sort and constant association lists and is not a member of a fixed theory it is translated on the basis of its definiens unary predicate expression or list of functionals This last way of translat
55. string syntax and briefly to explain how you can extend or modify this syntax 3 To explain how you can redefine the syntax altogether 16 1 Expressions As explained in Chapter 7 expressions are variables constants and com pound expressions formed by applying constructors to other expressions Expressions can thus be represented as Lisp s expressions e Formal symbols i e constants or variables correspond to atoms e Compound expressions correspond to certain lists of the form constructor c gt Cp where each c is itself an expression In the implementation an expression is a data structure which also caches a large amount of information such as the free and bound variables of the expression the constants contained in the expression the home language limps is designed so that it does not impose a syntax on the user 156 of the expression and so on For the IMPS user an expression is typically something which can be represented as text for instance f i ln zdz The cor respondence of an expression as a data structure to an external representa tion for input or output is determined by the user syntax which is employed IMPS allows multiple user syntaxes so for example the syntax that is used for reading in expressions usually text may be different from the syntax used to display expressions which could be text or text interspersed with TEX commands which would make the output suitable for input to the T
56. th assumption of the context of the given sequent with terms from the context Related commands auto instantiate existential instantiate universal antecedent backchain Script usage backchain assumption assumption can be given as an integer 7 or a string o Interactive argument retrieval e O based index of antecedent formula If there is only one as sumption this argument request is omitted Command Kind Single inference 228 Description This command includes the behavior described under backchain through formula However for a part of the assumption of one of the forms s t s t s t if a subexpression of the assertion matches s then it is replaced by the corresponding instance of t Related commands backchain backwards backchain repeatedly backchain through formula Key Binding b backchain backwards Script usage backchain backwards assumption assumption can be given as an integer 1 or a string o Interactive argument retrieval e O based index of antecedent formula Command Kind Single inference Description Backchain backwards differs from backchain in that sub formulas of the assumption of the forms s t s t s t are used from right to left Related commands backchain backchain repeatedly backchain through formula backchain repeatedly Script usage backchain repeatedly assumption list assumption list can be given as a list of numbers of strings or an assumption l
57. the false falsehood F not not p p and pi and and pn P1A NOn or pl or or pn p1V V On implies pi implies p2 poy iff pi iff p2 y if form if_form p1 p2 p3 if form y1 pa p3 forall forall v1 s1 vn sn p VVU Q1 UnAn P forsome forsome v1 s1 vn sn p dui ai UniQn Y equals t1 t2 ti ta apply f t1 tn Hibiasesha lambda lambda vi si vn sn t AU 07 UniAn t iota iota v1 s1 p LU Q p iota p iota_p v1 s1 p LpUQ p if if p t1 t2 if y t1 t2 is defined t tl defined in t s tla undefined s La Table 7 1 Table of Constructors 76 2 013 b 2 An bn An 1 s Bn 1 iff tiers al is Da Baral 3 If a 8 S with a lt 8 and a is compound then 8 is compound and has the same length as a 4 For every a S there is a unique 8 S such that a lt 8 and is maximal with respect to lt lt is intended to denote set inclusion The members of S which are maximal with respect to lt are called types A base type is a type which is atomic Every language has the base type which denotes the set T F of standard truth values The type of a sort a written T 0 is the unique type 8 such that a lt 8 The least upper bound of a and 8 written aU 8 is the least upper bound of a and 8 in the partial order lt The least upper bound of two sorts with the same type is always defined A function sort is a sort a such that T a has the form a1
58. the renaming function is that it not identify distinct constant names or distinct sort names A typical renaming function is one which affixes an underscore followed by a number to a name For each n gt 0 let Rn be a renaming function 117 e For each n gt 0 let 7 be a copy of 7 obtained by applying the renamer Rn Tn is called the n th theory replica of T e Let Un be the union of the theories To 7n 1 Un is called the n th theory multiple of T e For each 0 n 1 there is a theory interpretation UV of T in the replica 7 W is called i th replicating translation from the base theory These translations are actually constructed by the system when a multiple is built Note that Y composed with the inverse of WV is also an interpretation of 7 in 7 however this translation is not constructed by the system automatically e Let m lt n and f 0 m 1 gt 0 n 1 be an injective function In our documentation we refer to f as a per mutation Then there is a unique interpretation 9 Um Un with the property that for each i 0 m 1 Py extends the canonical interpretation of T in T qj Pf is called the canonical interpretation associated to f e A defined constant is natively defined in Um if and only if the following two conditions hold The constant is not the translation of a defined constant from a lower multiple by a canonical translation The constant is not t
59. the system depends is included in the core of IMPs The core is the specification and inference engine of IMPS The other components of the system provide the means for harnessing the power of the engine The organizing unit of the core is the IMPS theory Mathematically a theory consists of a LUTINS language plus a set of axioms A theory is im plemented however as a data structure to which a variety of information is associated Some of this information procedurally encodes logical con sequences of the theory that are especially relevant to low level reasoning within the theory For example the great majority of questions about the definedness of expressions are answered automatically by IMPS using tabu lated information about the domain and range of the functions in a theory Theories may be enriched by the definition of new sorts and constants and by the installation of theorems Proofs in a theory are constructed interactively using a natural style of inference based on sequent calculus IMPS builds a data structure which records all the actions and results of a proof attempt This object called a deduction graph allows the user to survey the proof and to choose the order in which he works on different subgoals Alternative approaches may be tried on the same subgoal Deduction graphs also are suitable for analysis by software The user is only allowed to modify a deduction through the application of primitive inferences which are akin
60. the translation of y by Step 3 gp is installed as a theorem in T with usage list symbol symbol If the modifier argument reverse is present evaluating this form is equivalent to evaluating the form without reverse followed by evaluating the form again without reverse but with e name changed to the concatenation of rev with name and e formula spec changed to a string which specifies the reverse of the formula specified by formula spec In other words the reverse argument allows you to install both a theorem and its reverse It is very useful for building a macete or transportable macete and its reverse by evaluating one form Of course it would not be wise to use the reverse argument when rewrite is a usage 198 Examples def theorem ABS IS TOTAL total_q abs rr rr theory h o real arithmetic usages d r convergence proof unfold single defined constant 0 abs insistent direct inference beta reduce repeatedly 229 def theorem RIGHT CANCELLATION LAW left cancellation law theory groups translation mul reverse proof existing theorem def theorem FUNDAMENTAL COUNTING THEOREM f_indic_q gg subgroup implies f_card gg subgroup f_card stabilizer zeta f_card orbit zeta 3 forall zeta uu a f_indic_q gg subgroup Pe implies e f_card gg subgroup ss f_card stabilizer zeta f_cardforbit zeta theory group actions home theory counting theorem theo
61. theory ensemble base together with N theory interpretations from the base theory into the multiple All ex isting definitions of the base theory are translated via these interpretations The N multiple is constructed to be a subtheory of the N 1 multiple Examples def theory ensemble multiple metric spaces 2 def theory ensemble overloadings Positional Arguments e ensemble name An error will result if no ensemble exists with en semble name e Ni Ng Each N is an integer Description Installs overloadings for constants natively defined in the theory multiples N Np Examples def theory ensemble overloadings metric spaces 1 2 205 def theory instance Positional Arguments e name The name of the theory to be created Keyword Arguments e source source theory name Required e target target theory name Required e translation trans name Required e fixed theories theory name theory name e renamer renamer Name of a renaming procedure e new translation name new trans name Name of the the transla tion to be created Description Let To and Tj be the source and target theories respectively of the trans lation named trans name Also let T and Tj be the theories named source theory name and target theory name respectively Lastly let F be the set of theories named theory name theory name Suppose that T and Jj are subtheories of T and T resp
62. theory source theory name e source theories source theory name source theory name Description This form imports into the theory named theory name all the transportable rewrite rules installed in the theory named source theory name or in the theories named source theory name source theory name 182 def inductor Positional Arguments inductor name induction principle Can be a string representing the induction prin ciple in the current syntax or a name of a theorem Keyword Arguments theory theory name Required translation name name is the name of a theory interpretation If this keyword is present the formula used in constructing the induction principle is actually the translation of induction principle base case hook name name is the name of a macete or a com mand induction step hook name name is the name of a macete or a command dont unfold name namen name is the name of a recursive constant in the theory or the symbol t This form instructs the induc tor not to unfold the recursive constant named name when processing the induction step If t is specified then no recursive definitions will be unfolded in the induction step Remarks The induction principle used for constructing an inductor must satisfy a number of requirements The induction principle must be a theorem The induction principle must be a universally quantified biconditional of the form
63. this command has the dis agreeable effect of exploding quasi constructors instantiate existential Script usage instantiate existential instantiations instantia tions is a list of strings denoting expressions Interactive argument retrieval e Instance for variable x of sort g1 tj e Instance for variable 2 of sort on tn n gt 1 Command kind Multi inference Description This command instantiates an existential assertion with the specified terms Conclusion T gt 321 01 Un On P Major Premise r gt y Minor Premises 1 lt i lt n T gt ti 05 Notes e is the result of simultaneously replacing each free occurrence of x1 in y with t for each i with 1 lt i lt n if necessary renaming bound variables in y to avoid variable captures Related commands auto instantiate existential instantiate theorem Script usage instantiate theorem theorem instantiations theorem is the name of a theorem and instantiations is a list of strings denoting expressions 251 Interactive argument retrieval e Theorem name The name of a theorem V2 0 n 0n W in the deduction graph s theory e Instance for variable x of sort 0 tj e Instance for variable x of sort On tn n gt 1 Command kind Multi inference Description This command instantiates the argument theorem with the specified terms t1 t and then adds the resulting formula to the context o
64. to remove an assumption but in fact in many cases this is a natural step to take e If an assumption is irrelevant then removing it will do no harm and will make the job of the simplifier a lot easier e It is often the case that sequent nodes are identical except for the addi tion of irrelevant assumptions In this case removing the irrelevant assumptions allows you to ground both sequents by just grounding one Key binding w 268 Chapter 19 The Primitive Inference Procedures In this chapter we list and document each of the primitive inference proce dures We will use the following format to describe them Parameters A list of the arguments other than the sequent node re quired by procedure These arguments can be of the following types e A formula e A list of formulas e A path represented as a list of nonnegative integers e A list of paths e A constant e A macete e Another sequent node usually referred to as the major premise Description A brief description of the primitive inference Some of prim itive inference procedures have descriptions which are identical to the description of the corresponding interactive proof command antecedent inference Parameters A sequent node assumption 269 Description The effect of applying this primitive inference procedure is given by the following table Conclusion TU yD vy
65. to rules of inference Most primitive inferences formalize basic laws of predicate logic and higher order functions Others implement computational steps in proofs For example one class of primitive inferences performs expression simplification which uses the logical structure of the expression 20 together with algebraic simplification deciding linear inequalities and applying rewrite rules Another special class of primitive inferences compute with theorems by applying extremely simple procedures called macetes An elementary macete which is built by IMPS whenever a theorem is installed in a theory 3 Macete in Portuguese means a chisel or in informal usage a clever trick 17 applies the theorem in a manner determined by its syntax e g as a con ditional rewrite rule Compound macetes are constructed from elementary and other kinds of atomic macetes including macetes that beta reduce and simplify expressions They apply a collection of theorems in an organized way In addition to the machinery for building theories and reasoning within them the core contains machinery for relating one theory to another via theory interpretations A theory interpretation can be used to transport a theorem from the theory it is proved in to any number of other theories Theory interpretations are also used in IMPS to show relative consistency of theorems to formalize symmetry and duality arguments and to prove universal facts
66. turn e These rules are used iteratively to descend through the structure of the assumption as deeply as necessary If IMPS cannot recognize that the terms returned by a match are defined in the appropriate sorts then these assertions are returned as additional minor premises that must later be grounded to complete the derivation Related commands backchain backchain backwards backchain repeatedly beta reduce Script usage beta reduce Interactive argument retrieval None Command kind Single inference Description This command attempts to beta reduce each lambda application in the assertion of the given sequent Related commands beta reduce antecedent beta reduce insistently beta reduce repeatedly beta reduce with minor premises simplify 231 Remarks Since beta reduction can often be applied several times in a row the command beta reduce repeatedly is usually preferable to this command Beta reduction is also performed by simplify beta reduce antecedent Script usage beta reduce antecedent assumption assumption can be given as an integer i or a string o Interactive argument retrieval e O based index of antecedent formula i If there is only one as sumption this argument request is omitted Command kind Multi inference Description This command is used for beta reducing an assumption in the context of the given sequent It is equivalent to the following sequence of commands incorporate antecedent
67. vector language component theories generic theory 1 axioms forall x y z uu x y z x y z forall x y uu x y yt x forall x uu x v0 x forall x y rr z uu x y z x y z forall x y uu a rr a xt t y a x a y forall a b rr x uu atb x a x b x forall x uu Oxx x v0 forall x uu 1 x x def theory ensemble Positional Arguments e ensemble name The name of the theory ensemble This will also be the name of the base theory unless the base theory keyword argu ment is provided Keyword Arguments e base theory theory name theory name is the name of the base the ory of the ensemble If this keyword argument is not included then the base theory is that theory with the name ensemble name fixed theories theory theory The theories listed are not replicated when the theory replicas and multiples are built If this argument is not provided then the fixed theories are those in the global fixed theories list at the time the form is evaluated e replica renamer proc name proc name is the name of a proce dure of one integer argument used to name sorts and constants of theory replicas The default procedure is to subscript the correspond ing sort and constant of the base theory Description This form builds a theory ensemble such that 201 1 The base theory is the theory with name theory name if the base theory keyword argument i
68. will post an additional sequent with the result of the rewrit ing This is identical to the formula you obtained in the first micro exercise Step 3 Again unfold the leftmost occurrence of comb As this formula has more than one defined constant in it factorial is also introduced by def inition IMPS will prompt with a menu displaying the syntactically available constants which may be chosen You will again need to type 0 to the prompt at the bottom of the Emacs screen to indicate the leftmost occurrence Result IMPs will post another sequent with the subgoal shown in Fig ure 5 5 Since this has a subexpression of the form a b c you will want to rewrite it to the form a b c b 48 for every k m Z implication e conjunction ol lt k ok lt m e conjunction o kl 1 4m kD7 o m k 1 m k DJ 7 kl m k 1 m Figure 5 5 Result of the Second Unfolding Step 4 Use the macete description menu item under Extend DG to find a macete to carry out this transformation Result The resulting sequent has a subexpression of the form a b c You will want to bring this to the form a c b Step 5 Use the macete description menu item under Extend DG to find a macete to carry out this transformation Clearly invoking individual macetes in this way can become unbearably tedious You can now see the importance of being able to group together a collection of lemmas into a compound macete
69. write prop def recursive constant Positional Arguments e names The name or lists of names of the constant or constants to be defined e defining functional strings A string or list of strings specifying the defining functionals of the definition Keyword Arguments e theory theory name Required e usages symbol symbol e definition name def name The name of the definition Description Let T be the theory named theory name const name const namen be the names given by names and fi fn be the functionals specified by the strings in defining functional strings This form creates a list of new constants C1 Cn called const name const name and a set of new axioms with usage list symbol symbol The axioms say that C Cn are a minimal fixed point of the family f1 fn of functionals The new constants and new axioms are added to T provided e each const name is not the name of any current constant of T or of a structural supertheory of T and 191 e each functional f is known to be monotone in T If the definition name keyword is present the name of the definition is def name otherwise it is const name Examples def recursive constant SUM lambda sigma zz zz zz rr rr lambda m n zz f zz rr if m lt n sigma m n 1 f f n 0 theory h o real arithmetic definition name sum def recursive constant EVEN ODD lambda even odd nn prop
70. 134 136 136 137 138 139 140 14 4 Building Macetes 0 00000000004 147 14 5 Applicable Macetes 2 0 0 e o 149 14 6 Hints and Cautions 2 0 0 0 0 202 eee 149 15 The Iota Constructor 151 15 1 Motivation rc A ae RO Re ee 151 15 2 Reasoning with Iota 2 020004 152 15 2 1 eliminate defined iota expression 152 15 2 2 eliminate iota ee ee 152 15 2 3 eliminate iota Macete 00004 152 15 3 Hints and Cautions 2 0 2 0 0 0000 2 eG 153 16 Syntax Parsing and Printing 156 16 sl Expressions a oe 156 16 2 Controlling Syntax 2 2 20 20 e 157 16 3 String Syntax ssoi 2 ese de eh ae ee A ees 158 16 4 Parsing 2 vo a p ota A eae Oe ta 159 16 5 Modifying the String Syntax 0 162 16 6 Hints and Cautions 0 2 0 0 0 0 002 2 ee 163 III Reference Manual 165 17 The IMPS Special Forms 167 17 1 Creating Objects 2 2 eee 169 def algebraic processor 1 0 ee a 169 def atomic sort ooe ceara E O E A a a TA G 171 delia es oa dd ee do das eA 172 def cartesian product soo o e 179 def compound macete o oo a 180 d ftconstant seag purunta e pan aae A nia Sow aa 181 def imported rewrite rules o oo 182 def inductor 2 a 183 deElanguasen cta e Bok Bl a in a 185 def order processor 1 0 a 187 def primitive recursive constant 048 188 def quasi constructor
71. 2 2 The IMPS Proof System In the traditional presentation of proofs in textbooks and journals the de ductive process appears as an inexorable progression from known facts to unknown ones In contrast the deductive process in IMPS begins with a conjecture and usually proceeds with a large amount of trial and error This view of the deductive process leads naturally to the idea of a proof as a graph Proofs in IMPS are represented by a data structure called a deduction graph which is a directed graph with two kinds of nodes inference nodes and sequent nodes A sequent node consists of a single formula called the asser tion together with a context The context is logically a set of assumptions although the implementation caches various kinds of derived information with a context An inference node i consists of a unique conclusion node c a possibly empty set of hypothesis nodes h1 hn and the mathe matical justification for asserting the relationship between c and hj hn This justification is called an inference rule As an interactive process a proof consists of a series of reductions of unproven sequent nodes of the graph which we think of as goals to new subgoals Each reduction is created by a procedure called a primitive infer ence procedure which takes a sequent node and possibly other arguments returns an inference node inf and as a side effect changes the deduction graph These changes include e The addition of i
72. 992 W M Farmer J D Guttman and F J Thayer Little theories In D Kapur editor Automated Deduction CADE 11 volume 607 of Lecture Notes in Computer Science pages 567 581 Springer Verlag 1992 W M Farmer J D Guttman and F J Thayer IMPS an Interactive Mathematical Proof System Journal of Automated Reasoning 11 213 248 1993 W M Farmer J D Guttman and F J Thayer Reasoning with contexts In A Miola editor Design and Implementation of Symbolic Computation Systems volume 722 of Lecture Notes in Computer Sci ence pages 216 228 Springer Verlag 1993 W M Farmer and F J Thayer Two computer supported proofs in metric space topology Notices of the American Mathematical Society 38 1133 1138 1991 J A Goguen Principles of parameterized programming Technical report SRI International 1987 J A Goguen and R M Burstall Introducing institutions In Logic of Programs volume 164 of Lecture Notes in Computer Science pages 221 256 Springer Verlag 1984 J D Guttman A proposed interface logic for verification environments Technical Report M91 19 The MITRE Corporation 1991 J D Guttman Building verification environments from components A position paper In Proceedings Workshop on Effective Use of Auto mated Reasoning Technology in System Development pages 4 17 Naval Research Laboratory Washington D C April 1992 D Kranz R Kelsey J Rees P Hudak J Philbin and N A
73. Enter all of the numbers from 1 to 12 separated by spaces You are now ready for the more interesting exercises which are intended to illustrate how interesting portions of mathematics and computer science can be developed using IMPS This is the topic of the next chapter of this manual 59 Chapter 6 Exercises 6 1 Introduction This chapter describes about a dozen self guided content based exercises to illustrate the use of Imps Each exercise uses a fairly self contained piece of mathematics logic or computer science to show how to organize and develop a theory in IMPS and how to carry out the proofs needed for the process We will try to describe in each case the main content of the exercise as well as the specific techniques that it is intended to illustrate We assume in this chapter that you are using the Lucid 19 menu system 6 1 1 How to Use an Exercise In order to start an exercise press down any mouse button while pointing to the IMPS Help menubar item Release the button while pointing to the entry Exercises IMPS will present a pop up menu listing the file names of the available exercises Clicking on a file name will cause the following actions e The system will create a new copy of the file under your own directory in the subdirectory imps theories Since this is a new file you can safely edit it or delete it If a file of the expected name already exists IMPS will prompt whether to overwrite the file thus de
74. Evaluation of Script Expressions Scripts are executed in an environment This environment is an association of symbols to values Every script expression has a value in the script s execution environment The value of a script expression is determined as follows e If the expression is a script variable n where n is an integer then the value is the n th argument in the script call e If the expression is a script variable name where name is a symbol its value is determined by the last assignment of that variable If there is no assignment preceding the call an error is raised e If the expression is a string an integer or a symbol which is not a variable then the value of the expression is itself e If the expression is a list whose first element is an expression operator that is one of the symbols then that operator is applied to the values of the arguments as follows format string arg arg The first argument must be a string with exactly n occurrences of the characters A The re maining arguments arg are plugged in succession for each occur rence of A sym format string arg gt arg The first argument must be a string with exactly n occurrences of the characters A The remaining arguments arg are plugged in succession for each oc currence of A and the resulting string is read in as a symbol arg arg The set of assumptions regarded as strings of the curre
75. J Sussman Structure and Interpretation of Com puter Programs MIT Press 1985 H B Enderton A Mathematical Introduction to Logic Academic Press 1972 W M Farmer Abstract data types in many sorted second order logic Technical Report M87 64 The MITRE Corporation 1987 W M Farmer A partial functions version of Church s simple theory of types Journal of Symbolic Logic 55 1269 91 1990 W M Farmer A simple type theory with partial functions and sub types Annals of Pure and Applied Logic 64 211 240 1993 W M Farmer A technique for safely extending axiomatic theories Technical report The MITRE Corporation 1993 W M Farmer Theory interpretation in simple type theory In Pro ceedings International Workshop on Higher Order Algebra Logic and Term Rewriting HOA 93 Amsterdam The Netherlands September 1993 Lecture Notes in Computer Science Springer Verlag 1994 Forth coming W M Farmer J D Guttman M E Nadel and F J Thayer Proof script pragmatics in IMPS In 12 International Conference on Automated Deduction CADE 12 Lecture Notes in Computer Science Springer Verlag 1994 Forthcoming W M Farmer J D Guttman and F J Thayer IMPS System descrip tion In D Kapur editor Automated Deduction CADE 11 volume 299 10 11 12 13 14 15 16 17 18 19 607 of Lecture Notes in Computer Science pages 701 705 Springer Verlag 1
76. MPS Help Imps will start yet another derivation of the combinatorial identity If you are unfamiliar with Emacs drag the mouse left and use the Edit menubar entries to remove the text describing four steps shown in Figure 5 11 These were the detailed steps used to prove the first definedness 56 Sequent 1 for every m Z implication e0 lt m Djaj m m 1 2 Figure 5 12 The Sum of the First n Natural Numbers assertion In their place it would suffice to use definedness manipulations Mark the following step by dragging the mouse left and then use the Copy and Paste entries in the Edit menu to duplicate the line Add a carriage return if appropriate Starting with your cursor on the first line of the new sequence of com mands click on the menu item Execute proof line under Scripts When IMPS updates the sequent nodes buffer with the new subgoal repeat the process At each step wait until the previous step has completed Six steps complete the proof 5 6 Induction Taking a Single Step Axioms or theorems that we may regard as induction principles play a crucial role in many theories IMPS provides good support for inductive reasoning in a form that is independent of particular theories That is when an axiom or theorem of the right form is available in any theory then it can be applied with the full power of the IMPS induction command We will illustrate IMPS s treatment of induction first in a manual
77. REMOVAL FOR EQUALITIES RIGHT DENOMINATOR REMOVAL FOR EQUALITIES RIGHT DENOMINATOR REMOVAL FOR STRICT INEQUALITIES LEFT DENOMINATOR REMOVAL FOR STRICT INEQUALITIES RIGHT DENOMINATOR REMOVAL FOR INEQUALITIES LEFT DENOMINATOR REMOVAL FOR INEQUALITIES MULTIPLICATION OF FRACTIONS LEFT MULTIPLICATION OF FRACTIONS RIGHT Figure 5 7 The Form of fractional expression manipulation 5l Sequent 4 for every k m Z_ implication e conjunction ol lt k ok lt m e conjunction o k l 1 m 1 40 7 o conjunction o k m 1 2 4 1 1 m 1 k 1 D o 14m k m 1 k 1 1 m 1 k 1 1 k 1 1 m 1 k 1 1 m kl m 1 k m k m 1 k Figure 5 8 The Result of fractional expression manipulation the Extend DG menubar item You will find fractional expression manipulation among the list of potentially useful macetes It will execute for about 20 seconds Result The macete will cause IMPS to carry out all the algebraic op erations involved in adding and multiplying fractions and will cause it to cross multiply eliminate denominators for equations such as a b c Since this is permissible only when b7 we obtain a conjunction of assertions The first two conjuncts assert that two denominators were nonzero and the third is a bulky algebraic equation which assuming the denominators were nonzero suffices for our previous subgoal to be true We want next to break up the logical st
78. Related commands apply macete apply macete locally apply macete locally with minor premises Remarks The convergence requirements which are posted as additional subgoals arise from two different sources 1 Convergence requirements are generated by the simplifier in the course of certain reductions including algebraic simplification and beta reduction 2 Convergence requirements are also generated by checks that instanti ations of universally valid formulas used by the macete are sound You should never assume that subgoals generated by this command are always true As always for nonreversible commands you should inspect the new subgoals to insure IMPS is not misdirecting your proof assume theorem Script usage assume theorem theorem Interactive argument retrieval e Theorem name The name of a theorem in the deduction graph theory Command kind Single inference Description This command adds the argument theorem to the context of the given sequent Related commands apply macete assume transported theorem instantiate theorem Remarks To apply a theorem to a sequent you will usually want to use apply macete or instantiate theorem instead of assume theorem 226 assume transported theorem Script usage assume transported theorem theorem interpretation Interactive argument retrieval e Theorem name The name of a theorem in T e Theory interpretation The name of a theory interpretation of T in th
79. S mailing list The second section contains a copy of IMPS copyright notice and public license 2 1 How to Get and Install IMPS 2 1 1 How to Get IMPS Ftp to math harvard edu login as anonymous and give your e mail ad dress as the password Then type cd imps The directory you will be in contains a directory named doc and four files 1 the text in this section README 2 the IMPS system imps tar gz 3 the IMPS manual imps manual dvi gz and 4 the IMPS public license public license The IMPS manual and public license are also included in the IMPS system To get a copy of the IMPS system type 21 binary get README get imps tar gz The transfer will take a few minutes 2 1 2 How to Install IMPS 1 Create a directory called imps or whatever you prefer somewhere in your file system where you have 35 40 MB free About 20 MB of this space is for IMPS the rest is needed only during installation Let us refer to this directory as imps Execute the shell command cd imps Copy the file imps tar gz to the imps directory Then execute the following commands gunzip imps tar gz tar xvf imps tar Each of these operations will take several minutes After they are done you may delete the file imps tar or recompress it and put it somewhere else Choose the version of Emacs you want to use with Imps The pre ferred version is Free Software Foundation GNU Emacs 19 but we also support GN
80. SAS Synta ver e A Re ee BAD 3 5 A Proofs Aves fy th a es Be ahh GRE che a RE 3 6 Extending IMPS n snag a 2 Boel ae SE te 3 7 The Little Theories Style On Line Help dale Phe Manual asti tie te A Soe ea ee AD Wet fOrmMss sina aaea ip Be ye Bo os a oh eee Gh ee ele Hes as 4 3 Using Menus iosop e eh amp eos Bee a ee Micro Exercises 5 1 A Combinatorial Identity 52 gt A First Step oe kc ka eke MAE Pa ba eh ee ee Gob 5 3 Taking More Steps 2 a 5 4 Taking Larger Steps e 5 5 Saving a Proof o e e 5 6 Induction Taking a Single Step o a 5 7 The Induction Command 0004 Exercises 6 1 Introduction s s a gon Gg be do eee a Be He Ewe eG 6 1 1 How to Use an Exercise 6 1 2 Paths Through the Exercises 6 2 Mathematical Exercises 0 00000 ee ee 6 2 1 Pme 2 4s be ba a Oa A we 6 2 2 A Very Little Theory of Differentiation 6 2 3 MONOS 000 4 poe heat oA oe ey he Ob awe Be es 6 2 4 Some Theorems on Limits 6 2 5 Banach s Fixed Point Theorem 6 2 6 Basics of Group Theory 6 3 Logical Exercises e 6 3 1 Indicators A Representation of Sets 6 3 2 Temporal LogiC o 6 4 Exercises related to Computer Science 6 4 1 The World s Smallest Compiler 6 4 2 A Linea
81. TION THEORIES 12 THEORY INTERPRETATIONS 1 THEOREMS 277 MACETES 360 EXPRESSIONS 3428 1 THEOREM NAME ANONYMOUS forall a c uu forsome b uu b prec a and c prec b implies c prec a THEORY PARTIAL ORDER SEQUENT NODES 10 PROOF STEPS 3 GROUNDED YES CONTEXTS 4 ASSUMPTIONS CONTEXT 1 0 virtual time 0 16 seconds 126 219 THEOREM NAME LOCALITY OF INTEGRALS forall phi psi ii uu a b ii a lt b and integrable phi and integrable psi and forall x ii a lt x and x lt b implies phi x psi x implies forall x ii a lt x and x lt b implies integral a x phi integral a x psi THEORY MAPPINGS FROM AN INTERVAL TO A NORMED SPACE SEQUENT NODES 54 PROOF STEPS 33 GROUNDED YES CONTEXTS 29 ASSUMPTIONS CONTEXT 5 551724137931035 virtual time 25 05 seconds O errors during test O failed proofs during test FINAL THEORY NETWORK INFORMATION THEORIES 32 THEORY INTERPRETATIONS 110 THEOREMS 915 MACETES 1108 127 EXPRESSIONS 89274 Mon May 3 21 06 38 EDT 1993 IMPS test completed 12 4 The Script Language Informally a script is a sequence of proof commands and control statements Essentially the script facility in IMPS allows users to build programs to prove theorems Scripts are a useful way to package and reuse common patterns of reasoning The paper 8 presents some practical methods for exploiting the IMPS proof script mechanism A script is a kind of s
82. The IMPS User s Manual First Edition Version 2 William M Farmer Joshua D Guttman F Javier Thayer The MITRE Corporation Bedford MA 01730 USA 617 271 2907 farmer guttman jt mitre org 11 April 1995 Contents I 1 Introductory Material Introduction 1 1 Overview of the Manual 12 GOALS A A A DN AI tod aa 1 2 1 Support for the Axiomatic Method di 22 DOIG ra A ae ono iene 1 2 3 Computation and Proof 1 3 Components of the System 004 Tide OOP fest gt ded ea bt e Mele ees eee Aiea Se 2 Se ee eS 1 3 2 Supporting Machinery 133 User Interface o o 022000004 1 3 40 Theory Library or A ee Eee 1 4 Acknowledgments a Distribution 2 1 How to Get and Install IMPS 2 1 1 Howto Get IMPS 0 2 2 1 2 How to Install IMPS 2 1 3 Instructions for IMPS Users 2 1 4 How to Start IMPS 2 1 5 The IMPS User s Manual 21 06 IMPS Papers i ah Meee a ao 2 1 7 Bug Reports and Questions 2 2 IMPS Copyright Notice o a A Brief Tutorial 3 1 Interacting with IMPS 3 2 On line Documentation 0 0 0 0000004 12 14 14 14 15 15 16 17 17 18 18 19 19 21 21 21 22 23 24 24 24 25 26 3 3 Languages and Theories 02 200004
83. U Emacs 18 and Lucid GNU Emacs 19 If you will be using Free Software Foundation GNU Emacs 19 or Lucid GNU Emacs 19 put the line setq tea use comint t in your emacs file Let us refer to the location of the Emacs exe cutable as emacs Warning Depending on the version of Emacs you choose you may have to recompile the el files in the directory imps el 22 4 Execute cd imps src and edit the file start_imps sh to change the two lines IMPS lt imps path gt tea IMPS_EMACS lt emacs path gt to IMPS imps tea IMPS_EMACS emacs Finally execute make You may ignore the error messages that are printed 2 1 3 Instructions for IMPS Users In your cshre or wherever you define your shell search path add imps bin to your path You may find it convenient to set the shell variable IMPS in your cshrc using the command setenv IMPS imps tea If you want a form of Emacs different than emacs the official IMPS Emacs set the shell variable EMACS_COMMAND in your cshrc to the form of Emacs you want for example setenv EMACS _COMMAND emacs18 w 94x56 250 20 If you will be using Free Software Foundation GNU Emacs 19 or Lucid GNU Emacs 19 put the line setq tea use comint t 23 in your emacs file If IMPS is being run with Free Software Foundation GNU Emacs 19 the frame parameters position background and foreground colors etc of the various IMPS windows are
84. a deduction graph provides a snapshot of the current status of the proof A deduction graph is a directed graph with nodes of two kinds called sequent nodes 35 ae Figure 3 1 An Inference Node and inference nodes An interactive proof in IMPS is carried out by adding inference nodes and sequent nodes to the deduction graph A sequent node consists of the following e A theory e A single formula B called the sequent node assertion e A set of formulas A A called the sequent node assumptions Logically a sequent node just represents the formula Aj A A AnD B In the Sequent nodes 1 buffer a sequent node is represented as a list A1 An Sa Inference nodes are to be understood in part by their relationship to sequent nodes Every inference node has a unique conclusion node c and a possibly empty set of hypothesis nodes h1 h An inference node represents the following mathematical relationship between c and hy hn if every one of the sequent nodes hj h y is valid then the sequent node c is valid Alternatively we can view this as asserting that the validity of the sequent node c can be reduced to the validity of h1 hn An inference node also contains other information providing the mathematical justification for asserting the relationship between c and hj hn This justification is called an inference rule 36 Note that if the inference node has no hypotheses then c is obviously valid Whe
85. a proof of A in T using the IMPS proof system see Chapter 12 particularly Section 12 3 A theorem is available to the user when working in a theory 7 only if it has been installed in 7 There are several ways a theorem can be installed e When a theory is built all of its axioms are installed in it e One or two theorems are installed in a theory when a def theorem form is evaluated See Section 8 4 for details 88 e When an atomic sort is defined in a theory the new sort s defining axiom and a few special consequences of it are installed in the the ory Something similar takes place when constants are defined either directly or recursively in a theory e When a theorem A is transported from 7 to T via an interpretation the translation of A A is installed in T2 When a theorem is installed in a theory 7 it is automatically installed in every structural supertheory of T A theorem is installed with a list of usages that tells IMPS how to use the theorem There are seven usages they have the following effect when they are in the usage list of a theorem installed in a theory T 1 elementary macete This causes an elementary macete to be created from the theorem For a theorem which is given a name this usage is always added by IMPS to the theorem s usage list whether this usage is explicitly included by the user or not transportable macete This causes a transportable macete to be created from
86. acete named macete name when there is a macete argument Also let T be the theory named theory name and let H be the theory named by home theory name If there is no home theory argument then H is the source theory of Y if there is a translation ar gument and otherwise H T Finally let p be the formula specified by formula spec in H 197 Step 1 IMPS verifies that y is a theorem of H If proof spec is the symbol existing theorem IMPS checks to see that y is alpha equivalent to some existing theorem of H If the theorem is being installed in batch mode see Section 12 3 1 IMPS verifies that y is a theorem of H by running the script proof spec Otherwise IMPS simply checks that is a formula in H and it is assumed that the user has verified that y is a theorem of H Step 2 The theorem vy to be installed is generated from y as follows e If there is no translation or macete argument and T H then Pp p e If there is no translation or macete argument and T is a subtheory of H is a formula of T which is the result of generalizing the constants of H which are not in T assuming each sort of T is also a sort of H e If there is a translation argument but no macete argument then y is the translation of y by e If there is a macete argument but no translation argument then y is the result of applying M to y e If there is both a translation and macete argument then y is the result of applying M to
87. alled macetes Formally a macete is a function M which takes as arguments a context I and an expres sion e called the source expression and returns another expression M T e called the replacement expression In general the replacement expression does not have to be equal to the source expression Macetes serve two somewhat different purposes e They are a straightforward way to apply a theorem or a collection of theorems to a sequent in a deduction graph e They are also a mechanism for computing with theorems 14 1 Classification A macete can be atomic or compound Compound macetes are obtained by applying a macete constructor to a list of one or more macetes Atomic macetes are classified as In Portuguese a macete is an ingenious trick Macete is pronounced with a soft c Do not pronounce it as in Government supporters dropped confetti on the man waving the machete 142 Schematic macetes A schematic macete is one in which the replace ment expression is obtained from the source expression by matching and substitution Schematic macetes can be thought of as conditional rewrite rules Procedural macetes These are macetes which compute the replace ment expression by a more complicated procedure There are only a few such procedures simplify beta reduce beta reduce insistently Having these procedures as macetes allows you to build more powerful and useful compound macetes Macetes ca
88. alse in T then T I e is undefined Each theory has a table of transforms indexed on two keys 1 a constructor a quasi constructor or the atom nil and 2 a constant or the atom no defined constant The simplifier determines what transforms in the table to apply to an expression as follows e It first computes the expression s lead constructor This is the quasi constructor of the expression if it has one Otherwise it is the con structor of the expression which is the atom nil for variables and constants e It then computes the given expression s lead constant This is the first constant in a left to right traversal of the expression tree if there is one or no defined constant otherwise Thus the lead constant of Ar y R x y is e Finally it applies in a nondeterministic order the transforms in the table whose keys are the same as the expression s lead constructor and lead constant 13 3 Transforms The transforms used by the IMPS simplifier include 1 Algebraic simplification of polynomial expressions 2 A decision procedure for linear inequalities based on the variable elim ination method used in many other theorem provers 3 Rewrite rules for the current theory T or for certain theories Jo for which IMPS can find interpretations from J into T The framework for applying rewrite rules is entirely general and uses pattern matching and substitution in a familiar way By contrast the trans f
89. and a left method Examples def parse syntax left method infix operator method binding 100 def parse syntax factorial token left method postfix operator method binding 160 213 def print syntax Positional Arguments e constant name This is a symbol Modifier Arguments e tex If this argument is present then the syntax is added to the global TREX print table Keyword Arguments e token spec spec is a symbol a string or a list of such If this argument is omitted by default it is constant name e method proc name proc name is the name of a procedure for print ing of the token e table table name table name is the name of the parse table being changed If this argument is omitted and the tex modifier argument is not given the default value is the global print table form e binding N Required N is the binding or precedence of the token Description This form allows you to set or reset the print syntax of a constant In particular you can change the precedence parsing method and token rep resentation of a constant Examples def print syntax method present binary infix operator binding 100 def print syntax factorial token method present postfix operator binding 160 214 17 3 Loading Sections and Files load section Positional Arguments e section name Modifier Arguments e reload Causes the section to be reloaded if the sec
90. ant to facilitate various kinds of lower level reasoning such as algebraic or order simplification In a different sense theory is also commonly used to refer to a collection of related facts about a given mathematical structure such as the theory of rings or the theory of ordinary differential equations Theory ensemble A data structure which bundles together theories which are unions of copies of a single base theory Theory ensembles are mainly used to treat multiple instances of structures such as triples of met ric spaces or pairs of vector spaces Theory interpretation A translation that maps theorems to theorems Translation An IMPS data structure created with the def form named def translation that is used to translate expressions from one theory to another Transportable macete A theorem macete that can be used in a theory different from the one in which it was installed Transportable macetes are named by the system by prefixing tr to the name of the theorem Type A sort that is maximal with respect to the subsort relation Variable A kind of IMPS expression An occurrence of a variable v within an expression is bound if it occurs with the body of a binding constructor which includes v as a binding variable Otherwise the occurrence of v is free 297 Xview An IMPS procedure for printing expressions in T X and then displaying them in an X window TFX previewer 298 Bibliography H Abelson and G
91. arget theories keyword is given constants const assoc const ass0Cp const assoc is a list const expry exprn where const is a constant in the base theory of the ensemble and expr is either A constant in the theory T or A string representing an expression in 74 In particular the length of each const assoc entry must be one more than the number N of theory entries This argument is valid only in case the target theories keyword is given multiples M Mn Each argument Mis an integer not exceed ing the number N of theory entries This instructs IMPS to translate constants defined in the ensemble M multiple permutations P P Each argument P is a list p1 p of integers in 0 N 1 The presence of this list instructs IMPS to translate constants defined in the ensemble multiple into the theory generated by the theories Tamah special renamings renaming renaming A list of entries name new name if you want to override the system s naming con ventions Note that name is the full constant name not just the root name 203 Description This form is used to build translations from selected theory multiples and to transport natively defined constants and sorts from these multiples To describe the effects of evaluating this form we consider a number of cases and subcases determined by the presence of certain keyword arguments e target theories nameg name
92. cases where the goal sequent does not exactly match the induction principle Remarks In a formal sense induction refers to an axiom or theorem in a particular theory for example the formula of weak induction below and in this sense applying induction means applying this formula to a sequent However induction alone rarely gets the job done Other tricks such as algebraic simplification beta reduction and unfolding of definitions especially recursive ones are usually needed In this broader sense induction can be thought of as a proof technique incorporating a large number of fairly standard inferences Despite its simplicity induction is one of the most powerful proof tech niques in mathematics especially in proofs for formulas involving the inte gers Moreover forms of induction are also used in theories of syntax or theories of lists An induction principle in one of these theories is usually referred to as structural induction The induction principle for the inductor integer inductor is the for mula Vs z m z Vt z m lt t D s t s m AVt z m lt t D s t gt s t 1 This formula is usually referred to as the principle of weak induction You might also be familiar with the principle of strong induction in fact both in duction principles are equivalent However some formulas cannot be proved directly with the principle of weak induction because the induction hypothe sis is not sufficient
93. ce the theories created with the def bnf are always model conservative extensions of the starting theory IMPS supports a general technique based on theory interpretation and theory instantiation for building safe theory extension methods The idea is that a model conservative extension type can be formalized as an abstract theory with a distinguished subtheory The theory can be shown to be a model conservative extension of the subtheory using Theorem 9 5 1 Model Conservative Verification Theorem Let Ta be an extension of T Ta is a model conservative extension of Ta if there is an interpretation of Ta in T which fixes T Then instances of the model conservative extension type are obtained by instantiating the theory Each such instance is guaranteed to be a model conservative extension by Theorem 9 5 2 Model Conservative Instantiation Theorem Let T be a model conservative extension of T and let T be an instance of T under the an interpretation of T in Tz Then T is a model conservative extension of Ta For a detailed description of this technique see 6 9 5 9 Theory Ensembles A theory ensemble consists of a base theory copies of the base theory called replicas and unions of copies of the base theory called theory multiples The constituents of a theory ensemble are related to each other by theory interpretations They allow you to make a definition or prove a theorem in just one place and then transport
94. cete must be entered into its usage list when the theorem is entered 14 2 2 Nondirectional Macetes Frequently it is useful to construct a schematic macete from an arbitrary formula by using a matching and substitution procedure which does not obey 145 the variable capturing protections and other restrictions of normal matching We refer to this as nullary matching and substitution For instance to apply a theorem which involves quantification over functions one often has to build a lambda abstraction of a sub expression We shall see later on how this can be done 14 3 Compound Macetes Compound macetes are built from atomic macetes and other compound macetes using macete constructors The constructors are e Series This constructor takes a list M M of macetes as ar guments and yields a macete Series M1 Mn which applies every macete in the list once from left to right Thus given a context I and an expression e Series M1 Mn T Mn T Mn_ 1 T M1 T e e Sequential This constructor takes any number of macetes as argu ments It works like the series constructor except that when a macete fails to change an expression subsequent macetes on the list are not applied e Parallel This constructor takes a list M1 Mn of macetes as argu ments and yields a macete Parallel M1 Mn which applies macetes in the list from left to right until a macete changes the expression Thus giv
95. ction graph permits the user to vi sually determine the set of unproven subgoals and to select a suitable continuation point for the proof The TX typesetting facilities allow the user to examine the proof in a mathematically more appealing no tation than is possible by raw textual presentation alone And with proof scripts the user can replay the proof in whole or in part The presentation of options for new proof steps For any particular subgoal the interface presents the user with a well pruned list of com mands and macetes to apply This list is obtained by using syntactic and semantic information which is made available to the interface by the IMPS supporting machinery For example in situations where over 400 theorems are available to the user there are rarely more than ten macetes presented to the user as options e The processing of user commands The commands are then submitted to the inference software while any additional arguments required to execute the command are requested from the user 1 3 4 Theory Library IMPS is equipped with a library of basic theories which can be augmented as desired by the user The theory of the reals the central theory in the library specifies the real numbers as a complete ordered field The completeness principle is formalized as a second order axiom and the rationals and inte gers are specified as the usual substructures of the reals The library also contains various generic the
96. d kind Single inference 256 Condition Procedure Action do simplify simplify lower do simplify 0 lt persist backchain through formula lower persist raise do simplify antecedent inference for existentials and conjunctions direct inference antecedent inference for other assumptions raise do simplify 0 lt persist backchain inference sort definedness definedness extensionality raise do simplify conditional inference followed raise do simplify by direct inference Notes 1 The variable persist is the backchaining persistence supplied as an argument to the command lower persist means reduce backchaining persistence by 1 2 do simplify is a boolean flag which starts off as true when the com mand is called Table 18 1 Search Order for prove by logic and simplification 257 Description This command will raise a subset of the conditional ex pressions i e expressions whose lead constructor is if specified by l in the assertion of the given sequent T gt y For the moment let us assume that n 1 Suppose the th occurrence of a conditional expression in is the a th occurrence of s if 0 t1 t2 in p the smallest formula containing the a th occurrence of s in y is the b th occurrence of 4 in y and the a th occurrence of s in y is the c th occurrence of s in w If every free occurrence of a variable in s is also a free occurrence in 4
97. d to provide you with a starting point for building your own theory library It also is a source of examples that illustrates some of the diverse ways mathematics can be formulated in IMPS This chapter contains only a sampling of the sections that are contained in the IMPS initial theory library with a partial description of each section Some of the descriptions contain a listing of the theories and some of the more important theorems and definitions included in that section Each section description begins with the symbol followed by the section name Each theory description begins with the symbol 4 followed by the theory name abstract calculus The main theory of this section is normed spaces The section develops the basic notions of calculus e g the derivative and the integral in the context of normed spaces 282 8 banach fixed point theorem This section has a proof of the Banach contractive mapping fixed point theorem which states that any contractive mapping on a complete metric space has a unique fixed point 8 basic cardinality This section introduces the basic notions of cardinality It also proves some basic theorems about finite cardinality such as the fact that every subset of a finite set is itself finite 8 basic fields The main theory of this section is fields The section develops the ma chinery of field theory sufficiently for installing an algebraic processor for simplification 8 basic group the
98. dams OR BIT An optimizing compiler for scheme In Proceedings of the SIGPLAN 86 Symposium on Compiler Construction volume 21 pages 219 233 1986 Proceedings of the 86 Symposium on Compiler Construction J D Monk Mathematical Logic Springer Verlag 1976 300 20 21 22 23 24 25 26 L G Monk Inference rules using local contexts Journal of Automated Reasoning 4 445 462 1988 Y N Moschovakis Elementary Induction on Abstract Structures North Holland 1974 Y N Moschovakis Abstract recursion as a foundation for the theory of algorithms In Computation and Proof Theory Lecture Notes in Mathematics 1104 pages 289 364 Springer Verlag 1984 J A Rees N I Adams and J R Meehan The T Manual Computer Science Department Yale University fifth edition 1988 J R Shoenfield Mathematical Logic Addison Wesley 1967 R M Stallman GNU Emacs Manual Version 18 Free Software Foundation sixth edition edition 1987 F J Thayer Obligated term replacements Technical Report MTR 10301 The MITRE Corporation 1987 301
99. dence are given by something called a proof system In this section we will describe the IMPS proof system To begin an interactive proof in IMPS select the start dg option in the Deduction Graphs pane of the menu For version 19 click on the menubar on DG and then select Start dg IMPS will then prompt you in the minibuffer with the text Formula or reference number This is an IMPS request for some formula to prove You can supply this formula by typing its reference number in the minibuffer Alternatively you can click the right mouse button on the formula provided that it is enclosed between double quotes and then press lt RET gt You are then ready to begin proving the formula After telling Emacs to start the deduction two new buffers will be cre ated One buffer labelled Deduction graph 1 displays a graphical rep resentation of a data structure called a deduction graph The other Emacs buffer labeled Sequent nodes 1 displays a textual representation of a data structure called a sequent node Notice that the mode line for the sequent node buffer also contains the text h o real arithmetic Sqn 1 of 1 This gives you the following information 1 h o real arithmetic is the theory in which the proof is being carried out 2 You are currently looking at the first sequent node of the deduction graph 3 There is only one sequent node in the deduction graph To understand the significance of the new buffer note that
100. description This will cause IMPS to compute all the macetes that can in fact alter the current goal In the case at hand there are 11 macetes that are potentially applicable to our goal out of 362 currently loaded A description of each applicable macete is sent to TEX and will be available after 10 15 seconds on the xdvi window When you have inspected the possibilities and have noted the number of left denominator removal on the list return to the Emacs window Type the number followed by a carriage return to cause IMPS to apply that macete Result You will now see a new subgoal on the Emacs display It is the result of the rewriting carried out by the selected macete The letters p and n will carry you to the previous display and then back to the next one To inspect both sequents using TEX pull down the TeX menu and select the Xview sqns item Emacs will prompt you at the bottom of the screen for the numbers Enter 1 and 2 separated by a space and terminated by a carriage return After 10 15 seconds you will be able to compare the two formulas on the xdvi screen Please also observe in the xdg window that Sequent 1 has been reduced to Sequent 2 by the inference left denominator removal for equalities If one later carries out inferences that complete the proof of Sequent 2 then they will also suffice to establish or ground Sequent 1 made available to the user for various kinds of rewriting depending
101. e Chapter 11 for details Task 9 Theory Extensions Ordinarily an extension of the theory is created with def theory and def theory instance but the theory can also be extended by adding an ab stract data type with def bnf or a record with def record theory Task 10 Quasi constructors Quasi constructors are global constants that can be used across a large class of theories They are created with def quasi constructor See Chapter 10 for details 87 Task 11 Renamers Renaming functions are used with def theory instance and def transported symbols to rename atomic sorts and constants They are created with def renamer Task 12 Syntax Special parse and print syntax for the vocabulary of the theory is created independently from the development of the theory with def parse syntax def print syntax and def overloading See Chapter 16 for details Task 13 Sections Theory library sections containing the theory or a part of the theory are created with def section See Section 8 6 for more information about sec tions 8 3 Languages An IMPS language is a representation of a LUTINS language An IMPS lan guage is built with def language from a possibly empty set of languages a set of base types and a list of atomic sort declarations 8 4 Theorems Mathematically a theorem of a theory is any logical consequence of the theory s axioms One usually verifies that a formula A is a theorem of a theory 7 by constructing
102. e is subject to compliance with United States export control and munitions control restrictions You agree that in the event you seek to export this software or any derivative work thereof you assume full responsibility for obtaining all necessary export licenses and approvals and for assuring compliance with applicable reexport restrictions 26 Chapter 3 A Brief Tutorial In this tutorial we will assume that you have the X Window System running on your workstation If your workstation can run X but it is not installed enlist the aid of a system guru to get him or her to set things up for you Although it is possible to run IMPS from a dumb terminal for example to work from home where mere mortals only have terminal emulators you will miss the functionality that X provides such as fancy TFX previewing of formulas and proofs and interaction with IMPS using the mouse and the menu facility We will also assume that you have the shell variable IMPS correctly set To start IMPS enter this command at the shell prompt IMPS bin start_imps Executing this command will do the following e Start an Emacs session e Start IMPS which is actually a Tea process subordinate to Emacs e Make two new directories in your home directory HOME imps and HOME imps theories needed for the IMPS exercises e Add some files to your tmp directory e Start one or more iconified T X preview windows 27 To quit IMPS type C x C c This w
103. e 6 1 The properties and their consequences are then grouped together into a macete that allows expres sions involving derivatives to be evaluated Purpose This exercise is intended to illustrate in addition to inductive reasoning the manipulation of higher order objects functions represented using A and the power of macetes to encode symbolic computations for everyn Z f R R x R implication e D f z A2 lt n e DA x R f x x n f a D F 2 Figure 6 1 Generalized Power Rule 63 for every f Z U m n Z implication e conjunction om lt n oVj Z m lt jAajen D gt fii l e TIm 9 f minus f n 1 f m Figure 6 2 Telescoping Product Formula 6 2 3 Monoids Contents This exercises introduces a theory of monoids a monoid being a domain U equipped with an associative operator and an identity element e A recursive definition introduces an iterated monoid product operator such that when i j Z and f Z U then i j f satisfies o T f e when j lt i e T f Ef G when i lt j By adding an inverse operator and axioms on it the monoid theory is extended to a theory of groups defined independently of the theory in Exercise 6 2 6 The file then defines slightly incongruously minus to mean Axy U x y and to mean AZ U A j Z minus f j 1 5 That is if f is a function of sort Z U then f is another function of the same sort
104. e argument retrieval None Command kind Multi inference Description This command replaces every occurrence of a defined con stant by its respective unfolding repeatedly until there are no occurrences of defined constants The command beta reduce repeatedly is called after all the unfoldings are performed Related commands unfold defined constants unfold directly defined constants repeatedly unfold recursively defined constants repeatedly unfold single defined constant Remarks If there are occurrences of recursively defined constants this command can run forever unfold directly defined constants Script usage unfold directly defined constants Interactive argument retrieval None Command kind Multi inference Description This command replaces every occurrence of a directly de fined constant by its respective unfolding A directly defined constant is a constant defined nonrecursively The command beta reduce repeatedly is called after all the unfoldings are performed Related commands unfold defined constants unfold directly defined constants repeatedly unfold recursively defined constants unfold single defined constant 263 unfold directly defined constants repeatedly Script usage unfold directly defined constants repeatedly Interactive argument retrieval None Command kind Multi inference Description This command replaces every occurrence of a directly de fined constant by its respective unfolding
105. e deduction graph s theory Command kind Single inference Description This command transports the argument theorem to the de duction graph s theory via the argument theory interpretation Then the transported theorem is added to the context of the given sequent using assume theorem Related commands apply macete assume theorem instantiate transported theorem Remarks To apply a theorem to a sequent from outside the deduction graph s theory you will usually want to use apply macete or instantiate transported theorem instead of assume transported theorem auto instantiate existential Script usage auto instantiate existential Interactive argument retrieval None Command Kind Multi inference Description This command tries to instantiate an existential assertion with terms from the context of the given sequent 227 Related commands auto instantiate universal antecedent instantiate existential auto instantiate universal antecedent Script usage auto instantiate universal antecedent assumption assumption can be given as an integer or a string o Interactive argument retrieval e O based index of universal antecedent formula ii da in i The 1 12 1n are the indices of the universal assumptions of the sequent node In case there is only one universal antecedent formula this argument request is omitted Command Kind Multi inference Description This command tries to instantiate the i
106. e defined constant will be added This may be an extension of the theory of the BNF with respect to which the recursion is performed e range sort range sort form Required This specifies the range of the function or predicator being introduced since the domain will be the base sort of the BNF this fixes the sort of the constant e atom name value Required one for each BNF atom This specifies one base case of the recursive definition 188 e constructor name var names operator body Required one for each BNF constructor This specifies one recursive step of the recursive definition The operator body specifies how the results of the recursive subcalls should be combined possibly with parameters not belonging to the datatype to produce the value of the recursive operator for an argument of this form Description Each BNF is automatically equipped with a principle of definition by struc tural primitive recursion A def primitive recursive constant form in stantiates this principle by stipulating the intended range sort the values for atoms of the BNF data type and how the recursively defined operator combines its results on the arguments of each datatype constructor Examples See for instance the compiler exercise file def quasi constructor Positional Arguments e name The name of the quasi constructor e lambda expr string Keyword Arguments e language language name Required language name may al
107. e following forms 1 ara ple 2 z a p a 3 ara p x E 4 ara p x AE 5 E vara ple 6 EF vara p x 7 vara p w E 8 E vara ple For forms 1 6 the macete can be applied immediately but for forms 7 and 8 the command insistent direct inference must be applied first Beware that for various reasons eliminate iota macete may fail to do anything in which case you should use one of the two iota elimination com mands 15 3 Hints and Cautions 1 Suppose F is an expression of sort a Sometimes it is convenient to have a new expression E of sort 8 where 7 8 T a but PB 4 a such that E and E have the same denotation Such an expression can be easily constructed from E and 8 using iota 12 8 1 E is quasi equal to E and is of sort 6 For example 2 N x 2 denotes the natural number 2 It is important to mention here that the IMPS simplifier reduces an iota expression of the form 1 B x E to the conditional if E 8 E Lg and further to E or Lg if it can decide the formula E 6 2 Suppose f is a function constant defined to be 153 such that the following existence implies uniqueness theorem holds for y A dy 8 p z y gt Aly 8 x y By virtue of this theorem there is an iota free characterization of Vag Vara y 3 f x y plz y which enables one to prove a formula f a b by showing only existence without
108. e given sequent universal instantiation Parameters A sequent node gt V21 01 2n 0n P 280 Description This primitive inference procedure proves a formula by proving a universal Conclusion gt p Premise T gt V21 01 Tn 0n P Notes e The command will fail unless the parameter sequent node is of the form I gt V21 01 Tn 0n P unordered conjunction direct inference Parameters None Description If the sequent node assertion is a conjunction this primi tive inference procedure does a direct inference without strengthening the context Conclusion TS gid AQn Premises 1 lt i lt n T gt yi weakening Parameters A set of formulas A Description This primitive inference procedure removes one or more as sumptions you specify from the context of the given sequent Conclusion TU A gt p Premise r y 281 Chapter 20 The Initial Theory Library An Overview A theory library is a collection of theories theory interpretations and theory constituents e g definitions and theorems which serves as a database of mathematics The basic unit of a theory library is a section each section is a body of mathematics Each section consists of a sequence of def form specifications which are stored in a set of text files The IMPS initial theory library contains a large variety of basic mathe matics It is intende
109. e new assumption is a consequence of the context Conclusion T gt 06 Major Premise TU 4 gt y Minor Premise T gt w Related commands cut using sequent Remarks To cut with several formulas at the same time use cut using sequent Key binding amp definedness Script usage definedness Interactive argument retrieval None Command kind Single inference Description This command applies to a sequent whose assertion is a definedness statement of the form t The command first tests whether the context entails the definedness of t If the test fails the command then tries to reduce the sequent to a set of simpler sequents Related commands sort definedness Remarks This command is mainly useful when t is an application or a conditional direct and antecedent inference strategy Script usage direct and antecedent inference strategy 238 Interactive argument retrieval None Command kind Multi inference Description This command repeatedly applies 1 direct inference to the given sequent and resulting sequents and 2 antecedent inference to newly created antecedents of the given sequent and resulting sequents until no more such direct and antecedent inferences are possible Related commands antecedent inference strategy direct and antecedent inference strategy with simplification direct inference strategy Key binding D direct and antecedent inference strategy with
110. e of a quasi constructor in the expression Command kind Null inference Description This command enables the quasi constructor given as argu ment extensionality Script usage extensionality Interactive argument retrieval None Command kind Single inference 244 Description If the sequent node assertion is an equality or quasi equality or the negation of an equality or quasi equality of n ary functions this com mand applies the extensionality principle Conclusion T gt f g Major Premise T gt V21 01 n 0n F 1 En X 9 21 Tp Minor Premise T gt f Minor Premise T gt gl Conclusion Tsferg Major Premise T gt V21 01 Lp 0n 1 En X 9 21 Tp Minor Premise TU gl gt f Minor Premise TU f gt gl Conclusion T gt f Y Premise I gt J 1 01 En On A E Conclusion Faaf ag Premise I gt J 1 01 One int En E En Notes e If the sorts of f and g are a1 Qn n 1 and 61 Bn Bn 1l respectively then o a U 6 for all with 1 lt i lt n e A sequent node corresponding to a minor premise is not created if the truth of the minor premise is immediately apparent to IMPS e If f and g are of kind x then is used in place of in the premise Remarks By substitution of quasi equals for quasi equals both f g and f g imply Vz1 01 ey san On
111. e real numbers Exponentiation to an integer power is a defined constant denoting a partial function Language e Sorts zz Z in the mathematical syntax denotes the set of integers qq Q in the mathematical syntax denotes the set of rational numbers rr R in the mathematical syntax denotes the set of real num bers e Constants denotes real addition 288 in the mathematical syntax denoted by juxtaposition of its arguments denotes rel multiplication denotes sign negation denotes division lt denotes the binary predicate less than There are also an infinite number of constants one for each rational number Thus 8 9 21 4 denote rational numbers Axioms The following is the list of all the axioms of the IMPs theory complete ordered field in the mathematical syntax 1 Trichotomy Wy 1 R x lt yVxr yVy lt zu 2 Irreflexivity 0 0 3 Strict Positivity for Products VWy x R 0 lt xA0 lt yD0 lt zy 4 lt Invariance Vz y T R 1 lt Yy t 2 lt YyH 2 5 Transitivity Vz y o R z lt yAy lt zD U lt z 6 Negative Characterization Va R x x 0 7 Characterization of 0 Va R x 0 2 8 Associative Law for Multiplication Vz y a R xy z x yz 9 Left Distributive Law Vz y a R x y z ty zz Multiplicative Identity Vx R 1 zx Commutative Law for Multiplication Vy x R xy yz Associative Law for Addition Vz y R 1 y 2 x y 2 Comm
112. e variables Table 3 3 String Syntax for Constructors 33 si U s2 is the smallest sort which syntactically includes s1 and s2 For equality and if then else term t1 t2 must be of the same type rn rl With is not a constructor it is merely a device to specify the sorts of Term Category Syntax Sort Sum tit tn rr Product tix tn rr Sign negation t rr Subtraction ti t2 rr Exponentiation t17t2 rr Division t1 t2 rr Sequential sum sum t1 t2 t3 rr Sequential product prod t1 t2 t3 rr Factorial t rr Less than t1 lt t2 prop Less than or equals ti lt t2 prop Greater than t1 gt t2 prop Greater than or equals t1 gt t2 prop Notes 1 The terms t1 tn must be of type ind Do not confuse this syn tactic requirement for well formedness with semantic conditions for well definedness 2 For sequential sum and product the term t3 must be of type ind ind 3 All operators associate on the left except exponentiation which asso ciates on the right Table 3 4 Syntax for h o real arithmetic 34 3 5 Proofs A formula in a theory is valid if it is true in every legitimate model of the theory if the formula has free variables we have to add with every legitimate assignment of values to its free variables To prove a formula means to offer conclusive mathematical evidence of its validity The rules for admissible evi
113. ecedent inferences Cii i2 im J1 j2 Jn The 11 19 1n are the indices of the assumptions of sequent node on which antecedent inferences can be done that is an implication conjunction disjunction biconditional conditional formula or an existential formula In case there is only one such formula this argument request is omitted Command kind Multi inference Description Call an assumption of the goal sequent node fixed if its index is not among j1 jn This command repeatedly applies the antecedent inference command to the goal node and resulting subgoal nodes until the only possible antecedent inferences are on fixed assumptions 222 Related commands antecedent inference direct and antecedent inference strategy Remarks This command is called as a subroutine by a number of other commands including instantiate theorem and instantiate universal antecedent Key binding A apply macete Script usage apply macete macete Interactive argument retrieval e Macete name The name of a macete Formally a macete is a function which takes as arguments a context and an expression and returns an expression Macetes are used to apply a theorem or a collection of theorems to a sequent in a deduction graph In order to use them effectively read the section on macetes in the manual Command kind Single inference Description This command applies the argument macete to the given sequent node Related comma
114. ecessary renaming bound variables in y to avoid variable captures Related commands auto instantiate universal antecedent instantiate universal antecedent multiply instantiate universal antecedent multiply Script usage instantiate universal antecedent multiply assump tion lists of instantiations assumption can be given as an integer i or a string o and lists of instantiations is a list of lists of strings which specify the expressions that instantiate the universally quantified assumption 254 Interactive argument retrieval e O based index of antecedent formula i If there is only one as sumption this argument request is omitted e First instance term t e Next instance term lt RET gt if done to e Next instance term lt RET gt if done tn n gt 1 e Input terms for another instance y or n Command kind Multi inference Description This command produces one or more instances of the i th assumption of the context of the given sequent provided the assumption is a universal statement in the same way that instantiate universal antecedent produces one instance of the assumption Related commands auto instantiate universal antecedent instantiate universal antecedent prove by logic and simplification Script usage prove by logic and simplification persistence Interactive argument retrieval e Backchaining persistence An integer which is 3 by default Command kind Multi inference
115. ection onto the i th coordinate o qj Examples def cartesian product complex rr rr constructor make complex accessors real imaginary theory h o real arithmetic 179 def compound macete Positional Arguments e name e spec A compound macete specification is defined recursively as either A symbol macete name A list of the form series spec spec repeat spec spec sequential spec spec sound spec Spec specs x parallel spec spec without minor premises spec where spec is itself a macete specification Keyword Arguments None Description This form adds a compound macete with the given name and components See the section on macetes for the semantics of macetes Examples def compound macete FRACTIONAL EXPRESSION MANIPULATION repeat beta reduce addition of fractions multiplication of fractions multiplication of fractions left multiplication of fractions right equality of fractions left denominator removal for equalities right denominator removal for equalities strict inequality of fractions 180 right denominator removal for strict inequalities left denominator removal for strict inequalities inequality of fractions right denominator removal for inequalities left denominator removal for inequalities def compound macete ELIMINATE IOTA MACETE sequential sound trhabstraction for iota body beta reduce beta reduce
116. ectively and that every member of F is a subtheory of T The theory named name is an extension U of T built as follows First the primitive vocabulary of T which is outside of To and F is added to the language of Ty the vocabulary is renamed using the value of renamer Next the translations of the axioms of T which are outside of Ty and F are added to the axioms of TY the axioms are renamed using the value of renamer U is union of the resulting theory and the members of F The translation from T to U extending is created with name new trans name Examples def theory instance METRIC SPACES COPY source metric spaces target the kernel theory 206 translation the kernel translation fixed theories h o real arithmetic def theory instance VECTOR SPACES OVER RR source vector spaces target h o real arithmetic translation fields to rr renamer vs renamer def theory processors Positional Arguments e theory name Keyword Arguments e algebraic simplifier spec spec Each entry spec is a list processor name Op Opn where processor name is the name of an algebraic processor and OP OPn are constant names denoting functions We will say that the operators op are within the scope of the specified processor e algebraic order simplifier spec spec Each spec is a list processor name pred pred where processor name is the name of an order processor and
117. eger referring to the sequent node with that number or as a list context string assertion string Interactive argument retrieval e Major premise number The number of a sequent node Command kind Single inference Description This command generalizes the assertion of the given se quent The node containing the major premise sequent must exist before the command can be called Usually you create this sequent node with edit and post sequent node Conclusion T gt 06 Major Premise PST Das e Minor Premises 1 lt i lt n T gt t 0 Notes e is the result of simultaneously replacing each free occurrence of zx in y with t for all with 1 lt i lt n e t is free for x in y for each with 1 lt i lt n incorporate antecedent Script usage incorporate antecedent assumption assumption can be given as an integer i or a string o Interactive argument retrieval e O based index of antecedent formula i If there is only one as sumption this argument request is omitted 247 Command kind Single inference Description This commands does the reverse of direct inference on an implication Conclusion TU y gt y Premise T gt pDY Notes e The index of y in the context PU vp is 7 Related commands direct inference Remarks This command is used for incorporating an assumption of a sequent s context into the sequent s assertion I
118. em In purpose of this chapter is to explain e The IMPS proof system e A description of how you prove theorems in IMPS in interactive mode and in script mode e A description of the proof script language 12 1 Proofs A proof of a statement y is conclusive mathematical evidence of why y is true A proof is usually thought of as a sequence of formulas p1 Pp such that Yn Y and every y is either 1 An axiom that is a formula which is assumed true to begin with 2 A theorem that is a formula whose truth has already been established by some other proof or 3 A consequence of one or more previous formulas in the sequence This means that p is related to these formulas by a relation called an inference The criterion for determining what constitutes an acceptable inference de pends on the purpose of the proof If the proof is for mechanical verification only whether by a digital computer or a human being acting like one then the criteria of acceptability can be specified unambiguously as a set of rules 123 for determining which sequences of symbols constitute proofs This set of rules is called a proof system For a human audience on the other hand it is usually a good idea to stress the essential or innovative steps in a proof and avoid routine computations Moreover for an expository article a textbook or a classroom lecture it is acceptable even desirable that inference steps appeal to intuition 1
119. en a context and an expression e Parallel M1 Mn T e M T e provided M T e e and M T e e for all 1 lt j lt i e Repeat Takes any number of macetes M1 Mn as arguments and yields a macete in the following way The series composition M of M Mn is applied repeatedly to the expression e until no more change occurs It may possibly compute forever Thus the macete terminates if MT M T M T e stabilizes to some expression t This expression is the value of Repeat M Mn T e 146 e Sound This constructor takes a list M Ma M3 of three macetes and yields a macete characterized as follows Given a context and an expression e Sound M Ma M3 T e is Mi T e if M3 T M T e is alpha equivalent to Ma T e e otherwise e Without minor premises This constructor takes a single argument macete M It returns a new macete which applies M without minor premises That is macete substitution is only done when the macete requirements are satisfied Now whether the resulting macete is bidirectional or backward directional can be determined by considering the bidirectionality or backward directionality each of the components e Series sequential parallel repeat and without minor premises macete constructors If all the M are bidirectional macetes then the com pound macete Constructor M Mn T e is bidirectional Similarly if all the argumen
120. ents This exercise introduces two syntaxes as abstract data types Each syntax is given a semantics as a simple programming language A function defined by primitive recursion on one language the source lan guage maps its expressions to values in the other the target language This function is the compiler We prove that the semantics of its output code matches the semantics of its input Purpose The primary purpose of this exercise is to illustrate the BNF mechanism for introducing a recursive abstract data type Connected with a BNF is a schema for recursion on the data type This is a form of primitive recursion as distinguished from IMPS s more general facility for monotone inductive definitions The primitive recursion schema is preferable when it applies because it automatically creates rewrite rules for the separate syntactic cases A secondary purpose is to illustrate in a very simple case an approach to compiler verification 6 4 2 A Linearization Algorithm for a Compiler Contents A linearizer is a compiler component responsible for trans forming a tree like intermediate code into a linear structure Its purpose is typically to transform potentially nested conditional statements into the representation using branch and conditional branch instructions that take numerical arguments The exercise is contained in the file flatten t 69 It also depends on the BNF and primitive recursion mechanisms How ever the p
121. ere is a sort a occurring earlier in the ordering and a is declared to be included within a or 3 There is at least one constructor c declared with range sort a and every domain sort of c is either some 3 belonging to the underlying theory or some a occurring earlier in the ordering that a When this condition is not met the implementation raises an error and identifies the uninhabited sort or sorts for the user 174 Axioms Generated The BNF mechanism generates six categories of ax ioms Constructor definedness A constructor is well defined for ev ery selection of arguments of the syntactically declared sorts Disjointness If a and b are atoms and co and c are construc tors then a b a ran co and ran co is disjoint from ran c1 Selector constructor If s is the ith selector for the construc tor c then s c xi Moreover if s y then y c Z for some 2 Sort Inclusions Vx ap x a1 when ay is specified as included within ay Induction The type 7 is the smallest containing the atoms and closed under the constructor functions in the sense given above No Junk Case Analysis If x a where a is the new type or one of its subsorts then one of the following holds 1 x is one of the atoms declared with sort a 2 x is in the range of some constructor declared with range a 3 x a where either a is the enclosing sort of a or else the inclusion of a within a is decla
122. escription This form finds the smallest sublanguage of the language L named super language name which contains the sublanguages of L named language name language name the atomic sorts of L named sort namej sort namen and the constants of L named constant name constant namen Each of superlanguage name language name language name may be the name of a theory instead of a language Examples def sublanguage REAL VECTOR LANGUAGE superlanguage vector spaces over rr language languages h o real arithmetic sorts uu constants vO 196 def theorem Positional Arguments e name The name of the theorem which may be e formula spec A string representing the formula using the current syn tax or the name of a theorem Modifier Arguments eo reverse e lemma Not loaded when quick loading Keyword Arguments e theory theory name Required The name of the theory in which to install the theorem e usages symbol symbol e translation translation name The name of a theory interpreta tion e macete macete name The name of a bidirectional macete e home theory home theory name The name of the home theory of the formula specified by formula spec e proof proof spec Description This form installs a theorem in three steps Let be the theory inter pretation named translation name when there is a translation argument and let M be the bidirectional m
123. expression that is a symbol a string an integer or a nested list of such objects To describe how IMPS interprets scripts to modify the state of the deduction graph we first establish some terminology to designate certain classes of script components Each script component is itself an s expression e A script form expression expression for short is a string a symbol a number or a list of expressions e An expression operator is one of the symbols e A script variable is a symbol beginning with e A keyword form is a list whose first element is one of the follow ing symbols which we refer to as keywords move to sibling move to ancestor move to descendent block if for nodes while let script let macete let val script comment label node jump to node skip e A command form is an expression which is either a command name or a list whose first element is a command name e A script is a list of script form expressions In Figure 12 1 we provide an example of a script This script can be used to prove the combinatorial identity discussed in Chapter 5 on the IMPS micro exercises The script consists of a number of forms each of which is applied to a unique node of the deduction graph called the current node 128 unfold single defined constant globally comb apply macete with minor premises fractional expression manipulation label node compound direct and antecedent inference strategy jump to
124. exts contain various kinds of cached information for example about definedness of terms used by the IMPS simplification machinery Core All the basic logical and deductive machinery of IMPs on which the soundness of the system depends Deduction graph An IMPS data structure representing a proof Deduc tion graphs contain two kinds of nodes inference nodes and sequent nodes Def form An s expression whose evaluation has some effect on the IMPS environment such as building a theory adding a theorem to a theory mak ing a definition in a theory or building a translation between theories There are about 30 such def forms Emacs A text editor Although various implementations of Emacs exist in this manual we mean exclusively GNU Emacs which is the extensible display editor developed by the Free Software Foundation Because of the many extension facilities it provides including a programming language with many string processing functions GNU Emacs is well suited for developing interfaces Expression An IMPS data structure representing an element of a language Expressions are used to describe mathematical entities or to make logical 293 assertions Two examples printed in TX are 2 1 and 1 m m m lt lt E Vk m 21 kn tm gt k a An expression is either a formal symbol or a compound expression Evaluate To cause an s expression to be read by the T process thereby creating an internal representation of a
125. f System developed at The MITRE Corporation by W Farmer J Guttman and J Thayer For a technical overview of the system see 11 1 1 Overview of the Manual The manual consists of three parts 1 Introductory Material This part should definitely be read first Chap ter 3 A Brief Tutorial provides a quick way to start using IMPS 2 User s Guide This part describes how to use IMPS particularly how to build theories 3 Reference Manual 1 2 Goals IMPS aims at computational support for traditional techniques of mathemat ics It is based on three observations about rigorous mathematics e Mathematics emphasizes the axiomatic method Characteristics of mathematical structures are summarized in axioms Theorems are derived for all structures satisfying the axioms Frequently a clever change of perspective shows that a structure is an instance of another theory thus also bringing its theorems to bear 14 e Many branches of mathematics emphasize functions including partial functions Moreover the classes of objects studied may be nested as are the integers and the reals or overlapping as are the bounded functions and the continuous functions e Proof proceeds by a blend of computation and formal inference 1 2 1 Support for the Axiomatic Method IMPS supports the little theories version of the axiomatic method as op posed to the big theory version In the big theory approach all reasoning
126. f poly morphism is not very useful unless we have results about constructors and quasi constructors that could be used in proofs regardless of the actual types that are involved For constructors most of these generic results are coded in the form of the primitive inferences given in Chapter 19 Since quasi constructors unlike constructors can be introduced by you it is imperative that there is some way for you to prove generic results about quasi constructors This can be done by proving theorems about quasi constructors in a theory of generic types and then transporting these results as needed to theories where the quasi constructor is used For example consider the quasi constructor m composition defined by def quasi constructor M COMPOSITION lambda f ind_2 ind_3 g ind_1 ind_2 lambda x ind_1 f g x language pure generic theory 3 fixed theories the kernel theory The basic properties about m composition such as associativity can be proved in the theory pure generic theory 4 which has four base types but no constants axioms or other atomic sorts 9 5 3 Symmetry and Duality Theory interpretations can be used to formalize certain kinds of arguments involving symmetry and duality For example suppose we have proved a theorem in some theory and have noticed that some other conjecture follows from this theorem by symmetry This notion of symmetry can frequently be made precise by creating a theory inter
127. f the functionals Fj F are verified to be monotone in 7 with respect to the subfunction order C The names n1 Nk then denote the simultaneous TfL giff f ai m g a1 Am for all m tuples a1 m in the domain of f 90 least fixed point of the functionals F F As an example the pair factorial Af Z Z An Z if n 0 1 n f n 1 is a recursive definition of the factorial function in our standard theory of the real numbers This approach to recursive definitions is very natural in IMPS because expressions of kind ind are allowed to denote partial functions Notice that there is no requirement that the functions defined by a recursive definition be total In a logic in which functions must be total a list of functionals can be a legitimate recursive definition only if it has a solution composed entirely of total functions This is a difficult condition for a machine to check especially when k gt 1 Of course in IMPS there is no need for a recursive definition to satisfy this condition since a recursive definition is legitimate as long as the defining functionals are monotone IMPS has an automatic syntactic check sufficient for monotonicity that succeeds for many common recursive function definitions Recursive predicate definitions are used to define one or more predicates by simultaneous recursion They are also created with the def recursive constant form Recursive predicate defin
128. f the given sequent Conclusion Tp Major Premise rufy gt Minor Premises 1 lt i lt n T gt til 0 Notes e y is the result of simultaneously replacing each free occurrence of 2 in w with t for each i with 1 lt i lt n if necessary renaming bound variables in 4 to avoid variable captures Related commands assume theorem instantiate transported theorem instantiate transported theorem Script usage instantiate transported theorem theorem interpreta tion instantiations theorem is the name of a theorem interpretation is the name of a theory interpretation and instantiations is a list of strings denot ing expressions 252 Interactive argument retrieval e Theorem name The name of a theorem V 1 01 n 0n in T e Theory interpretation lt RET gt to let IMPS find one The name of a theory interpretation 7 of T in the deduction graph s theory e Instance for variable x of sort g1 ti e Instance for variable 2 of sort On tn n gt 1 Command kind Multi inference Description This command transports the argument theorem to the de duction graph s theory via 7 Then the transported theorem is instantiated with the specified terms t t And finally the resulting formula is added to the context of the given sequent If no theory interpretation name is given IMPS will try to find a theory interpretation to play the role of using the sort information c
129. f the system can ascertain that each of these formulas is a theorem of T The user builds an algebraic processor using a specification such as def algebraic processor FIELD ALGEBRAIC PROCESSOR language fields base operations _kk _kk _kk zero o_kk unit i_kk commutes This specification has the effect of building a processor with a transform for handling terms of the form f a b where f is one the arithmetic functions K K K For example the entry _kk tells the transform to treat 139 the function symbol x as addition The transforms are installed in the theory fields by the specification def theory processors FIELDS algebraic simplifier field algebraic processor _kk _kk _kk algebraic term comparator field algebraic processor When this form is evaluated IMPS checks that the conditions for doing algebraic manipulation do indeed hold in the theory fields 13 5 Hints and Cautions 1 Though simplification is a powerful user command there are several reasons why you do not want to invoke it indiscriminately at every sequent node e If the sequent node context is very large or the expression is large a fact which may be masked by the presence of quasi constructors simplification may take considerable time e Simplification may transform an expression into a form which may be easier for IMPS to work with but may be harder for you to visualize For instance the expression
130. follow ing s expressions set imps reader lambda 1 port read port set imps printer lambda s exp port pretty print s exp port In the next section we describe the default syntax which is similar to the syntax of some computer algebra systems 16 3 String Syntax We begin with some notation if Term is a class of strings Term zero or more comma separated members of Term Term one or more comma separated members of Term A string is accepted by the string syntax exactly when IMPS can build an s expression s from it Otherwise IMPS will give you a parsing error However to say the string is accepted does not mean that the system can build an IMPS expression from s A number of things could go wrong e An atom in s has no sort specification so that IMPS assumes it is the name of a constant but no such constant exists in the language e The arguments of a function are of the wrong type or there are too many or too few arguments e A constructor was given components of the wrong type or the number of components is wrong The tables 16 1 16 2 and 16 3 are a description of those sequences of characters accepted by the string syntax This description is fairly close to a BNF grammar but fails to be one since some of the expression categories such as the category of binary infix operators or the category of quasi constructors are only specified partially or not at all This is because these 158
131. g to Q is skipped Similarly when a macete is applied to an expression Q E1 En subexpressions located in the part of the internal expression corresponding to Q are ignored In this mode quasi constructors are intended to behave as if they were ordinary constructors In the disabled mode the internal structure of Q has no special status That is deduction is performed on internal expressions as if Q was never 109 Quasi constructor Schema quasi equals E Ez Fi VE21 gt El E falselike a1 Qn41 A2 01 1 07 falselike A 1 domain f ATOM n On Tiata total Ch 81 PERO Bn 1 Vxi Br TAD Tn bn 21 gs jo nonvacuous p Jz1 01 ca En Notes e E and E gt must have the same type e falselike represents the same internal expression as F e The sort of f is ay Qn41 e T 01 On 1 7 61 gt Bn 1 e The sort of pis ay Qn Table 10 1 System Quasi Constructors 110 defined However in this mode expressions involving Q will still be printed using Q as an abbreviation The mode is activated by disabling Q and it inactivated by enabling Q The disabled mode is used for proving basic properties about Q Once a good set of basic properties are proven and formalized as theorems there is usually little need for the disabled mode Most quasi constructors are intended to be employed in multip
132. gg g in a and h in a implies g mul h in a with a sets gg forall g gg g in a implies inv g in a fixed theories h o real arithmetic sort pairs gg indic with a sets gg a constant pairs mul with a sets gg lambda x y gg if x in a and y in a x mul y gg inv with a sets gg lambda x gg if x in a inv x gg theory interpretation check using simplification def transported symbols Positional Arguments e names The name or lists of names of defined atomic sorts and con stants to be transported Keyword Arguments e translation translation name Required e renamer renamer Name of a renaming procedure Description Let T and T be the source and target theories respectively of the trans lation named translation name and let sym sym be the symbols whose names are given by names For each sym which is a defined symbol in T this form creates a corresponding new defined symbol sym in T by 211 translating the defining object of sym via If already translates sym to some defined symbol the new symbol is not created Examples def transported symbols last ahindex afinf afeven afodd translation schroeder bernstein symmetry renamer sb renamer def transported symbols prechincreasing prec majorizes prec sup translation order reverse renamer first renamer 17 2 Changing Syntax def overloading Positional Ar
133. ght c 1990 1994 The MITRE Corporation Authors W M Farmer J D Guttman F J Thayer The MITRE Corporation MITRE provides this software to you without charge to use copy modify or enhance for any legitimate purpose provided you reproduce MITRE s copyright notice in any copy or derivative work of this software This software is the copyright work of MITRE No ownership or other proprietary interest in this software is granted you other than what is granted in this license Any modification or enhancement of this software must identify the part of this software that was modified by whom and when and must inherit this license including its warranty disclaimers MITRE IS PROVIDING THE PRODUCT AS IS AND MAKES NO WAR RANTY EXPRESS OR IMPLIED AS TO THE ACCURACY CAPABILITY EFFICIENCY OR FUNCTIONING OF THIS SOFTWARE AND DOCUMEN TATION IN NO EVENT WILL MITRE BE LIABLE FOR ANY GENERAL CONSEQUENTIAL INDIRECT INCIDENTAL EXEMPLARY OR SPECIAL DAMAGES EVEN IF MITRE HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES You at your expense hereby indemnify and hold harmless MITRE its Board of Trustees officers agents and employees from any and all liability or damages to third parties including attorneys fees court costs and other related costs and expenses arising out of your use of this software irrespective of the cause of said liability The export from the United States or the subsequent reexport of this softwar
134. guments e symbol A symbol to overload that is to have multiple meanings which are determined by context e theory name pair theory name pair theory name pair is a list theory name symbol name Examples def overloading h o real arithmetic normed linear spaces def parse syntax Positional Arguments e constant name This is a symbol or a list of symbols 212 Keyword Arguments e token spec specis a symbol or astring If this argument is omitted by default it is constant name e left method proc name proc name is the name of a procedure for left parsing of the token e null method proc name proc name is the name of a procedure for null parsing of the token table table name table name is the name of the parse table being changed If this argument is omitted the default value is the global parse table parse Description binding N Required Nis the binding or precedence of the token This form allows you to set or reset the parse syntax of a constant In particular you can change the precedence parsing method and token rep resentation of a constant The most common parsing methods are e infix operator method For example multiplication and addition use this method e prefix operator method comb the binomial coefficient function uses this method e postfix operator method uses this method Note that an operator can have both a null method
135. h a way that it is possible to quickly throw out inapplicable ones using these heuristic conditions IMPS exploits this to provide users with a dynamic help facility for selecting macetes The use of this facility is explained more extensively in Chapter 4 14 6 Hints and Cautions 1 Conceptually the macete mechanism is extremely simple Users how ever should not underestimate its power usefulness and flexibility The utility of macetes hinges on three facts e The way a theorem is converted into a macete depends on the syntactic form of the the theorem as explained earlier in this section In particular it is important that theorems which are implications can be used as macetes along with those that are conditional equalities Moreover the conversion algorithm is based on a number of heuristics that in our experience work very well e Macetes can be combined using macete constructors It has been our experience that carefully building a collection of compound macetes is an important part of developing a theory e Macetes are tabulated in such a way that the macetes which are applicable to a given formula can be retrieved very effectively and displayed to the user in a menu In situations where over 500 macetes are installed the menu usually contains less than twenty entries and takes less than ten seconds to compute 2 Though there are various modes of applying macetes the default mode with minor premises is the one you
136. h differs from Z only by an appropriate renaming of sorts and constants By an embedding we mean a theory interpretation which maps distinct sorts and constants to distinct sorts and constants 116 In this section we explain the theory ensemble mechanism which implements the second approach above To illustrate how the machinery works in the case of a monoid let us define a new theory monoid theory 1 obtained by renaming the sorts and constants of monoid theory not in h o real arithmetic by affixing the characters _1 def language MONOID LANGUAGE 1 embedded languages h o real arithmetic base types uu_1 constants e_1 uu_1 xx_1 uu_1 uu_1 uu_1 def theory MONOID THEORY 1 component theories h o real arithmetic language monoid language 1 axioms associative law for multiplication for monoids forall z y x uu_l x x_1 y _1 z x _1 y _1 z foral1l x uu_1 x _1 e_1 x foral1 x uu_1 e_1 _1 x x Now define monoid pair as the union of monoid theory and monoid theory 1 def theory MONOID PAIR component theories monoid theory monoid theory 1 The theory ensemble facility automates these steps and also provides several bookkeeping devices for keeping track of theories and interpretations in the ensemble 11 2 Basic Concepts A copy of a theory T is a new theory 7 obtained from 7 by applying a renaming function to the constant and sort symbols in 7 The only condition on
137. have been y a x y apply macete locally with minor premises Script usage apply macete locally with minor premises macete expression occurrences 224 Interactive argument retrieval e Macete name The name of a macete e Expression to apply macete A subexpression of the sequent as sertion to which you want to apply the macete e Occurrences of expression 0 based The list occurrences of the expression you want to apply the macete to Command kind Single inference Description This command applies the argument macete to the given se quent node in the same way as apply macete locally but with the following important difference whenever the truth or falsehood of a definedness or sort definedness assertion cannot be settled by the simplifier the assertion is posted as a additional subgoal to be proved Related commands apply macete apply macete locally apply macete with minor premises apply macete with minor premises Script usage apply macete with minor premises macete Interactive argument retrieval e Macete name The name of a macete Command kind Single inference Description This command applies the argument macete to the given sequent node in the same way as apply macete but with the following important difference whenever the truth or falsehood of a convergence re quirement cannot be settled by the simplifier the assertion is posted as a additional subgoal to be proved 225
138. he translation of a defined constant from a higher multiple by an existing interpretation 11 3 Usage There are four def forms for building and manipulating theory ensembles e def theory ensemble This form is used to build a theory ensemble from a given theory 7 The theory T is called the base theory of the ensemble e def theory ensemble multiple This form is used to build a theory Tn which is the union of n copies of T 118 e def theory ensemble instances This form is used to build a the ory interpretation from a theory multiple 7 to a given theory e def theory ensemble overloadings This form establishes over loadings for the constants defined in 7 and all the multiples 7 11 4 Def theory ensemble This is the def form for building a theory ensemble from an IMPS theory In the simplest version the form requires only one argument the name of the theory ensemble which is then identical to the name of the base theory For example def theory ensemble METRIC SPACES Evaluating the def form builds a theory ensemble also named METRIC SPACES In general three additional keyword arguments are allowed e base theory theory name theory name is the name of the base theory of the ensemble This keyword arguiment is used when the name of the ensemble is different from that of the base theory fixed theories theory theory The presence of this argu ment causes IMPS to rename only those sorts and constants wh
139. hen the def translation form is evaluated IMPS does a series of syn tactic checks to make sure that the form correctly specifies a translation If all the checks are successful IMPS builds the translation or simply retrieves it if it had been built previously The second step is to verify that the translation is an interpretation IMPS first generates the obligations of the translation that are not trivially theorems of the target theory Next IMPS removes from this set those obli gations which are instances of installed theorems of the target theory If the line theory interpretation check using simplification is part of the def translation form IMPS will also remove obligations which are known to be theorems of the target theory by simplification When IMPS is done working on the obligations if there are none left the translation is marked as a theory interpretation Otherwise an error message is made that lists the outstanding obligations If there are outstanding obligations and you believe that they are indeed theorems of the target theory you will usually want to prove them in the target theory Then after installing them in the target theory the def translation form can be re evaluated The following is a simple example of an interpretation built from a def translation form def translation MONOID THEORY TO ADDITIVE RR source monoid theory 96 target h o real arithmetic fixed theories h o real arithmetic
140. heory exploits the fact that read and write are duals when the sense of the partial ordering on levels is inverted This duality is expressed by means of a theory interpretation mapping the theory to itself It is used to manufacture definitions for instance the property is defined to be the dual of the simple security property It is also used to create new theorems For instance the theorem that the property is preserved under get write is the dual of the theorem that the simple security property is preserved under get read hence it suffices to prove the latter and the former follows automatically 70 Purpose This exercise has three main purposes e To illustrate how to extend and to apply the state machine theory and how to prove theorems using state machine induction e To illustrate the use of an interpretation from a theory to itself to encode a symmetry or duality e To provide a model for a familiar kind of security verification 71 Part II User s Guide 72 Chapter 7 Logic Overview 7 1 Introduction The logic of IMPS is called LUTINS a Logic of Undefined Terms for Inference in a Natural Style LUTINS is a kind of predicate logic that is intended to support standard mathematical reasoning It is classical in the sense that it allows nonconstructive reasoning but it is nonclassical in the sense that terms may be nondenoting The logic however is bivalent formulas are always defined U
141. ich do not belong to any of the theories theory theory when building replicas The default value of this argument is the fixed theories set at the time the form is evaluated e replica renamer proc name proc name is the name of a proce dure of one integer argument used to name sorts and constants of theory replicas The default procedure is to affix an underscore fol lowed by a nonnegative integer to a name Most users should be content to use the default Another example which utilizes the fixed theories option is the theory en semble of vector spaces over a field def theory ensemble VECTOR SPACES fixed theories fields When a theory ensemble def form is evaluated IMPS builds a number of tables all of which are initially empty The table will be filled as multiples are built The tables are 119 e A table of the theory replicas The key is an integer k gt 1 and the entry is the k th replica of the base theory e A table of the theory multiples The key is an integer k gt 1 and the entry is the k th multiple of the base theory e A table of canonical interpretations between multiples The key is a pair of integers m n with 1 lt m lt n and the corresponding entry is a list of interpretations from the m multiple to the n multiple 11 5 Def theory multiple This form requires two arguments the name of a theory ensemble and an integer n For example def theory ensemble multiple metric spaces 2 Whe
142. ich is the second s expression of the form that is the name immediately following the string def Thus the tags of the two s expressions above are convergent to infinity and partial order Al The tag of the def form is usually the name of the object being defined or modified There are two good reasons you may want to locate def forms e You may need to know how an object is defined For example in the case of a theory you may want to know what the primitive constants of the theory are e You may want to define a new object modeled on an existing one Def forms can be viewed in an Emacs buffer by selecting the Find def form option in the Help menu or by typing C c in an IMPS buffer IMPS will then request a name As usual the Emacs input completion facility is available so that you only need to type in the first few letters of the entry When you complete your selection IMPS will then search in the theory library for those forms which define the selected entry Note that there may be more than one entry There are several reasons for this e There may be several theories which have an identically named object e An object may be defined in one def form and modified in another def form The definition finder will attempt to locate all such occurrences e A name may refer to different kinds of objects The name fuba might refer to a translation a theorem and a constant Note also that the located form may have a differe
143. ics Different theorems are proved in different theories depending on the amount and kind of mathematics that is required Theories are logically linked together by translations called theory interpretations which serve as conduits to pass results from one theory to another We argue in 10 that this way of organizing mathematics across a network of linked theories is advantageous for managing complex mathe matics by means of abstraction and reuse IMPS supports both the big theory and little theories versions of the ax iomatic method However the IMPs little theories machinery of multiple theories and theory interpretations offers the user a rich collection of for malization techniques described in Chapter 9 that are not easy to imitate in a strict big theory approach 39 Chapter 4 On Line Help Most of the help and documentation facilities described in this chapter re quire that you have a workstation running Emacs under X windows In particular you need a TpX previewer and one of the Emacs X menu facili ties On line help falls into three categories e Retrieval of specific entries in the manual such as documentation of an interactive proof command e Retrieval of def forms These are the forms which when evaluated define the various IMPS objects e Presentation and selection of options via pull down or pop up menus This is especially important if you are new to IMPS because most of your interaction with IMPS can be in
144. ier to do mul tiplicative cancellation Keyword Arguments e language language name Required e base spec forms Required e exponent spec forms Instructs processor how to simplify expo nents if there are any e coefficient spec forms Instructs processor how to simplify coef ficients for modules In all of the above cases spec forms is either a name of an algebraic processor or is a list with keyword arguments and modifier arguments of its own The keyword arguments for spec forms are e scalars numerical type e operations operation alist operation alist operation alist is a list of entries operation type operator operation type is one of the symbols x sub zero unit operator is the name of a constant in the processor language The modifier arguments for spec forms are e use numerals for ground terms e commutes 169 Description This form builds an object called a processor for algebraic simplification Processors are used by IMPS to generate algebraic and order simplification procedures used by the simplifier for the following purposes e To utilize theory specific information of an algebraic nature in per forming simplification For example the expression x x x should simplify to x or x lt x 1 should simplify to true e To reduce any expression built from formal constants whose value can be algebraically computed from the values of the components Thus the expressio
145. ight cancellation follows by symmetry from left cancel lation 6 3 Logical Exercises 6 3 1 Indicators A Representation of Sets Contents An indicator is a function used to represent a set It has a sort of the form a unit sort where a is an arbitrary sort In the string syntax the sort a unit sort is printed as sets a unit sort is a type in the kernel theory that contains exactly one element named an individual The type is of kind 1 so indicators may be partial functions Since the kernel theory is a component theory of every IMPS theory unit sort is available in every theory Indicators are convenient for representing sets The basic idea is that a set s containing objects of sort can be represented by an indicator of sort a unit sort namely the one whose domain is s itself Simplifying expressions involving indicators is to a large extent a matter of checking definedness for which the simplifier is equipped with special purpose al gorithms The theory indicators consists of just a single base sort U for the universe of some unspecified domain Since the theory indicators contains no constants nor axioms theory interpretations of indicators are trivial to construct and thus theorems of indicators are easy to use as transportable macetes The logical operators in IMPS are fixed but quasi constructors can in some respects effectively serve as additional logical operators Quasi constructors are desirable fo
146. igure 5 10 which will complete the proof after another 30 seconds of computation You will note that it uses a macete constructor without minor premises This as well as the phrase with minor premises appearing on the Extend DG menu may be explained with reference to the macete factorial out The substitution of m 1 m in place of m is permissible only when 1 lt m is defined by a syntactic recursion rather than by reference to the T function thus in particular 0 1 4 1 0 0 There are two ways then to use the macete both of them perfectly sound from a logical point of view The first is conservative do the substitution only when we can immediately see that the condition is satisfied for the instance at hand The second approach is more speculative do the sub stitution but post an additional subgoal for the user to prove later The 54 REPEAT WITHOUT MINOR PREMISES REPEAT FACTORIAL OUT FACTORIAL OF NONPOSITIVE SIMPLIFY Where 1 factorial out Replace withm Z ml By withm Z m 1 m Subject to withm Z 1 lt m 2 factorial of nonpositive Replace withj Z j By 1 Subject to withj Z j lt 0 Figure 5 10 The factorial reduction Macete 55 apply macete with minor premises domain of inverse apply macete with minor premises nonzero product apply macete with minor premises factorial nonzero simplify Figure 5 11 Commands to Delete additional subgoal s
147. ill kill Tea and the Emacs process If you are trying to learn to use IMPS it would be a good idea to work through the exercises described in Chapters 5 and 6 after reading this tu torial 3 1 Interacting with IMPS Most of your interaction with IMPS can be initiated by selecting of one of a number of menu options The menu format depends on the version of Emacs you are using e Free Software Foundation version 19 menus are invoked by clicking on the menubar The resulting menu has a number of options e Version 18 menus are invoked by clicking the right mouse button on the mode line Moreover the menu consists of one or more panes which are stacked like cards each individual pane has a label plus a number of options e Lucid version 19 menus are invoked by clicking on the menubar The resulting menu has a number of options Some of the options open up to new submenus These three menu systems are quite similar to each other it is easy to translate instructions for one menu system into instructions for the other You select an option within a menu or pane by pointing with the mouse notice the selected option is enclosed in a box and clicking the right mouse button If you do not want to select anything after the menu appears click right on the option CANCEL MENU REQUEST or just click right when the mouse points to somewhere off the menu This will cause the menu to disappear Notice that some of the options are followed by a
148. imentary algebraic simplification Pro cessors are created with def algebraic processor and def order processor and installed with def theory processors The system will check that the theory contains the right theorems before anything is installed so even if you build a weird processor one that wants to treat ring multiplication as ring addition it cannot be installed 2 Install rewrite rules An ordinary rewrite rule is created and installed in the theory by installing a theorem with the usage rewrite A transportable rewrite rule is created by installing a theorem with the usage transportable rewrite and is installed in the theory with def imported rewrite rules 3 Add information to the theory s domain range handler Information about the domain and range of function constants can be added to a theory by installing theorems in the theory with the usages d r convergence and d r value See Chapter 13 for more details Task 4 Theory Interpretations It is a good idea early in the development of a theory to create the principal theory interpretations involving the theory in either the role of source or target Symmetry interpretations of theory in itself are often quite useful if they exist Theory interpretations are created with def translation See Chapter 9 for details Task 5 Definitions Atomic sorts and constants can be defined throughout the course of de veloping a theory They are usually defined with def atomic
149. implify is then applied to each of the newly created sequents Related commands case split raise conditional Remarks Avoid using this command with more than two occurrences of conditionals choice principle Script usage choice principle Interactive argument retrieval None Command kind Single inference Description This command implements a version of the axiom of choice Conclusion I gt 3f l01 0n T V21 0 Eno P Premise T gt Vero Says A eT Ole figs Ban at Notes 235 e c and o have the same type for all i with 1 lt i lt n e The command fails if there is any occurrence of f in y which is not in an application of the form f x1 tn Remarks The existential sequence is often introduced into the deduction graph using cut with single formula contrapose Script usage contrapose assumption assumption can be given as an integer 7 or a string o Interactive argument retrieval e O based index of antecedent formula i If there is only one as sumption this argument request is omitted Command kind Single inference Description This command interchanges the given sequent s assertion and its assumption given by i Conclusion PU p gt y Premise TU Ay gt p Notes e The index of y in context PU y is 2 Remarks Use contrapose if you want to do proof by contradiction However if there is nothing to con
150. ing are some options that can be selected from the menus in this mode List applicable commands in a menu Each entry in this menu can in turn be selected buy clicking right with the mouse This will apply the corresponding command to the sequent node displayed in the buffer List applicable macetes in a menu Each entry in this menu can in turn be selected with the mouse This will apply the corresponding macete to the sequent node displayed in the buffer List applicable macetes with a brief description in an Emacs buffer Each macete can be selected by moving the cursor to the corresponding menu entry and typing m Note that the applicable commands and macetes are determined dynami cally based on the form of the current sequent 43 Chapter 5 Micro Exercises The purpose of these micro exercises is to familiarize you with the basic techniques used in IMPs Hence we will want to illustrate aspects of the interface as well as several of the basic deductive methods To describe the micro exercises we will assume that you are using the Free Software Foundation Emacs version 19 menu system If you have not already done so start IMPS by issuing the command start_imps to a Unix shell from within the X Window System When IMPS is ready and has informed you of the current theory the theory of real arithmetic pull down the IMPS Help menu on the menubar by depressing and holding any mouse button while pointing to it Point t
151. ing expressions based on their logical structure and e By discharging the great majority of definedness and sort definedness assertions needed to apply many forms of inference The simplifier can be invoked directly by the user as an IMPS command As such it is an exceedingly powerful tool More significantly the simplifier is a central element in the IMPS inference architecture since it is routinely invoked by other commands 136 The simplifier can be viewed as a function of a context I and an expres sion e which returns an expression S T e The following condition serves as the correctness requirement for the simplifier For any context I in a theory 7 and expression e J and IT must together entail e S T e That is to say either e and e are both defined and share the same denotation or else they are both undefined 13 2 Implementation The simplifier is a highly recursive procedure For instance simplification of a compound expression may require prior simplification of all its compo nents that this is not always true reflects the fact that the simplification procedure for an expression depends on the constructor of the expression Simplification of individual expression components is done with respect to the local context of that component in the expression Thus for instance in simplifying an implication A gt B A may be assumed true in the local context relative to which B is simplified Similarly in simplifying the
152. ing the course of a single proof are recorded as a component of the deduc tion graph These commands can be inserted as text into a buffer provided the major mode of the buffer is scheme mode by selecting the option Insert proof script or by entering C c i The text that is inserted in the buffer is a script of proof commands which can be edited and used in other proofs To run a command script select the option Execute region or enter C c r This will run the commands in the current region Note that an interactive proof can be combined with one or more proof segments run in script mode This is especially useful for redoing similar arguments 12 3 1 Checking Proofs in Batch To check a large number of proofs for example to check an addition to the theory library proof scripts can be run in batch by using the shell command IMPS bin run_test testfile logfile where testfile is a text file which may contain any def form Typically it will consist of a series of include files and load section forms The file logfile will contain the output of the process For example entering on a machine called veraguas the shell command 125 IMPS bin run_test testy loggy where testy contains load section abstract calculus will produce a logfile loggy which will look something like HOST veraguas starting IMPS test File tested testy Executable imps sys executables foundation Mon May 3 18 21 56 EDT 1993 INITIAL THEORY NETWORK INFORMA
153. ion of the expression printed string is generated from the internal expression as if the latter had the form Ej Ez In other words in string representation of the expression looks like EH Ez an operator applied to a list of two arguments but it is actually represented internally as Fy VE 2l gt F Eo Abstractly a quasi constructor definition consists of three components a name a list of schema variables and a schema In our example above quasi equals is the name E E gt is the list of schema variables and the right hand side of the biconditional above is the schema A quasi constructor is defined by a user with the def quasi constructor form The list of schema variables and the schema are represented together by a lambda expression which is specified by a string and a name of a language or theory quasi equals is written as in the string syntax and as in the mathematics syntax infixed between its operands 108 The variables of the lambda expression represent the list of schema variables and the body of the lambda expression represents the schema For instance quasi equals could be defined by def quasi constructor QEQUALS lambda el e2 ind e1 or e2 implies el e2 language the kernel theory The name of the quasi constructor is qequals and the lambda expression is the expression specified by the string in the kernel theory After this form has been evaluated an expression of the form
154. ion requires some explanation Suppose amp is a defined sort of 71 which is not mentioned in the sort association list of Let U be the unary predicate that was used to define a If there is a atomic sort 3 of Ta defined by a unary predicate U such that U and U are alpha equivalent then a is translated as if the pair a 8 were in the sort association list of Otherwise it is translated as if the pair a U were in the sort association list of 97 Suppose a is a directly defined constant of 71 which is not mentioned in the constant association list of Let e be the expression that was used to define a If there is a constant b of 7 directly defined by an expression e such that e and e are alpha equivalent then a is translated to b Otherwise a is translated to e Suppose a is constant which is not mentioned in the constant association list of but which is a member of a list a an of constants of Ty defined by recursion Let F Fn be the list of functionals that was used to define aj Gy If there is a list b1 b of constants of 72 recursively defined by the list of functionals Fj Fy such that F and F are alpha equivalent for each j with 1 lt j lt n then a is translated to b Otherwise a is translated to an iota expression which denotes the ith component of the minimal fixed point of f F 9 5 Reasoning and Formalization Techniques This secti
155. ion_theory name 2 For recursively defined constants a number of macetes are installed a The equation axioms named constant name equation_theory name b The minimality axiom named definition name strong minimality_theory name c The minimality theorem named definition name minimality _theory name 3 For defined atomic sorts a number of macetes are installed a The sort defining axiom named sort name defining axiom_theory name b Some auxiliary theorems named sort name in quasi sort_theory name and sort name in quasi sort domain_theory name Nondirectional schematic macetes usually are not associated to theo rems The form def schematic macete can be used for building schematic macetes of all kinds You can build compound macetes using the form def compound macete 148 14 5 Applicable Macetes A macete is applicable to a formula if applying the macete modifies the for mula in some way The only sure fire way of determining whether a macete is applicable is to actually apply the macete and see the result However there are simple heuristic conditions which can be used to quickly deter mine that some macetes are not applicable For example for an elementary bidirectional macete if the left hand side of the macete does not match any subexpression of the formula then clearly the macete it is not applicable For transportable macetes other similar inapplicability conditions are used Macetes are tabulated in suc
156. ions and subtypes the logic of IMPS Macete A user defined extension of the simplifier When a theorem is installed it is also automatically installed as a macete The way the corre sponding macete works depends on the syntactic form of the theorem In the simplest case in which the theorem is a universally quantified equality the theorem is used as a rewrite rule Macetes can be composed using the def form named def compound macete The word macete comes from 295 Brazilian Portuguese where it means clever trick Theorem macetes can also be made into transportable macetes Mode Line The line at the bottom of each buffer window It provides information about the displayed buffer such as its name and mode Parser A program which takes user input usually represented as text and builds a data structure suitable for computer processing Primitive inference procedure An IMPS procedure that implements one of the primitive rules of inference of the IMPS proof system IMPS has about 30 primitive inference procedures Proof Conclusive mathematical evidence of the validity of some assertion The rules for admissible evidence are given by a proof system Quasi constructor A user defined macro abbreviation for building ex pressions Quasi constructors are used much like constructors Quasi equality A quasi constructor written as infix in the mathemat ical syntax t s means that either t and s are both undefined or they are
157. ions of kind are used to refer to mathematical objects they may be undefined Expressions of kind are primarily used in making assertions about mathematical objects they are always defined Lambda application An application whose operator is a lambda expression For example A x y R x 3 y 1 z Lambda expression A compound expression whose lead constructor is named lambda denoted in the mathematical syntax by A A lambda expression has the form A 1 01 n 0n Y It denotes the function of n arguments whose value at x1 t is given by the value of term p pro vided the x are of sort 0 Language Mathematically a language in IMPS consists of expressions sorts and user supplied information about sort inclusions At the imple mentation level a language is a Lisp data structure having additional struc ture which procedurally encodes this information This is meant to facilitate various kinds of lower level reasoning such as reasoning about membership of an expression in a sort Little theories A version of the axiomatic method in which mathematical reasoning is distributed over a network of theories linked to one another by theory interpretations in contrast to the big theory approach in which all reasoning is performed within a single usually very expressive theory Local context The set of assumptions relevant to a particular location in an expression LUTINS A version of type theory with partial funct
158. irect inference e 267 Weakest aa a AS Mak te a e 267 19 The Primitive Inference Procedures 269 antecedent inference 2 269 backchain inference e 270 backchain backwards inference 271 backchain through formula inference 271 CHOICE 2 o e a A oe age 272 COMTAPOSIUION ds Li AA A ee 272 A O EN at te hes 272 defin dness 22 a tt A eh de Re ee ee LS el A 273 defined constant unfolding 2004 273 direct inference ooa 273 disjunction elimination a 274 elimin t iota a r ay Ade weed Whe pra Pee Re a a 274 existential generalization o e 275 extensionality 22 da disa s a A ea BE a a 275 force substitution ooa e a 276 incorporate antecedent a a 277 insistent direct inference a 277 insistent simplification a 278 macete application at paths 278 macete application with minor premises at paths 278 raise conditional inference o 278 Simplification iaa ek den as Ae a ee bh oe ts ed 279 simplification with minor premises 280 sort defined Ness a a4 A es doe en A 280 theorem assumption sooo a 280 universal instantiation 2 0 02 20 0000022 2a ee 280 unordered conjunction direct inference 24 281 Weakening 2 105 Mek te 2 habe ead ee be lade oe dk ad 281 20 The Initia
159. is form builds a language with name language name satisfying the follow ing properties e This language contains the sorts and constants given by the sort and constant specification subforms e It contains the languages named name as sublanguages e If the language contains the extensible keyword then the language may contain an infinite number of constants these constants are in one to one correspondence with elements of the numerical types present in the type sort alist Examples def language NUMERICAL STRUCTURES extensible integer type zz rational type qq sorts rr ind qq rr zz qq constants rr zz rr rr rr rr rr rr rr sub rr rr rr rr rr rr rr rr lt rr rr prop lt rr rr prop def language METRIC SPACES LANGUAGE embedded language h o real arithmetic 186 base types pp constants dist pp pp rr def language REAL VECTOR LANGUAGE embedded language h o real arithmetic base types uu constants uu uu uu vO uu rr uu uu def language HAM SANDWICH LANGUAGE base types sandwich embedded language h o real arithmetic constants hamhsandwich sandwich tuna sandwich sandwich refrigerator sandwich unit sort def order processor Positional Arguments e name Keyword Arguments e algebraic processor name The name of an algebraic processor operation alist e operations operation alist
160. is known to be a theorem of T If there is a witness argument the systems tries to verify condition 2 by simplifying p a where a is the expression specified by witness expr string Examples def atomic sort NN lambda x zz O lt x theory h o real arithmetic witness 0 def bnf Positional Arguments e name A symbol to serve as the name of the theory that will be created as a consequence of this def form In addition a second im plementation object with this name is also created it represents the BNF definition itself together with the axioms and theorems that it generates 172 Keyword Arguments e theory theory name Required The theory that will be conser vatively extended by adding the new datatype We will refer to this theory as the underlying theory base type type name Required The name of the new data type sorts subsort enclosing sort subsort enclosing sort Subsorts of the new datatype All these subsorts must be included within the new base type Thus the enclosing sort of the first subsort must be the new base type and the enclosing sort of a later subsort must be either the base type or a previously mentioned subsort of it e atoms atom sorti atom sort Individual constants declared to belong to the base type or one of its subsorts e constructors constr sort sort selectors s 8n 1 Function constants declared to construct element
161. ist form 229 Interactive argument retrieval e List of O based indices of antecedent formulas If there is only one assumption this argument request is omitted Command Kind Multi inference Description A succession of backchains are performed using the indi cated assumptions Execution terminates when every backchaining oppor tunity against those assumptions has been used up Related commands backchain backchain backwards backchain through formula backchain through formula Script usage backchain through formula assumption assumption can be given as an integer or a string o Interactive argument retrieval e O based index of antecedent formula If there is only one as sumption this argument request is omitted Command kind Single inference Description This command attempts to use the assumption with the given index to replace the assertion to be proved In the simplest case if the given assumption is y gt w and the assertion is 4 then backchain through formula replaces the assertion with y Similarly if the assertion is ay it is replaced with y The command extends this simplest case in four ways e If the assumption is universally quantified then matching is used to select a relevant instance 230 e If the assumption is a disjunction V Pi ici then for any j i it may be treated as N mi D p ici i j e If the assumption is a conjunction each conjunct is tried separately in
162. iterates of a function which are perfectly generic and independent of the fact that we will eventu ally apply them to functions f P gt P e A third group of theorems proved in the theory of a metric space applying the previous theorems Purpose The exercise has three purposes e To illustrate the little theories approach and how natural it is in math ematics e To illustrate inductive proof in combination with some other tech niques in real arithmetic and also in the generic theory covering iter ation e To provide a richer more extended example of how to develop a sub stantial proof using IMPS 6 2 6 Basics of Group Theory Contents This file develops the very rudiments of group theory only up to a definition of subgroup and a proof that subgroups are groups Most of the content is devoted to building up computational lemmas This exercise covers only a very small part of the portion of group theory that is developed in the IMPS theory library in the files contained in the directory IMPS theories groups 66 Purpose The purpose of this exercise is to illustrate how to handcraft the simplification mechanism by proving rewrite rules In addition a compound macete is introduced to carry out computations not suited to the simplifier The file also illustrates the use of a symmetry translation mapping the theory to itself This translation maps the multiplication operator to AL Y YL Thus for instance r
163. itiated using the menus 4 1 The Manual The manual can be viewed on a T X preview window by selecting the Manual option in the Help menu or by entering the Emacs command M x imps manual entry You will be prompted for a specific entry in the manual The entry can be in one the following categories e A command name e A def form name e A glossary entry 40 As usual the Emacs input completion facility is available so that you only need to type in the first few letters of the entry When you complete your selection the previewer window which might be iconified will display the IMPS manual on the page which contains the entry However other pages of the IMPS manual are accessible by using the previewer s page motion commands This allows you to easily examine related entries in the manual 4 2 Def forms All IMPS objects are built using a specification form called a def form The following are some examples of def forms def constant CONVERGENTYTO INFINITY lambda s zz rr forall m rr forsome x zz forall j zz x lt j implies m lt s j theory h o real arithmetic def theory PARTIAL ORDER language language for partial order component theories h o real arithmetic axioms prec transitivity forall a b c uu a prec b and b prec c implies a prec c prec reflexivity forall a uu a prec a prec anti symmetry forall a b uu a prec b and b prec a implies a b Def forms have a tag wh
164. itions are implemented in essen tially the same way as recursive function definitions using the order C on predicates The approach is based on the classic theory of positive inductive definitions see 21 For an example consider the pair even odd F1 F2 where e F e 0 N gt prop An N if n 0 truth o n 1 e Fy e 0 N gt prop An N if n 0 falsehood e n 1 It defines the predicates even and odd on the natural numbers by simultane ous recursion As with recursive function definitions there is an automatic syntactic check sufficient for monotonicity that succeeds for many recursive predicate definitions 29 C q iff p ai m D q ar am for all m tuples a1 am in the common domain of p and q 91 8 6 Theory Libraries A theory library is a collection of theories theory constituents definitions theorems proofs etc and theory interpretations that serves as a database of mathematics A theory library is composed of sections each section is a particular body of knowledge that is stored in a set of files consisting of def forms A section can be loaded as needed into a running IMPS process A section is built from a possibly empty set of subsections and files with def section The forms load section and include files will load a section and a list of files respectively These forms are useful for organizing sections Supplied with IMPs is an initial theory library which con
165. l Theory Library An Overview 282 abstract caleulus s s o poega i eao pak fh Seay See ae RS 282 banach fixed point theorem 0000000 eee 283 basic cardinality s ir senson p a 283 Dasiertelds te mo Ainea A A i E ik Velie 283 basic group theory 2 0 0 a 283 basic MONO AS s asc e a da See ae a ee 283 binary relations ee ee 284 binomial theorem e 284 counting theorems for groups e 284 FOUN ATION or e a aa it 284 groups as monoids 1 1 ee a 285 knaster fixed point theorem o e e 285 Metri spaces es Re Dele ee ee eS 285 metric space pairs s ee 286 metric space continuity 0 000000 00 2 ae 286 mumber theory s oso s socedi ra a eR a a a A 287 PAIS NE A A ot ee TAO E E E oe a Se Ba ar 287 partial orders oo vie aa La tee e 287 PLC ts AA ee ah eo te ay ae ee ic 288 SEQUENCES Sides Ah nner at E poe Ps Bose oe eed BO ea BO 291 GlOSSARY ia Ho acd het Poo A a SG 292 Bibliography e p ai uena Ace A a e 299 List of Tables 3 1 3 2 3 3 3 4 6 1 7 1 16 1 16 2 16 3 16 4 Domains of Arithmetic Operators Sorts for h o real arithmetic String Syntax for Constructors Syntax for h o real arithmetic Exercise Files by Tier o Table of Constructors 0 0 0 0 eee eee System Quasi Constructors 2 0080004 Description of String Syntax 1
166. l representation of an expression containing quasi constructors might be much larger than what one might expect from the printed representation of the expres sion especially if the quasi constructors are defined in terms of other quasi constructors Consequently the processing speed of IMPS on ex pressions containing quasi constructors sometimes seems unjustifiably slow An expression may sometimes implode when parsed That is quasi constructors may appear in the printed string in places where they did not occur in the preparsed string This happens because the IMPS printing routine will use quasi constructors as abbreviations wherever possible regardless of whether these quasi constructors were used in the preparsed string Expression implosion can be caused by simplifi cation and macete application Due to the implosion phenomenon the preparsed and printed strings may not parse into the same internal expressions but the two internal 112 expressions will always be a equivalent For example consider the preparsed string Sy with f ind ind forall x ind x It parses into an internal expression Ej which is printed as the string S2 with f ind ind total_qtf lind ind with quasi constructor abbreviations and is printed as S without quasi constructor abbreviations However S parses into an internal expression Ea which is printed as 52 with quasi constructor abbrevia tions and is printed as the string 53
167. lambda n nn if_form n 0 truth odd n 1 lambda even odd nn prop lambda n nn if_form n 0 falsehood even n 1 theory h o real arithmetic definition name even odd def recursive constant OMEGA EMBEDDING lambda f nn nn a sets nn lambda k nn if k 0 iota n nn n in a and forall m nn m lt n implies not m in a lambda z nn iota n nn n in a and z lt n forall m nn z lt m and m lt n implies not m in a k 1 theory h o real arithmetic definition name omega embedding def renamer Positional Arguments e name A symbol naming the renamer 192 Keyword Arguments e pairs pair patr pair is of the form old name new name Description This form defines a T procedure named name which given a symbol zx returns the symbol y if x y is one of the pairs and otherwise returns zx Examples def renamer SB RENAMER pairs last ahindex last b index afinf bhinf a even b even ahodd b odd def schematic macete Positional Arguments e macete name A symbol naming the schematic macete e formula A string representing the formula using the current syntax Modifier Arguments e null The presence of this modifier means the macete is nondirec tional This means that schematic macete which is built uses a match ing and substitution procedure which does not obey the variable cap turing protections and other restrictions of normal matching and sub s
168. le theories Hence you will usually want to install a theorem about a quasi constructor with the usage transportable macete For a few of the interactive proof commands there is a dual command with the word insistent put somewhere into the command s name For example the dual of simplify is the simplify insistently Calling the dual of a command C is equivalent to disabling all quasi constructors and then calling C itself In other words the dual commands behave as if there were no quasi constructors at all These insistent commands are intended to be used sparingly because they can disturb the internal structure cor responding to a quasi constructor creating a new internal expression that can no longer be abbreviated by the quasi constructor In visual terms the quasi constructor explodes One of the advantages of working in a logic like LUTINS with a rich structure of functions is that generic objects like sets and sequences can be represented directly in the logic as certain kinds of functions For in stance sets are represented in IMPS as indicators which are similar to characteristic functions except that x is a member of an indicator f iff f x is defined Operators on indicators and other functions representing generic objects are formalized in IMPS as quasi constructors and theorems about these operators are proved in generic theories that contain neither constants nor axioms except for possibly the
169. lem and as a verification that the transformation is valid 100 9 5 5 Definition Transportation A list of definitions atomic sort directly defined constant or recursively defined constant can be transported from T to T gt via an interpretation of T in 73 using def transported symbols For example consider the following def forms def translation ORDER REVERSE source partial order target partial order fixed theories h o real arithmetic constant pairs prec rev prec rev prec prec theory interpretation check using simplification def renamer FIRST RENAMER pairs prec majorizes prec minorizes prechincreasing rev prec increasing prec sup prec inf def transported symbols prec majorizes prec increasing prec hsup translation order reverse renamer first renamer The def transported symbols form installs three new definitions prec minorizes rev prec increasing and prec inf in partial order These new definitions are created by translating the definiens of prec majorizes prec increasing and prec sup respectively via order reverse 9 5 6 Theory Instantiation As argued by R Burstall and J Goguen e g in 14 15 a flexible notion of parametric theory can be obtained with the use of ordinary theories and theory interpretations The key idea is that the primitives of a subtheory of a theory are a collection of parameters which can be instantiated as a group via a theory interpre
170. lity to the developer of a theory to control what heuristics will be used in induction This is encoded in an object called an inductor An inductor contains the induction principle to be used in the form of a macete similar to the little integer induction macete used above In addition it may contain additional macetes or commands to be used in the base case or induction step It may also control whether definitions are expanded and if so which ones Clicking on the next micro exercise will restart a derivation for the sum of the first n natural numbers 58 Step 1 Within the Extend DG menubar item click on the Commands entry Near the top of the resulting menu will be the induction com mand Click on it IMPS will respond with another menu prompting for the name of an inductor integer inductor is the most frequent choice which expands recursive and nonrecursive definitions in syntactically appropriate contexts The nonrecursive integer inductor expands only nonrecursive definitions and the trivial integer inductor expands none In the case we are currently considering select the option integer inductor Result After about 10 15 seconds IMPS will post 11 new subgoals all of which are grounded thus completing the proof To inspect the proof in detail under the DG menubar item click on Verbosely update dg display This will show the structure of the deriva tion To view all of the individual nodes under TeX click on Xview sqns
171. ll not affect theory simplification in any way To add algebraic simplification to a theory eval uate the form def theory processors It is also important to note that an algebraic processor can only be installed in the simplifier when certain theorems generated by the processor are valid in the theory Examples def algebraic processor RR ALGEBRAIC PROCESSOR language numerical structures base scalars rational type operations me C Sf sub sub use numerals for ground terms commutes def algebraic processor VECTOR SPACE ALGEBRAIC PROCESSOR language real vector language base operations xx zero v0 coefficient rr algebraic processor def atomic sort Positional Arguments e sort name The name of the atomic sort to be defined sort name also is the name of the newly built definition e quasi sort string 171 Keyword Arguments e theory theory name Required e usages symbol symbol e witness witness expr string Description This form creates a new atomic sort o called sort name from a unary pred icate p of sort o specified by quasi sort string and adds a set of new theorems with usage list symbol symbol The new atomic sort and new theorems are added to the theory T named theory name provided e sort name is not the name of any current atomic sort of T or of a structural supertheory of T and e the formula 3x 0 p x
172. lly constant Interactive argument retrieval e Constant name c 266 Command kind Multi inference Description This command replaces every occurrence of the defined con stant c by its unfolding e Conclusion gt p Premise T gt yle clan The command beta reduce repeatedly is called after all the unfoldings are performed Related commands unfold single defined constant Key binding U unordered direct inference Script usage unordered direct inference Interactive argument retrieval None Command kind Single inference Description Ifthe sequent node assertion is a conjunction this command does a direct inference without strengthening the context Conclusion TS gid AQn Premises 1 lt i lt n T gt yi Related commands direct inference weaken Script usage weaken assumption list assumption list can be given as a list of numbers a list of strings or an assumption list form 267 Interactive argument retrieval e List of formula indices to omit 0 based A list 1 given in the form Eh gt Shes Command Kind Single inference Description This command removes one or more assumptions you spec ify from the context of the given sequent Conclusion TU A gt Premise Tso Notes e The indices of the members of A in the context I UA are given by I Remarks You might wonder why you would ever want
173. ly strong to prove the induction conclusion In such cases instead of using a different induction principle you first prove a stronger for mula by using the same weak induction principle You can build inductors using the form def inductor See Section 17 1 Key binding i 249 insistent direct inference Script usage insistent direct inference Interactive argument retrieval None Command kind Single inference Description This command is equivalent to disabling all quasi construc tors and then calling direct inference Related commands direct inference insistent direct inference strategy Remarks There is rarely any need to use this command It has the disagreeable effect of exploding quasi constructors insistent direct inference strategy Script usage insistent direct inference strategy Interactive argument retrieval None Command kind Multi inference Description This command repeatedly applies the insistent direct in ference command to the goal node and resulting subgoal nodes until no more insistent direct inferences are possible In other words it adds to the deduction graph the smallest set of sequents containing the goal sequent and closed under insistent direct inferences This command is equivalent to dis abling all quasi constructors and then calling direct inference strategy Related commands direct inference strategy insistent direct inference 250 Remarks Like insistent direct inference
174. me Required e assumptions formula string formula string e fixed theories theory name theory name e sort pairs sort pair spec sort pair spec Each sort pair spec has one of the following forms sort name sort name sort name sort string sort name pred expr string sort name indic expr string e constant pairs const pair spec const patr spec where const pair spec has one of the following forms constant name constant name constant name expr string e core translation core translation name The name of a theory interpretation e theory interpretation check check method Description This form builds a translation named name from the source theory S named source theory name to the target theory T named target theory name The target context in T is the set of assumptions specified by formula string formula string The translation is specified by the set of fixed theories the set of sort pairs and the set of constant pairs If there is a core translation argument an extension of the translation named core translation name is build using the information given by the other arguments The argument theory interpretation check tells IMPS how to check if the translation is a theory interpretation relative to the set of assumptions 209 If the modifier argument force is present the obligations of the transla tion are not generated
175. mitive inference procedure interchanges the given sequent s assertion and the assumption y Conclusion TU 9 gt 4 Premise TU Av gt p cut Parameters A sequent node to be the major premise Description Conclusion T gt 0 Major Premise TU 41 Yn gt p Minor Premises 1 lt i lt n T gt 4 Notes e The major premise is the sequent I U 41 Yn gt y 272 definedness Parameters None Description This primitive inference procedure applies to a sequent whose assertion is a definedness statement of the form t The primitive inference procedure first tests whether the context entails the definedness of t If the test fails the primitive inference then tries to reduce the sequent to a set of simpler sequents defined constant unfolding Parameters e A list of paths p Pn to occurrences of a defined constant c e The constant c itself Description This primitive inference procedure replaces occurrences of the defined constant c at the paths p by its unfolding e direct inference Parameters None Description This primitive inference procedure applies an analogue of an introduction rule of Gentzen s sequent calculus in reverse based on the lead constructor of the assertion of the given sequent 273 Conclusion T yD Premise TU p sv C
176. n 9 5 9 Theory Ensembles 0204 9 5 10 Relative Satisfiability 2 9 6 Hints and Cautions o 72 74 74 75 75 TT 78 79 82 82 84 84 85 88 88 90 92 92 10 Quasi Constructors 10 1 Motivation 10 2 Implementation 10 3 Reasoning with Quasi Constructors 10 4 Hints and Cautions 11 Theory Ensembles 11 1 Motivation 11 2 Basic Concepts 11 3 Usage 11 4 Def theory ensemble 11 5 Def theory multiple 11 6 Def theory ensemble instances o 11 7 Def theory ensemble overloadings 11 8 Hints and Cautions 12 The Proof System 12 1 Proofs 12 2 The IMPS Proof System 2000 12 3 Theorem Proving 12 3 1 Checking Proofs in Batch 12 4 The Script Language a 12 4 1 Evaluation of Script Expressions 12 5 The Script Interpreter o 12 6 Hints and Cautions 13 Simplification 13 1 Motivation 13 2 Implementation 13 3 Transforms 13 4 Algebraic Processors 2 0 0 2 ee ee ee 13 5 Hints and Cautions 14 Macetes 14 1 Classification 14 2 Atomic Macetes 14 2 1 Schematic Macetes 14 2 2 Nondirectional Macetes 14 3 Compound Macetes 107 107 108 109 111 115 115 117 118 119 120 120 121 122 123 123 124 125 125 128 130 131
177. n e A sequent node corresponding to a minor premise is not created if the truth of the minor premise is immediately apparent to IMPS e If f and g are of kind x then is used in place of in the premise force substitution Parameters e Paths A list of paths p1 Pn e Replacements A list of expressions 1j Y 276 Description This primitive inference procedure changes part of the se quent assertion It yields two or more new subgoals One subgoal is obtained from the original sequent assertion by replacing the subexpression e at the path p with r The other subgoals assert that the replacements are sound Conclusion T gt 0 Major Premise T gt plri es Minor Premises 1 lt i lt n Ti gt yj Notes e T is the local context of T gt y at the path p i e pj is e r if e is a formula and the parity of the path p is 0 ri D es if e is a formula and the parity of the path p is 1 e D ri if e is a formula and the parity of the path p is 1 e r in all other cases incorporate antecedent Parameters A sequent node assumption y Description This primitive inference procedure does the reverse of direct inference on an implication Conclusion TU p gt y Premise Tso ody insistent direct inference Parameters None Description This primitive inference procedure is equivalent to disabling all quasi con
178. n 2 3 should reduce to 5 In order for simplification to reduce expressions involving only formal constants for instance 2 3 a processor associates such IMPS terms to executable T expressions involving algebraic procedures and objects from some data type S This type is specified by the scalars declaration of the def algebraic processor form We refer to this data type as a numerical type Each formal constant o which denotes an algebraic function such as or is associated to an operation f o on the data type This corre spondence is specified by the operations keyword of processor Finally certain terms must be associated to elements of S This is accomplished by a predicate and two mappings constructed by IMPS when the processor is built e A predicate that singles out certain terms as numerical constants These are called numerical terms For the processor used in the the ory h o real arithmetic the numerical constants are those formal constants whose names are rational numbers e A function m T m which maps certain elements of S to terms e A function t N t which maps certain terms to S The simplifier uses these functions to reduce expressions containing numeri cal terms according to the following rule If f denotes a processor operation and s t denote numerical terms and o s t is defined then o s t is replaced by T f 0 N s N 4 170 Remarks Evaluating a def algebraic processor form by itself wi
179. n argument to the deduction graph Key binding e eliminate defined iota expression Script usage eliminate iota index symbol Interactive argument retrieval e O based index of iota expression occurrence i e Name of replacement variable y Command kind Multi inference Description This command replaces the i th occurrence of an iota expression in the given sequent s assertion with the variable y The com mand is predicated upon the iota expression being defined with respect to the sequent s context An iota expression is an expression whose lead con structor is iota or a quasi constructor that builds an iota expression Conclusion T gt 4 Major Premise TU ply t free Vz 0 Y 2 2 free D z y gt Y Minor Premise T gt za 0 y 242 Notes e 12 0 is the i th iota expression occurrence in Y e 1 is the result of replacing the i th iota expression occurrence in w with y Related commands eliminate iota Remarks This command is very useful for dealing with iota expressions that are known to be defined with respect to the sequent s context The minor premise is grounded automatically if the sequent s context contains tx 0 p l eliminate iota Script usage eliminate iota index Interactive argument retrieval e O based index of iota expression occurrence i Command kind Single inference Description This command applies to a sequent whose asserti
180. n be also classified according to the relation between the source and replacement expressions Bidirectional Whatever the context and source expression the re placement expression is quasi equal to the source expression that is given any legitimate model in which the context assumptions are true either both source expression and replacement expression have no value or their value is identical Backward directional Whatever the context and source expression the replacement expression is quasi equal to or implies the source ex pression Notice that implication only makes sense for formulas of sort Nondirectional There are contexts and source expressions in which the target expression is neither quasi equal to nor implies the source expression 14 2 Atomic Macetes 14 2 1 Schematic Macetes A schematic macete can be associated to any formula in two ways depending on the kind of matching procedure used IMPS has two general forms of matching called expression matching and translation matching 143 Let us consider first the case of expression matching To any IMPS for mula we can associate e A source pattern This is an expression s e A replacement pattern This is an expression r e A list of condition patterns This is a list of expressions 1 Cn e A direction specifier this specifier can be either bidirectional or back ward directional Suppose the formula is Vx1 01 n 0n Y where y itself is not a uni
181. n this form is evaluated IMPS builds a 2 multiple of the theory metric spaces IMPS automatically names this theory metric spaces 2 tuples Once the theory metric spaces 2 tuples is available several important concepts can be defined For instance def constant CONTINUOUS lambda f pp_0 pp_1 forall v sets pp_1 open v implies open inv_image f v theory metric spaces 2 tuples 11 6 Def theory ensemble instances This form is used to build interpretations from selected theory multiples and to transport natively defined constants and sorts from these multiples using these interpretations The syntax for this def form is very elaborate so we refer you to Chapter 17 for its general use As an example suppose we wanted to consider the pair consisting of a normed linear space and the real numbers as a special case of the the ory metric spaces 2 tuples One reason for doing this is to make all the mathematical machinery developed in the abstract theory metric spaces 2 tuples available in the particular case This machinery includes defini tions such as the definition of continuity for mappings and theorems such as the various characterizations of continuity 120 We would like to build a theory interpretation from metric spaces 2 tuples to the union of normed linear spaces and h o real arithmetic which is normed linear spaces itself since normed linear spaces is a super theory of h o real arithmetic Moreover we would like
182. n this is the case c is said to be immediately grounded More gen erally c is valid if all the hypotheses hy hy of i are valid Thus validity propagates from hypotheses to conclusion A sequent node which is recog nized as valid in this way is said to be grounded The system indicates that it has recognized validity of a sequent node when it marks it as grounded A proof is complete when the original sequent node of the deduction graph i e the deduction graph s goal node is marked as grounded Sequent nodes and inference nodes are added to a deduction graph using deduction graph commands Some commands correspond to the use of one inference rule for example extensionality or force substitution fall into this category Applying such a command either does nothing or adds exactly one inference node to the deduction graph Moreover this one inference node corresponds quite closely to the application of one mathematical fact Other commands such as simplify have similar behavior in that they either do nothing or add exactly one inference node Yet they are fundamentally different because behind the scene they are often carrying out thousands of very low level inferences such as logical and algebraic simplification and rewrite rule application Finally a third class of commands are essentially strategies developed to systematically apply primitive commands in search of a proof 3 6 Extending IMPS IMPS can be extended in the following ways
183. name language name is the name of a language or theory in which to build the expression 216 Chapter 18 The Proof Commands This chapter is intended to provide users with documentation for IMPS proof commands However it is not suggested that users read this chapter before using IMPS Commands can be used in two modes e Interactive mode In this mode an individual command is invoked by supplying the command s name The system will then prompt you for additional arguments Script mode In this mode a command is invoked by a command form Command forms are s expressions command name ay an To use commands in this way you must know the possible command arguments Commands in script mode can be invoked line by line by region or in batch mode Moreover if the command requires no arguments then the name of the command by itself is a command form We will use the following template to describe use of individual commands The last three entries are optional Script usage Describes the use of the command in scripts Arguments such as theories macetes and theorems are specified by name Some arguments can be specified in various ways When an argument is an assumption it can be specified as follows 217 e A nonnegative integer i This denotes the i th assumption e A string o If o denotes an expression which is alpha equivalent to an assumption then it denotes that assumption If o matches one or more assump
184. nce produces subgoals which together are equivalent to the original goal Thus it is always safe to do direct inferences in the sense that they do not produce false subgoals from true goals Key binding d direct inference strategy Script usage direct inference strategy Interactive argument retrieval None Command kind Multi inference Description This command repeatedly applies direct inference to the given sequent and resulting sequents until no more direct inferences are possible In other words it adds to the deduction graph the smallest set of sequents containing the given sequent and closed under direct inferences Related commands antecedent inference strategy direct inference direct and antecedent inference strategy disable quasi constructor Script usage disable quasi constructor quasi constructor Interactive argument retrieval e Quasi constructor name The name of a quasi constructor in the expression Command kind Null inference Description This command disables the quasi constructor given as ar gument 241 edit and post sequent node Script usage edit and post sequent node context string assertion string Interactive argument retrieval e Edit sequent and C c C c when finished A sequent presented as a string of formulas using gt to separate the sequent assumptions from the sequent assertion Command kind Null inference Description This commands adds the sequent given as a
185. nds apply macete locally apply macete locally with minor premises apply macete with minor premises Remarks Macetes are an easy and very effective way of applying lemmas in a proof In fact in the course of developing a theory we suggest that some effort be expended in formulating lemmas with a view to applying them as macetes Key binding m 223 apply macete locally Script usage apply macete locally macete expression occurrences Interactive argument retrieval e Macete name The name of a macete e Expression to apply macete A subexpression of the sequent as sertion to which you want to apply the macete e Occurrences of expression 0 based The list occurrences of the expression you want to apply the macete to Command kind Single inference Description This command applies the argument macete to the given sequent node at those occurrences of the expression supplied in response to the minibuffer prompt Related commands apply macete apply macete locally with minor premises apply macete with minor premises Remarks This command is useful when you need to control where a macete is applied in cases where it applies at several locations For example if the sequent assertion is z y y z then applying the macete commutative law for addition to the 0 th occurrence of x y yields a new sequent with assertion y 2 y x If the macete had been applied globally the resulting assertion would
186. neral logical methods to reduce the sequent to a logically equiva lent sequent The theory specific methods include algebraic simplification deciding rational linear inequalities and applying rewrite rules Related commands beta reduce simplify antecedent simplify insistently simplify with minor premises Remarks This is a very powerful command that can be computationally expensive Computation can often be saved by using the weaker command beta reduce Key binding C c s simplify antecedent Script usage simplify antecedent assumption assumption can be given as an integer 1 or a string o Interactive argument retrieval e O based index of antecedent formula i If there is only one as sumption this argument request is omitted Command kind Multi inference 259 Description This command is used for simplifying an assumption in the context of the given sequent with respect to this context It is equivalent to the following sequence of commands contrapose applied to the given sequent with argument i simplify applied to the sequent yielded by the previous command and contrapose applied to the sequent yielded by the previous command with the index of the negated assertion of the original sequent The commands halts if simplify grounds the first produced se quent Related commands beta reduce antecedent simplify simplify insistently Script usage simplify insistently Interactive argument retrieval None C
187. nf to the set of inference nodes of the deduction graph e The addition of the hypotheses of inf to the set of sequent nodes There are about 25 primitive inference procedures Primitive inference procedures are the only means by which inference nodes can be added to a deduction graph As a user of IMPS however you will never apply primitive 124 inference procedures directly you will only apply them indirectly by apply ing proof commands convenient procedures which add sequent nodes and inference nodes to a deduction graph by calling primitive inferences Proof commands are documented in Chapter 18 12 3 Theorem Proving There are two modes of proving theorems in IMPS interactive mode and script mode Interactive mode is used for proof discovery and interactive experimentation with new proof techniques Script mode is used primarily for proving theorems whose proofs are similar to previously constructed proofs or for checking a large number of proofs To begin an interactive proof select the Start dg option in the menu or use the Emacs command M x imps start deduction IMPS will then prompt you in the minibuffer with the text Formula or reference number which you can supply by clicking the right mouse button on the formula you want to prove provided it is enclosed between double quotes or by typing the reference number of the formula provided it has already been built All the proof commands and node movement commands given dur
188. nlike first order predicate logic LUTINS provides strong support for specifying and reasoning about partial functions i e functions which are not necessarily defined on all arguments including the following mecha nisms e notation for specifying functions e an infinite hierarchy of function types for organizing higher order func tions i e functions which take other functions as arguments e full quantification universal and existential over all function types In addition to these mechanisms LUTINS possesses a definite description operator and a system of subtypes both of which are extremely useful for reasoning about functions as well as other objects The treatment of partial functions in LUTINS is studied in 4 while the treatment of subtypes is the subject of 5 In this chapter we give a brief Pronounced as the word in French 74 overview of LUTINS For a detailed presentation of LUTINS see 16 7 2 Languages A LUTINS language contains two kinds of objects sorts and expressions Sorts denote nonempty domains of elements mathematical objects while expressions denote members of these domains Expressions are used for both referring to elements and making statements about them In this section we give a brief description of a hypothetical language This language will be presented using the mathematical syntax which will be used throughout the rest of the manual There are other syntaxes for
189. ns and rational linear inequalities These routines allow the system to perform a great deal of low level reasoning without user intervention The theory contains several defined entities e g the natu ral numbers are a defined sort and the higher order operators and Il are defined recursively h o real arithmetic is a useful building block for more specific theories If a theory has h o real arithmetic as a subtheory the theory can be developed with the help of a large portion of basic everyday mathematics For example in a theory of graphs which includes h o real arithmetic one could introduce the concept of a weighted graph in which nodes or edges are assigned real numbers We imagine that h o real arithmetic will be a subtheory of most theories formulated in IMPS 290 sequences Sequences over a sort a are represented as partial functions from the natural numbers to a Lists are identified with sequences whose domain is a finite initial segment of the natural numbers The basic operations on sequences and lists including nil car cdr cons and append are formalized as quasi constructors 291 Glossary Alpha equivalence Two expressions are alpha equivalent if one can be obtained from the other by renaming bound variables Application An expression whose lead constructor is named apply Ap plications must have at least two components The first component of an application is called the operator and the remaining compone
190. nt sequent node which match any argument 130 x arg arg The set of assumptions regarded as strings of the current sequent node which match no argument e If the expression is a list whose first element is not an expression operator its value is the list of values of the arguments 12 5 The Script Interpreter A script is a list form form of script expressions The interpreter executes each form in the script in left to right order Once a form is executed by the script interpreter at a sequent node S execution of the script continues at a new sequent node j called the natural continuation node of the script This node is usually the first ungrounded relative of S after the form is executed The only exception is when the form is a node motion keyword form The rules for script interpreter execution are given below Interpreting a script expression form usually causes side effects on the current deduction graph and other structures associated to the current proof The side effects depend on the kind of form being handled by the interpreter Keyword Forms Recall that a keyword form is a script expression which is a list whose first element is a keyword The execution of keyword forms depends on the keyword e Node motion forms These forms cause script execution to continue at a node other than the natural continuation node The following are the node motion keyword forms move to sibling n This cau
191. nt tag than the name selected For example the definition of the theory partial order contains the axiom prec transitivity 4 3 Using Menus Almost all user interaction with IMPS can be initiated using menus The method of menu invocation as well as the menu format depends on the version of Emacs you are using e Free Software Foundation version 19 and Lucid version 19menus are invoked by clicking on the menubar The menus are of the more famil iar pull down variety available on most home computers The resulting menu has a label plus a number of options In the case of Lucid Emacs some of the options open up to new submenus 42 e Version 18 menus are invoked by clicking the right mouse button on the mode line Moreover the menu consists of one or more panes which are stacked like cards each individual pane has a label plus a number of options The options available to the user are determined by the buffer of the selected window The following is a partial list of the options associated to the two IMPSs related buffer modes e Scheme Mode This is the mode used for files of def forms The fol lowing are some of the options that can be selected from the menus in this mode Start a deduction graph Set the current theory Insert a def form template Insert a proof script Run a proof script by line or by region e Sequent Mode This is the mode used for examining sequent nodes in Emacs buffers The follow
192. nt to a logi cally equivalent sequent The theory specific methods include algebraic sim plification deciding rational linear inequalities and applying rewrite rules 279 simplification with minor premises Parameters None Description This primitive inference procedure is the same as simpli fication except that instead of failing when convergence requirements are not verified it posts the unverified convergence requirements as additional subgoals to be proved sort definedness Parameters None Description This primitive inference procedure applies to a sequent whose assertion is a definedness statement of the form t a The primitive inference procedure first tests whether the context entails the definedness of t in o If the test fails the primitive inference procedure then tries to reduce the sequent to a set of simpler sequents In particular when is a conditional term if y to t1 it distributes the sort definedness assertion into the consequent and alternative If t and t are not themselves conditional terms the new subgoal has the assertion if form y to 0 t 0 If one or both of them is a conditional term then the sort definedness assertion is recursively distributed into the consequents and alternatives theorem assumption Parameters A formula which must be a theorem of the context theory Description This primitive inference procedure adds the argument the orem to the context of th
193. nts are called arguments Applications are usually denoted by prefixing the operator to the arguments enclosed in parentheses as f 21 2 n However other forms such as infix for algebraic operations are also used Beta reduction An inference rule which plugs in the values of lambda applications For example beta reduction transforms the expression Aa y bf Z 6 y 1 2 to 13 Buffer An Emacs data structure for representing portions of text for ex ample text files which are being edited To the user a buffer has the appearance of a scrollable page More than one buffer may exist at a given time in an Emacs session Users will also use buffers to build edit and evaluate def forms Command form An s expression command name arg arg used in proof scripts The number and type of arguments is command dependent If the command takes no arguments then the form command name is also valid 292 Compound expression An expression with a constructor and a pos sibly empty list of components 1 2 is a compound expression whose constructor is named apply and whose components are 1 2 Constant A kind of IMPS expression For example in the theory named h o real arithmetic the expressions 1 2 are constants Constructor One of the 19 logical constants of LUTINS Constructors are used to build compound expressions Context An IMPS data structure representing a set of of formulas to be used as assumptions Cont
194. nvironment let macete name compound macete specification This form adds a macete with name name The value of name is this name in the current execution environment let val name expression The value of name is this name in the current execution environment e Deduction graph node labels label node name This form assigns the label name to the current node All these forms modify the current execution environment e Comments script comment comment string Adds a comment to the preceding history entry This keyword form has no other effect Other Forms Execution of any other form form in a script has the following result The value of form must be a command form which is applied to the current node In other words 133 e If the value of form is a symbol this value should be the name of a command which takes no arguments otherwise an error results The script interpreter then applies that command to the current sequent node If the value of form is a list the first expression of the list must be the name of a command while the remaining elements should be ar guments of the command otherwise an error results The script in terpreter then applies that command with the resulting arguments to the current sequent node The following are possible arguments to a command e A symbol Depending on the command and the location of the argu ment this symbol may refer to a theorem a macete a transla
195. o build an s expression from the input tokens it is necessary to dis ambiguate the tokens which are operators from the tokens which are argu ments The association of tokens to operators is determined by the operator 2Note that the word operator is being used here in a different sense than it is used in logic an operator is simply a token which is parsed as the first element of a list 159 Exp Aexp Oxp Oxp Function application Exp BInfxOp Exp Binary infix application Oxp Parenthesized Oxp Exp oo Exp Composition Oxp Oxp Oxp Oxp not Exp Exp and Exp Exp or Exp Exp implies Exp Exp iff Exp Binder Binding Exp Binders including with iota Atom Sort Exp if Exp Exp Exp Requires an odd number of Exp Qc Exp Prefix quasi constructor Exp Qc Exp Sort Prefix quasi constructor Exp Sort Undefined from sort Exp Sort Sort definedness assertion Exp Definedness assertion Oxp Exp Operator or expression PrefxOp LogfxOp BInfxOp PostfxOp Aexp Num Numerical constants Atom Variables amp other constants Table 16 1 Description of String Syntax 1 160 Sort z Asort These are base sorts Sort Sort N ary function sort constructor Binder lambda forall forsome with Binding Sortdecl Sortdecl Atom Sort PrefxOp comb Combinatorial coefficients lim Limit operator for sequences LogfxO
196. o so progresses script form True if script form applied to cur rent sequent node makes any progress May cause side effects on the deduction graph and is usually intended to do so not test form True if test form fails May cause side effects on the deduction graph and test form test form True if all test form are true May cause side effects on the deduction graph or test form test form True if at least one test form is true May cause side effects on the deduction graph e Blocks block script form script form A block form merely provides a grouping for a list of script forms e Iteration forms These are of two kinds 132 Range iterations provide for execution over a specified range of nodes These have the form for nodes range form script form range form can be one of the following unsupported descendents minor premises node and siblings Conditional iterations provide for execution while a specified con dition holds These have the form while test form script form where test form is specified in the same way as for conditional forms e Skip skip This is a form used to insert in locations where at least one script form is required It is essentially equivalent to block e Assignments let script name arg count script This form adds a command with name name The value of name is this name in the current execution e
197. o the entry Next micro exercise and then release the mouse button At any point in this sequence of exercises you can always restart the exercise you are working on advance to the next exercise or return to the previous one by selecting the appropriate entry under IMPS Help 5 1 A Combinatorial Identity The first four micro exercises use variants of a single formula which IMPS prints through T X in the form shown in Figure 5 1 The word implica tion here asserts that the implication that follows holds between the bul leted items Similarly the word conjunction on the next line refers to the conjunction of the following subbulleted items The symbol gt which we will encounter later asserts that the the following items are equivalent This formula asserts that the comb function 4 often read m choose k may be computed by Pascal s triangle in which each entry is the sum of 44 the two entries above it In our development 7 is defined to be equal to m k m k for any integers m and k The proof of our combinatorial identity will involve unfolding the definition of comb and using a number of algebraic laws including the recursive properties of factorial Because of the role of division here and the fact that we must avoid division by zero we will also need to reason about the well definedness of several expressions The exercises will involve carrying out portions of the proof several times At firs
198. ommand kind Single inference Description This command is equivalent to disabling all quasi construc tors and then calling simplify Related commands beta reduce insistently insistent direct inference simplify Remarks There is rarely any need to use this command It has the disagreeable effect of exploding quasi constructors simplify with minor premises Script usage simplify with minor premises Interactive argument retrieval None 260 Command kind Single inference Description This command is the same as simplify except that instead of failing when convergence requirements are not verified it posts the un verified convergence requirements as additional subgoals to be proved Related commands beta reduce with minor premises simplify Remarks This command is useful for identifying convergence require ments that the simplifier cannot verify sort definedness Script usage sort definedness Interactive argument retrieval None Command kind Single inference Description This command applies to a sequent whose assertion is a definedness statement of the form t o The command first tests whether the context entails the definedness of t in If the test fails the command then tries to reduce the sequent to a set of simpler sequents In particular when is a conditional term if y to t1 it distributes the sort definedness assertion into the consequent and alternative If ty and t are not them
199. on briefly describes most of the ways interpretations are used in IMPS for formalizing mathematics and proving theorems 9 5 1 Transporting Theorems The most important use of theory interpretations is for transporting theo rems from one theory to another There are several ways that a theorem can be transported 1 The translation of a theorem of T via an interpretation of 71 in Ta can be installed in 72 using def theorem with the modifier argument translation 2 In the course of a proof the translation of a theorem can be added to the context of a sequent with the proof command assume transported theorem Similarly an instantiation of a translation of a theorem can be added with instantiate transported theorem Both of these commands ask for the theory interpretation to be used If no interpretation is given with the command instantiate transported theorem IMPS will try to find or build an interpreta tion on its own using the information in the variable instances supplied by the user 98 3 When a transportable macete or transportable rewrite rule is applied a theorem is effectively transported to the current theory but it is not actually installed in the current theory Theorems are usually transported from an abstract theory to a more con crete theory 9 5 2 Polymorphism Constructors and quasi constructors are polymorphic in the sense that they can be applied to expressions of several different types This sort o
200. on is an atomic formula or negated atomic formula containing a specified occurrence of an iota expression The command reduces the sequent to an equivalent sequent in which the specified iota expression occurrence is eliminated An iota expression is an expression whose lead constructor is iota or a quasi constructor that builds an iota expression Conclusion T gt w Major Premise T gt Jy 0 yly Z tree AVz 0 pl2 Ultree D z y AV Conclusion T gt 4 Major Premise T gt Jy 0 y y 2 free AVz 0 plz tltree D z y gt Jy 0 ply tltree ay Notes 243 Y is an atomic formula e ix 0 p is the i th iota expression occurrence in w an atomic formula 1 is the result of replacing the i th iota expression occurrence in w with y The occurrence of x 0 y in y is within some argument component s of Y Moreover the occurrence is an extended application component of s where a is an extended application component of b if either a is b or bis an application of kind and a is an extended application component of a component of b Related commands eliminate defined iota expression Remarks If y is an equation or a definedness expression the macete eliminate iota macete is more direct than eliminate iota enable quasi constructor Script usage enable quasi constructor quasi constructor Interactive argument retrieval e Quasi constructor name The nam
201. on syntactic form 47 5 3 Taking More Steps Under the IMPS Help menu please select the next micro exercise You will now see the combinatorial identity displayed as the goal of a new deduction Step 1 Under the Extend DG menu please select the item Commands this function may also be invoked without menus by typing a This will cause IMPS to examine which proof steps other than macetes are applicable to the current sequent Of the 70 commands currently loaded only 16 are possible given the syntactic form of the goal They will be displayed on a menu Move your mouse to the item unfold single defined constant and click on it this function may also be invoked without menus by typing a lower case u IMPS will prompt at the bottom of the screen for the numerical index of the occurrence to unfold This is a zero based index Please unfold the leftmost occurrence by typing 0 followed by a carriage return Result IMPs will post a new sequent with the leftmost occurrence re placed by its definition This is identical to the formula you started the first micro exercise with Step 2 Invoke the macete left denominator removal again This may be done as before by using the macete description item Alternatively it is less cumbrous to find Macetes with minor premises entry under Extend DG Clicking on this will put up a menu of names of the currently applicable macetes Click on left denominator removal for equalities Result IMPs
202. onclusion T gt gi A AQn Premises 1 lt i lt n TU qg1 yi 1 gt Yi Conclusion T gt yV Ven Premise T U ny1 Pn 1 gt Pn Conclusion T gt p Y Premises TU p gt Y PU y gt Conclusion T if form y y 0 Premises TU p gt Y PU 0 gt 9 Conclusion T gt V21 01 Un 0n P Premise p Notes e is obtained from y by renaming the variables among 21 Tn which are free in both p and the context T disjunction elimination Parameters A sequent node Description NO DESCRIPTION eliminate iota Parameters A path p to an iota expression occurrence in the assertion Description This primitive inference procedure applies to a sequent whose assertion is an atomic formula or negated atomic formula contain ing a specified occurrence of an iota expression The command reduces the sequent to an equivalent sequent in which the specified iota expression oc currence is eliminated 274 Conclusion T gt w Major Premise IT 3y 0 oly 2ltree AVz 0 z Zltree DZS y A Y Conclusion T gt 4 Major Premise T gt 3y 0 ply t tree AV2 0 y 2 2 free D z y gt Jy 0 ply zltree 2 4 Notes e y is an atomic formula e x 0 pis the expression located at the path p in y e 1 is the result of replacing the i th iota expression occurrence in w with y The occurrence of x 0 y in y is within some argument component s of Y Moreo
203. ontained in the terms t1 tn Related commands assume transported theorem instantiate theorem Remarks IMPS can often find an appropriate theory interpretation auto matically when the home theory of the theorem is a generic theory i e a theory which contains neither constants nor axioms instantiate universal antecedent Script usage instantiate universal antecedent assumption instan tiations assumption can be given as an integer i or a string o and instan tiations is a list of strings denoting expressions 253 Interactive argument retrieval e O based index of universal antecedent formula Cii la in i The 11 12 1 are the indices of the universal assumptions of the sequent node In case there is only one universal antecedent formula this argument request is omitted e Instance for variable x of sort 01 tj e Instance for variable 2 of sort on tn n gt 1 Command kind Multi inference Description This command instantiates the i th assumption of the con text of the given sequent provided the assumption is a universal statement Conclusion PUAN GHC 5 Uni Y gt Major Premise rufy gt p Minor Premises 1 lt i lt n T gt t ci Notes e The index of the assumption Vx1 01 Tn 0n Y in the context TU IO e En On Y is i e 1 is the result of simultaneously replacing each free occurrence of x1 in w with t for each 7 with 1 lt i lt n if n
204. or premise which has the cut formula as the assertion The minor premise can be proved by instantiating y with f a To proceed with this part of the proof you will need to establish the definedness of f a For a precise description of the sequent nodes added by cut see the documentation on the command cut with single formula e To deal with the major premise do an antecedent inference on the cut formula to remove its existential quantifier This yields a new goal with an assumption of the form f a v e Backchain repeatedly on f a v This replaces all occurrences of f a with v Incorporate the antecedent f a v and apply the iota free char acterization of f as a macete This should replace all such oc currences with some condition not involving f and more impor tantly not involving iota 4 The iota p constructor is a definite description operator for objects of kind x It has a different semantics than iota if there is no unique x of sort a satisfying a unary predicate y then tpx a p is defined like all expressions of kind but has the value F a There is currently no support in IMPS for reasoning about the iota p This should not cause you any concern because iota p has little practical value 155 Chapter 16 Syntax Parsing and Printing The purpose of this chapter is threefold 1 To explain the relation between syntax and IMPS expressions 2 To explain the default syntax which we refer to as the
205. ories that contain no nonlogical axioms ex cept possibly the axioms of the theory of the reals These theories are used for reasoning about objects such as sets unary functions and sequences 1 4 Acknowledgments IMPS was designed and implemented at The MITRE Corporation under the MITRE Sponsored Research program Ronald D Haggarty Vice President of Research and Technology deserves special thanks for his strong unwa vering support of the IMPS project 19 Several of the key ideas behind IMPS were originally developed by Dr Leonard Monk on the Heuristics Research Project also funded by MITRE Sponsored Research during 1984 1987 Some of these ideas are described in 20 The IMPS core and support machinery are written in the T programming language 18 23 developed at Yale by N Adams R Kelsey D Kranz J Philbin and J Rees The IMPS user interface is written in the GNU Emacs programming language 25 developed by R Stallman We are grateful to the Harvard Mathematics Department for providing an ftp site for IMPS 20 Chapter 2 Distribution IMPS is available without fee via anonymous ftp under the terms of a public license at math harvard edu IMPS runs under the X Window System or OpenWindows on Sun 4 SPARCstations that have at least 24 MB physical memory preferably more and at least a 60 MB swap partition The first section of this chapter describes how to get and install IMPs report bugs and join the IMP
206. orms that perform algebraic manipulation use specially coded procedures 138 they are applied to expressions in a way that may not be easily expressed as patterns Nevertheless their validity like the validity of rewrite rules depends on theorems many of which are universal unconditional equalities e g associative and commutative laws 13 4 Algebraic Processors Instead of providing a fixed set transforms for manipulating expressions in a limited class of algebraic structures we have implemented a facility for automatically generating and installing such transforms for general classes of algebraic structures This is possible since algorithmically the transforms are the same in many cases only the names have to be changed so to speak The algebraic manipulation transform is one component of a data structure called an algebraic processor An algebraic processor has either two or three associated transforms There is one transform for handling terms of the form f a b where f is one of the algebraic operations in the processor definition A separate transform handles equalities of algebraic expressions Frequently when the structure has an ordering relation there is a third transform for handling inequalities of algebraic expressions When an algebraic processor is created the system generates a set of formulas which must hold in order for its manipulations to be valid The processor s transforms are installed in a theory 7 only i
207. ory This section contains two principle theories groups and group actions The section includes a proof that the quotient of a group by a normal sub group is itself a group Also several interpretations of group actions in groups are defined 8 basic monoids This section contains the theories monoid theory and commutative monoid theory In monoid theory a constant monoid prod is defined recursively as the iterated product of the primitive monoid operation Ba sic properties of this constant are proved in monoid theory and then are transported to theories with their own iterated product operators such as h o real arithmetic with the operators gt and J 283 binary relations Binary relations are represented in this section as certain partial functions in the same way that sets are represented as indicators Several basic op erations on binary relations are formalized as quasi constructors As an exercise the transitive closure of the union of two equivalence relations is shown to be an equivalence relation binomial theorem This section proves the combinatorial identity and the binomial theorem for fields counting theorems for groups This section contains a proof of the fundamental counting theorem for group theory Several consequences of this theorem are proved including Lagrange s theorem foundation This section is always loaded with Imps It contains the theory h o real arithmetic and a number of
208. ota expression This command which is described in Chapter 18 is the best iota elimination tool in IMPS Generally you should use it whenever you want to eliminate an iota expression whose definedness is implied by the sequent s context It can also be used effectively in some cases on an iota expression whose definedness is not implied by the sequent s context This is done by applying case split with E V E followed by applying eliminate defined iota expression on the E case The eliminate defined iota expression command is multi inference it adds about 20 new sequent nodes to a deduction graph 15 2 2 eliminate iota This command is also described in Chapter 18 It is a single inference com mand that is applicable to just atomic and negated atomic formulas You should use it when you want to eliminate an iota expression whose defined ness is not implied by the sequent s context 15 2 3 eliminate iota macete This is a compound macete with built in abstraction specified by def compound macete ELIMINATE IOTA MACETE sequential iota abstraction macete series tr defined iota expression elimination tr negated defined iota expression elimination tr left iota expression equation elimination tr right iota expression equation elimination 152 beta reduce The four elimination theorems are in the file IMPS theories generic theories iota t You should try eliminate iota macete when the asser tion has one of th
209. oups constants a sets gg b sets gg def theory LCT THEORY language lct language component theories groups axioms a is a subgroup subgroup a b is a subgroup subgroup b def theorem LITTLE COUNTING THEOREM f_indic_q gg subgroup implies f_card a set mul b f_card fa inters b f_card a f_card b forall b a setsl gg lt 3 subgroup a and subgroup b pe implies F f_indic_q gg subgroup o implies see f_cardf a set mul b f_card a inters b aA f_card a f_card b theory groups home theory lct theory usages transportable macete proof show that the little counting theorem is proved in an extension of groups but is installed in groups by generalizing over the constants a and b 9 5 8 Model Conservative Theory Extension Suppose Ta is an extension of 71 Ta is a model conservative extension of T if every model of 71 expands to a model of T Model conservative 104 extensions are safe extensions since they add new machinery without com promising the old machinery For instance a model conservative extension preserves satisfiability The most important model conservative extensions are definitional extensions which introduce new symbols that are defined in terms of old vocabulary Logically IMPs definitions create definitional extensions Many natural methods of extending theories correspond to a class or type of model conservative extensions For instan
210. p BInfxOp lt lt i in i subset PostfxOp Table 16 2 Description of String Syntax 2 Atom TextChar followed by TextChar s or Digit s SpecialSeq SpecialSeq followed by _ and TextChar s or Digit s TextChar s J al z _ amp Digit n O 9 SpecialSeq 7 77 t 1 lt lt gt gt Table 16 3 Description of Atoms 161 Operator Binding 100 110 120 121 140 160 80 80 i subset 101 i in 101 gt 80 gt 80 lt 80 lt 80 not 70 iff 65 implies 59 and 60 or 50 Table 16 4 Operator Binding Powers binding powers For example the string x 2 3 is parsed as apply x apply 2 3 because the operator has a higher binding power than Table 16 4 is a list of the bindings of some common operators 16 5 Modifying the String Syntax The string syntax can be modified or extended using the def forms def parse syntax and def print syntax The use of def forms is documented in Chapter 17 162 16 6 Hints and Cautions 1 A parsing error is indicated by an error message Error Parsing error This means IMPS was unable to build an s expression from your in put IMPS will provide some indication as to where the error occurred Following are some examples of common parsing errors gt qr with a b rr a b Error Parsing erro
211. p s iff p nil ind_1 and forall s nn ind_1 e ind_1 f_seq_q s and p s implies p cons e s theory sequences base case hook simplify def language Positional Arguments language name A symbol Keyword Arguments embedded languages name name name is the name of a language or theory embedded language name name is the name of a language or the ory base types type name type name sorts sort spec sort spec sort spec is a list of the form sort enclosing sort called a sort specification sort must be a symbol and enclosing sort must satisfy one of the following It occurs in a previous sort specification It is a sort in one of the embedded languages It is a compound sort which can be built up from sorts of the preceding kinds extensible type sort alist type sort alist type sort alist is a list of the form numerical type name sort numerical type name is the name of a numerical type that is a class of objects defined in 185 T For example integer type and rational type are names of numerical types This keyword argument is used for defining self extending languages This is a language that incorporates new formal symbols when the expression reader encounters numerical objects of the given type e constants constant spec constant spec constant spec is a list constant name sort or compound sort Description Th
212. pX processor This flexible arrangement means users can freely change from one syntax to another even during the course of an interactive proof 16 2 Controlling Syntax The process of building an IMPS expression from user input can be broken up into two steps 1 Parsing a string into an s expression s 2 Building an IMPS expression from the s expression s Similarly the process of displaying an expression also consists of two parts 1 Building an s expression s from an IMPS expression 2 Providing some representation of s as a string The phases string to s expression for reading and s expression to string for printing are under direct user control They can be modified by resetting the following switches e imps reader is a T procedure which takes a language and a port and returns an s expression If proc is a procedure of this type you can reset the imps reader switch by evaluating set imps reader proc e imps printer is a procedure which takes an s expression and a port and prints something to this port If proc is a procedure of this type you can reset the imps printer switch by evaluating set imps printer proc 157 To write your own reader and printer procedures you will have to do some programming in the T language However some reader and printer pro cedures are particularly easy to write For example to write your own reader and printer for s expression syntax you could evaluate the
213. pair in a given interval if one exists A more extensive treatment of primes including the material of this exercise is included in the IMPs theory library in the file IMPS theories reals primes t That file also contains statements and proofs of the following e the infinity of primes e the main properties of gcd e the existence and uniqueness of prime factorizations the Fundamental Theorem of Arithmetic 1A macete meaning a clever trick in Portuguese slang is a lemma or group of lemmas made available to the user for various kinds of rewriting depending on syntactic form 62 Purpose This exercise illustrates basic definitions and it illustrates how to carry out several simple proofs Its main interest however is to illustrate the mix of computation and proof in IMPS This balance is reflected in the macete mechanism and in the script that searches for a pair of twin primes 6 2 2 A Very Little Theory of Differentiation Contents This file develops a little axiomatic theory of the derivative operator on real functions Its axioms include the rules for e sum e product e constant functions e the identity function as well as the principle that the derivative of f is defined at a value x only if f is Naturally these properties hold true of the derivative as explicitly defined in the usual way The exercise then develops a succession of consequences of these prop erties such as the power rule shown in Figur
214. plication in Script Mode For the precise definition of what a script is see the section on the proof script language in Chapter 12 Essentially a proof script is a sequence of forms of the following kinds e keyword az an e command name ay Gn Each command form that is a form which begins with a command name instructs IMPS to do the following two things 219 e Apply the command with name command name to the current sequent node with the arguments a an e Reset the current sequent node to be the first ungrounded relative To apply a single command in script mode to the current sequent node place the cursor on the first line of the command form and type C c 1 In order for the interface software to recognize the form to execute there cannot be more than one command form per line However a single command form can occupy more than one line To apply in sequence the command forms within a region type C c r 220 antecedent inference Script usage antecedent inference assumption assumption can be given as an integer 1 or a string o Interactive argument retrieval e O based index of antecedent formula ii i2 in i The 71 2 are the indices of the assumptions of sequent node on which antecedent inferences can be done that is an implication conjunction disjunction biconditional conditional formula or an ex istential formula In case there is only one such formula this argument reque
215. predicate in 7 intended to specify the extension of the new sort 6 can be installed in 7 only if the formula 3x U x is known to be a theorem of T As an example the pair N Ar Zi 0 lt 2 defines N to be an atomic sort which denotes the natural numbers Constant definitions are used to define new constants from defined ex pressions They are created with the def constant form A constant def inition for T is a pair 6 n e where n is a symbol intended to be the name of a new constant of 7 and e is a expression in 7 intended to specify the value of the new constant can be installed in 7 only if the formula el is verified to be a theorem of 7 As an example the pair floor Ax R 2 Z 2 lt xAtr lt 1 2 defines the floor function on reals using the constructor Recursive function definitions are used to define one or more functions by simultaneous recursion They are created with the def recursive constant form The mechanism for recursive function definitions in IMPS is modeled on the approach to recursive definitions presented by Y Moschovakis in 22 A recursive definition for T is a pair 6 ni nx F1 Fx where k gt 1 n nf is a list of distinct symbols intended to be the names of k new constants and F Fx is a list of functionals i e functions which map functions to functions of kind ind in 7 intended to specify as a system the values of the new constants 6 can be installed in 7 only i
216. pretation from the theory to itself which translates the theorem to the conjecture As an illustration consider the theory interpretation defined by 99 def translation MUL REVERSE source groups target groups fixed theories h o real arithmetic constant pairs mul lambda x y gg y mul x force under quick load theory interpretation check using simplification This translation which reverses the argument order of x and holds every thing else fixed in groups maps the left cancellation law def theorem LEFT CANCELLATION LAW forall x y z gg x mul y x mul z iff y z theory groups usages transportable macete proof C to the right cancellation law def theorem RIGHT CANCELLATION LAW forall x y z gg y mul x z mul x iff y z left cancellation law theory groups usages transportable macete translation mul reverse proof existing theorem Since this translation is in fact a theory interpretation we need only prove the left cancellation law to show that both cancellation laws are theorems of groups 9 5 4 Problem Transformation Sometimes a problem is easier to solve if it is transformed into an equivalent but more convenient form For example often geometry problems are easier to solve if they are transformed into algebra problems and vice versa Many problem transformations can be formalized as theory interpretations The interpretation serves both as a means of transforming the prob
217. program which is then executed by T This sequence of events usually has a number of side effects on the IMPS environment For example to define a constant named square in the theory h o real arithmetic evaluate the s expression def constant SQUARE lambda x rr x72 theory h o real arithmetic Formal symbol A primitive IMPS expression A formal symbol has no components although it is possible for an expression with no components to be a compound expression A formal symbol can be a variable or a constant Every formal symbol has a name which is used for display The name is a Lisp object such as a symbol or a number Formula Intuitively an expression having a truth value for example Yz y z R lt y y lt zDr lt zZ In IMPS a formula is an expression whose sort is IMPS A formal reasoning system and theorem prover developed at The MITRE Corporation Inference node A node in a deduction graph connecting a conclusion sequent node with zero or more hypothesis sequent nodes that represents an instance of a rule of inference Iota expression A compound expression whose lead constructor is named iota denoted in the mathematical syntax by v An iota expression has the form z o y It denotes the unique object in the sort o which satisfies the condition y if such an object exists Otherwise the iota expression is un defined 294 Kind Each sort and expression is of kind v also written as iota or prop Express
218. qequals A B is well formed in any language containing the language of the kernel theory provided A and B are well formed expressions of the same type of kind 1 Separate from the definition special syntax may be defined for parsing and printing qequals e g as the infix symbol The quasi constructor quasi equals is not actually defined using a def quasi constructor form in IMPs It is one of a small number of system quasi constructors which have been directly defined by the IMPs implemen tors A system quasi constructor cannot be defined using the def quasi constructor form because the schema of the quasi constructor cannot be fully represented as a LUTINS lambda expression This is usually because one or more variables of the schema variables ranges over function expres sions of variable arity or over expressions of both kind and x For ex ample qequals A B is not well defined if A and B are of kind x but quasi equals A B is well defined as long as A and B have the same type regardless of its kind The major system quasi constructors are listed in Table 10 1 10 3 Reasoning with Quasi Constructors There are two modes for reasoning with a quasi constructor Q In the en abled mode the internal structure of Q is ignored For example in this mode when an expression Q F En is simplified only the parts of the internal expression corresponding to the arguments Ey En are simplified and the part correspondin
219. r Illegal token A encountered with a b rr a lt lt b This error occurred because the variable sort specifications have to be followed by a comma gt qr forall a b rr a b Error Parsing error Expecting or or forall a b rr a b lt lt This error results from a missing right parenthesis An error message of one of the following kinds is usually an indication that the current theory this is the value of the switch current theory is different from what you expected This typically happens when you begin an interactive proof of a formula without having set the current theory to its desired value gt qr with x rr x 1 Error QUANTIFIER DECODE VAR SUB LIST RR is not a sort in IMPS basic language 12 THE KERNEL LANGUAGE This error message indicates that IMPS was unable to build an expres sion in the current theory because there is no sort named rr gt qr with x ind x x Error SEXP gt EXPRESSION 1 Cannot locate in IMPS basic language 12 THE KERNEL LANGUAGE 163 This error message indicates that IMPS was unable to build an expres sion in the current theory because there is no constant named To remedy an error of the above type reset the current theory switch by using the menu 164 Part III Reference Manual 165 Chapter 17 The IMPS Special Forms In this chapter we document a number of user forms for defining and mod ifying IMPS objec
220. r definition of a theorem does not depend on the IMPS proof system or any other proof system for LUTINS In the implementation a theory is represented by a data structure which encodes the language and axioms of the theory The data structure also en codes in procedural or tabular form certain consequences of the theory s axioms This additional information facilitates various kinds of low level reasoning within theories that are encapsulated in the IMPS expression sim plifier the subject of Chapter 13 Let 7 and T be IMPS theories T is subtheory of T and T isa supertheory of T2 if the language of T is a sublanguage of the language of T and each axiom of T is a theorem of T Each IMPS theory T is 84 assigned a set of component theories each of which is a subtheory of T T is structural subtheory of Ta and T1 is a structural supertheory of To if Ty is either a component theory of T or a structural subtheory of a component theory of Ta 8 2 How to Develop a Theory The user creates a theory and the IMPS objects associated with it by evalu ating expressions called definition forms or def forms for short There are approximately 30 kinds of def forms each described in detail in Chapter 17 The user interface provides templates to you for writing def forms The def forms supplied by the system and created by you are stored in files which can be loaded as needed into a running IMPS process In this section we gi
221. r several reasons e Once a quasi constructor is defined it is available in every theory whose language contains the quasi constructor s home language That is a quasi constructor is a kind of global constant that can be freely 67 used across a large class of theories A constructor which we also call a logical constant is available in every theory e Quasi constructors are polymorphic in the sense that they can be ap plied to expressions of several different types Several of the construc tors such as and if are also polymorphic in this sense e Quasi constructors are preserved under translation Hence to reason about expressions involving a quasi constructor we may prove laws involving the quasi constructor in a single generic theory The transla tion mechanism can then be used to apply the theorems to expressions in any theory that involve the same quasi constructor e Quasi constructors can be used to represent operators in nonclassical logics such as modal or temporal logics see Section 6 3 2 and op erators on generic objects such as sets as represented by indicators and sequences Quasi constructors are implemented as macro abbreviations The IMPS reader treats them as macros which cause the creation of a particular syntac tic pattern in the expression while the IMPS printer is responsible for print ing them in abbreviated form wherever those patterns may have arisen The exercise derives a few
222. rall a b c rr b lt a and c lt a implies forsome d rr d lt a and b lt d and c lt d theory h o real arithmetic proof direct and antecedent inference strategy instantiate existential max b c unfold single defined constant globally max case split b lt c simplify simplify apply macete with minor premises maximum 1st arg apply macete with minor premises maximum 2nd arg 33 135 Chapter 13 Simplification 13 1 Motivation One of the goals of the IMPS system is to assist users in producing formal proofs in which the number of steps and the kinds of justification used for each step are close to those of a rigorous and detailed but informal proof One of the main reasons that formal proofs are usually so long is that many proof steps involve replacement of an occurrence of a term t with a term to having the same value as t and which is obtained from t by a variety of theory specific transformations A formal proof might require hundreds of steps to justify such a replacement In IMPS the simplifier is designed to handle many of these inferences directly without user intervention and to bundle them into a single inference step The simplifier accomplishes this as follows e By invoking a variety of theory specific transformations on expressions such as rewrite rules and simplification of polynomials given that the theory has suitable algebraic structure such as that of a field e By simplify
223. red as a sort inclusion Strictly speaking this should be a theorem rather than an axiom as it follows from the induction principle Primitive Recursion A data type introduced via the BNF mechanism justifies a schema for defining functions by primitive recursion Roughly speaking a function g of sort T o is uniquely determined if a sort is given together with the following e For each atom a value of sort g e For each constructor c with sort Q1 X X An X 81X X Bm ao 175 a functional of sort OX as WOK Pp Ke X By So is given The primitive recursively defined function g will have the property that g c 11 Tn Y1 gt Ym is quasi equal to DCG Gi sos La Yi Un Thus in effect says how to combine the results of the recursive calls for arguments in the primary type with the values of the parameters from sorts 3 of the underlying theory Additional Theorems A number of consequences of the axioms are in stalled Examples The simplest example possible is def bnf nat theory pure generic theory 1 base type nat atoms zero nat constructors succ nat nat selectors pred The axioms generated from this definition are displayed in Figure 17 1 on page 177 As a more complicated example consider a programming language with phrases of three kinds namely identifiers expressions and statements The data type to be introduced corresponds to set of phrases of all
224. repeatedly until there are no occurrences of directly defined constants A directly defined constant is a constant defined nonrecursively The command beta reduce repeatedly is called after all the unfoldings are performed Related commands unfold defined constants repeatedly unfold directly defined constants unfold recursively defined constants repeatedly unfold single defined constant Remarks This command will always terminate unlike unfold defined constants repeatedly and unfold recursively defined constants repeatedly unfold recursively defined constants Script usage unfold recursively defined constants Interactive argument retrieval None Command kind Multi inference Description This command replaces every occurrence of a recursively defined constant by its respective unfolding The command beta reduce repeatedly is called after all the unfoldings are performed 264 Related commands unfold defined constants unfold directly defined constants unfold recursively defined constants repeatedly unfold single defined constant unfold recursively defined constants repeatedly Script usage unfold recursively defined constants repeatedly Interactive argument retrieval None Command kind Multi inference Description This command replaces every occurrence of a recursively defined constant by its respective unfolding repeatedly until there are no occurrences of recursively defined constants The command beta reduce
225. resented as a function whose domain equals the singleton set a b The basic operations on pairs are formalized as quasi constructors partial orders This section contains the following theories e partial order e complete partial order partial order Language e Base Types uu U in the mathematical syntax denotes the underly ing set of points e Constants prec lt in the mathematical syntax denotes a binary relation on uu Axioms e Transitivity Va b cU a lt bAb cDa xc e Reflexivity Va U a lt a e Anti symmetry Va b U a lt bAb lt ada b 287 Y complete partial order Axioms In addition to the axioms for the theory partial order this theory has the completeness axiom which states that any nonempty set with an upper bound has a least upper bound In a complete partial order it is also true that any nonempty set bounded below has a greatest lower bound pre reals Two IMPS theories of the real numbers are included in the pre reals section e complete ordered field e h o real arithmetic These theories are equivalent in the sense that each one can be interpreted in the other moreover the two interpretations compose to the identity These interpretations are constructed in the section using the IMPS translation machinery Y complete ordered field In this theory the real numbers are specified as a complete ordered field and the rational numbers and integers are specified as substructures of th
226. rization Algorithm for a Compiler 6 43 The Bell LaPadula Exercise 40 40 41 42 44 44 46 48 49 56 57 58 II User s Guide 7 Logic Overview Tel IntrOdUCtIOR sec 8 seo Soe ok ee A ee oy eh een we C2 AUS E A AAA oe ee RS a TZIN SOS Mele oe oe de Bae Wen seh ee bets eS 72 2 Expressions ne adot erana Gea e we eee a eS 7 2 3 Alternate Notation aooaa 0 0004 T3 SEMANTICS aie iaaa a ee ar pa e detent 7 4 Extensions of the Logic aoaaa 7 5 Hints and Cations m ogra un n k a e a A a a an ee eee Theories Sil Introducir ida ee a ag a S 8 2 How to Develop a Theory oaoa a 8 3 Languages e Sd Phersia A sk ws Ns a cet GAN Ea 8 5 Definitions oci a 26 hee Se a a a 8 6 Theory Libraries oaoa 8 7 Hints and Cautions sr Hk EE A Pe a e Theory Interpretations gI Introductions 2 5 ease ch oe hes Se eon ie A A eS 972 Translations 3 4 2 Soar ENE E oct Boao eats a 9 3 Building Theory Interpretations 9 4 Translation of Defined Sorts and Constants 9 5 Reasoning and Formalization Techniques 9 5 1 Transporting Theorems 9 5 2 Polymorphism 2 204 9 5 3 Symmetry and Duality 9 5 4 Problem Transformation 9 5 5 Definition Transportation 9 5 6 Theory Instantiation 04 9 5 7 Theory Extension 0 2 000000 9 5 8 Model Conservative Theory Extensio
227. roofs have more interesting induction hypotheses than in the world s smallest compiler and the development calls for an auxiliary notion of regular instruction sequences Purpose This exercise can be used as a more realistic and open ended example of a computer science verification 6 4 3 The Bell LaPadula Exercise Contents This exercise consists of two files namely e IMPS theories exercises fun thm security t e SIMPS theories exercises bell lapadula t The first file proves the Bell LaPadula Fundamental Theorem of Security in the context of the theory of an arbitrary deterministic state machine with a start state augmented by an unspecified notion of secure state A similar theorem also holds for nondeterministic state machines The proof is by induction on the accessible states of the machine The second file instantiates this theory in the case of a simple access control device reference monitor The states are functions which given a subject and an object returns a pair one component of the pair represents whether the subject has current read access to the object while the other represents current write access The operations of the machine correspond to four requests by a subject concerning an object the request may be to add or delete and access which may in turn be either read or write access The subjects and objects have security levels and the requests are adjudicated based on their levels The t
228. ructure of this subgoal To dispense with the leading for all we will consider an arbitrary k and m To break up the implication we will pull the antecedent into the left hand side of the sequent We refer to this as its context That is we shall try to prove the consequent of the conditional in a context where the antecedent is assumed true Finally we will break up the conjunction so that we can prove each conjunct separately Step 3 To break up the sequent in this way look for direct and antecedent inference strategy under the command menu The com 52 Sequent 9 Let m k Z Assume 0 k lt m 1 1 lt k Then kl 1I 4m 1 07 1 Figure 5 9 The Simpler Definedness Subgoal mand menu may be invoked from Extend DG Result As a consequence nine new sequent nodes will be added to the deduction graph Of these three are leaf nodes and will need to be proved separately They correspond to the three conjuncts of the previous subgoal We will prove one of them in a slightly tedious step by step process and the other two by applying compound macetes The first subgoal Sequent 9 is shown in Figure 5 9 To prove this in a step by step process we will need to use the the following facts 1 the domain of inverse is R 0 2 a product z y is nonzero just in case both x and y are 3 a factorial j is always nonzero We will then use the IMPS simplifier to complete the proof of this subgoal
229. ry def theory Positional Arguments e theory name Keyword Arguments e language language name 199 e component theories theory name theory name e axioms axiom spec axiom spec ariom spec is a list name formula string usage usage where name a symbol is the optional name of the axiom and formula string is a string representing the axiom in the syntax of the language of the theory e distinct constants distinct distinct distinct is a list constant name constant name Description This form builds a theory named theory name The language of this theory is the union of the language language name and the languages of the com ponent theories The axioms of the theory are the formulas represented by the strings in the list axiom spec The distinct constants list implicitly adds new axioms asserting that the constants in each list distinct are not equal Examples def theory METRIC SPACES component theories h o real arithmetic language metric spaces language axioms positivity of distance forall x y pp O lt dist x y transportable macete point separation for distance forall x y pp x y iff dist x y 0 transportable macete symmetry of distance forall x y pp dist x y dist y x transportable macete triangle inequality for distance forall x y z pp dist x z lt dist x y dist y z 200 def theory VECTOR SPACES OVER RR language real
230. s is usually possible if the constant is a function symbol which occurs as an operator of an application In this case the appropriate function symbol may be unambiguously determined from the sorts of the arguments 11 8 Hints and Cautions 1 In principle any theory can be used to build a theory ensemble How ever the theory ensemble facility is useful only if the following two conditions on the base theory are met e The base theory is fairly general so that there are likely to be numerous instances of the base theory Thus it would make little sense to make a theory with essentially only one model into a theory ensemble e There is a need for dealing with at least two distinct instances of the base theory 2 There is a certain amount of overhead in building theory multiples This overhead includes building and tabulating theory replicas and building canonical theory interpretations from the m multiples to n multiples where m lt n Recall that there is a canonical interpretation Bf Um Up for each injective map 0 m 1 gt 0 n 1 There are n n 1 n m 1 such mappings This overhead can become forbidding when the multiples get too large As a general rule multiples of order greater than 4 should be avoided 3 Before the system builds an n multiple it checks whether all j multiples for j lt n already exist building the missing multiples as needed 122 Chapter 12 The Proof Syst
231. s such as and if are also polymorphic in this sense 3 The definition of a translation see Chapter 9 is not directly dependent on the definition of any quasi constructor Consequently translations 107 can be applied to expressions involving quasi constructors that were defined after the translation itself was defined 4 Quasi constructors can be defined without modifying the Imps deduc tive machinery Note that the deductive machinery of a ordinary constructor is hard wired into IMPS 5 Quasi constructors can be used to represent operators in nonclassical logics and operators on generic objects likes sets and sequences 10 2 Implementation Quasi constructors are implemented as macro abbreviations For exam ple the quasi constructor quasi equals is defined by the following bicon ditional Ei 2 E Eil VE2l D E E Hence two expressions are quasi equal if and only if they are either both undefined or both defined with the same value When the preparsed string representation of an expression preparsed string for short of the form Ej Ez is parsed is treated as a macro with the list of arguments E E2 an internal representation of the expression internal expression is built from the preparsed string as if it had the form E VE2 gt Er Ez When an internal expression of the form Eil VE2 D El Ez is printed is used as an abbreviation the printed string representat
232. s of the new type or its subsorts Each range sort must be the new base type or one of its subsorts Each domain sort may belong to the underlying theory or alternatively it may be the new base or one of its subsorts It may not be a higher sort involving the new type e sort inclusions subsort supersort subsort supersort Declare that every element of subsort is also a member of supersort This is not needed when subsort is a syntactic subsort of supersort in the sense that there are zero or more intermediate sorts Q1 Qn such that the enclosing sort of subsort is a1 the enclosing sort of ap is supersort and the enclosing sort of a is a 41 for each i with 1 lt i lt n Description The purpose of the def bnf form is to define a new recursive data type to be added as a conservative extension to some existing theory The members of the new data type are the atoms in the declaration together with the objects returned constructed by the constructor functions We will use the 7 to refer to the base type symbols such as a will stand for any sort included in the base type such as the base sort 7 itself 6 will be used for any sort of the underlying theory 173 The logical content of a data type definition of this kind is determined by two main ideas e No Confusion If cy and c are two different constructor functions then the range of cp is disjoint from the range of c1 If a and b are two atoms then a
233. s provided or ensemble name otherwise 2 The fixed theories are those given in the fixed theories keyword ar gument list if the fixed theories keyword argument is provided or those theories in the global fixed theories list at the time the form is evaluated Remarks If there is already a theory ensemble with name ensemble name but with different fixed theories set or different renamer an error will result Examples def theory ensemble METRIC SPACES def theory ensemble instances Positional Arguments e ensemble name An error will result if no ensemble exists with en semble name Keyword Arguments e target theories nameg nameyn 1 For each i name must be the name of a theory 7 or an error will result e target multiple N N must be an integer This is equivalent to giving a keyword argument target theories namep namen_ 1 where name is the name of the i th theory replica The target multiple and target theories keyword arguments are exclusive e sorts sort assoc sort assoc sort assoc is a list sort sorto sortn 1 where sort is an atomic sort in the base theory of the ensemble and sort is either 202 A sort specification in the theory Tor A string representing a quasi sort in 7 In particular the length of each sort assoc entry must be one more than the number N of theory entries given in the target theories keyword argument This argument is valid only in case the t
234. s the set of all partial functions f Do X X Dan gt Dangi 4 If a aj Qn Qn41 is of kind x then Da is the set of all to tal functions f Dra X X Dean gt Dany Such that for all bi T On Dilan XX Dran Fl O bn Fr an41 whenever bi Z Da for at least one i with 1 lt i lt n For a type a S of kind x Fa is defined inductively by 79 1 F F 2 Ifa a1 an 1 then Fa is the function which maps every n tuple a E Dar X0 X Dan tO Fangi A model for L is a pair Da a S I where Da a S is a frame for S and J is a function which maps each constant of of sort a to an element of Da Let M Da a S I be a model for L A variable assign ment into M is a function which maps each variable x a of to an el ement of Da Given a variable assignment y into M distinct variables Tons En Qn n gt 1 and ay E Dazs an E Dan let p 11 07 gt 47 Enin an be the variable assignment 4 such that ai if A zia for some i with1 lt i lt n VAS l A otherwise V V is the partial binary function on variable assignments into M and expressions of defined by the following statements 1 Vo x a y z a 2 If A is a constant V A I A 1 2 3 Vo T T 4 Vo F F o T if VA F g Kolala F EA 6 V AD B oo F or V B T 7 V A B E pee V B VB if V A 2 V C otherwise
235. selves conditional terms the new subgoal has the assertion if form y to 0 t a If one or both of them is a conditional term then the sort definedness assertion is recursively distributed into the consequents and alternatives Related commands definedness Remarks This command is mainly useful when is an application a function or a conditional term 261 sort definedness and conditionals Interactive argument retrieval None Command kind Multi inference Description This strategy invokes sort definedness Insistent direct in ference and repeated beta reduction are then invoked followed by case split on conditionals applied to the first conditional term Related commands sort definedness Remarks This command is useful for a goal t 7 when the definition of involves a conditional term unfold defined constants Script usage unfold defined constants Interactive argument retrieval None Command kind Multi inference Description This command replaces every occurrence of a defined con stant by its respective unfolding The command beta reduce repeatedly is called after all the unfoldings are performed Related commands unfold defined constants repeatedly unfold directly defined constants unfold recursively defined constants unfold single defined constant Key binding C c u unfold defined constants repeatedly Script usage unfold defined constants repeatedly 262 Interactiv
236. sequence of keystrokes enclosed in parentheses This means that these options can also be invoked directly using these keystrokes As you become more familiar with IMPS you will probably want to use these more direct invocations Note that you can use the menus to change buffers or modify the number of windows on the screen IThis is the preferred version of Emacs 28 You should also be aware that the panes which appear on the menu and the options within each pane usually depend on the window you clicked on to bring up the menu 3 2 On line Documentation The following documentation is available on line e The User s Manual If you have a TRX previewer the IMPS manual is available on line You can locate specific items in the manual by clicking right on the option IMPS manual entry in the pane Help e Def forms A def form is essentially a specification of an IMPS entity In the course of your interaction with IMPS you may want to exam ine the definition of some object You can locate the def form which specifies it by clicking right on the option Find def form C in the pane Help For more details on on line documentation see Chapter 4 3 3 Languages and Theories For now you can think of a theory as a mathematical object consisting of a language and a set of closed formulas in that language called axioms For example one of the last things that was printed out in the startup procedure was the line Current theor
237. series tr defined iota expression elimination tr negated defined iota expression elimination tr left iota expression equation elimination tr right iota expression equation elimination beta reduce def constant Positional Arguments e constant name The name of the constant to be defined constant name is also the name of the newly built definition e defining expr string Keyword Arguments e theory theory name Required e sort sort string e usages symbol symbol Description This form creates a new constant c called constant name and a new axiom of the form c e with usage list symbol symbol where e is the expression 181 specified by defining expr string The sort o of cis the sort specified by sort string if there is a sort argument and otherwise is the sort of e The new constant and new axiom are added to the theory T named theory name provided e constant name is not the name of any current constant of T or of a structural supertheory of T and e the formula e 0 is known to be a theorem of T Examples def constant ABS lambda r rr if O lt r r r theory h o real arithmetic def constant gt lambda x y rr y lt x theory h o real arithmetic usages rewrite def constant POWER ZOF ZTWO lambda x zz 2 x sort zz zz theory h o real arithmetic def imported rewrite rules Positional Arguments e theory name Keyword Arguments e source
238. ses execution to proceed at the n th sibling node move to ancestor n This causes execution to proceed at the n th ancestor node move to descendent l 1 This causes execution to proceed at the specified descendent node Each l is an integer or a dotted pair a b of integers Given the way scripts are usually presented on a page this really means from top to bottom 131 jump to node label label is a deduction graph sequent node label e Conditionals if test form consequent alternative These are forms which provide conditional execution of command forms The test form can be of the following kinds matches assertion assumption list assumption list where assertion and assumption list are script expressions The condition is true if the value of assertion matches the assertion of the current sequent node and every formula in the value of assumption list matches an assumption of the current sequent node minor True if the current sequent node is the minor premise of some inference node major True if the current sequent node is the major premise of some inference node generated by rule rule name True if the current sequent node is an assumption of an inference node with name rule name succeeds script form True if script form applied to current sequent node grounds it May cause side effects on the deduction graph and is usually intended to d
239. so be the name of a theory e fixed theories theory name theory name Description This form builds a quasi constructor named name from the schema spec ified by lambda expr string which is a lambda expression in the language named language name The sorts in the theories named theory name theory name are held fixed 189 Examples def quasi constructor PREDICATE TO INDICATOR lambda s uu prop lambda x uu if s x an individual unit sort language indicators fixed theories the kernel theory def quasi constructor GROUP lambda a sets gg mul g8 88 881 eh 88 inv gg gg forall x y gg x in a and y in a implies mul x y in a and ef in a and forall x gg x in gg implies inv x in gg and forall x gg x in a implies mul e x x and forall x gg x in a implies mul x e x and forall x gg x in a implies mul inv x x e and forall x gg x in a implies mul x inv 4 x e and forall x y z gg x in a and y in a and z in a implies mul mul x y z mul x mul y z language groups def record theory Positional Arguments e theory name The name of a theory Keyword Arguments e type symbol Required e accessors accessor specy accessor spec accessor spec is a list accessor name target sort 190 Description NO DESCRIPTION Examples def record theory ENTITIES AND LEVELS type access accessors read prop
240. sort def constant and def recursive constant but they can also be created by transporting definitions to the theory from some other theory with def transported symbols An atomic sort with constants for representing a cartesian product with a constructor and accessors is created with def cartesian product See Section 8 5 for details 86 Task 6 Macetes Theorems are applied semi automatically in the course of a proof by means of procedures called macetes A set of carefully crafted macetes is an es sential part of a well developed theory An elementary macete is created whenever a theorem is installed and a transportable macete is created by installing a theorem with the usage transportable macete Other kinds of macetes are created with def compound macete and def schematic macete See Chapter 14 for details Task 7 Induction Principles If your theory has a theorem which you think can be treated like an induction principle then you can build an inductor with def inductor The name of the inductor can be used as an argument to the induction command Note that most often you can get by with using integer inductor which is already supplied with the system Task 8 Theory Ensembles Sometimes copies and unions of copies of the theory are needed These can be created and managed as an IMPS theory ensemble with def theory ensemble def theory ensemble instances def theory ensemble overloadings and def theory ensemble multiple Se
241. specified in the file imps el frame specs el Background colors and the default font have been commented out You will probably want to modify these specifications to suit your own taste To do this first copy the file frame specs el to home imps imps emacs el where home is your home directory and imps is a subdirectory of your home directory that is created when you first run IMPS Then change the frame specifications in this file as you like To subscribe to the IMPS mailing list send your name and e mail address to imps requestOlinus mitre org We strongly urge that all users of IMPS subscribe to the IMPS mailing list 2 1 4 How to Start IMPS To run IMPS start X or OpenWindows and then execute start_imps amp 2 1 5 The IMPS Users Manual The IMPS user s manual is written in TX and is available on line The dvi file of the manual is located in the directory imps doc manual Also both dvi and ps files of the manual are located in the imps directory at math harvard edu The manual is approximately 300 pages long 2 1 6 IMPS Papers In the imps doc directory at math harvard edu there are several papers on IMPS in compressed TX dvi and ps formats 24 2 1 7 Bug Reports and Questions Please mail information about bugs or problems with using IMPS to imps bugs linus mitre org Other questions can be mailed to imps request linus mitre org 25 2 2 IMPS Copyright Notice Copyri
242. ssion whose free variables are 11 01 Ln Q Then A is abbreviated as with 21 01 2n 0n A where A is the result of replacing each free or bound occurrence of a variable x a in A with zi This mode of abbreviation preserves meaning as 78 long as there are not two variables x and x 8 with a 4 8 which are either both free in A or both in the scope of the same binder in A Parentheses in expressions may be suppressed when meaning is not lost In addition the following alternate notation may be used in the IMPS math ematical syntax 1 prop and ind in place of the base sorts x and v respectively 2 ay X X an B in place of a compound sort a1 n 3 and a1 X X Qn f in place of a compound sort aj Qn 8 with 8 of kind 3 The symbol in place of at the end of variable sort sequence e g J1 a x x instead of Jx amp x 4 in place of the biconditional 5 Ala a p x in place of 3x a p x A Vy a ply D z y 6 AF B in place of A B 7 3 Semantics The semantics for a LUTINS language is defined in terms of models that are similar to models of many sorted first order logic Let be a LUTINS language and let S denote the set of sorts of A frame for S is a set Da a S of nonempty domains sets such that De T F T F 2 YS If a x p then Da C Dg 3 If a aq Qn An 1 is of kind v then Da i
243. st is omitted Command kind Single inference Description Conclusion TU podyv 0 Premises rU p gt 90 PU Y gt 0 Conclusion TU i A Apn gt Y Premise PU yi n gt Y Conclusion TU g1 VV Pn gt Y Premises 1 lt i lt n TU yi gt Y Conclusion rU p y 90 Premises TU p y gt 0 ru p a gt 0 Conclusion PU if form y v 0 gt Premises TU o gt E ru Lp 0 Conclusion T U 321 01 En On P gt Y Premise rU y sy Notes e Each sequent in the preceding table is of the form TU py gt y e The index of the assumption in context I U pj is i 221 e is obtained from y by renaming the variables among 71 2n which are free in both y and the original sequent Related commands antecedent inference strategy direct and antecedent inference strategy direct inference Remarks Keep in mind that any antecedent inference produces subgoals which together are equivalent to the original goal Thus it is always safe to do antecedent inferences in the sense that they do not produce false subgoals from true ones Key binding a antecedent inference strategy Script usage antecedent inference strategy assumption list assumption list can be given as a list of numbers a list of strings or an assumption list form Interactive argument retrieval e List of formula indices for ant
244. stroying the previous copy e IMPS will create a new Emacs buffer displaying the copy You will use this buffer to view and edit the file 60 e IMPS will search for the first item in the file meriting your attention Each such item will be marked by the string These items may be candidate theorems to prove theory declarations or definitions to read or macetes or scripts to create e Anything above the first will be sent as input to the underlying T process Thus IMPS will define any notions mentioned at the top of the file At any point in the exercise to proceed to the next item of interest select from the IMPS Help menubar item the Current Exercise Next En try request e IMPS will search for the next item in the file marked by the string e Anything beyond the first up to the current occurrence will be sent as input to the underlying T process Thus IMPS will install the definitions theorems and so forth described in that portion of the file If you want to restart an exercise in a clean way click on Exit IMPS under General and then on Run IMPS The system will prompt you to confirm the desired amount of virtual memory the default is plenty for current purposes Having started a fresh invocation of IMPS put your cursor in the buffer that you want to work on Click on the item Restart Exercise in Current Buffer under IMPS Help 6 1 2 Paths Through the Exercises The exercises divide roughly in
245. structors and then calling direct inference 277 insistent simplification Parameters None Description This primitive inference procedure is equivalent to disabling all quasi constructors and then calling simplification macete application at paths Parameters e A list of paths pi Dn e A macete Description This primitive inference procedure applies the argument macete to the sequent node assertion at those occurrences specified by the paths p1 Pn macete application with minor premises at paths Parameters e A list of paths pi Dn e A macete Description This primitive inference procedure applies the argument macete to the given sequent node in the same way as macete application but with the following important difference whenever the truth or false hood of a convergence requirement cannot be determined by the simplifier the assertion is posted as a additional subgoal to be proved raise conditional inference Parameters A list of paths p1 pn to conditional subexpressions 278 Description This primitive inference procedure will raise a subset of the conditional expressions i e expressions whose lead constructor is if specified by the paths p in the assertion of the given sequent T gt y For the moment let us assume that n 1 Suppose the conditional expression in y located at p is the a th occurrence of s if 0 t1 t2 in p the smallest formula containing the a th
246. t for didactic reasons only we will do the proofs in the slowest most explicit way imaginable A Word about the IMPS Interface In the course of these micro exercises several X windows will be used 1 One or more Emacs windows This is the primary way of interacting with IMPS which is implemented by a process running a Lisp like language under Emacs s control 2 A T X previewer This window displays typeset output created by IMPS When IMPS creates new output raising the window will suffice to have it refresh its contents with the new output If the window is already raised a capital R for Redisplay will cause it to do the same The lower case letters n and p can be used to display the next and previous pages when more than one page is available To raise a partly obscured window click with the left button on its header stripe We also refer to this as the xview window and the process of displaying something in this form as xviewing it for every k m Z implication e conjunction ol lt k ok lt m Ce Got G Figure 5 1 The Combinatorial Identity 45 Sequent 1 for every k m Z implication e conjunction ol lt k ok lt m o 1 m k 1 m k 421 7 Figure 5 2 The Combinatorial Identity with One Occurrence Unfolded for every z y z R lt e y z 7 e conjunction o z7 l og z y Figure 5 3 The left denominator removal for
247. t be used to denote mathematical objects Normally formulas or predicates i e expressions having a sort of the form aj Qn are the only useful expressions of kind Consequently there is little support in IMPs for the constructor tp the definite description operator for the world The character is often used in the names of variables and constants in the string syntax to denote a space the character _ is used to denote the start of a subscript This character is printed in the mathematics syntax as either or _ 83 Chapter 8 Theories 8 1 Introduction As a mathematical object an IMPS theory consists of a LUTINS language L and a set of sentences in called azioms The theory is the basic unit of mathematical knowledge in IMPS In fact IMPS can be described as a system for developing exploring and relating theories How a theory is developed is the subject of several chapters an overview is given in the next section The principal technique for exploring a theory is to discover the logical implications of its axioms by stating and trying to prove conjectures the IMPS proof system is described in Chapter 12 Two theories are related by creating an interpretation of one in the other theory interpretations are discussed in Chapter 9 We define a theorem of an IMPS theory T to be a formula of 7 which is valid in each model for 7 That is a theorem of T is a semantic consequence of J The reader should note that ou
248. t is particularly useful as a preparation for applying such commands as apply macete beta reduce and simplify Key binding induction Script usage induction inductor variable inductor is a symbol nam ing an inductor and variable is a string or If O is supplied as argument IMPS will choose the variable of induction itself Interactive argument retrieval e Inductor An inductor is an IMPS structure which has an associated induction principle together with heuristics in the form of macetes and commands to handle separately the base and induction cases e Variable to induct on lt RET gt to use IMPS default IMPS will choose a variable of the appropriate sort to induct on Thus in general there is no danger that it will attempt to induct on a variable for which induction makes no sense However if various choices for an induction variable are possible the choice is more or less arbitrary In these cases you should be prepared to suggest the variable 248 Command kind Multi inference Description This command attempts to apply a formula called an induc tion principle to a sequent and applies some auxiliary inferences as well The induction principle used by IMPS is determined by the inductor you give as an argument When using the induction command the system will attempt to reformulate the sequent in a form which matches the induction principle In particular you can use the induction command directly in
249. t path that will avoid this confusing situation 113 8 A quasi constructor can be disabled and then later enabled in the midst of a deduction using the appropriate proof commands However disabling a quasi constructor in the midst of a proof can cause severe confusion if one forgets to later enable it As a general rule you should always try to find ways to avoid disabling quasi constructors 114 Chapter 11 Theory Ensembles 11 1 Motivation Much of mathematics deals with the study of structures such as monoids fields metric spaces or vector spaces which consist of an underlying set S some distinguished constants in S and one or more functions on S In IMPS an individual structure of this kind can be easily formalized as a theory For example the IMPS theory for monoids is specified by two def forms def language MONOID LANGUAGE embedded languages h o real arithmetic base types uu constants e uu uu uu uu def theory MONOID THEORY component theories h o real arithmetic language monoid language axioms associative law for multiplication for monoids forall z y x uu x y z x y z forall x uu x e x forall x uu e x x In the mathematical syntax the sort uu is written U and the constants e are written e e 115 Notice that the theory of a monoid as presented here is suitable for concept formulation and proof in a single monoid Here are some examples
250. tains a variety of basic mathematics In no sense is the initial theory library intended to be complete We expect it to be extended by IMPS users In the course of using IMPS you should build your own theory library on top of the IMPS initial theory library The initial theory library contains many examples that you can imitate An outline of the initial theory library is given in Chapter 20 8 7 Hints and Cautions 1 The IMPS initial theory library contains no arithmetic theory weaker than h o real arithmetic e g there is no theory of Peano arith metic This is in accordance with our philosophy that there is rarely any benefit in building a theory with an impoverished arithmetic Fur thermore since full powered arithmetic is so useful and so basic we advise the IMPS user to include h o real arithmetic in every theory he or she builds 2 When building a theory it is usually a good idea to minimize the primitive constants and axioms of the theory This will make it easier to use the theory as a source of a theory interpretation 3 The best way to learn how to develop a theory is to study some of the theory building techniques and styles which are demonstrated in the IMPS initial theory library 4 Since the sort of an expression gives immediate information about the value of the expression it is often very advantageous to define new atomic sorts rather than work directly with unary predicates Also a nonnormal translation see
251. tates that the condition is satisfied and the user can use whatever ingenuity is needed in order to prove it We refer to such an additional subgoal as a minor premise Experience shows that in the great majority of cases it is more useful to make the sub stitution and to post any conditions that cannot be discharged immediately as future obligations However in the case of a computational macete such as this one the opposite is the case We want to compute out as many of the occurrences of factorial as we can in the expression at hand But we can reduce a particular instance of t only if we know which rule to use In particular if whether t is positive depends on the particular choice of values for free variables in t then no expansion can be correct in general The macete constructor without minor premises ensures that the macetes within its scope will be used without minor premises no matter how the macete is called by the user 5 5 Saving a Proof Do not start another micro exercise Instead open a new file You may use the File menubar item clicking on the Open file item supplying an unused filename With your cursor in the buffer for the new file open the Scripts menubar item and click on Insert proof script You will see a textual summary of the interactive proof that you have constructed This textual summary can be executed again or edited as text and then re executed Now click on the Next micro exercise item within I
252. tation In IMPS theories are instantiated using 101 def theory instance each subtheory of a theory can serve as a parameter of the theory For example consider the following def forms def translation FIELDS TO RR source fields target h o real arithmetic fixed theories h o real arithmetic sort pairs kk rr constant pairs o_kk 0 i_kk 1 _kk _kk _kk inv lambda x rr 1 x theory interpretation check using simplification def theory instance VECTOR SPACES OVER RR source vector spaces target h o real arithmetic translation fields to rr renamer vs renamer The last def form creates a theory of an abstract vector space over the field of real numbers by instantiating a theory of an abstract vector space over an abstract field The parameter theory is fields a subtheory of vector spaces and the source theory of fields to rr For a detailed description of this technique see 3 6 9 5 7 Theory Extension Let T Li Ti be a LUTINS theory for i 1 2 To is an extension of T and 71 is a subtheory of T2 if Li is a sublanguage of L and Ty C To A very useful reasoning technique is to 1 add machinery to a theory by means of a theory extension and 2 create one or more interpretations from the theory extension to the original theory This setup allows one to prove results in a an enriched theory and then transport them back to the unenriched theory 102 For example
253. tax of an expression enclosed in double quotes select the entry Check expression syntax in the pane IMPS help Imps will request an expression which you can supply by clicking the right mouse but ton on the formula You can also type the formula directly in the minibuffer As an exercise build the formula which asserts that for every nonnegative integer n the sum of squares of the first n integers is n n 1 2n 1 6 32 Expression Category Syntax Sort Truth truth prop Falsehood falsehood prop Negation not p prop Conjunction pl and and pn prop Disjunction pl or or pn prop Implication p implies p2 prop Biconditional pi iff p2 prop If then else formula if_form p1 p2 p3 prop Universal forall v1 s1 vn sn p prop Existential forsome v1 s1 vn sn p prop Equality t1 t2 prop Application f t1 tn r Abstraction lambda v1 s1 vn sn t s1 sn s Definite description iota v s p s If then else term if p t1 t2 s1 U s2 Definedness t prop Sort definedness t s prop Undefined expression s s With with v1 s1 vn sn t s Notes 1 p pt pn are syntactic variables which denote formulas that is expressions of sort prop t t1 tn denote arbitrary expressions of sort s s1 sn For application f is an arbitrary expression of sort r1 and the sorts ri and si must have the same enclosing type fre
254. the command reduces the sequent to P gt gfitform 9 Y ti s c lt2 s e Y b and otherwise the command fails Now assume n gt 1 The command will then simultaneously raise each specified occurrence of a conditional expression in y in the manner of the previous paragraph if there are no conflicts between the occurrences The kinds of conflicts that can arise and how they are resolved are listed below e If two or more specified occurrences of a conditional expression s in p are contained in same smallest formula they are raised together e If two or more specified occurrences of distinct conditional expressions in y are contained in same smallest formula at most one of the occur rences is raised e If y and we are the smallest formulas respectively containing two specified occurrences of a conditional expression in y and 71 is a proper subexpression of 2 then the first specified conditional expression is not raised Related commands case split on conditionals Remarks This command can be used to change a conditional expression if 0 1 2 in a sequent s assertion where y and pa are formulas to the conditional formula if form 0 p1 p2 Key binding r simplify Script usage simplify 258 Interactive argument retrieval None Command kind Single inference Description This command simplifies the assertion of the given sequent with respect to the context of the sequent It uses both theory specific and ge
255. the definition or theorem to other members of the theory ensemble as needed They are used in a similar way to relate a theory multiple to one of its instances See Chapter 11 for a detailed description of the IMPS theory ensemble mechanism 105 9 5 10 Relative Satisfiability If there is a theory interpretation from a theory 71 to a theory T2 then 7 is satisfiable in other words semantically consistent if T is satisfiable Thus theory interpretations provide a mechanism for showing that one theory is satisfiable relative to another One consequence of this is that IMPS can be used as a foundational system In this approach whenever one introduces a theory one shows it to be satisfiable relative to a chosen foundational theory such as perhaps h o real arithmetic 9 6 1 Hints and Cautions The application of a nonnormal translation to an expression containing quasi constructors will often result in a devastating explosion of quasi constructors One way of avoiding this problem is to normalize the translation by defining new atomic sorts in the translation s target theory to replace the unary predicates used in the translation Suppose a defined atomic sort or constant a is transported to a new atomic sort or constant b via a theory interpretation From that point on will map a to b Translations must be updated to take advantage of new definitions see Section 9 4 above The updating is called transla
256. the theorem rewrite This causes a rewrite rule to be created and installed in the transform table of 7 Although the theorem can have any form usually this usage is used only with a theorem which is an equation a quasi equation or a biconditional transportable rewrite This causes a transportable rewrite rule to be created but not installed Transportable rewrite rules are installed in 7 or other theories with def imported rewrite rules simplify logically first If rewrite and transportable rewrite are in the usage list this marks the generated rewrite and trans portable rewrite rules so that logical simplification is used just before they are applied d r convergence If the theorem has an appropriate form a conver gence condition is created and installed in the domain range handler of T d r value If the theorem has an appropriate form a value condition is created and installed in the domain range handler of T 89 8 5 Definitions IMPS supports four kinds of definitions atomic sort definitions constant definitions recursive function definitions and recursive predicate definitions In the following let 7 be an arbitrary theory Atomic sort definitions are used to define new atomic sorts from nonempty unary predicates They are created with the def atomic sort form An atomic sort definition for T is a pair 6 n U where n is a sym bol intended to be the name of a new atomic sort of 7 and U is a nonempty unary
257. three syntactic categories each syntactic category will be represented by a subsort A BNF for the language might take the form given in Figure 17 2 with x ranging over numbers and s ranging over strings A corresponding IMPS def form is shown in Figure 17 3 where it is assumed that the underlying theory String theory contains a sort string representing ASCII strings as well as containing R 176 bnf data type nat Constructor definedness axioms Theorem succ definedness_nat is total succ nat nat Disjointness axioms Theorem succ zero distinctness_nat is Vyo nat succ yo zero Selector constructor axioms Theorem succ pred_nat is Vyo nat pred succ yo yo Selector undefinedness axioms Theorem pred definedness_nat is Vaemat pred x D Ayo nat succ yo x Sort case axioms Theorem nat cases_nat is Ve nat e zero V succ pred e e Induction axiom Theorem nat induction_nat is Vpmat x Vaomat Xo lt y zero A Yy succgo nat y succo D y succ y_succg Figure 17 1 Axioms for Nat as Introduced by BNF S i E while Edo S od if E then S else S2 skip E 1 Er E2 Er x Es Num z I Ide s Figure 17 2 BNF Syntax for a Small Programming Language 177 def bnf pl syntax theory string theory base type phrase sorts statement phrase expression phrase identifier expression atoms skip statement cons
258. tician devotes considerable effort to proving lemmas that justify computational procedures Although these are frequently equations or conditional equations they are sometimes more complicated quantified expressions and sometimes they involve other relations such as ordering relations Once the lemmas are available they are used repeatedly to trans form expressions of interest Algorithms justified by the lemmas may also be used the algorithm for differentiating polynomials for example The mathematician has no interest in those parts of a formal derivation that implement these processes within predicate logic On the other hand to understand the structure of a proof or especially a partial proof attempt the mathematician wants to see the premises and conclusions of the informative formal inferences Thus the right sort of proof is broader than the logician s notion of a for mal derivation in say a Gentzen style formal system In addition to purely formal inferences IMPS also allows inferences based on sound computations They are treated as atomic inferences even though a pure formalization might require hundreds of Gentzen style formal inference steps We believe that this more inclusive conception makes IMPS proofs more informative to lts users 16 1 3 Components of the System The IMPS system consists of four components 1 3 1 Core All the basic logical and deductive machinery of IMPS on which the soundness of
259. tion an inductor a quasi constructor or a constant A string This string can be used to refer to an expression a theorem or a context An integer This integer can be used to refer to a sequent node an occurrence number within an expression or the number of an assump tion A list of strings A list of integers 12 6 Hints and Cautions 1 To build a proof script for insertion in a def theorem form it is much easier to first prove the theorem interactively and then record the proof script using C c i A novice user should not attempt to build scripts from scratch without thoroughly understanding how scripts replay interactive proofs More experienced users can build new scripts by modifying existing ones For example the following is a def theorem form with a valid proof def theorem MIN LEMMA 134 forall a b c rr a lt b and a lt c implies forsome d rr a lt d and d lt b and d lt c theory h o real arithmetic proof direct and antecedent inference strategy instantiate existential min b c unfold single defined constant globally min case split b lt c simplify simplify apply macete with minor premises minimum 1st arg apply macete with minor premises minimum 2nd arg To get a valid proof for an analogous theorem where the arguments to lt and lt are interchanged one can edit the previous script replacing min by max everywhere in the proof def theorem MAX LEMMA fo
260. tion enrichment and it performed periodically by Imps For example enrichment is done when a translation is evaluated and when the macete help mechanism is called In rare occasions IMPS will not work as expected because some interpretation has not been enriched This may happen for ex ample when a transportable macete is applied directly without using the macete help mechanism In some cases you can get around the problem by re evaluating a relevant def translation form 106 Chapter 10 Quasi Constructors The purpose of this chapter is fourfold 1 To explain why quasi constructors are desirable 2 To describe how they are implemented 3 To show how they are created and reasoned with 1 2 3 4 To point out the pitfalls associated with their use 10 1 Motivation The constructors of LUTINS are fixed but you can define quasi constructors which effectively serve as additional constructors Quasi constructors are desirable for several reasons 1 Once a quasi constructor is defined it is available in every theory whose language contains the quasi constructor s home language That is a quasi constructor is a kind of global constant that can be freely used across a large class of theories A constructor as a logical con stant is available in every theory 2 Quasi constructors are polymorphic in the sense that they can be ap plied to expressions of several different types Several of the construc tor
261. tion has already been loaded e reload files only Causes the files of the section but not the com ponent sections to be reloaded if the section has already been loaded e quick load Causes the section to be quick loaded Keyword Arguments None Description If there are no modifier arguments this form will simply load the component sections and files of the section named section name which have not been loaded include files Positional Arguments None Modifier Arguments e reload Causes a file to be reloaded if the file has already been loaded e quick load Causes the files to be quick loaded 215 Keyword Arguments e files file spec file spec Description If there are no modifier arguments this form will simply load the files with specifications file spec file spec which have not been loaded 17 4 Presenting Expressions view expr Positional Arguments e expression string A string representing the expression to be built and viewed Modifier Arguments e fully parenthesize Causes the expression to be viewed fully paren thesized e fully Same as fully parenthesize e no quasi constructors Causes the expression to be viewed without quasi constructor abbreviations e no qcs Same as no quasi constructors e tex Causes the expression to be xviewed i e printed in T X and displayed in an X window T X previewer Keyword Arguments e language language
262. tions then it refers to the first of those as sumptions Matching here is done in a way that does not preserve scopes of binding constructors and places only type constraints on the matching of variables Interactive argument retrieval This tells you how arguments are re quested in the minibuffer when used interactively with a brief de scription of each argument In cases where IMPS can determine that there is only one possible choice for an argument for example if the argument is an index number for an assumption when there is exactly one assumption then IMPS will make this choice and not return for additional input Command Kind Null inference single inference or multi inference A null inference command never adds any inference nodes to the deduc tion graph A single inference commands adds exactly one inference node to the deduction graph when it is successful A multi inference command adds more than one inference node to the deduction graph in some cases Description A brief description of the command Some commands can be described as rules of inference in a logical calculus For each such command we use a table composed of the following units Conclusion TEMPLATE Premise TEMPLATE where the item TEMPLATE for the conclusion refers to the form for the given goal sequent while the TEMPLATE item for the premise indicates the form for the resulting subgoal In general there will be more than one
263. titution e transportable The presence of this modifier means the macete is transportable Keyword Arguments e theory theory language name Required The name of the lan guage in which expression should be read in 193 Examples def schematic macete ABSTRACTION FOR DIFF PROD with a b rr y rr diff lambda x rr a b y diff lambda x rr lambda x rr a x lambda x rr b x y null theory calculus theory def script Positional Arguments e script name The name of the new command being created e N The number of arguments required by the script e form form A proof script consisting of O or more forms Keyword Arguments e retrieval protocol proc procis the name of an Emacs procedure which IMPS uses to interactively request command arguments from the user The default procedure is general argument retrieval protocol which requires the user to supply all the arguments in the minibuffer e applicability recognizer proc proc is the name of a T predi cate or is the symbol t The inclusion of this argument will cause the command name to appear as a selection in the command menu when ever the current sequent node satisfies the predicate Supplying t as an argument is equivalent to supplying a predicate which is always true Description This form is used to build a new command named script name This new command can be used in either interactive mode or in script mode The script
264. to four tiers of difficulty which are summa rized in Table 6 1 We recommend that you do one or more exercises in a tier before moving on to those in the next tier 6 2 Mathematical Exercises One of the main goals of the IMPS system is to support the rigorous develop ment of mathematics We hope that it will come to serve as a mathematical data base storing mathematical concepts theories theorems and proof techniques in a form that makes them available when they are relevant to new work We believe that as a consequence IMPS will develop into a system that can serve students as a general mathematics laboratory In addition we hope it will eventually serve as a useful adjunct in mathematics research 61 Tier Exercise file name Section 1 primes exercise t 6 2 1 calculus exercise t 6 2 2 2 indicators exercise t 6 3 1 monoid exercise t 6 2 3 3 compiler t 6 4 1 limits t 6 2 4 contraction t 6 2 5 groups exercise t 6 2 6 4 flatten t 6 4 2 temporal t 6 3 2 Table 6 1 Exercise Files by Tier 6 2 1 Primes Contents This exercise introduces two main definitions into the theory of real arithmetic namely divisibility and primality It then includes a few lemmas which lead to a computational macete to determine whether a positive integer is prime After introducing the notion of twin primes the exercise develops two proof scripts that can be used to find a twin prime
265. trapose with because the sequent has no assumptions you will have to add an assumption by using cut with single formula or instantiate theorem Key binding c 236 cut using sequent Script usage cut using sequent sequent node sequent node can be given as an integer referring to the sequent node with that number or as a list context string assertion string Interactive argument retrieval e Major premise number The number of a sequent node Command kind Single inference Description This command allows you to add some new assumptions to the context of the given sequent Of course you are required to show separately that the new assumptions are consequences of the context The node containing the major premise sequent must exist before the command can be called Usually you create this sequent node with edit and post sequent node Conclusion Tso Major Premise PUNO Un Se Minor Premises 1 lt i lt n T gt yi Related commands cut with single formula Remarks To cut with one formula you should usually use cut with single formula cut with single formula Script usage cut with single formula formula Interactive argument retrieval e Formula to cut String specifying a formula y Command kind Single inference 237 Description This command allows you to add a new assumption to the context of the given sequent Of course you are required to show separately that th
266. tructors assign identifier expression statement selectors lvar rexp while expression statement statemen whil exp i tat t stat tJ selectors while test bo select hile test body i expression statement statement statemen if exp i tat t stat t stat t selectors if test consequent alternative select if test quent alt tive plus expression expression expression selectors first addend second adden selectors first addend d addend times expression expression expression selectors first factor second factor numcons rr expression t p J selectors num value select value ide string identifier Ga letrines identirier selectors ide name Figure 17 3 IMPS def bnf Form for Programming Language Syntax 178 def cartesian product Positional Arguments e name A symbol to name the product sort e sort name sort namem sort name is the name of a sort a Keyword Arguments e constructor constructor name e accessors accessor name accessor name e theory theory name Required Description This form creates a new atomic sort called name This sort can be regarded as the cartesian product of the sorts a Q m The sort actually created is a subsort of the function sort 01 X X Am unit_sort e constructor name is the name of the canonical n tuple mapping Qa X X Am 0 e accessor name is the name of the canonical proj
267. truth falsehood Table 3 2 Sorts for h o real arithmetic into the range sort sn an exception to this rule about intended meanings of sorts is discussed in the Chapter 7 A language distinguishes certain sorts as types and assigns a type to every sort Distinct types are intended to denote sets of elements which need not be related prop is a base type which belongs to every language and which is intended to denote the set of truth values The sorts for h o real arithmetic are given in Table 3 2 The expressions of a language are built from language constants and variables as specified by Table 3 3 below A constant is a character string specified as such by the def language form A variable is also character string Variables however must begin with a text character that is an alphabetic character or one of the symbols _ and contain only text characters or digits Moreover the sorting of a variable within an expression must be specified either by an enclosing binder or by an enclosing with declaration In the theory h o real arithmetic there is additional syntax for arith metic operators described in Table 3 4 For example is used for both sign negation and the binary subtraction operator The binary operators are all infix with different binding powers to reduce parentheses on input and output In order of increasing binding power the arithmetic operators are k To check the syn
268. ts for loading sections and files and for presenting ex pressions We will use the following template to describe each one of these forms Positional Arguments This is a list of arguments that must occur in the order given and must precede the modifier arguments and the keyword arguments All IMPs definition forms have a name as first argument or a list of names as first argument Modifier Arguments Each modifier argument is a single symbol called the modifier Keyword Arguments Each keyword argument is a list whose first ele ment is a symbol called the keyword Keyword arguments have one of two forms e keyword arg component e keyword arg component arg component Note By default nearly every special form in this chapter is allowed to have a keyword argument of the form syntaxsyntaz name where syntax name is the name of a syntax e g string syntax or sexp syntax which specifies what syntax to use when reading the 167 form If this keyword argument is missing the current syntax is used when reading the form Modifier and keyword arguments can occur in any order Description A brief description of the definition form Remarks Hints or observations that we think you should find useful Examples Some example forms 168 17 1 Creating Objects def algebraic processor Positional Arguments e processor name Modifier Arguments e cancellative This modifier argument tells the simplif
269. ts M are backward directional macetes then the compound macete is also backward directional e Sound macete constructor If M2 M3 are bidirectional then the com pound macete Sound M1 Mo M3 T e is always bidirectional regardless of My If Ma is backward directional and M3 is bidirectional then the compound macete is backward directional In all other cases the compound macete is nondirectional 14 4 Building Macetes Schematic macetes are for the most part installed by the system when the orems installed 1 Elementary macetes are automatically installed when a theorem is added to a theory The name of the installed macete is the same as the name of the theorem which generates it 147 2 Transportable macetes are installed when the transportable macete modifier is present in the usage list of a theorem or axiom Moreover in this case the name of the installed macete is the name of theorem which generates it with the prefix tr Macetes are also automatically built when atomic sort and constant def initions are made by the user 1 For directly defined constants the macete corresponding to the con stant defining equation is installed This macete is named constant name equation_theory name If the usage list of the definition includes the rewrite modifier and the defined constant is a function the constant defining equation in applied form is also include as a macete named constant name applied equat
270. ulation followed by a few spaces and Emacs will complete the name by comparing against the possible macete names In 10 15 seconds you will see the description of this bulky compound macete It first applies beta reduction to plug in the arguments of any functions expressed using the A variable binding constructor After that it repeatedly applies a sequence of elementary macetes until none of them can be applied any more It then moves on to a second sequence of elementary macetes and applies them repeatedly until no further progress is made It is possible to write nonterminating macetes using the repeat oper ator IMPS is designed so that it can be interrupted easily and safely To do so type ESC x interrupt tea process If you decide that you should not have interrupted it you can cause it to return to the computation at which it was interrupted To do so put your cursor at the end of the tea buffer and type ret followed by a carriage return To execute the macete fractional expression manipulation on your current goal use the item Macetes with minor premises under 50 SERIES BETA REDUCE REPEAT REPEAT INVERSE REPLACEMENT SUBTRACTION REPLACEMENT NEGATIVE REPLACEMENT ADDITION OF FRACTIONS LEFT ADDITION OF FRACTIONS RIGHT MULTIPLICATION OF FRACTIONS LEFT MULTIPLICATION OF FRACTIONS RIGHT DIVISION OF FRACTIONS DIVISION OF FRACTIONS 2 EXPONENTS OF FRACTIONS NEGATIVE EXPONENT REPLACEMENT LEFT DENOMINATOR
271. utative Law for Addition Vy R r y Yy x Characterization of Division Va b R b 40D b a b a Division by Zero Undefined Va b ind b 0 D a b Z Additive Closure Vz y Z c y Z 289 17 Z Negation Closure Vx Z x Z 18 Induction Vs Z gt x Vt Z 0 lt tD s t s 1 AVt Z 0 lt t D s t D s t 1 19 Characterization of 1 1 1 20 Q is the field of fractions of Z Va R x Q 3a b Z x a b 21 Order Completeness Vp R gt x nonvacuous p A Ja R V0 R p 0 D80 lt a gt 3y R VOR p 0 D0 lt y A VYR V0 R p 0 D0 lt 11 DYS Y h o real arithmetic This is another axiomatization of the real numbers which we consider to be our working theory of the real numbers The axioms of h o real arithmetic include the axioms of complete ordered field formulas characterizing ex ponentiation as a primitive constant and formulas which are theorems proven in complete ordered field These theorems are needed for installing an algebraic processor and for utilizing the definedness machinery of the simpli fier The proofs of these theorems in the theory complete ordered field require a large number of intermediate results with little independent inter est The use of two equivalent axiomatizations frees our working theory of the reals from the burden of recording these uninteresting results The theory h o real arithmetic is equipped with routines for simpli fying arithmetic expressio
272. ve an overview of the tasks that are involved in creating a well developed theory Along the way we list the def forms that are relevant to each task Task 1 The Primitive Theory The first task in developing a theory is to build a primitive bare bones theory T from a possibly empty set of theories a language and a set of axioms This is done with the def theory form T is the smallest theory which contains the theories the language and the set of axioms The theories are made the component theories of 7 A language is created with def language or def sublanguage A primitive theory can also be created by instantiating an existing theory with def theory instance Task 2 Theorems The information held in the axioms of the primitive theory is unlocked by proving theorems using the IMPS proof system see Chapter 12 Theorem proving is crucial to developing a theory and is involved in most of the tasks below Proven theorems are installed in the theory with def theorem using various usages See Section 8 4 for details Task 3 Simplification Once the primitive theory is built usually the next task is to specify how simplification should be performed in the theory There are three mecha nisms for doing this that can be used separately or in combination 85 1 Install a processor For theories of an algebraic nature e g rings fields or modules over a ring you may want to install an alge braic processor to perform rud
273. ver the occurrence is an extended application component of s where a is an extended application component of b if either a is b or bis an application of kind and a is an extended application component of a component of b existential generalization Parameters A sequent node Tl gt y Description This primitive inference procedure proves an existential as sertion by exhibiting witnesses Conclusion T gt 321 01 lt En On P Premise T gt 0 Notes e The command will fail unless the parameter sequent node is of the form T gt y extensionality Parameters None 275 Description If the sequent node assertion is an equality or quasi equality or the negation of an equality or quasi equality of n ary functions this prim itive inference applies the extensionality principle Conclusion T gt f g9 Major Premise T V21 01 n 0n f 1 2n X 9 21 Tp Minor Premise gt f Minor Premise T gl Conclusion Tif eg Major Premise T gt Va1 01 n 0n f 1 En X 9 11 Tn Minor Premise TU g gt fl Minor Premise TU fl gt gl Conclusion T gt f yY Premise US ana ad a Oi En Conclusion LESA Premise TV O igs pn NAAA Notes e If the sorts of f and g are qj Qn Qn41 and 61 Bn Bn 1l respectively then g a U 6 for all i with 1 lt i lt
274. versal formula The patterns are extracted from y depending on the form of y as described by the following table Form Source Replacement Conditions Spec pid Agn Dt taf t to Vision Bid Pid ApnDti t21 ti to Y1 Yn Bid Pid A Pn D Yi gt p Y Ya 1 Pn Bid poy Y p None Back tix tot ty ta None Bid ti tof ty ta None Bid pi Ya Yi Ya None Bid Y Y F None Bid Y Y T None Bid Notes e If the replacement pattern y according to the above table is of sort x and contains free variables y1 Ym not occurring freely in the source pattern y then consider instead the replacement pattern yi 61 Ymi6n P e Nested implications p1 D p2 D Yn gt Y are treated as single implications y1 A A Yn gt Y when applying the above table e In those cases marked with y if t2 contains free variables which do not occur freely in t then consider instead the source pattern t ta or t to and replacement pattern y1 A A pp or T 144 We now describe how a schematic macete M is obtained from the source replacement condition patterns and direction specifier of a formula Given a context and an expression t the result of applying M toT and t is deter mined as follows Let P be the set of paths l l ln to subexpressions e of t which satisfy all of the following conditions e If the directional specifier is backward directional
275. want to use in most 149 cases The without minor premises macete constructor is often useful for building compound macetes to be used in this mode 150 Chapter 15 The Iota Constructor 15 1 Motivation The iota or y constructor is a definite description operator for objects of kind v Given a variable x of sort a of kind and a unary predicate y ix a p x denotes the unique x that satisfies y if there is such an x and is undefined otherwise For example ia U lt xArrxr 2 denotes v2 but Hi L 2 is undefined The iota constructor is very useful for specifying functions especially partial functions For example ordinary division of sort R R R which is undefined whenever its second argument is 0 can be defined from the times function by the lambda expression Ar y R iz R xz y Of course this kind of definite description operator is only possible in a logic that admits undefined expressions 151 15 2 Reasoning with Iota An iota expression is any expression which begins with the iota constructor without any abbreviations by quasi constructors Proving a sequent with an assertion containing an iota expression can be tricky The key idea is to reduce the sequent to a new sequent with one less iota expression This is called eliminating iota There are two commands and one macete for eliminating iota each of which is discussed below in a separate subsection 15 2 1 eliminate defined i
276. way that shows only the single most crucial step If you again click the menu item for the next micro exercise you will be relieved to see a new goal also shown in Figure 5 12 Step 1 Invoke the macete little integer induction on the macete menu Result The macete will identify the predicate of induction and apply the induction principle on the integers resulting in the subgoal shown in Figure fig inductdone The first conjunct here is the base case and the second conjunct is the induction step Within the induction step we see the 57 Sequent 2 conjunction eN i 0j 0 0 1 2 e foreveryt Z implication o0 lt t o implication o Ej oj t t 1 2 o Vioj t 1 t 1 1 2 Figure 5 13 Result of Applying the little integer induction Macete hypothesis 0 lt t which is needed because we are working with Z rather than N Subject to this assumption the induction step asserts that the predicate remains true of t 1 assuming that it held true of t 5 7 The Induction Command There are many heuristics that pay off with induction principles For in stance recursively defined operators applied to the inductive term should be expanded in the induction step For this reason IMPS contains a command for induction which will ap ply an induction principle as in the previous micro exercise after which it separates the base case from the induction step and applies appropriate heuristics to each IMPS offers some flexibi
277. x y simplifies to x 1 y 2 The simplifier may at times appear to exhibit temperamental be havior At one extreme it may seem to the user that the simplifier does too little or that it has ignored an assumption that would have immediately grounded the sequent At the other extreme the simpli fier may do too much work reducing the assertion in unintuitive or unusable ways What may be especially infuriating to the user is that the presence of additional assumptions may actually cause the simplifier to return a much less usable answer For instance in the theory h o real arithmetic the simplifier will reduce the formula Va y R 1 lt 2ry D0 lt 2xy to T However Va y R 0 lt yA1 lt 2ay D0 lt 2ry 140 simplifies to Va y R 0 lt yAI1 lt 2ay D0 lt 2r This discrepancy results from its factoring the positive y in 0 lt 2xy before applying the decision procedure for linear inequalities 141 Chapter 14 Macetes In addition to its simplifier IMPS also provides a separate mechanism for ma nipulating formal expressions by applying theorems Unlike simplification 1t is under the control of the user The basic idea is that some expression ma nipulation procedures for instance conditional rewrite rules are in fact direct applications of theorems Other expression manipulation procedures can be formed from existing ones using a simple combination language These expression manipulation procedures are c
278. y imps theory 3 H 0 REAL ARITHMETIC h o real arithmetic is a basic IMPS theory which contains an axiomatic theory of the real numbers characterized as a complete ordered field with the integers and rationals as imbedded structures This is a fairly extensive theory so we only describe it informally here The atomic sorts of the language are N Z Q R denoting the natural numbers integers rationals and reals The language constants of this theory are of three kinds e The primitive function and relation constants sub lt lt that denote the arithmetic operations of addition multiplication divi sion exponentiation subtraction negation and the binary predicates less than and less than or equal to respectively The IMPS manual is the document you are looking at 29 Operator Domain RxR RxR R sub RxR 7 E R x RA 0 sum S prod S N lt RxR lt RxR gt RxR gt RxR where e E R 0 x Z U 0 x 2 Z 0 lt z eS mn EZxZx Z gt R VWkeZ m lt k lt n gt f k 1 Table 3 1 Domains of Arithmetic Operators e An infinite set of individual constants one for each rational number e Various defined constants such as the operator gt The domains of the primitive constants and some of the defined constants are given in Table 3 1 The axioms of this theory are the usual field and order axioms
279. y 1 Let Ti be the theory with name name In this case evaluation of the form builds translations and transports natively defined constants and sorts by these transla tions from selected theory multiples into the theory union TU The theory multiples that are selected as translation source theories are determined by the multiples or permutations keyword argu ments as follows permutations Pi Py Each argument P is a list p1 pe of integers in 0 N 1 which instructs IMPS to translate constants defined in the ensemble multiple into the theory union Ta Wo WOT py The translation data are provided by the sorts and constants keyword arguments multiples M Mn This case can be reduced to the case of the permutations P Pa argument by considering all lists of length M of nonnegative integers lt N 1 e target multiple n This case can be reduced to the case of the target theories name name argument by letting name be the name of the i th theory replica Examples def theory ensemble instances METRIC SPACES target theories h o real arithmetic metric spaces multiples 1 2 sorts pp rr pp constants dist lambda x y rr abs x y dist 204 def theory ensemble multiple Positional Arguments e ensemble name An error will result if no ensemble exists with en semble name e N An integer Description Builds a theory which is an N multiple of the
280. y macete with minor premises s ooo a 225 assume theorem sooo e 226 assume transported the0orem ee 227 auto instantiate existential o o ee ee 227 auto instantiate universal antecedent 228 packehain arpa e A iia ee uot ee ok oe eS oe 228 backchain backwards e so 229 backchain repeatedly o o 229 backchain through formula o e o 230 DetasTe duce liada a a BES 231 beta reduce antecedent 0 a 232 beta reduce insistently 0 0 o a 232 beta reduce repeatedly 2 a a a 233 beta reduce with minor premises a 233 CASC S Plita AO ist ce cide ewe eer oh e Os 234 case split on conditionals 2 0 0 0 eee ee ee 235 choice principle ys adage eH eRe De E es De eS 235 COMETADOSE 3 Da we Bore FL o i dn beak Gly da een Ge hg Bes 236 cut using sequent 2 ee 237 cut with single formula o o e e 237 dele ddesS Do il AA ir sa e S 238 direct and antecedent inference strategy 238 direct and antecedent inference strategy with simplification 239 direct inference 2 240 direct inference strategy o 241 disable quasi constructor osooso 241 edit and post sequent node a 242 eliminate defined iota expression o osoa oo a 242 eliminateiota ta hen r aa a a ie oe Sal aad 243 enable quasi constructor ooo a e a 244 extensionality

The IMPS User's Manual - Interactive Mathematical Proof System

Contents

Download Pdf Manuals

Related Search

Related Contents