------------------------------------------------------------------------ r2552 | schwicht | 2012-03-16 08:58:36 +0100 (Fri, 16 Mar 2012) | 1 line Updated ------------------------------------------------------------------------ r2551 | schwicht | 2012-03-16 08:57:50 +0100 (Fri, 16 Mar 2012) | 2 lines permutative-aconst-proof-to-eta-expansion-aux corrected: proof-to-formula replaced by aconst-to-inst-formula ------------------------------------------------------------------------ r2550 | schwicht | 2012-03-15 21:57:19 +0100 (Thu, 15 Mar 2012) | 1 line Updated ------------------------------------------------------------------------ r2549 | schwicht | 2012-03-15 21:56:19 +0100 (Thu, 15 Mar 2012) | 2 lines Removed add-totality for pos and int. They are already in numbers.scm. ------------------------------------------------------------------------ r2548 | schwicht | 2012-03-15 21:55:36 +0100 (Thu, 15 Mar 2012) | 1 line Removed add-mr-ids for TotalNat. It is already in lib/nat.scm. ------------------------------------------------------------------------ r2547 | schwicht | 2012-03-13 23:38:36 +0100 (Tue, 13 Mar 2012) | 1 line Updated ------------------------------------------------------------------------ r2546 | schwicht | 2012-03-13 23:26:31 +0100 (Tue, 13 Mar 2012) | 1 line RatEq replaced by RatEqv ------------------------------------------------------------------------ r2545 | schwicht | 2012-03-13 23:25:46 +0100 (Tue, 13 Mar 2012) | 4 lines In ord-field-simp-bwd the newly generated global assumption ex k RealLt 0(abs x)k -> ... 0 ... -> atom -> simp-atom now is formulated (as it should) with an integer k, not a pos. RatEq replaced by RatEqv ------------------------------------------------------------------------ r2544 | schwicht | 2012-03-13 23:25:03 +0100 (Tue, 13 Mar 2012) | 1 line Updated ------------------------------------------------------------------------ r2543 | schwicht | 2012-03-13 23:21:30 +0100 (Tue, 13 Mar 2012) | 1 line Updated ------------------------------------------------------------------------ r2542 | schwicht | 2012-03-13 23:20:56 +0100 (Tue, 13 Mar 2012) | 8 lines Added totality proofs. The successor S for pos renamed in PosS, to avoind conflict with the reserved name STotal. CpxMax CpxMin removed. SOne pos1--SZero pos2 mapsto SZero pos1--(SZero pos2--1) replaced by mapsto SOne(pos1--pos2). ALGEBRA-EDGE-TO-EMBED-TERM-ALIST needs to be updated once PosToNat and NatToInt have been proved to be total. replace-item-in-algebra-edge-to-embed-term-alist provided for this. Postponed: some rewrite rules, and totality proofs of PosMax PosMin. RatEq renamed into RatEqv to avoid clash with ordinary equality. ------------------------------------------------------------------------ r2541 | schwicht | 2012-03-13 23:20:22 +0100 (Tue, 13 Mar 2012) | 4 lines TotalListMR and STotalListMR added. ListAppendTotalSound ListAppendSTotalSound ListAppendNilPartialSound ListAppdTotalSound ListAppdSTotalSound ListAppdNilPartialSound ListLengthTotalSound ListLengthSTotalSound ListProjTotal ListProjTotalSound added. ------------------------------------------------------------------------ r2540 | schwicht | 2012-03-13 23:19:53 +0100 (Tue, 13 Mar 2012) | 29 lines TotalNatMR added. Inductively defined predicate TotalBoole moved to boole.scm. (add-theorem AndConstTotal and-const-total-proof) moved to ets.scm. NatIfTotal NatEqTotal NatLtToLe and NatLeGeToEq added. NatLtToLePred and NatLtMonPred added. NatEqToEqD added. NatIfTotal NatEqTotal NatLtToLe and NatLeGeToEq added. NatLtToLePred and NatLtMonPred added. Monotonicity properties NatLeMonPlus, NatLeMonTimes, NatLeMonPred, NatLeMonMinus added. NatPlusMinus NatMinusPlus NatMinusPlusEq NatMinusMinus added. Further rewrite rules added: nat1*Pred nat2 => nat1*nat2--nat1 Pred nat2*nat1 => nat2*nat1--nat1 nat1*(nat2--nat3) => nat1*nat2--nat1*nat3 (nat2--nat3)*nat1 => nat2*nat1--nat3*nat1 nat1+nat2 False nat1+nat2 False nat1<=nat2+nat1 => True Pred nat<=nat => True nat1--nat2<=nat1 => True 0--nat => 0 nat1+nat2--nat2 => nat1 nat2+nat1--nat2 => nat1 nat1--nat2--nat3 => nat1--(nat2+nat3) Renamed Nat=Trans into NatEqTrans, etc. Generally: = -> Eq. For Leibniz equality use EqD ------------------------------------------------------------------------ r2539 | schwicht | 2012-03-13 23:10:49 +0100 (Tue, 13 Mar 2012) | 33 lines In formula-to-et-type treatment of preconst TotalMR included. formula-of-nulltype? and formula-of-nulltype-under-extension? in the preconst case Total corrected (the result then must be #f). proof-to-extracted-term-aux corrected for an ExR elim aconst with c.i. kernel. proof-to-extracted-term and theorem-to-extracted-term get an unfold-let-flag as optional argument. If it is present and true, than cId's will be unfolded. axiom-to-extracted-term theorem-to-extracted-term and global-assumption-to-extracted-term added. imp-formulas-to-et-rec-const adapted to c.r. Total predconsts. efeqd-proof added. This allows to put EFEqD into THEOREMS when loading init. It is done here, since the proof uses EqDCompat. constructors-overlap-imp-falsity-proof added. This can be used for formula-to-efq-proof and this in turn for inversion. Added (before the internal proof of soundness): and-const-total-proof boole-if-total-proof . Theorem BooleIfTotal added. idpredconst-to-mr-idpredconst corrected. In real-and-formula-to-mr-formula-aux c.r. idpcs with identity instead of an alg name (i.e., ExL, ExR, ExLT, ExRT, AndR) are treated separately. In the predconst case the predconst Total (which is c.r.) gets a special treatment. Local variable pvar-to-mr-pvar replaced by reference to a newly introduced global variable PVAR-TO-MR-PVAR, which refers to and updates PVAR-TO-MR-PVAR-ALIST. proof-to-soundness-proof-aux extended to Intro and Elim axioms for inductively defined predicates. Auxiliary functions number-and-idpredconst-to-intro-mr-proof imp-formulas-to-mr-elim-proof proof-to-allnc-impnc-proof real-mr-clause-proof-and-clause-to-clause-proof allnc-impnc-to-exu-imp-proof added. exl-formula-to-exl-intro-mr-proof exr-formula-to-exr-intro-mr-proof exu-formula-to-exu-intro-mr-proof andr-formula-to-andr-intro-mr-proof eqd-elim-aconst-to-eqd-mr-elim-proof added. axiom-to-soundness-proof theorem-to-soundness-proof and global-assumption-to-soundness-proof added. proof-to-soundness-formula added. ------------------------------------------------------------------------ r2538 | schwicht | 2012-03-13 23:10:08 +0100 (Tue, 13 Mar 2012) | 2 lines elem-form? redefined, to make formulas built with (inductively defined) binary connectives (ord, andd etc) elementary. ------------------------------------------------------------------------ r2537 | schwicht | 2012-03-13 23:09:24 +0100 (Tue, 13 Mar 2012) | 20 lines set-goal displays the goal with the originally chosen variable names: it uses display-num-goal with fold-formula only. This overrides the default display function (with rename-variables) in display-num-goal . Error message introduced for sg . INITIAL-THEOREMS updated, InhabTotalMR included. INITIAL-COQ-GOAL-DISPLAY set to true. display-num-goal uses rename-variables (default case). If renaming of variables in a goal is not desired, use display-current-goal-with-original-variables abbreviated dcgo . assert and cut both accept a string as argument, which is parsed into a formula. drop-except added. In (drop-except . x-list), x-list is a list of numbers or strings identifying hypotheses from the context. A new goal is created, which differs from the previous one only in display aspects: all hypotheses except the listed ones are hidden (but still present). split extended to inductively defined conjunctions andd andr andu. msplit adapted to right-associative and. ex-intro accepts a string as argument, which is parsed into a term. compat-at and compat-rev-at rewritten, using Leibniz equality EqD rather than Equal. This makes Equal obsolete. Auxiliary functions finalg-to-string and finalg-to-=-to-eqd-aconst added. simphyp-with-intern corrected. simp-with-to removed. ------------------------------------------------------------------------ r2536 | schwicht | 2012-03-13 23:08:15 +0100 (Tue, 13 Mar 2012) | 14 lines Corrected (free variables were forgotten): make-proof-in-andd-elim-left-form make-proof-in-andd-elim-right-form make-proof-in-andr-elim-left-form make-proof-in-andr-elim-right-form make-proof-in-andu-elim-left-form make-proof-in-andu-elim-right-for display-proof display-normalized-proof proof-to-expr and proof-to-expr-with-formulas now have opt-proof-or-thm-name as argument. opt-proof-or-thm-name-and-ignore-deco-flag now has opt-proof-or-thm-name-and-ignore-deco-flag as argument. Adapted to admissible substitutions: proof-to-goedel-gentzen-translation-aux spreading-formula-to-proof spreading-formula-to-proof-aux wiping-formula-to-proof wiping-formula-to-proof-aux isolating-formula-to-proof isolating-formula-to-proof-aux Suffix Real (for realize) changed to MR. In reset TotalMR included. Typo corrected: myerreor -> myerror. ------------------------------------------------------------------------ r2535 | schwicht | 2012-03-13 23:07:37 +0100 (Tue, 13 Mar 2012) | 30 lines aconst=? gives #f in case one argument is not of aconst form. check-aconst corrected for Elim and Gfp aconsts. total-aconst removed. It is obsolete because Total f unfolds via unfold-formula into allnc x^(Total x^ -> Total(f x^)). STotal make-stotal stotal-aconst and the initial theorem Stotal removed. Reason: stotality does not make sense abstractly, but only for an algebra. There it can be defined inductively. Example: STotalList. constr-name-to-constr-total-aconst removed: this is just what the clauses of TotalNat say. constr-name-and-index-to-constr-total-args-aconst removed. Reason: TotalNat(Succ n^) -> TotalNat n^ can be proved by inversion (cf test.scm for the idpc Even). total-pair-aconst and total-proj-aconst removed, because for instance Total(x^ @y^) unfolds via unfold-formula into Total x^ & Total y^ . Moreover one should use the inductively defined TotalYprod(x^ pair y^) instead. finalg-to-eq-to-=-1-aconst and finalg-to-eq-to-=-2-aconst and finalg-to-=-to-eq-aconst are obsolete because Equal is. TotalInhab renamed into InhabTotal. inhabtotalmr-aconst added. sfinalg-to-se-to-stotal-aconst and sfinalg-to-stotal-to-se-aconst removed since they contain the obsolete predconct STotal. allnc-allncpartial-aconst and its converse allncpartial-allnc-aconst and also ex-expartial-aconst expartial-ex-aconst exnc-exncpartial-aconst exncpartial-exnc-aconst conflict with Total being c.r. and are discarded. idpc-clause-to-rec-premises added. non-computational-invariant? extended to inductively defined connectives. theorem-or-global-assumption-name-to-pconst-name changed: RatTimesTotal maps to RatTimes, not cRatTimesTotal. add-theorem adapted to the case where the theorem name ends with Total. add-global-assumption accepts a string as argument, which is parsed into a formula. Suffix Real (for realize) changed to MR. ------------------------------------------------------------------------ r2534 | schwicht | 2012-03-13 23:03:25 +0100 (Tue, 13 Mar 2012) | 1 line STotal removed and TotalMR added predconst-names. ------------------------------------------------------------------------ r2533 | schwicht | 2012-03-13 23:02:47 +0100 (Tue, 13 Mar 2012) | 5 lines make-totalmr added. formula-substitute extended to predconst TotalMR. make-stotal removed. unfold-formula now unfolds (Total r) via term-to-totality-formula and (TotalMR r0 r) via terms-to-mr-totality-formula. rename-variables-aux simplified for identity substitutions. formula-subst-and-beta0-nf added. ------------------------------------------------------------------------ r2532 | schwicht | 2012-03-13 23:02:17 +0100 (Tue, 13 Mar 2012) | 27 lines Suffix Real (for realize) changed to MR. terms-to-mr-totality-formula alg-to-mr-totality-idpredconst and alg-name-to-mr-totality-idpredconst-name added. string-and-arity-to-predconst-parse-function rewritten with formula-substitute, to parse Total and (arity nat) into TotalNat. check-idpredconst added, as test function for idpredconsts. If the argument is not an idpredconst, an error is returned. idpredconst-name-to-tvars corrected for mr-idpcs. We must distinguish whether we have an original idpc or an mr-idpc. In the former case take orig-idpredconst-name-to-tvars, i.e., the tvars in the original clauses. In the latter case from et-types take all tvars associated to param-pvars. These mr-tvars are appended in front of orig-tvars. add-ids-aux adapted: param-tvars and param-pvars are only computed after idpc-names are added to IDS. This enables the new idpredconst-name-to-tvars (which distinguishes original idpc-names and mr-idpc-names) to produce correct results. add-mr-ids corrected. cr-param-pvars and ci-param-pvars treated differently. Its auxiliary functions formula-to-et-type-for-mr-clauses and real-and-idpc-clause-to-mr-idpc-clause both need additional arguments mr-et-tvars and idpc-pvars. Notice that the general real-and-formula-to-mr-formula-aux does not need these additional arguments mr-et-tvars and idpc-pvars: in the pvar case the h-deg of the pvar suffices. term-to-totality-formula and term-to-stotality-formula corrected for terms with type in star form. In real-and-idpc-clause-to-mr-idpc-clause and formula-to-et-type-for-mr-clauses in the predconst case the predconst Total (which is c.r.) gets a special treatment. ------------------------------------------------------------------------ r2531 | schwicht | 2012-03-13 23:01:38 +0100 (Tue, 13 Mar 2012) | 4 lines token-tree-to-string extended to tokens case-op and caseitem-op. Auxiliary function token-tree-tag-to-precedence added. token-tree-to-pp-tree added. pretty-print-with-case-display (abbreviated ppc) added. ------------------------------------------------------------------------ r2530 | schwicht | 2012-03-13 23:00:14 +0100 (Tue, 13 Mar 2012) | 14 lines app-term-with-low-original-types? added. It is used in term-to-token-tree, to display coercions where the strategy of doing arthmetical operations at the lowest possible level has not been observed. Example: (IntPlus pos n) has this display, not (pos+n). The pconst RealPos does not appear, since it has no special display. formula-to-token-tree need not be changed, since a prime formula is either given by a boolean term or else has no special display (examples: RealEq RealNNeg RealLe). default-term-to-token-tree in case term-in-if-form and a newly introduced global variable CASE-DISPLAY is true returns a token tree with case-op, which includes token trees with case-item. In term-to-expr NatMax and NatMin etc allowed. term-in-rec-normal-form? corrected. term-to-rec-nf added. match-aux extended to match Total xs with TotalList ns. huet-unifiers-rigid-rigid extended similarly. ------------------------------------------------------------------------ r2529 | schwicht | 2012-03-13 22:59:46 +0100 (Tue, 13 Mar 2012) | 7 lines display-pconst corrected for external code. In add-rewrite-rule reference (via make-eq) to the obsolete predicate constant Equal removed. In change-t-deg-to-one usage of (term-to-string lhs) replaced by (token-tree-to-string (default-term-to-token-tree lhs)). This avoids disappearance of coercion functions like NatToInt, which can lead to type errors in subsequent parsing. In destruct-at wrong parenthesis moved to the right place. ------------------------------------------------------------------------ r2528 | schwicht | 2012-03-13 22:59:08 +0100 (Tue, 13 Mar 2012) | 5 lines TotalMR added as reserved name. check-admissible-tpsubst added, as test function for tpsubsts. If the argument is not an admissible tpsubst, an error is returned. type-match-modulo-coercion-aux corrected. For the rigid components of the type type-le? had to be used in the ~other direction. ------------------------------------------------------------------------ r2527 | schwicht | 2012-03-13 22:58:09 +0100 (Tue, 13 Mar 2012) | 1 line list-and-test-to-head-up-to-last added. ------------------------------------------------------------------------ r2526 | schwicht | 2012-03-13 22:57:16 +0100 (Tue, 13 Mar 2012) | 1 line Theory of spreading, wiping and isolating formulas included. ------------------------------------------------------------------------ r2525 | miyamoto | 2011-10-10 20:10:43 +0200 (Mon, 10 Oct 2011) | 3 lines The latest minitab.scm from the latest grammar.scm. In pconst.scm, a bug in destruct-at fixed. ------------------------------------------------------------------------ r2524 | schwicht | 2011-08-27 16:52:09 +0200 (Sat, 27 Aug 2011) | 1 line Updated ------------------------------------------------------------------------ r2523 | schwicht | 2011-08-27 16:50:59 +0200 (Sat, 27 Aug 2011) | 2 lines Proof of totality of Test updated. Totality predicate for the algebra par added. ------------------------------------------------------------------------ r2522 | schwicht | 2011-08-27 16:49:53 +0200 (Sat, 27 Aug 2011) | 4 lines Adapted to the the new convention in psym.scm: in add-ids et-constr-names written with capital C followed by the clause name (like CInitEv) to avoid clash with program constants for the clause-theorems. Hence we need CGenQ rather than cGenQ. ------------------------------------------------------------------------ r2521 | schwicht | 2011-08-14 15:32:47 +0200 (Sun, 14 Aug 2011) | 1 line Initial commit ------------------------------------------------------------------------ r2520 | schwicht | 2011-08-14 14:52:24 +0200 (Sun, 14 Aug 2011) | 1 line Updated ------------------------------------------------------------------------ r2519 | schwicht | 2011-08-14 14:51:41 +0200 (Sun, 14 Aug 2011) | 1 line Extended. ------------------------------------------------------------------------ r2518 | schwicht | 2011-08-14 14:50:33 +0200 (Sun, 14 Aug 2011) | 1 line Major extension, and adaption to the present state. ------------------------------------------------------------------------ r2517 | schwicht | 2011-08-14 14:49:12 +0200 (Sun, 14 Aug 2011) | 1 line For tutor.tex second call to pdflatex and dependencies added. ------------------------------------------------------------------------ r2516 | schwicht | 2011-08-14 14:48:26 +0200 (Sun, 14 Aug 2011) | 1 line Updated, and sychronized with examples/tutor.scm. ------------------------------------------------------------------------ r2515 | schwicht | 2011-08-14 14:47:03 +0200 (Sun, 14 Aug 2011) | 1 line Adapted to list.scm (not listrev.scm which should be removed). ------------------------------------------------------------------------ r2514 | schwicht | 2011-08-14 14:46:29 +0200 (Sun, 14 Aug 2011) | 1 line Adapted to list.scm (not listrev.scm which should be removed). ------------------------------------------------------------------------ r2513 | schwicht | 2011-08-14 14:45:21 +0200 (Sun, 14 Aug 2011) | 1 line Major cleanup and extension. ------------------------------------------------------------------------ r2512 | schwicht | 2011-08-14 14:44:38 +0200 (Sun, 14 Aug 2011) | 6 lines atom-to-eqd-true-aconst and eqd-true-to-atom-aconst added. formula-to-et-type for the predicate constant Total_rho returns rho. idpredconst-to-et-type corrected: et-types must use all clauses. In number-and-idpredconst-to-et-constr-term et-constr-names written with capital C followed by the clause name (like CInitEv) to avoid clash with program constants for the clause-theorems. ------------------------------------------------------------------------ r2511 | schwicht | 2011-08-14 14:44:09 +0200 (Sun, 14 Aug 2011) | 8 lines by-assume and by-assume-intern extended to the inductively defined existential quantifiers exd, exr, exl, exu. exnc marked as obsolete. It can be replaced by exr. Display function for display-num-goal now has as default case (lambda (fla) (rename-variables (fold-formula fla))). STotal as a premise in ind and simind and cases and casedist with a partial variable removed: one should use elim instead. dec-stotal-cases-proof removed. coind-intern corrected in the simultaneous case. ------------------------------------------------------------------------ r2510 | schwicht | 2011-08-14 14:43:41 +0200 (Sun, 14 Aug 2011) | 2 lines proof-substitute changed to avoid superfluous renaming (work of Anton Freund). ------------------------------------------------------------------------ r2509 | schwicht | 2011-08-14 14:43:14 +0200 (Sun, 14 Aug 2011) | 14 lines check-aconst adapted to atom-to-eqd-true-aconst and eqd-true-to-atom-aconst. Both all-allpartial-aconst and allpartial-all-aconst written with allnc alpha^(Total alpha^ -> (Pvar alpha)alpha^) rather than with all alpha^(Total alpha^ -> (Pvar alpha)alpha^). This is necessary since the predicate constant Total is c.r. In all-formulas-to-uninst-imp-formulas-and-tpsubst only all-formulas with total variables are allowed. stotal-imp-formula? stotal-or-se-imp-formula? stotal-or-se-or-e-imp-formula? all-partial-stotal-imp-formula? marked as obsolete. imp-formulas-to-uninst-gfp-formulas-etc corrected in the simultaneous case: all clauses are needed, and the original ordering of the idpcs needs to be introduced at various places (corrections due to Kenji Miyamoto). In add-theorem totality-flag is used to indicate that no proof of totality is needed. ------------------------------------------------------------------------ r2508 | schwicht | 2011-08-14 14:42:45 +0200 (Sun, 14 Aug 2011) | 3 lines Token and display for desyprod (destructor w.r.t. yprod) added. term-to-components rewritten. It now works for the primitive product (via make-star) as well as for the defined product (via make-yprod). ------------------------------------------------------------------------ r2507 | schwicht | 2011-08-14 14:41:53 +0200 (Sun, 14 Aug 2011) | 3 lines make-eq marked as obsolete. mk-and rewritten. make-and-without-truth added. In formula-substitute the predicate form Total r now uses term-to-totality-formula for the substituted term r. ------------------------------------------------------------------------ r2506 | schwicht | 2011-08-14 14:41:21 +0200 (Sun, 14 Aug 2011) | 2 lines pretty-print-string uses rename-variables for names of theorems or global-assumptions. ------------------------------------------------------------------------ r2505 | schwicht | 2011-08-14 14:40:55 +0200 (Sun, 14 Aug 2011) | 3 lines nbe-mk-prod-obj added. rec-op-and-args-to-if-term rewritten. simplify-simrec-appterm corrected: alg-names-with-val-tvars should remain in the order given by the recursion operator. ------------------------------------------------------------------------ r2504 | schwicht | 2011-08-14 14:40:06 +0200 (Sun, 14 Aug 2011) | 22 lines clauses-with-idpc-pvars-to-nullary-clauses added. It is used in add-ids to check that nullary clauses are present (and might be used in formula-to-efq-proof to construct such a proof for an idpc). In add-ids-aux total program constants for the clause-theorems added. In add-ids et-constr-names written with capital C followed by the clause name (like CInitEv) to avoid clash with program constants for the clause-theorems. term-to-totality-formula extended to terms of type in star form. add-stotality and its auxiliary function alg-name-to-stotality-clauses-and-pvars removed. Instead one should use add-ids with the proper clauses for e.g. STotalList. Then one can provide a known alg name (nat in this case). term-to-stotality-formula rewritten. For an sfinalg it uses STotalAlg rather than TotalAlg, assuming STotalAlg exists (otherwise: error) In alg-name-to-totality-clauses-and-pvars pvar name totality-idpc-name replaced by the empty string. In add-totality double occurrence of constr-names-list removed. display-idpc added. remove-idpc-name corrected (more was to be removed). add-co takes an optional argument opt-prim-prod-flag. If this is not present or true, the clause is formed with mk-ex, mk-and (generating extracted terms with the primitive product make-star). If this is present and #f, the clause is formed with mk-exi, mk-andu, mk-andd (generating extracted terms with the defined product yprod) ------------------------------------------------------------------------ r2503 | schwicht | 2011-08-14 14:39:33 +0200 (Sun, 14 Aug 2011) | 17 lines In add-program-constant an optional totality-flag can indicate that no proof of totality is needed. display-pconst added. It replaces display-program-constants and display-program-constant. Terminology in arrow-types-to-uninst-recop-types-and-tsubst clarified. alg-or-arrow-types-to-uninst-corecop-types-and-tsubst corrected in the simultaneous case: the uninst-step-types need to be taken in their original order (correction due to Kenji Miyamoto). In corec-const-and-bound-to-bcorec-term again in the simultaneous case the resulting application term of product type (with a recursion constant as operator) is replaced by an appropriate component. This makes both bcorec-term-and-alg-name-to-component and bcorec-term-and-alg-name-to-component-aux (which were originally intended for this purpose) superfluous. They are discarded. display-constructors renamed into display-alg and moved to typ.scm. undelay-delayed-corec corrected: terms in lcomp and rcomp form included. alg-to-uninst-destr-type-and-tsubst alg-to-destr-const and destruct-at all take opt-prim-prod-flag as an optional argument. ------------------------------------------------------------------------ r2502 | schwicht | 2011-08-14 14:38:49 +0200 (Sun, 14 Aug 2011) | 6 lines mk-star added. In compose-substitutions compose-substitutions-and-beta-nf compose-substitutions-and-beta0-nf it is now checked that the second substitution is admissible for the values of the first substitution (work of Anton Freund). display-constructors renamed into display-alg and moved from pconst.scm to typ.scm. ------------------------------------------------------------------------ r2501 | schwicht | 2011-08-14 14:38:08 +0200 (Sun, 14 Aug 2011) | 3 lines Inductively defined predicate TotalList added. Arguments of Consn switched: the parameter argument now comes first. Usage of finalg-to-e-to-total-aconst removed from proofs totality theorems. ------------------------------------------------------------------------ r2500 | schwicht | 2011-08-14 14:37:32 +0200 (Sun, 14 Aug 2011) | 3 lines Inductively defined predicate TotalNat and TotalBoole added. Usage of finalg-to-e-to-total-aconst removed from the proof of NatPlusTotal and other totality theorems. ------------------------------------------------------------------------ r2499 | schwicht | 2011-08-14 14:34:26 +0200 (Sun, 14 Aug 2011) | 1 line Renamed. Was tutorial.scm ------------------------------------------------------------------------ r2498 | schwicht | 2011-06-18 16:56:23 +0200 (Sat, 18 Jun 2011) | 1 line Updated ------------------------------------------------------------------------ r2497 | schwicht | 2011-06-18 16:55:11 +0200 (Sat, 18 Jun 2011) | 2 lines arrow-types-to-corec-const replaced by alg-or-arrow-types-to-corec-const ------------------------------------------------------------------------ r2496 | schwicht | 2011-06-18 16:54:34 +0200 (Sat, 18 Jun 2011) | 2 lines Adapted to corecursion with improper argument types. Inversion for coinductively defined predicates considered. ------------------------------------------------------------------------ r2495 | schwicht | 2011-06-18 16:53:57 +0200 (Sat, 18 Jun 2011) | 2 lines In is-comparison and simp-comparison EqD with synt-total arguments admitted. ------------------------------------------------------------------------ r2494 | schwicht | 2011-06-18 16:52:56 +0200 (Sat, 18 Jun 2011) | 1 line arrow-types-to-corec-const replaced by alg-or-arrow-types-to-corec-const ------------------------------------------------------------------------ r2493 | schwicht | 2011-06-18 16:51:52 +0200 (Sat, 18 Jun 2011) | 3 lines In formula-with-total-extract? typo corrected. Double occurrence of proof-to-extracted-term-aux removed. In proof-to-extracted-term-aux case Gfp corrected. ------------------------------------------------------------------------ r2492 | schwicht | 2011-06-18 16:51:21 +0200 (Sat, 18 Jun 2011) | 3 lines In coind-intern imp-form-to-conclusion replaced (twice) by imp-form-to-final-conclusion . Order of arguments for Gfp axiom corrected. ------------------------------------------------------------------------ r2491 | schwicht | 2011-06-18 16:50:51 +0200 (Sat, 18 Jun 2011) | 1 line Double occurrence of proof-to-extracted-term-aux removed. ------------------------------------------------------------------------ r2490 | schwicht | 2011-06-18 16:50:05 +0200 (Sat, 18 Jun 2011) | 4 lines In imp-formulas-to-uninst-gfp-formulas-etc make-ord replaced by make-orl if the premise of an imp-formula is non-computational. In h-deg-violations-aux Closure and Gfp added as aconst receiving a special treatment in proof-to-extracted-term . ------------------------------------------------------------------------ r2489 | schwicht | 2011-06-18 16:49:27 +0200 (Sat, 18 Jun 2011) | 1 line Prefix display des for Destr introduced. ------------------------------------------------------------------------ r2488 | schwicht | 2011-06-18 16:48:49 +0200 (Sat, 18 Jun 2011) | 3 lines mk-andi-for-sorted-formulas added and used for a better mk-andi . formula-substitute changed to avoid superfluous renaming (work of Anton Freund). ------------------------------------------------------------------------ r2487 | schwicht | 2011-06-18 16:48:19 +0200 (Sat, 18 Jun 2011) | 1 line In add-co make-= replaced by make-eqd . ------------------------------------------------------------------------ r2486 | schwicht | 2011-06-18 16:47:46 +0200 (Sat, 18 Jun 2011) | 5 lines make-term-in-app-form adapted to present terminology. term-in-const-form-to-string adapted to corecursion with improper argument types. term-substitute changed to avoid superfluous renaming (work of Anton Freund). ------------------------------------------------------------------------ r2485 | schwicht | 2011-06-18 16:47:06 +0200 (Sat, 18 Jun 2011) | 9 lines In add-computation-rule add-rewrite-rule types-to-embedding inserted, to allow the same input as in the displayed computation rule. Corresponding change in change-t-deg-to-one . Double occurrence of add-rewrite-rule removed. In rec-at definition of rec-args corrected, using a new constr-name-to-rec-args-indicator (work of Kenji Miyamoto). arrow-types-to-uninst-corecop-types-and-tsubst replaced by alg-or-arrow-types-to-uninst-corecop-types-and-tsubst , and constructor-type-to-product-type adapted to corecursion with improper argument types. ------------------------------------------------------------------------ r2484 | schwicht | 2011-05-24 21:05:46 +0200 (Tue, 24 May 2011) | 1 line Section on axioms updated ------------------------------------------------------------------------ r2483 | schwicht | 2011-05-24 14:06:20 +0200 (Tue, 24 May 2011) | 1 line Updated sections on constants, predicates, terms and formulas ------------------------------------------------------------------------ r2482 | schwicht | 2011-05-19 11:30:11 +0200 (Thu, 19 May 2011) | 1 line Section on predicates extended (coinductive definitions). ------------------------------------------------------------------------ r2481 | schwicht | 2011-05-18 11:40:20 +0200 (Wed, 18 May 2011) | 1 line Initial commit ------------------------------------------------------------------------ r2480 | schwicht | 2011-05-18 11:20:04 +0200 (Wed, 18 May 2011) | 1 line Initial commit ------------------------------------------------------------------------ r2479 | schwicht | 2011-05-18 08:46:37 +0200 (Wed, 18 May 2011) | 1 line Section on program constants extended (general recursion, corecursion). ------------------------------------------------------------------------ r2478 | schwicht | 2011-05-17 15:06:05 +0200 (Tue, 17 May 2011) | 1 line Updated ------------------------------------------------------------------------ r2477 | schwicht | 2011-05-17 15:05:08 +0200 (Tue, 17 May 2011) | 1 line Adapted to the new lib/natinf.scm (with ysumu). Dot notation removed. ------------------------------------------------------------------------ r2476 | schwicht | 2011-05-17 15:00:44 +0200 (Tue, 17 May 2011) | 1 line Extended and updated ------------------------------------------------------------------------ r2475 | schwicht | 2011-05-16 21:29:01 +0200 (Mon, 16 May 2011) | 1 line Updated ------------------------------------------------------------------------ r2474 | schwicht | 2011-05-16 21:28:13 +0200 (Mon, 16 May 2011) | 1 line Discarded code removed ------------------------------------------------------------------------ r2473 | schwicht | 2011-05-16 21:24:28 +0200 (Mon, 16 May 2011) | 1 line Now obsolete; its main contents have been moved in the trunk. ------------------------------------------------------------------------ r2472 | schwicht | 2011-05-16 21:23:11 +0200 (Mon, 16 May 2011) | 1 line Cleaned up. ------------------------------------------------------------------------ r2471 | schwicht | 2011-05-16 21:22:02 +0200 (Mon, 16 May 2011) | 1 line Adapted to add-co. ------------------------------------------------------------------------ r2470 | schwicht | 2011-05-16 21:21:05 +0200 (Mon, 16 May 2011) | 1 line Adapted to the algebra ysumu. ------------------------------------------------------------------------ r2469 | schwicht | 2011-05-16 21:19:16 +0200 (Mon, 16 May 2011) | 2 lines Typo in exercise 4.5(3) corrected. ------------------------------------------------------------------------ r2468 | schwicht | 2011-05-16 21:18:27 +0200 (Mon, 16 May 2011) | 2 lines yplus replaced by ysum, and ytensor replaced by ypair, and then ypair replaced by yprod. ------------------------------------------------------------------------ r2467 | schwicht | 2011-05-16 21:16:59 +0200 (Mon, 16 May 2011) | 2 lines multiline-comment added. ------------------------------------------------------------------------ r2466 | schwicht | 2011-05-16 21:16:16 +0200 (Mon, 16 May 2011) | 5 lines ypair replaced by yprod. Addition of uysum and ysumu is not reported. remove-tvar-name gives a warning instead of an error if no tvar with the give name exists. remove-alg-name gives a warning instead of an error if no algebra with the give name exists. ------------------------------------------------------------------------ r2465 | schwicht | 2011-05-16 21:15:10 +0200 (Mon, 16 May 2011) | 2 lines remove-var-name uses multiline-comment rather than comment when a non-existing variable is removed. ------------------------------------------------------------------------ r2464 | schwicht | 2011-05-16 21:14:17 +0200 (Mon, 16 May 2011) | 19 lines remove-program-constant uses multiline-comment rather than myerror when a non-existing program-constant is removed. fixed-rules-name? extended by CoRec and Destr. arrow-types-to-uninst-recop-types-and-tsubst rewritten. constructor-type-to-step-type simplified. arrow-types-to-rec-const introduced to replace the obsolete arrow-type-to-rec-const and type-info-to-rec-const . arrow-type-to-uninst-casesop-type-and-tsubst corrected. arrow-types-to-uninst-corecop-types-and-tsubst constructor-type-to-product-type arrow-types-to-corec-consts arrow-types-to-corec-const corec-at corec-const-to-uninst-corecop-types corec-const-to-corec-consts corec-const-to-uninst-arrow-types corec-const-and-bound-to-bcorec-term corec-test-and-abstr-constr-terms-to-if-term bcorec-term-and-alg-name-to-component bcorec-term-and-alg-name-to-component-aux and undelay-delayed-corec added. The latter replaces every corec constant term by the result of (corec-const-and-bound-to-bcorec-term corec-const bound). Destructors added, via alg-to-uninst-destr-type-and-tsubst alg-to-destr-const destruct-at . ------------------------------------------------------------------------ r2463 | schwicht | 2011-05-16 21:12:02 +0200 (Mon, 16 May 2011) | 2 lines term-in-const-form-to-string adapted to CoRec and Destr. term-in-rec-normal-form? corrected. ------------------------------------------------------------------------ r2462 | schwicht | 2011-05-16 21:10:56 +0200 (Mon, 16 May 2011) | 11 lines ypair replaced by yprod. remove-pvar-name and remove-predconst-name use multiline-comment rather than comment when a non-existing predicate variable or constant is removed. In add-ids it is enforced that every newly created algebra has as its name the string alg followed by the idpredconst-name. This is to allow removal of this algebra when removing the idpredconst-name. In remove-idpc-name only those alg-name are removed which were newly created with the idpc-name (like algEven for Even). COIDS and INITIAL-COIDS added. add-co adds companions for inductively defined predicate constants to COIDS, for instance CoEv, CoOd for Ev, Od. The optional algebra names and pvars are the same as for the corresponding idpcs. ------------------------------------------------------------------------ r2461 | schwicht | 2011-05-16 21:09:30 +0200 (Mon, 16 May 2011) | 4 lines make-= now returns an atom if the term arguments are of finitary algebra type, and Leibniz equality otherwise. mk-andd mk-andr mk-andu mk-andi make-andr-without-truth mk-ord mk-orl mk-orr mk-oru mk-ori added. formula-with-total-extract? added. ------------------------------------------------------------------------ r2460 | schwicht | 2011-05-16 21:08:30 +0200 (Mon, 16 May 2011) | 13 lines make-term-in-cons-form mk-term-in-cons-form term-in-cons-form? term-in-cons-form-to-left term-in-cons-form-to-right make-term-in-car-form make-term-in-cdr-form term-to-components added. Typo corrected (Inl -> InL). ypair renamed into yprod. lft and rht made prefix-op rather than postfix-op. make-yprod yprod-form-to-left-type yprod-form-to-right-type yprod-form? mk-yprod yprod-form? added. make-ysum ysum-form-to-left-type ysum-form-to-right-type ysum-form? mk-ysum ysum-form? mk-ysum-without-unit and its inverse ysum-without-unit-to-components added. Algebra uysum added as prefix-typeop, with constructors DummyL and InrUysum (prefix display string Inr). Similarly algebra ysumu added as postfix-typeop, with constructors InlYsumu (prefix display string Inl) and DummyR. ------------------------------------------------------------------------ r2459 | schwicht | 2011-05-16 21:07:38 +0200 (Mon, 16 May 2011) | 10 lines In aconst-to-inst-formula Gfp is treated as Elim: it can have free variables in its uninstantiated formula. imp-formulas-to-uninst-gfp-formulas-etc imp-formulas-to-uninst-gfp-formula-etc imp-formulas-to-gfp-aconst added. In check-aconst Closure and Gfp added. In aconst-without-rules? Exnc-Intro and Exnc-Elim added. coidpredconst-to-closure-aconst added. remove-theorem gives a warning instead of an error if no theorem with the give name exists. In add-theorem the generated program constant now has the same degree of totality as the extracted term of the proof. ------------------------------------------------------------------------ r2458 | schwicht | 2011-05-16 21:05:57 +0200 (Mon, 16 May 2011) | 1 line proof-substitute adapted to Gfp aconsts. ------------------------------------------------------------------------ r2457 | schwicht | 2011-05-16 21:04:18 +0200 (Mon, 16 May 2011) | 1 line coind added. Dot notation in comment removed. ------------------------------------------------------------------------ r2456 | schwicht | 2011-05-16 21:03:22 +0200 (Mon, 16 May 2011) | 4 lines Everything connected to and, or made rightassociative. Reason: ypair, ysum were (and will be) rightassociative, but and, or not. Exchanged arguments in grammar clauses for orformula, tail-orformula, andformula, tail-andformula, orterm, andterm. CoRec and Destr added. ------------------------------------------------------------------------ r2455 | schwicht | 2011-05-16 21:02:39 +0200 (Mon, 16 May 2011) | 4 lines token-tree-tag-left-assoc? and token-tree-tag-right-assoc? adapted: and-op and or-op are now rightassociative. In token-tree-to-string and token-tree-to-pp-tree in case alg-typeop an unnecessary space before a parenthesis is removed. ------------------------------------------------------------------------ r2454 | schwicht | 2011-05-16 21:02:00 +0200 (Mon, 16 May 2011) | 4 lines ypair replaced by yprod. proof-to-extracted-term-aux adapted to Closure and Gfp axioms. idpredconst-to-et-type need not be changed. Idpreconst OrR now with algebra uysum instead of algOrR, and similarly OrL with ysumu instead of algOrL. formula-with-total-extract? added. ------------------------------------------------------------------------ r2453 | schwicht | 2011-04-13 12:00:53 +0200 (Wed, 13 Apr 2011) | 1 line Updated ------------------------------------------------------------------------ r2452 | schwicht | 2011-04-13 12:00:24 +0200 (Wed, 13 Apr 2011) | 10 lines Completely rewritten. Proofs in minimal logic for the Orevkov formulas A_i with an (unfolded) weak existential quantifier are constructed. These can be seen as proofs of bot from a (false) assumption u_i. Then A-translation can be applied to obtain a constructive existence proof, from which a witness can be extracted. One obtains logical proofs of existential formulas E_i (example for i=2: ex z578,z1,z0(R zero zero z578 & R zero z578 z1 & R zero z1 z0) from the two open assumptions hyp1: all y R y zero(S y) and hyp2: all y,x,z,z1(R y x z -> R z x z1 -> R y(S x)z1) whose length is linear in i, but whose witnesses are suberexponential in i. ------------------------------------------------------------------------ r2451 | schwicht | 2011-03-29 23:32:09 +0200 (Tue, 29 Mar 2011) | 1 line Minor editorial changes ------------------------------------------------------------------------ r2450 | schwicht | 2011-03-29 08:02:39 +0200 (Tue, 29 Mar 2011) | 1 line Major extension; was Tutorial2011.tex ------------------------------------------------------------------------ r2449 | schwicht | 2011-03-29 07:55:09 +0200 (Tue, 29 Mar 2011) | 1 line References updated ------------------------------------------------------------------------ r2448 | schwicht | 2011-03-28 21:38:48 +0200 (Mon, 28 Mar 2011) | 1 line Updated ------------------------------------------------------------------------ r2447 | schwicht | 2011-03-28 21:38:27 +0200 (Mon, 28 Mar 2011) | 1 line Initial commit ------------------------------------------------------------------------ r2446 | schwicht | 2011-03-28 21:37:11 +0200 (Mon, 28 Mar 2011) | 1 line Updated ------------------------------------------------------------------------ r2445 | schwicht | 2011-03-27 15:01:59 +0200 (Sun, 27 Mar 2011) | 1 line load for exi.scm remowed. It is now in the trunk. ------------------------------------------------------------------------ r2444 | schwicht | 2011-03-27 14:59:14 +0200 (Sun, 27 Mar 2011) | 1 line add-global-assumption for NatNotLtToLe removed. It is in nat.scm ------------------------------------------------------------------------ r2443 | schwicht | 2011-03-27 14:58:24 +0200 (Sun, 27 Mar 2011) | 1 line Examples for decorate rewritten. ------------------------------------------------------------------------ r2442 | schwicht | 2011-03-27 14:57:44 +0200 (Sun, 27 Mar 2011) | 1 line Examples for decorate added. ------------------------------------------------------------------------ r2441 | schwicht | 2011-03-27 14:56:16 +0200 (Sun, 27 Mar 2011) | 1 line Tokens andi, ori, exi, exnci added. ------------------------------------------------------------------------ r2440 | schwicht | 2011-03-27 14:55:23 +0200 (Sun, 27 Mar 2011) | 27 lines exi, exnci, ori and andi provided for input of inductively defined connectives. Depending on whether the formulas involved are of nulltype or not, internally one uses for exi: ExD, ExDT, ExL, ExLT, for exnci: ExR, ExRT, ExU, ExUT, for ori: OrD, OrL, OrR, OrU. for andi: AndD, AndR (if necessary with reversed formulas), AndU. Idpc-names ExL ExR ExLT ExRT AndR removed and added again, now with the string identity where we had an alg-name before. Idpc-name OrU removed and added again, now with the algebra boole as known-alg-name. idpredconst-to-et-type and formula-of-nulltype? adapted to identity as a possible opt-alg-name. formula-to-et-type and idpredconst-to-et-type are defined simultaneously. This makes sense, since the clauses and also the cterms of an idpredconst are prior to the idpredconst. formula-of-nulltype? and formula-of-nulltype-under-extension? rewritten. proof-to-extracted-term-aux adapted to identity as a possible opt-alg-name. Then a new identity-idpredconst-to-intro-et-term is used instead of number-and-idpredconst-to-et-constr-term . [x,f]f x is used as realizer for the elim axiom. ------------------------------------------------------------------------ r2439 | schwicht | 2011-03-27 14:52:47 +0200 (Sun, 27 Mar 2011) | 48 lines proof-to-free-cr-avars added. It returns all free avars with are not above a n.c. formula in the proof. It needs id-deco? as an extra argument, and depending on its value uses formula-of-nulltype? or formula-of-nulltype-under-extension? decorate corrected. Nothing is done if decfla is of nulltype, and all free avars are available initially. They will be reduced in case allnc-intro is applied. fully-decorate added. proof-to-ppat rewritten It turns every imp, all formula in the given proof into an impnc, allnc formula, and in case id-deco? is true moreover (i) every existential quantification exd, exl, exr into exu, (ii) every total existential quantification exdt, exlt, exrt into exut, (iii) every conjunction andd, andr into andu (andb is for the boolean operator), and (iv) every disjunction or, orl, orr into oru (orb is for the boolean operator). This includes the parts of an aconst which come from its uninstatiated formula. proof-to-ppat does not touch the c.i. parts of the proof, i.e., those which are above a c.i. formula. ppat is in general not a proof. ppat-and-decseq-and-availavars-to-proof-and-decavars corrected and its efficiency improved. We avoid the do loop in ppat-and-decseq-and-availavars-to-proof-and-decavars and use a named let instead. Both proof-to-ppat and ppat-and-decseq-and-availavars-to-proof-and-decavars take id-deco? as an additional argument. op-and-args-and-altop-and-decfla-and-availavars-to-proof rewritten It assumes that op applied to args proves an extension of decfla, and that altop differs from op only in possibly requiring additional premises. In case id-deco? this is w.r.t. full extension, otherwise w.r.t. imp-all extension. It is tested whether altop applied to args and some of availavars is between op applied to args and decfla w.r.t. the respective extension. If so, a proof based on altop is returned, else #f. ppat? as test function for proof patterns added. In aconst-and-decfla-to-proof a proof is returned (not an aconst) because of possible all's instead of allnc's binding free variables of the instantiated formula. Hence all-allnc-form-to-prefix and aconst-and-prefix-to-proof-of-modified-aconst suffice. cr-strengthened-dec-variants-to-proof added. check-and-display-proof corrected: initial tests for arguments were insufficient. check-and-display-proof-aux corrected: in case proof-in-imp-elim-form, an impnc-form with n.c premise is allowed. ------------------------------------------------------------------------ r2438 | schwicht | 2011-03-27 14:50:44 +0200 (Sun, 27 Mar 2011) | 42 lines exi, exnci, ori and andi provided for input of inductively defined connectives. Depending on whether the formulas involved are of nulltype or not, internally one uses for exi: ExD, ExDT, ExL, ExLT, for exnci: ExR, ExRT, ExU, ExUT, for ori: OrD, OrL, OrR, OrU. for andi: AndD, AndR (if necessary with reversed formulas), AndU. Added accordingly: make-andi, make-ori, make-exi, mk-exi, make-exnci, mk-exnci. all-allnc-form-to-prefix added. It computes the list of the first (car x) lists ('all/allnc var) of a formula. Decoration is split into an ordinary one restricted to imp and all, and a full one. In the latter the inductively defined connectives ExU, ExL, ExR, ExD, ExUT, ExLT, ExRT, ExDT, OrU, OrL, OrR, OrD, AndU, AndR, AndD are considered as (fully) decorated. A flag id-deco? indicates what is meant. Corresponding changes in formula.scm: formula-to-undec-formula prepares for decoration. It changes all occurrences of imp, all into impnc, allnc, and in case id-deco? is true, (i) every existential quantification exd, exl, exr into exu, (ii) every total existential quantification exdt, exlt, exrt into exut, (iii) every conjunction andd, andr into andu (andb is for the boolean operator), and (iv) every disjunction or, orl, orr into oru (orb is for the boolean operator). It does not touch formulas of nulltype under extension, and in case id-deco? is false it does not touch any formula of nulltype. cterm-to-undec-cterm , aconst-and-dec-inst-formula-to-extended-tpsubst idpredconst-to-undec-idpredconst dec-variants-to-lub extending-dec-variants? dec-variants? aconst-to-undec-aconst changed accordingly. They all take id-deco? as an additional argument . In bicons-to-lub-bicon cases for imp and impnc removed. In quants-to-lub-quant cases for all and allnc removed. formula=-aux? changed. A -> B and A --> B are considered equal if A is of nulltype. ------------------------------------------------------------------------ r2437 | schwicht | 2011-03-27 14:47:48 +0200 (Sun, 27 Mar 2011) | 7 lines add-ids and add-ids-aux extended to also cover the case of a string identity in the field where an opt-alg-name is expected. This is allowed iff there is exactly one clause with et-type of the form et-tvar=>idpc-pvar-tvar. Then no new algebra is created. Later [x]x will be taken as realizer for the (single) clause, and [x,f]f x as realizer for the elim axiom. AndL removed from idpredconst-to-string . ------------------------------------------------------------------------ r2436 | schwicht | 2011-03-27 14:46:18 +0200 (Sun, 27 Mar 2011) | 2 lines rec-at in case (and (nbe-constr-value? rec-val) (not nbe-for-idps?)) simplified: pd-objs selected first. ------------------------------------------------------------------------ r2435 | schwicht | 2011-03-27 14:43:19 +0200 (Sun, 27 Mar 2011) | 1 line In alg-name-to-tvars terminology corrected. ------------------------------------------------------------------------ r2434 | miyamoto | 2011-03-25 19:43:11 +0100 (Fri, 25 Mar 2011) | 2 lines Path names modified ------------------------------------------------------------------------ r2433 | schwicht | 2011-03-25 19:31:31 +0100 (Fri, 25 Mar 2011) | 1 line Initial commit ------------------------------------------------------------------------ r2432 | schwicht | 2011-03-25 19:25:23 +0100 (Fri, 25 Mar 2011) | 2 lines Initial commit ------------------------------------------------------------------------ r2431 | miyamoto | 2011-03-18 21:22:42 +0100 (Fri, 18 Mar 2011) | 2 lines cterm-to-arity fixed ------------------------------------------------------------------------ r2430 | miyamoto | 2011-03-18 14:02:29 +0100 (Fri, 18 Mar 2011) | 2 lines the computation rule for IntLe changed. ------------------------------------------------------------------------ r2429 | senjak | 2011-03-18 12:29:31 +0100 (Fri, 18 Mar 2011) | 2 lines Dontpublish again. ------------------------------------------------------------------------ r2428 | senjak | 2011-03-18 12:09:54 +0100 (Fri, 18 Mar 2011) | 2 lines Dontpublish was extended. ------------------------------------------------------------------------ r2427 | miyamoto | 2011-02-05 23:36:01 +0100 (Sat, 05 Feb 2011) | 2 lines Token "coRec" added. ------------------------------------------------------------------------ r2426 | schwicht | 2011-01-12 09:51:06 +0100 (Wed, 12 Jan 2011) | 1 line Updated ------------------------------------------------------------------------ r2425 | schwicht | 2011-01-12 09:50:30 +0100 (Wed, 12 Jan 2011) | 1 line NatNotLeToLt and NatNotLtToLe added. ------------------------------------------------------------------------ r2424 | schwicht | 2011-01-12 09:41:47 +0100 (Wed, 12 Jan 2011) | 1 line Updated ------------------------------------------------------------------------ r2423 | schwicht | 2011-01-12 09:40:59 +0100 (Wed, 12 Jan 2011) | 1 line Item for the Martelli-Montanari paper added. ------------------------------------------------------------------------ r2422 | schwicht | 2011-01-12 09:39:50 +0100 (Wed, 12 Jan 2011) | 21 lines Major extension of the sections ob types and constants. Section on parsing extended (with a large selection of variable names). Definition of rigid variables added. Definition of the Huet unification algorithm clarified in case flex-rigid. simphyp-with-to added. Typos corrected. Plan: extend and adapt normalization issues in term.scm. Among others: change nbe-normalize-term into nbe-normalize-term-without-eta term-to-eta-nf term-to-term-with-eta-expanded-if-terms term-to-outer-eta-expansion if-term-to-eta-expansion-and-unfolded-simrecs nbe-normalize-term term-to-term-without-predecided-ifs term-to-one-step-beta-reduct term-to-beta-nf term-to-beta-eta-nf term-to-beta-pi-eta-nf term-to-let-candidates term-to-term-with-let ------------------------------------------------------------------------ r2421 | schwicht | 2011-01-12 09:39:13 +0100 (Wed, 12 Jan 2011) | 3 lines Definition of rigid variables added. Definition of the Huet unification algorithm clarified in case flex-rigid. Citation according to natbib. Index added. ------------------------------------------------------------------------ r2420 | schwicht | 2011-01-12 09:38:11 +0100 (Wed, 12 Jan 2011) | 1 line aconst-to-repro-formulas renamed into aconst-to-repro-data . ------------------------------------------------------------------------ r2419 | schwicht | 2011-01-12 09:37:36 +0100 (Wed, 12 Jan 2011) | 6 lines In all-formulas-to-et-rec-const and imp-formulas-to-et-rec-const arrow-types removed from the constructed rec-const (they can be computed). all-formula-to-gind-aconst renamed into all-formula-and-number-to-gind-aconst . ------------------------------------------------------------------------ r2418 | schwicht | 2011-01-12 09:36:44 +0100 (Wed, 12 Jan 2011) | 3 lines all-formula-to-gind-aconst renamed into all-formula-and-number-to-gind-aconst . UNFOLDING-FLAG renamed into REC-UNFOLDING-FLAG ------------------------------------------------------------------------ r2417 | schwicht | 2011-01-12 09:36:18 +0100 (Wed, 12 Jan 2011) | 9 lines In proof-and-genavar-var-alist-to-pterm cases for Exnc-Intro and Exnc-Elim added (were forgotten). type-info-or-repro-formulas replaced by repro-data. aconst-to-repro-formulas renamed into aconst-to-repro-data . all-formula-to-gind-aconst renamed into all-formula-and-number-to-gind-aconst . ------------------------------------------------------------------------ r2416 | schwicht | 2011-01-12 09:35:53 +0100 (Wed, 12 Jan 2011) | 11 lines all-pair-formula-to-pair-elim-aconst and formula-to-efq-aconst and ex-formula-to-ex-intro-aconst and ex-formula-and-concl-to-ex-elim-aconst and exnc-formula-to-exnc-intro-aconst and exnc-formula-and-concl-to-exnc-elim-aconst corrected: psubst now constructed with make-subst-wrt pvar-cterm-equal? aconst-to-repro-formulas renamed into aconst-to-repro-data . aconst-to-computed-repro-formulas renamed into aconst-to-computed-repro-data . all-formula-to-gind-aconst renamed into all-formula-and-number-to-gind-aconst . ------------------------------------------------------------------------ r2415 | schwicht | 2011-01-12 09:35:22 +0100 (Wed, 12 Jan 2011) | 18 lines In term-in-const-form-to-string cases-const-to-param-types removed. In term-to-expr grecguard-const-to-param-types removed. posrecparam and natrecparam removed. In term-to-expr and rec-op-and-args-to-if-term and term-to-eta-nf-with-simplified-simrec-appterms and term-to-term-with-eta-expanded-if-terms-and-unfolded-simrecs rec-const-to-param-types removed. term-in-const-form-to-string rewritten. type-info-to-rec-string removed. type-info-or-repro-formulas replaced by repro-data. In formula.scm aconst-to-repro-formulas renamed into aconst-to-repro-data . cterm-to-arity corrected. ------------------------------------------------------------------------ r2414 | schwicht | 2011-01-12 09:34:44 +0100 (Wed, 12 Jan 2011) | 41 lines General recursion mentioned in the introduction. Typos corrected. Description of the format of type-info-or-repro-formulas extended to grecguard-const and grec-const. arrow-types-to-uninst-paramless-recop-types-and-tsubst renamed into arrow-types-to-uninst-recop-types-and-tsubst arrow-type-to-uninst-paramless-casesop-type-and-tsubst renamed into arrow-type-to-uninst-casesop-type-and-tsubst param-types-and-arrow-type-to-cases-const removed. arrow-type-to-cases-const defined directly. Description of constants made more complete and clearer. type-info-or-repro-formulas renamed into repro-data. check-const added. It assumes that the constant is not one of those used during proof normalization. type-info-etc-to-grecguard-const corrected: the constant needs a type-info as repro-data. As for recursion constants, the type of a grecguard constant is split into an uninst-grecguardop-type and a type substitution. grecguard-const-for-gind? removed, since this holds if and only if repro-data is a pair. type-info-to-grecguard-type renamed into type-info-to-uninst-grecguardop-type-and-tsubst . exnc-formula-to-exnc-intro-const exnc-formula-and-concl-to-exnc-elim-const exnc-formula-and-concl-to-exnc-elim-const-aux exnc-formula-and-concl-to-exnc-elim-const-obj added (were forgotten). const-substitute extended to also cover GRecGuard. UNFOLDING-FLAG renamed into REC-UNFOLDING-FLAG Removed rec-const-to-param-types and cases-const-to-param-types and grecguard-const-to-param-types . They are nowhere really needed. ------------------------------------------------------------------------ r2413 | schwicht | 2011-01-12 09:34:01 +0100 (Wed, 12 Jan 2011) | 4 lines var-to-string corrected: a type variable whose name ends with an ordinary character (e.g., alpha) needs a modifier _ before its index (e.g., alpha_1 and not alpha1). Reason: alpha1 is read as a variable of type alpha1 with index -1. ------------------------------------------------------------------------ r2412 | schwicht | 2011-01-12 09:33:32 +0100 (Wed, 12 Jan 2011) | 2 lines RESERVED-NAMES extended. In add-algebras-with-parameters del-constr renamed into delayed-constr. ------------------------------------------------------------------------ r2411 | schwicht | 2011-01-12 09:32:51 +0100 (Wed, 12 Jan 2011) | 1 line Major extension ------------------------------------------------------------------------ r2410 | schwicht | 2010-12-23 11:00:43 +0100 (Thu, 23 Dec 2010) | 1 line Correction: the file just commited was not the updated one. ------------------------------------------------------------------------ r2409 | schwicht | 2010-12-23 10:54:04 +0100 (Thu, 23 Dec 2010) | 1 line Updated ------------------------------------------------------------------------ r2408 | schwicht | 2010-12-23 10:52:47 +0100 (Thu, 23 Dec 2010) | 2 lines Adapted to replacement of algOrD by ysum, and of algExD, algExDT, algAndD by ypair. ------------------------------------------------------------------------ r2407 | schwicht | 2010-12-23 10:52:09 +0100 (Thu, 23 Dec 2010) | 2 lines Replaced algOrD by ysum. Similarly replaced algExD, algExDT, algAndD by ypair. ------------------------------------------------------------------------ r2406 | schwicht | 2010-12-22 15:50:42 +0100 (Wed, 22 Dec 2010) | 1 line Updated ------------------------------------------------------------------------ r2405 | schwicht | 2010-12-22 15:50:05 +0100 (Wed, 22 Dec 2010) | 2 lines imp-formulas-to-uninst-elim-formulas-etc corrected: parameters were not properly treated. ------------------------------------------------------------------------ r2404 | schwicht | 2010-12-22 11:00:14 +0100 (Wed, 22 Dec 2010) | 1 line Updated ------------------------------------------------------------------------ r2403 | schwicht | 2010-12-22 10:59:32 +0100 (Wed, 22 Dec 2010) | 3 lines use-intern corrected: sig-tvars were not treated properly. fla-and-sig-tvars-and-vars-and-goal-fla-to-use-data corrected: ord-form? orl-form? orr-form? oru-form? were forgotten. ------------------------------------------------------------------------ r2402 | schwicht | 2010-12-22 10:59:00 +0100 (Wed, 22 Dec 2010) | 3 lines context-to-tvars added. aconst-substitute corrected: psubst was not defined. fla-and-sig-tvars-and-vars-and-goal-fla-to-use-data corrected: ord-form? orl-form? orr-form? oru-form? were forgotten. ------------------------------------------------------------------------ r2401 | schwicht | 2010-12-22 10:58:26 +0100 (Wed, 22 Dec 2010) | 3 lines intro-aconst-to-computed-repro-data idpc-clause? check-aconst and number-and-idpredconst-to-intro-aconst adapted to the presence of parameter variables. ------------------------------------------------------------------------ r2400 | schwicht | 2010-12-22 10:58:02 +0100 (Wed, 22 Dec 2010) | 6 lines Superfluous log text removed. idpredconst-name-to-params added. Adaption of add-ids and add-ids-aux to inductively defined predicates with object parameters. This is necessary when defining natural numbers in an abstractly (by a type variable) given type of reals, with abstractly (by object variables) given zero and successor functions ------------------------------------------------------------------------ r2399 | schwicht | 2010-12-22 10:57:13 +0100 (Wed, 22 Dec 2010) | 3 lines add-prefix-display-string and add-postfix-display-string corrected: both expected in their add-token parts that valtype is of alg-form, which need not be the case. Now type-match is used. ------------------------------------------------------------------------ r2398 | schwicht | 2010-12-10 09:38:11 +0100 (Fri, 10 Dec 2010) | 4 lines simp-with-to added. It expects a string as its last argument, which is used (via name-hyp) to name the newly introduced simplified hypothesis. Typo corrected: imp--impnc-form-to-premise replaced by imp-impnc-form-to-premise. ------------------------------------------------------------------------ r2397 | schwicht | 2010-12-07 14:54:30 +0100 (Tue, 07 Dec 2010) | 1 line Tests for huet-match with products and projections added. ------------------------------------------------------------------------ r2396 | schwicht | 2010-12-07 14:42:55 +0100 (Tue, 07 Dec 2010) | 3 lines huet-unifiers-xi, huet-unifiers-rigid-rigid, huet-unifiers-match and huet-imitate-term corrected in case of terms in pair, lcomp or rcomp form. ------------------------------------------------------------------------ r2395 | schwicht | 2010-10-04 23:58:25 +0200 (Mon, 04 Oct 2010) | 1 line Updated ------------------------------------------------------------------------ r2394 | schwicht | 2010-10-04 23:57:17 +0200 (Mon, 04 Oct 2010) | 2 lines Cleaned variant with emphasis on symmetry. Based on work of Diana Ratiu and Trifon Trifonov. ------------------------------------------------------------------------ r2393 | schwicht | 2010-09-01 18:10:05 +0200 (Wed, 01 Sep 2010) | 1 line tcf included ------------------------------------------------------------------------ r2392 | schwicht | 2010-09-01 14:46:28 +0200 (Wed, 01 Sep 2010) | 1 line Updated ------------------------------------------------------------------------ r2391 | schwicht | 2010-08-14 18:41:19 +0200 (Sat, 14 Aug 2010) | 1 line Updated ------------------------------------------------------------------------ r2390 | schwicht | 2010-08-14 18:40:38 +0200 (Sat, 14 Aug 2010) | 3 lines Equal replaced by Leibniz equality. Adapted to usage of add-prefix-display-string add-postfix-display-string add-infix-display-string . :+: (for append) replaced by ++. ------------------------------------------------------------------------ r2389 | schwicht | 2010-08-14 18:40:06 +0200 (Sat, 14 Aug 2010) | 3 lines Equal replaced by Leibniz equality. Adapted to usage of add-prefix-display-string add-postfix-display-string add-infix-display-string . ------------------------------------------------------------------------ r2388 | schwicht | 2010-08-14 18:39:22 +0200 (Sat, 14 Aug 2010) | 3 lines In add-rewrite-rule a preceding proof of lhs eqd rhs is accepted. For readability of program constants add-prefix-display-string add-postfix-display-string add-infix-display-string added. ------------------------------------------------------------------------ r2387 | schwicht | 2010-08-09 19:49:19 +0200 (Mon, 09 Aug 2010) | 1 line Updated ------------------------------------------------------------------------ r2386 | schwicht | 2010-08-09 19:48:49 +0200 (Mon, 09 Aug 2010) | 2 lines In use2-closed-proof-intern pvars from sig-topvars removed from > uninst-pvars (this makes Efq-Log and Stab-Log behave as expected) ------------------------------------------------------------------------ r2385 | schwicht | 2010-08-09 11:35:23 +0200 (Mon, 09 Aug 2010) | 1 line Updated: major extension ------------------------------------------------------------------------ r2384 | schwicht | 2010-08-09 11:34:31 +0200 (Mon, 09 Aug 2010) | 1 line Updated ------------------------------------------------------------------------ r2383 | schwicht | 2010-08-09 11:33:49 +0200 (Mon, 09 Aug 2010) | 2 lines Moved to doc/tcf.tex: (1) material on admissible substitutions, (2) proofs for unification and proof search (3) (further) case studies. ------------------------------------------------------------------------ r2382 | schwicht | 2010-08-09 11:33:04 +0200 (Mon, 09 Aug 2010) | 1 line Initial commit ------------------------------------------------------------------------ r2381 | schwicht | 2010-07-29 15:38:22 +0200 (Thu, 29 Jul 2010) | 1 line Updated ------------------------------------------------------------------------ r2380 | schwicht | 2010-07-29 15:36:28 +0200 (Thu, 29 Jul 2010) | 6 lines Major update. The role of optional arguments in normalize-goal described. Description of use, use-with, cut, split, ind, simind, elim, cases, casedist updated. Description of assert, msplit, gind, intro-with, inversion, by-assume-minimal-with added. make-gind-aconst, make-min-pr-aconst, make-exc-intro-aconst, exc-formula-to-exc-intro-aconst described. ------------------------------------------------------------------------ r2379 | schwicht | 2010-07-29 15:30:36 +0200 (Thu, 29 Jul 2010) | 2 lines Removed var-name y before loading lib/list.scm. Added it later again. Switched COMMENT-FLAG off and on to speed up loading. ------------------------------------------------------------------------ r2378 | schwicht | 2010-07-29 15:30:05 +0200 (Thu, 29 Jul 2010) | 1 line Updated and extended. ------------------------------------------------------------------------ r2377 | schwicht | 2010-07-29 15:17:30 +0200 (Thu, 29 Jul 2010) | 8 lines term-to-beta-eta-nf added. In simultaneous substitution for type and object variables in a term it is allowed that the substitution affects variables whose type is changed by the substitution. Then the substitution must be admissible for the free variables in the term. compose-o-substitutions and compose-substitutions removed: they are superseded by the new compose-substitutions. match2 replaced by huet-match, which is defined as a special case of huet-unifiers: no flexible variables in the instance. huet-match picks a most ------------------------------------------------------------------------ r2376 | schwicht | 2010-07-29 15:16:16 +0200 (Thu, 29 Jul 2010) | 14 lines idpredconst-to-tpsubst replaces idpredconst-to-pinst. Comment to format of IDS updated. Part of add-ids moved into a new function add-ids-aux, which does not parse clause-strings any more. This is useful when after adding idpredconst one adds mr-idpredconst: it can now be done by a further call of add-ids-aux, via add-mr-ids. new-pvar renamed into idpc-pvar, new-tvar renamed into idpc-tvar. add-totality and add-stotality added In add-ids non-computational idpcs are allowed. Then (except in special cases) the elimination scheme must be restricted to n.c. formulas. Also, all (n.c.) clauses must be invariant. This ensures that the soundness theorem holds: every intro and elim axiom is invariant, i.e., nullterm mr A is the same as A. In add-ids-aux the (non-used) argument all-with-content? is removed. ------------------------------------------------------------------------ r2375 | schwicht | 2010-07-29 15:15:24 +0200 (Thu, 29 Jul 2010) | 2 lines Adapted to more general substitutions. term-substitute-aux replaced by term-substitute. pinst replaced by psubst. ------------------------------------------------------------------------ r2374 | schwicht | 2010-07-29 15:14:42 +0200 (Thu, 29 Jul 2010) | 2 lines A general compose-substitutions replaces compose-t-substitutions . admissible-substitution? added. ------------------------------------------------------------------------ r2373 | shuber | 2010-04-11 13:21:04 +0200 (Sun, 11 Apr 2010) | 3 lines Adapted commandline options for mzscheme version >=4; the parser now can also be built using guile. (Thanks to Freiric Barral and Trifon Trifonov.) ------------------------------------------------------------------------ r2372 | ratiu | 2010-03-18 15:17:44 +0100 (Thu, 18 Mar 2010) | 1 line Small fix in the proof of QuotRemTotal. ------------------------------------------------------------------------ r2371 | schwicht | 2010-03-13 02:37:43 +0100 (Sat, 13 Mar 2010) | 1 line Small corrections ------------------------------------------------------------------------ r2370 | shuber | 2010-03-12 21:02:22 +0100 (Fri, 12 Mar 2010) | 1 line minitab.scm updated ------------------------------------------------------------------------ r2369 | schwicht | 2010-01-14 16:15:53 +0100 (Thu, 14 Jan 2010) | 1 line Updated ------------------------------------------------------------------------ r2368 | schwicht | 2010-01-14 16:15:27 +0100 (Thu, 14 Jan 2010) | 2 lines In avar-full=? the test formula=? replaced by classical-formula=?. Reason: classical-formula=? also tests for equal normal forms. ------------------------------------------------------------------------ r2367 | schwicht | 2010-01-14 16:10:07 +0100 (Thu, 14 Jan 2010) | 1 line Line (lpar grecguard-op number typelist rpar) : ( (cons )) added. ------------------------------------------------------------------------ r2366 | schwicht | 2010-01-14 16:09:27 +0100 (Thu, 14 Jan 2010) | 2 lines grecguard-const-for-gind? corrected. It gave wrong results in case the value type tau had one argument type. ------------------------------------------------------------------------ r2365 | ratiu | 2009-12-29 14:29:28 +0100 (Tue, 29 Dec 2009) | 1 line The rewrite rules for dialectica cannot be proven, as they contain partial terms. ------------------------------------------------------------------------ r2364 | ratiu | 2009-12-29 14:25:49 +0100 (Tue, 29 Dec 2009) | 3 lines Removed from the repository, as all these examples are grouped in one file now: ../examples/classical/combinatorics/booleantape.scm ------------------------------------------------------------------------ r2363 | ratiu | 2009-12-29 14:19:09 +0100 (Tue, 29 Dec 2009) | 2 lines Renamed, to have a more suggestive name. ------------------------------------------------------------------------ r2362 | ratiu | 2009-12-29 14:17:49 +0100 (Tue, 29 Dec 2009) | 7 lines The directory combinatorics will contain examples from the field, such as the infinite Pigeonhole Principle (which can be used to show Ramsey's Theorem) and the finite Pigeonhole Principle, used in the proof of the Erdoes-Szekeres Theorem. The file booleantape.scm contains a simplified version of the infinite Pigeonhole Principle, referred to as Stolzenberg's Principle. ------------------------------------------------------------------------ r2361 | schwicht | 2009-12-10 18:14:49 +0100 (Thu, 10 Dec 2009) | 1 line NatLeLtCases added ------------------------------------------------------------------------ r2360 | schwicht | 2009-12-10 18:13:48 +0100 (Thu, 10 Dec 2009) | 2 lines token-tree-tag-left-assoc? and token-tree-tag-right-assoc? changed: tensor-op should be right associative ------------------------------------------------------------------------ r2359 | schwicht | 2009-12-10 18:12:32 +0100 (Thu, 10 Dec 2009) | 1 line predconst? corrected (order tsubst - index was wrong) ------------------------------------------------------------------------ r2358 | schwicht | 2009-12-10 18:11:39 +0100 (Thu, 10 Dec 2009) | 2 lines In avar-to-string (+ 1 index) replaced by index. This allows avars u0 in displays. ------------------------------------------------------------------------ r2357 | schwicht | 2009-12-10 18:10:45 +0100 (Thu, 10 Dec 2009) | 14 lines rename-bound-avars replaces all bound avars by new ones with the same name but a new index. Properties: (i) rename-bound-avars transforms a proof satisfying the avar convention w.r.t. its free avars into a proof satisfying the avar convention completely. (ii) In every subproof of the result no free avar occurs (w.r.t. avar=?) bound as well. Property (ii) is assumed in proof-substitute-aux. check-and-display-proof extended by checking the avar convention: two avars with the same name and index are equal. This done via avar-convention-violations . In proof-substitute-aux we must assume that in every subproof no free avar occurs bound as well. This is ensured by a preprocessing step, using rename-bound-avars. ------------------------------------------------------------------------ r2356 | schwicht | 2009-12-10 18:07:58 +0100 (Thu, 10 Dec 2009) | 3 lines (duplicates-wrt equality? l) returns a list of two-element sublists (x x') of equal elements of l whose transitive closure consists of all such two-element sublists. ------------------------------------------------------------------------ r2355 | schwicht | 2009-12-10 18:06:13 +0100 (Thu, 10 Dec 2009) | 1 line proof-to-extracted-term-aux corrected: atr-x-formula removed ------------------------------------------------------------------------ r2354 | schwicht | 2009-11-13 12:48:39 +0100 (Fri, 13 Nov 2009) | 1 line Updated ------------------------------------------------------------------------ r2353 | schwicht | 2009-11-13 12:47:37 +0100 (Fri, 13 Nov 2009) | 1 line Minor cleanup. ------------------------------------------------------------------------