New patches: [unrevert anonymous**20070211092027] < > { hunk ./peano/peano-thms.gh 129 (-> (E. x ph) (E. x ps)) (hyp x gen x ph ps 19.22 ax-mp)) +thm (19.32 () + ((hyp (nfi x ph))) + (<-> (A. x (\/ ph ps)) (\/ ph (A. x ps))) + (hyp ax-nfinot ps 19.21 + ph ps df-or x albii + ph (A. x ps) df-or + 3bitr4 +)) + +thm (19.31 () + ((hyp (nfi x ps))) + (<-> (A. x (\/ ph ps)) (\/ (A. x ph) ps)) + (hyp ph 19.32 + ph ps orcom x albii + (A. x ph) ps orcom + 3bitr4 +)) + +thm (19.23 () + ((hyp (nfi x ps))) + (<-> (A. x (-> ph ps)) (-> (E. x ph) ps)) + (ph ps imor x albii + hyp (-. ph) 19.31 bitr + x ph alnex ps orbi1i bitr + (E. x ph) ps imor bitr4 +)) + +thm (19.23v ((ps x)) () + (<-> (A. x (-> ph ps)) (-> (E. x ph) ps)) + (x ps ax-nfidv ph 19.23 +)) + thm (19.23ai () ((hyp1 (nfi x ps)) (hyp2 (-> ph ps))) hunk ./peano/peano-thms.gh 205 B eqid B A B ax-eqtr mpan2 impbi )) + +thm (eqcomi () + ((hyp (= A B))) + (= B A) + (hyp A B eqcom mpbi)) + +thm (eqcomd () + ((hyp (-> ph (= A B)))) + (-> ph (= B A)) + (hyp A B eqcom sylib)) + +thm (eqcoms () + ((hyp (-> (= A B) ph))) + (-> (= B A) ph) + (B A eqcom hyp sylbi +)) + +thm (eqeq1 () () + (-> (= A B) (<-> (= A C) (= B C))) + ( + A B C ax-eqtr exp + B A C ax-eqtr exp eqcoms + impbid +)) + +thm (eqeq2 () () + (-> (= A B) (<-> (= C A) (= C B))) + (A B C eqeq1 + A C eqcom B C eqcom bibi12i + sylib +)) + +thm (eqeq1i () + ((hyp (= A B))) + (<-> (= A C) (= B C)) + (hyp A B C eqeq1 ax-mp)) + +thm (eqeq1d () + ((hyp (-> ph (= A B)))) + (-> ph (<-> (= A C) (= B C))) + (hyp A B C eqeq1 syl)) + +thm (eqeq2i () + ((hyp (= A B))) + (<-> (= C A) (= C B)) + (hyp A B C eqeq2 ax-mp)) + +thm (eqeq2d () + ((hyp (-> ph (= A B)))) + (-> ph (<-> (= C A) (= C B))) + (hyp A B C eqeq2 syl)) + +thm (eqeq12d () + ((hyp1 (-> ph (= A B))) + (hyp2 (-> ph (= C D)))) + (-> ph (<-> (= A C) (= B D))) + (hyp1 C eqeq1d + hyp2 B eqeq2d bitrd +)) + +thm (eqtr3 () + ((hyp1 (= A B)) + (hyp2 (= A C))) + (= B C) + (hyp1 hyp2 A B C ax-eqtr mp2an +)) + +thm (eqtr () + ((hyp1 (= A B)) + (hyp2 (= B C))) + (= A C) + (hyp1 eqcomi hyp2 eqtr3 +)) + +thm (eqtr4 () + ((hyp1 (= A B)) + (hyp2 (= C B))) + (= A C) + (hyp1 hyp2 eqcomi eqtr +)) + +thm (eqtrd () + ((hyp1 (-> ph (= A B))) + (hyp2 (-> ph (= B C)))) + (-> ph (= A C)) + (hyp1 hyp2 A eqeq2d mpbid +)) + +thm (syl5eq () + ((hyp1 (-> ph (= A B))) + (hyp2 (= C A))) + (-> ph (= C B)) + (hyp2 ph a1i hyp1 eqtrd +)) + +thm (syl5eqr () + ((hyp1 (-> ph (= A B))) + (hyp2 (= A C))) + (-> ph (= C B)) + (hyp2 eqcomi ph a1i hyp1 eqtrd +)) + +thm (syl6eq () + ((hyp1 (-> ph (= A B))) + (hyp2 (= B C))) + (-> ph (= A C)) + (hyp1 hyp2 ph a1i eqtrd +)) + +thm (syl6eqr () + ((hyp1 (-> ph (= A B))) + (hyp2 (= C B))) + (-> ph (= A C)) + (hyp1 hyp2 eqcomi ph a1i eqtrd +)) + +thm (vtocl ((A x) (ps x)) + ((hyp1 (-> (= (cv x) A) (<-> ph ps))) + (hyp2 ph)) + ps + (hyp2 hyp1 mpbii vtocle)) + +thm (ceqsal ((A x)) + ((hyp1 (nfi x ps)) + (hyp2 (-> (= (cv x) A) (<-> ph ps)))) + (<-> (A. x (-> (= (cv x) A) ph)) ps) + ( + hyp2 pm5.74i x albii + hyp1 (= (cv x) A) 19.23 bitr + x A tyex ps a1bi bitr4 +)) + +thm (ceqsalv ((A x) (ps x)) + ((hyp (-> (= (cv x) A) (<-> ph ps)))) + (<-> (A. x (-> (= (cv x) A) ph)) ps) + (x ps ax-nfidv hyp ceqsal)) + +# Peano arithmetic + +thm (addeq1 () () + (-> (= A B) (= (+ A C) (+ B C))) + (C eqid A B C C addeq12 mpan2)) + +thm (addeq2 () () + (-> (= A B) (= (+ C A) (+ C B))) + (C eqid C C A B addeq12 mpan)) + +thm (suceqd () + ((hyp (-> ph (= A B)))) + (-> ph (= (S A) (S B))) + (hyp A B pa_ax2 sylib)) + +thm (finds ((x y) (A x) (ps x) (ch x) (th x) (ta x) (ph y)) + ((hyp1 (-> (= (cv x) (0)) (<-> ph ps))) + (hyp2 (-> (= (cv x) (cv y)) (<-> ph ch))) + (hyp3 (-> (= (cv x) (S (cv y))) (<-> ph th))) + (hyp4 (-> (= (cv x) A) (<-> ph ta))) + (hyp5 ps) + (hyp6 (-> ch th))) + ta + ( + hyp4 + hyp5 hyp1 mpbiri x gen + hyp6 + hyp2 ceqsalv + hyp3 ceqsalv + 3imtr4 y gen + x ph y pa_ind mp2an + x ph ax-4 ax-mp + vtocl +)) + +thm (pa_ax3r () () + (= (+ (0) A) A) + ( + (cv x) (0) (0) addeq2 (= (cv x) (0)) id eqeq12d + (cv x) (cv y) (0) addeq2 (= (cv x) (cv y)) id eqeq12d + (cv x) (S (cv y)) (0) addeq2 (= (cv x) (S (cv y))) id eqeq12d + (cv x) A (0) addeq2 (= (cv x) A) id eqeq12d + (0) pa_ax3 + (+ (0) (cv y)) (cv y) pa_ax2 + (0) (cv y) pa_ax4 (S (cv y)) eqeq1i + bitr4 biimp + finds +)) + +thm (pa_ax4r () () + (= (+ (S A) B) (S (+ A B))) + ( + (cv x) (0) (S A) addeq2 (cv x) (0) A addeq2 suceqd eqeq12d + (cv x) (cv y) (S A) addeq2 (cv x) (cv y) A addeq2 suceqd eqeq12d + (cv x) (S (cv y)) (S A) addeq2 (cv x) (S (cv y)) A addeq2 suceqd eqeq12d + (cv x) B (S A) addeq2 (cv x) B A addeq2 suceqd eqeq12d + (S A) pa_ax3 A pa_ax3 (+ A (0)) A pa_ax2 mpbi eqtr4 + + (+ (S A) (cv y)) (S (+ A (cv y))) pa_ax2 biimp + A (cv y) pa_ax4 (+ A (S (cv y))) (S (+ A (cv y))) pa_ax2 mpbi + syl6eqr + (S A) (cv y) pa_ax4 + syl5eq + finds +)) + } Context: [add a few peano thms, and support for those raph.levien@gmail.com**20070211055912] [initial checkin of peano dir raph.levien@gmail.com**20070211014453] [add prettyprinting, translation of mm markup raph.levien@gmail.com**20070113060634] [convert Metamath markup in comments to Barghest markup raph.levien@gmail.com**20061230062050] [add python module and script for interactive display raph.levien@gmail.com**20061022011109] [commit unicode math fonts into repo raph.levien@gmail.com**20061022010607] [update app to do interactive typeset; minor peano raph.levien@gmail.com**20061017224852] [update set.mm to 17 Oct 2006 version raph.levien@gmail.com**20061017224818] [2d layout, refactor of opr logic (typesetting) raph.levien@gmail.com**20060905090310] [initial checkin of ghilbert app and typeset utility raph.levien@gmail.com**20060903040521] [prove trichotomies of le and lt raph.levien@gmail.com**20060829101937] [prove peano-thms/addcan, fix broken df-mu raph.levien@gmail.com**20060822232632] [developing peano-thms, new work in pred-thms raph.levien@gmail.com**20060821065317] [some new peano thms (1 is not leq 0, etc.) raph.levien@gmail.com**20060729215028] [lots of new pred and set thms raph.levien@gmail.com**20060705082823] [fix type assum in set.ghi; pred renames and eu thms raph.levien@gmail.com**20060704061905] [fix zfc-pair to point to real location of set_mm raph.levien@gmail.com**20060702005842] [fixes to pred to harmonize with set.mm; new set thms raph.levien@gmail.com**20060702005446] [modularize proof step checking; fix dv checking bug raph.levien@gmail.com**20060702004204 This version splits out the application of a single proof step into its own method. It also fixes a bug in dv checking caused by two different variables sharing the name 'hyps'. Now, the one local to check_proof_step does not interfere with the one in check_proof. ] [update hol-zfc to new set_mm raph.levien@gmail.com**20060701223000 This patch just does the renaming of theorems up to 23-jun-2006 set.mm. There's still a fair amount of cleanup possible because there are new constructions (notably [_/]_ and 1st and 2nd) and theorems that are now duplications of what's in hol-zfc. ] [remove duplicate copy of set_mm from pax dir raph.levien@gmail.com**20060701221126] [update zfc-pax construction to new set_mm raph.levien@gmail.com**20060701221025] [update set.mm to 23-jun-2006 raph.levien@gmail.com**20060701220252] [update mm_xlat.py to current set.mm raph.levien@gmail.com**20060701212457] [begin the development of the set interface in pax raph.levien@gmail.com**20060701191833] [check in peano-thms.ghi, which peano-thms.gh exports raph.levien@gmail.com**20060701035134] [pax pair interface, with zfc construction raph.levien@gmail.com**20060701034358 This commit adds a general pairing mechanism to pax, along with a construction in zfc. In order to support the interface hierarchy, we refactor set_mm a bit so that the propositional calculus is a parameter. To minimize breakage, I've added a copy of the refactored set_mm to the pax directory, rather than making the changes in zfc, but ultimately that should be reunified. ] [changes to interface kindbind semantics raph.levien@gmail.com**20060701033608 This patch changes the way kindbind in .ghi files are interpreted, and fixes some kind/interface bugs along the way. In the new semantics, importing an interface with a kindbind statement causes the two kinds to be unified. Exporting an interface with a kindbind checks whether the two kinds are actually the same. In both cases, it's expected that both kinds in the kindbind are defined in the kind namespace. ] [add zfc-pax.gh, a construction of pax in set.mm raph.levien@gmail.com**20060628050227] [a bunch of fixes to pred-thms raph.levien@gmail.com**20060624224634] [prove peano >=tr; slight reorg of 19.21 variants raph.levien@gmail.com**20060617084609] [checkin of pax peano module; pred-thms updates raph.levien@gmail.com**20060614052756] [add simple "basetype" interface for constant type raph.levien@gmail.com**20060611045031] [glue logic to connect typed and untyped pax raph.levien@gmail.com**20060611044440] [gh_verify.py: return exit code 1 if verification fails Marnix Klooster **20060610061141 This is useful when calling gh_verify.py from within a makefile, like I usually do. ] [gh_verify.py: now also check that an exported interface defines all variables which it uses. Marnix Klooster **20060610061008] [gh_verify.py: fixed minor format string error Marnix Klooster **20060610060937] [Added 'calcpropeq': calcprop + equality operator. Marnix Klooster **20060609212556] [Calcprop: fix in exported interface: added missing variable. Marnix Klooster **20060609212416 Note that this should have been caught by gh_verify.py, but obviously it wasn't. Well, it is, but only when you actually try to *import* this exported interface somewhere (which is how I found this). ] [Calcprop: added (-> F G), and derived modus ponens inference rule (30). Marnix Klooster **20060605190911] [Calcprop: exporting th-25. Marnix Klooster **20060605190819] [Calcprop: added proof for theorem 15. Marnix Klooster **20060605190752] [Calcprop: added proof of theorem (19). Marnix Klooster **20060605190657] [Calcprop: added proof of theorem (25). Marnix Klooster **20060525112110] [Calcprop: switched steps in proof of (24), to match [Lifschitz] closer. Marnix Klooster **20060525110335] [Completed the list of propositional DS axioms. Marnix Klooster **20060525064455] [Added proof sketches to prove (1a)+(1b) equivalent to (mpbi)+(leibniz). Marnix Klooster **20060525064421] [Initial version of 'calculational propositional logic'. Marnix Klooster **20060524150840] [Fix error message: a proof step which is a term resulted in a TypeError. Marnix Klooster **20060524145544] [Added necessary variable to hol/hol.ghi interface. (Found by latest .ghi checking improvement.) Marnix Klooster **20060518043225] [tighten up kind/arity checking of ghi stmt's raph.levien@gmail.com**20060517194940] [Debugging fix: properly print a step that is a term instead of a atom (variable or hypothesis/statement label). Marnix Klooster **20060517101817] [new thms for beta conversion and type definition raph.levien@gmail.com**20060218070549] [fix "stack at end of proof" error report raph.levien@gmail.com**20060218070349] [add type environment to ghol proving signature raph.levien@gmail.com**20051226223808] [initial commit of ghol (prototype HOL) raph.levien@gmail.com**20051226220552] [fix up error printing for term sexps raph.levien@gmail.com**20051124221330] [Added hash-bang lines to python scripts to make them executable. Marnix Klooster **20051124111722] [use a more straightfoward lexical interface raph.levien@gmail.com**20051123205702] [checking of interface export; small fixes in db raph.levien@gmail.com**20051122074815] [make dummy dv's optional raph.levien@gmail.com**20051118095501] [separate stack for mand hyps (improve error reporting) raph.levien@gmail.com**20051118015702] [change to sexp representation of terms in proof steps raph.levien@gmail.com**20051117214729] [partial implementation of export; fixes raph.levien@gmail.com**20051117211232] [initial checkin of pax subdir, new prop naming raph.levien@gmail.com**20051031221611] [minor fixup of import/export raph.levien@gmail.com**20051031192418] [make HOL derived proofs go through raph.levien@gmail.com**20051031191524] [fix of dummy var; checkin of base hol and zfc raph.levien@gmail.com**20051031184645] [fixups to mm_xlat for new set.mm raph.levien@gmail.com**20051025075111] [initial checkin of basic python implementation raph.levien@gmail.com**20051025064439] Patch bundle hash: a6ca1797147fce8ac2a17925ee295daba7b86407