diff --git a/axioms.lisp b/axioms.lisp index 4c7e90fd4e9..15d7a56c0d2 100644 --- a/axioms.lisp +++ b/axioms.lisp @@ -17170,7 +17170,7 @@ evaluated. See :DOC certify-book, in particular, the discussion about ``Step ; Without the setting of custom:*default-file-encoding* for clisp in ; acl2.lisp, the build breaks with the following string (note the accented "i" ; in Martin, below): -; Francisco J. Martín Mateos +; Francisco J. Martín Mateos ; With that setting, we do not need an explicit :external-format argument for ; the call of with-open-file in acl2-check.lisp that opens a stream for ; "acl2-characters". diff --git a/books/defexec/dag-unification/dag-unification-l.lisp b/books/defexec/dag-unification/dag-unification-l.lisp index 0527cd16014..a42f0ea749c 100644 --- a/books/defexec/dag-unification/dag-unification-l.lisp +++ b/books/defexec/dag-unification/dag-unification-l.lisp @@ -1,6 +1,6 @@ ;;; ============================================================================ ;;; dag-unification-l.lisp -;;; Título: A dag based unification algorithm +;;; Título: A dag based unification algorithm ;;; ============================================================================ #| To certify this book: @@ -22,7 +22,7 @@ ;;; ============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;; ============================================================================ diff --git a/books/defexec/dag-unification/dag-unification-rules.lisp b/books/defexec/dag-unification/dag-unification-rules.lisp index 7eb28655d67..118d488e271 100644 --- a/books/defexec/dag-unification/dag-unification-rules.lisp +++ b/books/defexec/dag-unification/dag-unification-rules.lisp @@ -1,6 +1,6 @@ ;;; ============================================================================ ;;; dag-unification-rules.lisp -;;; Título: Unification rules on term dags +;;; Título: Unification rules on term dags ;;; ============================================================================ #| To certify this book: @@ -21,7 +21,7 @@ ;;; ============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;; ============================================================================ diff --git a/books/defexec/dag-unification/dag-unification-st.lisp b/books/defexec/dag-unification/dag-unification-st.lisp index 295237574e6..16b15d632e6 100644 --- a/books/defexec/dag-unification/dag-unification-st.lisp +++ b/books/defexec/dag-unification/dag-unification-st.lisp @@ -1,6 +1,6 @@ ;;; ============================================================================ ;;; dag-unification-st.lisp -;;; Título: A dag based unification algorithm using stobjs +;;; Título: A dag based unification algorithm using stobjs ;;; ============================================================================ #| To certify this book: @@ -21,7 +21,7 @@ ;;; ============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;; ============================================================================ @@ -571,7 +571,7 @@ ;;; Guard verification: -;;; REPETIDOS ¿ LOS DEJO? +;;; REPETIDOS ¿ LOS DEJO? (local @@ -1176,7 +1176,7 @@ ;;; Guard verification -;;; AVERIGUAR POR QUé ESTE TEOREMA TARDA TANTO!!!!!!!! +;;; AVERIGUAR POR QUé ESTE TEOREMA TARDA TANTO!!!!!!!! ;;; I don't know why, but the following theory has an important diff --git a/books/defexec/dag-unification/dags.lisp b/books/defexec/dag-unification/dags.lisp index 0809e887446..42c0be522e6 100644 --- a/books/defexec/dag-unification/dags.lisp +++ b/books/defexec/dag-unification/dags.lisp @@ -1,6 +1,6 @@ ;;; ============================================================================ ;;; dags.lisp -;;; Título: Term dags in ACL2 +;;; Título: Term dags in ACL2 ;;; ============================================================================ #| To certify this book: @@ -18,7 +18,7 @@ ;;; ============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;; ============================================================================ @@ -510,7 +510,7 @@ (not (dag-p-aux hs rp g))))) ;;; Finally, the soundness theorem: -;;; ······························· +;;; ............................... (defthm dag-p-soundness (implies (not (dag-p g)) @@ -554,7 +554,7 @@ ;;; The main lemma for completeness: -;;; ································ +;;; ................................ (local (defthm dag-p-aux-completeness-main-lemma @@ -1601,7 +1601,7 @@ ;;; RECALL: These two theorems would allow us to define functions like these: -;;; ········································································· +;;; ......................................................................... ; (defun occur-check-l (flg x h g) diff --git a/books/defexec/dag-unification/list-unification-rules.lisp b/books/defexec/dag-unification/list-unification-rules.lisp index 6857b2dad79..1ca954decf3 100644 --- a/books/defexec/dag-unification/list-unification-rules.lisp +++ b/books/defexec/dag-unification/list-unification-rules.lisp @@ -1,5 +1,5 @@ ;;; ============================================================================;;; list-unification-rules.lisp -;;; Título: Unification as transformation rules +;;; Título: Unification as transformation rules ;;; (using a prefix representation of terms) ;;; ============================================================================ @@ -17,7 +17,7 @@ ;;; ============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;; ============================================================================ diff --git a/books/defexec/dag-unification/matching.lisp b/books/defexec/dag-unification/matching.lisp index 5f41e45c884..df18988d543 100644 --- a/books/defexec/dag-unification/matching.lisp +++ b/books/defexec/dag-unification/matching.lisp @@ -89,9 +89,9 @@ ;;; ---------------------------------------------------------------------------- -;;; ············································································ +;;; ............................................................................ ;;; 1.2.1 How we deal with selection. -;;; ············································································ +;;; ............................................................................ ;;; Firs we prove that equal-set is a congruence w.r.t. the second @@ -139,9 +139,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 1.2.2 transform-subs-sel preserves the set of matchers. -;;; ············································································ +;;; ............................................................................ (local @@ -211,7 +211,7 @@ (not (matcher sigma S))))) ;;; The three main theorems of this subsubsection -;;; ············································· +;;; ............................................. (defthm transform-subs-sel-preserves-matchers-1 (implies @@ -235,10 +235,10 @@ -;;; ············································································ +;;; ............................................................................ ;;; 1.2.3 (system-substitution (cdr S-match)) is an invariant in the rules ;;; of transformation. -;;; ············································································ +;;; ............................................................................ @@ -261,9 +261,9 @@ (system-substitution (cdr (transform-subs-sel S-match))))))) -;;; ············································································ +;;; ............................................................................ ;;; 1.2.4 Main property of the property system-substitution -;;; ············································································ +;;; ............................................................................ (local @@ -362,7 +362,7 @@ (length-term nil args2)))))) ;;; And the main result: -;;; ···················· +;;; .................... (defthm transform-subs-sel-decreases-length-of-first-system (implies (not (normal-form-syst S-match)) @@ -460,7 +460,7 @@ ;;; Three lemmas to state that the set of matchers is preserved by ;;; subs-system-sel -;;; ·········································································· +;;; .......................................................................... (local (defthm subs-system-sel-preserves-matchers-1 @@ -488,7 +488,7 @@ (in-theory (enable union-systems)) ;;; subs-system-sel preserves the property of being a system-substitution. -;;; ·································································· +;;; .................................................................. (local (defthm subs-system-sel-preserves-system-substitution @@ -496,7 +496,7 @@ (system-substitution (cdr (subs-system-sel S-match)))))) ;;; Guard verification: a substitution-s-p is returned -;;; ··················································· +;;; ................................................... (local (defthm @@ -604,7 +604,7 @@ ;;; ---------------------------------------------------------------------------- ;;; Soundness -;;; ········· +;;; ......... (defthm subs-sel-soundness @@ -618,7 +618,7 @@ ;;; Completeness -;;; ············ +;;; ............ (defthm subs-sel-completeness @@ -632,7 +632,7 @@ ;;; Closure property: ;;; (the following theorem is needed for guard verification) -;;; ························································ +;;; ........................................................ (defthm matching-sel-substitution-s-p diff --git a/books/defexec/dag-unification/subsumption-subst.lisp b/books/defexec/dag-unification/subsumption-subst.lisp index 6eefb93b664..376e8836953 100644 --- a/books/defexec/dag-unification/subsumption-subst.lisp +++ b/books/defexec/dag-unification/subsumption-subst.lisp @@ -26,15 +26,15 @@ ;;; Our goal is to define the subsumption relation between ;;; substitutions. In the literature, this relation is defined in this ;;; way: -;;; sigma <= delta iff (exists gamma) gamma·sigma = delta -;;; where "·" stands for composition. +;;; sigma <= delta iff (exists gamma) gamma.sigma = delta +;;; where "." stands for composition. ;;; Note that equality between substitutions is functional equality (we cannot ;;; use equal), so we reformulate this property as: ;;; (*) sigma <= delta iff (exists gamma) ;;; s.t. for all term -;;; gamma·sigma(term) = delta(term) +;;; gamma.sigma(term) = delta(term) ;;; Our goal in this book is to define the subsumption relation between @@ -285,9 +285,9 @@ ;;; if (subs-sust sigma delta) ;;; WE DISTINGUISH THREE CASES. -;;; ············································································ +;;; ............................................................................ ;;; 3.1.1 Case 1: x is a variable outside V -;;; ············································································ +;;; ............................................................................ @@ -303,14 +303,14 @@ :hints (("Goal" :in-theory (enable x-not-in-domain-remains-the-same))))) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.2. Case 2: x is a variable of (domain-var sigma) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.2.1 A lemma for this case 2: ;;; subs-subst composed with sigma is equal to delta in V. -;;; ······················································ +;;; ...................................................... (local (encapsulate @@ -373,7 +373,7 @@ (local (in-theory (disable subs-subst matching-subst))) ;;; 3.1.2.2 Another lemma for case 2: -;;; ······························· +;;; ............................... (local (defthm variables-co-domain-var @@ -383,7 +383,7 @@ ;;; 3.1.2.3 The main result for Case 2 -;;; ································ +;;; ................................ (local (defthm @@ -396,14 +396,14 @@ (val x delta))))) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.3. Case 3: x in V but not in (domain-var sigma) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.3.1 A lemma for Case 3 ;;; In this case, matching and matching-subst-r take the same values. -;;; ································································· +;;; ................................................................. (local (defthm @@ -472,7 +472,7 @@ ;;; With terms and list of terms (not only with variables) -;;; ······················································ +;;; ...................................................... (local (defthm @@ -512,7 +512,7 @@ ;;; following version will be used as a rewrite rule. ;;; With terms but without using composition -;;; ········································ +;;; ........................................ (defthm subs-subst-implies-matching-subst-r-appplied-to-sigma-term-is-delta-term @@ -526,7 +526,7 @@ ;;; With respect to subsumption between terms -;;; ········································· +;;; ......................................... ;;; Trivial consequence of completeness of subsumption and the previous @@ -563,7 +563,7 @@ ;;; existence of two substitutions, called sigma-w and delta-w and the ;;; only property we will assume about them is that sigma-w <= ;;; delta-w. That is, exists another substitution gamma-w such that -;;; delta-w = gamma-w·sigma-w. +;;; delta-w = gamma-w.sigma-w. ;;; We will use encapsulate for that purpose. Let sigma-w, delta-w and ;;; gamma-w three susbtitutions such that delta-w is functionally equal diff --git a/books/defexec/dag-unification/subsumption.lisp b/books/defexec/dag-unification/subsumption.lisp index c746ba3c0f1..c14a737f388 100644 --- a/books/defexec/dag-unification/subsumption.lisp +++ b/books/defexec/dag-unification/subsumption.lisp @@ -1,7 +1,7 @@ ;;; subsumption.lisp Definition of a particular RULE-BASED matching ;;; algorithm between terms. We use functional instantion of the ;;; pattern given in matching.lisp Using this algorithm, we define the -;;; subsumption relñation between terms and lists of terms in a +;;; subsumption relñation between terms and lists of terms in a ;;; constructive way, and we prove that subsumption is a preorder. ;;; Created: 11-10-99 Last revison: 07-12-2000 ;;; ============================================================================= @@ -287,7 +287,7 @@ ;;; Most of these properties are obtained by functional instantiation. ;;; Soundness -;;; ········· +;;; ......... (defthm subs-soundness (implies (subs t1 t2) @@ -298,7 +298,7 @@ ;;; Completeness -;;; ············· +;;; ............. (defthm subs-completeness (implies (equal (instance t1 sigma) t2) @@ -308,7 +308,7 @@ (:instance match-mv-completeness (S (list (cons t1 t2))))))) ;;; Substitution-s-p (closure property) -;;; ··································· +;;; ................................... (defthm matching-substitution-s-p @@ -318,7 +318,7 @@ (:instance match-mv-substitution-s-p (S (list (cons t1 t2))))))) ;;; Substitution-p (needed for guard verification) -;;; ·············································· +;;; .............................................. (defthm matching-substitution-p @@ -409,7 +409,7 @@ (second (pair-args l1 (apply-subst nil sigma l1))))) ;;; Soundness -;;; ········· +;;; ......... (defthm subs-list-soundness @@ -421,7 +421,7 @@ ;;; Completeness -;;; ············· +;;; ............. (defthm subs-list-completeness (implies (equal (apply-subst nil sigma l1) l2) @@ -431,7 +431,7 @@ (:instance match-mv-completeness (S (first (pair-args l1 l2))))))) ;;; Substitution-s-p (closure property) -;;; ··································· +;;; ................................... (defthm matching-list-substitution-s-p @@ -444,7 +444,7 @@ ;;; Substitution-p (needed for guard verification) -;;; ·············································· +;;; .............................................. (defthm matching-list-substitution-p @@ -498,7 +498,7 @@ ;;; ---------------------------------------------------------------------------- ;;;; Subsumption reflexive -;;;; ····················· +;;;; ..................... (defthm subsumption-reflexive (subs t1 t1) @@ -508,7 +508,7 @@ ;;;; Subsumption transitive -;;;; ······················ +;;;; ...................... (defthm subsumption-transitive @@ -528,7 +528,7 @@ ;;; ---------------------------------------------------------------------------- ;;; An useful rule: -;;; ··············· +;;; ............... (defthm subsumption-apply-subst (subs term (instance term sigma)) @@ -536,7 +536,7 @@ (t1 term) (t2 (instance term sigma)))))) ;;; Variables are minimum elements in this quasi-order -;;; ·················································· +;;; .................................................. (defthm variable-minimum-subsumption (implies (variable-p x) diff --git a/books/defexec/dag-unification/terms-as-dag.lisp b/books/defexec/dag-unification/terms-as-dag.lisp index b95751e1249..c85ce606185 100644 --- a/books/defexec/dag-unification/terms-as-dag.lisp +++ b/books/defexec/dag-unification/terms-as-dag.lisp @@ -1,6 +1,6 @@ ;;; ============================================================================ ;;; terms-as-dag.lisp -;;; Título: Storing first--order terms as dags +;;; Título: Storing first--order terms as dags ;;; ============================================================================ #| To certify this book: @@ -20,7 +20,7 @@ ;;; ============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;; ============================================================================ diff --git a/books/defexec/dag-unification/terms-dag-stobj.lisp b/books/defexec/dag-unification/terms-dag-stobj.lisp index 5c900f66b9c..ea0e6c3c28d 100644 --- a/books/defexec/dag-unification/terms-dag-stobj.lisp +++ b/books/defexec/dag-unification/terms-dag-stobj.lisp @@ -1,6 +1,6 @@ ;;; ============================================================================ ;;; terms-dag-stobj.lisp -;;; Título: The single--threaded object {\tt terms-dag} +;;; Título: The single--threaded object {\tt terms-dag} ;;; ============================================================================ #| To certify this book: @@ -16,7 +16,7 @@ ;;; ============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;; ============================================================================ diff --git a/books/defexec/dag-unification/terms.lisp b/books/defexec/dag-unification/terms.lisp index 84899b0f27a..a8ccc824571 100644 --- a/books/defexec/dag-unification/terms.lisp +++ b/books/defexec/dag-unification/terms.lisp @@ -939,7 +939,7 @@ (disjointp (variables nil (co-domain S)) (domain S)))) ;;; REMARK: In the literature, idempotent substitutions are defined as -;;; substitutions sigma such that sigma·sigma = sigma. But this +;;; substitutions sigma such that sigma.sigma = sigma. But this ;;; definition involves functional equality. We will see that the above ;;; definition implies this property (see main-property-mgs in the book ;;; unification-definition.lisp) Nevertheless, the definition does not @@ -949,9 +949,9 @@ ;;; functionally equivalent idempotent (in our sense) substitution, ((x ;;; . y)) in this case. -;;; ············································································ +;;; ............................................................................ ;;; 3.3.1 The main property of idempotent substitutions. -;;; ············································································ +;;; ............................................................................ ;;; .... PROOF PLAN: @@ -1103,9 +1103,9 @@ ;;; 4.2 Some results concerning the tree structure of a term ;;; ---------------------------------------------------------------------------- -;;; ············································································ +;;; ............................................................................ ;;; 4.2.1 Concatenation of positions -;;; ············································································ +;;; ............................................................................ (defthm position-p-append (implies (position-p p1 term) @@ -1128,9 +1128,9 @@ q x))))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.2 Substitutions and positions -;;; ············································································ +;;; ............................................................................ (defthm nth-apply-subst (implies (and (integerp i) @@ -1165,9 +1165,9 @@ (instance (replace-term term pos t1) sigma)))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.3 Prefix positions -;;; ············································································ +;;; ............................................................................ (local (defthm equal-len-replace-list @@ -1202,9 +1202,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 4.2.4 Disjoint positions -;;; ············································································ +;;; ............................................................................ (local (defun induct-position-p-disjoint (pos1 pos2 term) @@ -1267,9 +1267,9 @@ (position-p (cons i pos) (cons fn args))))))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.5 Disabling the theory -;;; ············································································ +;;; ............................................................................ (defconst *tree-structure-of-terms* '(position-p-append occurrence-append replace-term-append diff --git a/books/workshops/2000/medina/polynomials/polynomial.lisp b/books/workshops/2000/medina/polynomials/polynomial.lisp index 9a347e32d85..35b0ab260ed 100644 --- a/books/workshops/2000/medina/polynomials/polynomial.lisp +++ b/books/workshops/2000/medina/polynomials/polynomial.lisp @@ -6,7 +6,7 @@ ;;; Polynomial recognizer ;;; --------------------- -;;; Similar to «integer-listp» function. +;;; Similar to «integer-listp» function. (defun monomial-listp (l) (cond ((atom l) diff --git a/books/workshops/2000/medina/polynomials/term.lisp b/books/workshops/2000/medina/polynomials/term.lisp index ebb88be3ffc..46725c3ae2c 100644 --- a/books/workshops/2000/medina/polynomials/term.lisp +++ b/books/workshops/2000/medina/polynomials/term.lisp @@ -4,7 +4,7 @@ ;;; Natural recognizer ;;; ------------------ -;;; Similar to «integerp» macro. +;;; Similar to «integerp» macro. (defmacro naturalp (x) `(and (integerp ,x) (COMMON-LISP::<= 0 ,x))) @@ -13,7 +13,7 @@ ;;; True list of naturals recognizer ;;; -------------------------------- -;;; Similar to «integer-listp» function. +;;; Similar to «integer-listp» function. (defun natural-listp (l) (cond ((atom l) diff --git a/books/workshops/2000/ruiz/multiset/examples/ackermann/ackermann.lisp b/books/workshops/2000/ruiz/multiset/examples/ackermann/ackermann.lisp index 3aab40781fb..6bb98278df7 100644 --- a/books/workshops/2000/ruiz/multiset/examples/ackermann/ackermann.lisp +++ b/books/workshops/2000/ruiz/multiset/examples/ackermann/ackermann.lisp @@ -25,7 +25,7 @@ ;;; =========================================================================== ;;; This is the Ackermann function, classical definition: -;;; ····················································· +;;; ..................................................... (defun ack (m n) (declare (xargs :measure (cons (+ (nfix m) 1) (nfix n)) @@ -44,7 +44,7 @@ (verify-guards ack) ;;; Our goal is to define an iterative version of ack: -;;; ·················································· +;;; .................................................. ; (defun ack-it-aux (s z) ; (declare (xargs :mode :program)) @@ -136,7 +136,7 @@ ;;;---------------------------------------------------------------------------- ;;; Some lemmas needed to the admission of ack-it-aux -;;; ················································· +;;; ................................................. ;;; 1) @@ -192,7 +192,7 @@ ;;; At last, admission of ack-it-aux and definition of ack-it -;;; ························································· +;;; ......................................................... (defun nn-integer-true-listp (s) (declare (xargs :guard t)) diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.lisp b/books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.lisp index dfc78990a0c..8b869a9824a 100644 --- a/books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.lisp +++ b/books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.lisp @@ -327,9 +327,9 @@ (defun provably-equivalent (x y) (equal (normal-form x) (normal-form y))) -;;; ············································································ +;;; ............................................................................ ;;; 2.2.1 Completeness -;;; ············································································ +;;; ............................................................................ ;;; A proof between normal forms (local @@ -386,9 +386,9 @@ (p (make-proof-between-normal-forms x y p))))))) -;;; ············································································ +;;; ............................................................................ ;;; 2.2.1 Soundness -;;; ············································································ +;;; ............................................................................ ;;; A proof between x and y (if their normal forms are equal) diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/confluence.lisp b/books/workshops/2000/ruiz/multiset/examples/newman/confluence.lisp index f1940ac598a..5b84dd45ba9 100644 --- a/books/workshops/2000/ruiz/multiset/examples/newman/confluence.lisp +++ b/books/workshops/2000/ruiz/multiset/examples/newman/confluence.lisp @@ -305,9 +305,9 @@ (defun r-equiv (x y) (equal (normal-form x) (normal-form y))) -;;; ············································································ +;;; ............................................................................ ;;; 2.2.1 Completeness -;;; ············································································ +;;; ............................................................................ ;;; A proof between normal forms (local @@ -364,9 +364,9 @@ (p (make-proof-between-normal-forms x y p))))))) -;;; ············································································ +;;; ............................................................................ ;;; 2.2.1 Soundness -;;; ············································································ +;;; ............................................................................ ;;; A proof between x and y (if their normal forms are equal) diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp b/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp index 9ca2fd16186..b2b3a55b9d1 100644 --- a/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp +++ b/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp @@ -159,7 +159,7 @@ ;;; A noetherian and locally confluent reduction relation -;;; ····················································· +;;; ..................................................... (encapsulate @@ -227,7 +227,7 @@ ;;; See newman.lisp for details. ;;; Well-founded multiset extension of rel -;;; ······································ +;;; ...................................... ;(acl2::defmul-components rel) ;The list of components is: @@ -237,7 +237,7 @@ ;;; Auxiliary functions in the definition of transform-to-valley -;;; ··························································· +;;; ........................................................... (local (defun exists-local-peak (p) @@ -260,7 +260,7 @@ ;;; transform-to-valley terminates -;;; ······························ +;;; .............................. ;;; By functional instantiation of the same result in newman.lisp @@ -283,7 +283,7 @@ ;;; Definition of transform-to-valley -;;; ································· +;;; ................................. (local (defun transform-to-valley (p) @@ -298,7 +298,7 @@ ;;; Properties of transform-to-valley: the Church-Rosser property -;;; ····························································· +;;; ............................................................. ;;; By functional instantiation of the same results in newman.lisp @@ -338,7 +338,7 @@ ;;; axioms. ;;; Definition of proof-irreducible -;;; ······························· +;;; ............................... ;;; REMARK: Iteratively apply reduction steps until an irreducible ;;; element is found. This function termination can be justified by the @@ -358,7 +358,7 @@ ;;; Properties of proof-irreducible (normalizing property) -;;; ······················································ +;;; ...................................................... ;;; REMARK: These are the assumed proerties of proof-irreducible in ;;; confluence.lisp, in rewriting rule form: @@ -404,7 +404,7 @@ ;;; This is the same function as r-equiv in confluence.lisp -;;; ······················································· +;;; ....................................................... ;;; REMARK: normal-form-aux is analogue NWM::normal-form, but ;;; normal-form is more eficcient. The same for r-equiv. @@ -428,7 +428,7 @@ ;;; ---------------------------------------------------------------------------- ;;; Completeness -;;; ············ +;;; ............ ;;; By functional instantiation of the same results in confluence.lisp @@ -448,7 +448,7 @@ ;;; Soundness -;;; ········· +;;; ......... ;;; By functional instantiation of the same results in confluence.lisp diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/newman.lisp b/books/workshops/2000/ruiz/multiset/examples/newman/newman.lisp index c6406f1d7e0..f2dc72dd603 100644 --- a/books/workshops/2000/ruiz/multiset/examples/newman/newman.lisp +++ b/books/workshops/2000/ruiz/multiset/examples/newman/newman.lisp @@ -322,9 +322,9 @@ ;;; In the sequel, we build a collection of rules to prove these two goals. -;;; ············································································ +;;; ............................................................................ ;;; 3.2.1 Removing initial and final common parts -;;; ············································································ +;;; ............................................................................ (local @@ -396,9 +396,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 3.2.2 Removing the first element of the local peak -;;; ············································································ +;;; ............................................................................ ;;; First, let's prove that the local peak and the transformed are ;;; proofs with the same endpoints, so their proof measures have the @@ -533,12 +533,12 @@ ;;; (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))). -;;; ············································································ +;;; ............................................................................ ;;; 3.2.3 An explicit reference to the peak-element -;;; ············································································ +;;; ............................................................................ ;;; Definition and properties of peak-element -;;; ········································· +;;; ......................................... ;;; See the definition in abstract-proofs.lisp @@ -592,13 +592,13 @@ ;;; (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))). -;;; ············································································ +;;; ............................................................................ ;;; 3.2.4 The peak element is bigger than any element of ;;; (transform-local-peak (local-peak p)) -;;; ············································································ +;;; ............................................................................ ;;; Definition of being bigger (w.r.t rel) than every element of a list -;;; ··································································· +;;; ................................................................... (local (defun rel-bigger-than-list (x l) @@ -610,7 +610,7 @@ ;;; Conditions assuring that an element m is rel-bigger-than-list than ;;; the elements of the proof-measure of a proof, when the proof is, ;;; respectively, steps-up or steps-down: -;;; ··································································· +;;; ................................................................... ;;; A previous lemma: transitivity of rel is needed here @@ -653,7 +653,7 @@ ;;; (transform-local-peak (local-peak p)) in two proofs: the proof ;;; before the valley (steps-up) and the proof after the valley ;;; (steps-down). The following lemmas are needed for that purpose. -;;; ···································································· +;;; .................................................................... ;;; If p is a proof, so they are the proofs after and before the ;;; valley. @@ -682,7 +682,7 @@ ;;; The transformed proof is a valley -;;; ································· +;;; ................................. (local (defthm local-peak-local-peak-p @@ -707,7 +707,7 @@ ;;; steps-up-proof-measure-w-f-v (and then prove that the peak-element ;;; is bigger than every element of the complexities of the ;;; proof-after-valley and the proof-before-valley, respectively. -;;; ···································································· +;;; .................................................................... @@ -734,7 +734,7 @@ ;;; Some technical lemmas -;;; ····················· +;;; ..................... (local (defthm consp-proof-after-proof-instance @@ -750,7 +750,7 @@ ;;; And finally, the intended lemma -;;; ······························· +;;; ............................... (local (defthm valley-rel-bigger-peak-lemma @@ -763,9 +763,9 @@ (transform-local-peak (local-peak p)))))))) -;;; ············································································ +;;; ............................................................................ ;;; 3.2.5 Using valley-rel-bigger-peak-lemma to simplify the goals -;;; ············································································ +;;; ............................................................................ ;;; The two unresolved goals, as stated at the end of 3.2.3, can be ;;; simplified to t by using the previously proved @@ -776,7 +776,7 @@ ;;; following lemma (stating that the peak-element is not a member of ;;; the proof-meassure of the transformed proof), ;;; the calls to multiset-diff in the goals now disappear. -;;; ··································································· +;;; ................................................................... (local (encapsulate @@ -813,7 +813,7 @@ ;;; in the unresolved goal above, is reduced to a call to ;;; rel-bigger-than-list (and then valley-rel-bigger-peak-lemma will be ;;; applied) -;;; ··································································· +;;; ................................................................... (local @@ -830,9 +830,9 @@ ;;; With this two rules altogether with valley-rel-bigger-peak-lemma our ;;; unresolved goal becomes T, so we have: -;;; ············································································ +;;; ............................................................................ ;;; 3.2.6 The main lemma of this book -;;; ············································································ +;;; ............................................................................ (defthm transform-to-valley-admission (implies (exists-local-peak p) @@ -866,13 +866,13 @@ ;;; 4.1 Some previous events ;;; ---------------------------------------------------------------------------- -;;; ············································································· +;;; ............................................................................. ;;; 4.1.1 Previous rules needed to show that (transform-to-valley p) is eqv. to p -;;; ············································································· +;;; ............................................................................. ;;; We have to see that (replace-local-peak p) is equivalent to p -;;; ·································································· +;;; .................................................................. ;;; An useful rule to deal with concatenation of proofs (local @@ -936,9 +936,9 @@ ;;; three pieces of p (before, at and after the peak), using the ;;; previous bridge lemma. -;;; ············································································· +;;; ............................................................................. ;;; 4.1.2 A rule needed to show that (transform-to-valley p) is a valley -;;; ············································································· +;;; ............................................................................. @@ -950,9 +950,9 @@ (equal (steps-valley p) (not (exists-local-peak p)))))) -;;; ············································································· +;;; ............................................................................. ;;; 4.1.3 Disabling the induction rule for equiv-p -;;; ············································································· +;;; ............................................................................. (local (in-theory (disable equiv-p-induct))) @@ -969,7 +969,7 @@ ;;; It returns an equivalent proof -;;; ······························ +;;; .............................. (defthm equiv-p-x-y-transform-to-valley @@ -980,7 +980,7 @@ ;;; It returns a valley proof -;;; ························· +;;; ......................... (defthm valley-transform-to-valley diff --git a/books/workshops/2000/ruiz/multiset/multiset.lisp b/books/workshops/2000/ruiz/multiset/multiset.lisp index efbc20a396f..3ff38ec1aea 100644 --- a/books/workshops/2000/ruiz/multiset/multiset.lisp +++ b/books/workshops/2000/ruiz/multiset/multiset.lisp @@ -561,9 +561,9 @@ ;;; (e0-ord-< (map-fn-e0-ord n) (map-fn-e0-ord m)) -;;; ············································································ +;;; ............................................................................ ;;; 2.5.1 The measure is an ordinal. -;;; ············································································ +;;; ............................................................................ (local (defthm e0-ordinalp-insert-e0-ord-< @@ -579,9 +579,9 @@ (e0-ordinalp (map-fn-e0-ord m))))) -;;; ············································································ +;;; ............................................................................ ;;; 2.5.2 The measure is an embedding -;;; ············································································ +;;; ............................................................................ @@ -615,7 +615,7 @@ ;;; max-fn1-list (an element in l with maximal (fn1 ..)) and properties. -;;; ······································································ +;;; ...................................................................... (local (defun max-fn1-list (l) @@ -654,7 +654,7 @@ ;;; An "alternative definition" of "map-fn-e0-ord". -;;; ··············································· +;;; ............................................... (local (encapsulate @@ -788,7 +788,7 @@ ;;; Needed for forall-exists-rel-bigger-max-fn1-list -;;; ················································ +;;; ................................................ ;;; We prove forall-exists-rel-bigger-max-fn1-list-lemma, establishing ;;; that if (mul-rel n m), and x is in n and not in m, then (fn1 x) is @@ -884,7 +884,7 @@ ;;; Previous lemmas to map-fn-e0-ord-measure, handling every subgoal -;;; ································································ +;;; ................................................................ ;;; Needed for "Subgoal *1/8": @@ -966,7 +966,7 @@ ;;; At last: map-fn-e0-ord-measure. -;;; ······························· +;;; ............................... (local (encapsulate diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/dags.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/dags.lisp index 7cb181d5752..16d47355428 100644 --- a/books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/dags.lisp +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/dags.lisp @@ -498,7 +498,7 @@ (not (dag-p-aux hs rp g)))) ;;; Finally, the soundness theorem: -;;; ······························· +;;; ............................... (defthm dag-p-soundness (implies (not (dag-p g)) @@ -542,7 +542,7 @@ ;;; The main lemma for completeness: -;;; ································ +;;; ................................ (local (defthm dag-p-aux-completeness-main-lemma @@ -642,7 +642,7 @@ ;; Finally, the completeness theorem: -;;; ·································· +;;; .................................. (defthm dag-p-completeness @@ -1106,7 +1106,7 @@ ;;; RECALL: These two theorems would allow us to define functions like these: -;;; ········································································· +;;; ......................................................................... ; (defun occur-check-l (flg x h g) diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/terms.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/terms.lisp index 34306028d1b..ac65947a2b4 100644 --- a/books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/terms.lisp +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/terms.lisp @@ -928,7 +928,7 @@ (disjointp (variables nil (co-domain S)) (domain S)))) ;;; REMARK: In the literature, idempotent substitutions are defined as -;;; substitutions sigma such that sigma·sigma = sigma. But this +;;; substitutions sigma such that sigma.sigma = sigma. But this ;;; definition involves functional equality. We will see that the above ;;; definition implies this property (see main-property-mgs in the book ;;; unification-definition.lisp) Nevertheless, the definition does not @@ -938,9 +938,9 @@ ;;; functionally equivalent idempotent (in our sense) substitution, ((x ;;; . y)) in this case. -;;; ············································································ +;;; ............................................................................ ;;; 3.3.1 The main property of idempotent substitutions. -;;; ············································································ +;;; ............................................................................ ;;; .... PROOF PLAN: @@ -1092,9 +1092,9 @@ ;;; 4.2 Some results concerning the tree structure of a term ;;; ---------------------------------------------------------------------------- -;;; ············································································ +;;; ............................................................................ ;;; 4.2.1 Concatenation of positions -;;; ············································································ +;;; ............................................................................ (defthm position-p-append (implies (position-p p1 term) @@ -1117,9 +1117,9 @@ q x))))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.2 Substitutions and positions -;;; ············································································ +;;; ............................................................................ (defthm nth-apply-subst (implies (and (integerp i) @@ -1154,9 +1154,9 @@ (instance (replace-term term pos t1) sigma)))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.3 Prefix positions -;;; ············································································ +;;; ............................................................................ (local (defthm equal-len-replace-list @@ -1191,9 +1191,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 4.2.4 Disjoint positions -;;; ············································································ +;;; ............................................................................ (local (defun induct-position-p-disjoint (pos1 pos2 term) @@ -1256,9 +1256,9 @@ (position-p (cons i pos) (cons fn args))))))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.5 Disabling the theory -;;; ············································································ +;;; ............................................................................ (defconst *tree-structure-of-terms* '(position-p-append occurrence-append replace-term-append diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/anti-unification.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/anti-unification.lisp index b5fd3667ea5..771eeadaa9c 100644 --- a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/anti-unification.lisp +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/anti-unification.lisp @@ -206,9 +206,9 @@ ;;; (pre-anti-unify-aux flg t1 t2 phi) computes a glb of t1 and t2, ;;; whenever it exists. -;;; ············································································ +;;; ............................................................................ ;;; 2.2.1 Assumptions on phi -;;; ············································································ +;;; ............................................................................ ;;; The following function defines the properties we are going to ;;; assume about an injection phi: it has to be an association such that @@ -232,9 +232,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 2.2.2 pre-anti-unify-aux computes a generalization of t1 and t2 -;;; ············································································ +;;; ............................................................................ ;;; We have to prove something like: ; (let* ((glb (pre-anti-unify-aux flg t1 t2 phi)) @@ -449,10 +449,10 @@ (equal (apply-subst flg sigma (first glb)) t2))))) -;;; ············································································ +;;; ............................................................................ ;;; 2.2.3 pre-anti-unify-aux computes the least common generalization of ;;; t1 and t2 -;;; ············································································ +;;; ............................................................................ ;;; This means, using completeness, that we have to construct, given an ;;; lower bound of t1 and t2, term, a matching substitution for term and diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/matching.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/matching.lisp index 62e2c5b26cf..11608432956 100644 --- a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/matching.lisp +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/matching.lisp @@ -89,9 +89,9 @@ ;;; ---------------------------------------------------------------------------- -;;; ············································································ +;;; ............................................................................ ;;; 1.2.1 How we deal with selection. -;;; ············································································ +;;; ............................................................................ ;;; Firs we prove that equal-set is a congruence w.r.t. the second @@ -139,9 +139,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 1.2.2 transform-subs-sel preserves the set of matchers. -;;; ············································································ +;;; ............................................................................ (local @@ -211,7 +211,7 @@ (not (matcher sigma S))))) ;;; The three main theorems of this subsubsection -;;; ············································· +;;; ............................................. (defthm transform-subs-sel-preserves-matchers-1 (implies @@ -235,10 +235,10 @@ -;;; ············································································ +;;; ............................................................................ ;;; 1.2.3 (system-substitution (cdr S-match)) is an invariant in the rules ;;; of transformation. -;;; ············································································ +;;; ............................................................................ @@ -261,9 +261,9 @@ (system-substitution (cdr (transform-subs-sel S-match))))))) -;;; ············································································ +;;; ............................................................................ ;;; 1.2.4 Main property of the property system-substitution -;;; ············································································ +;;; ............................................................................ (local @@ -360,7 +360,7 @@ (length-term nil args2)))))) ;;; And the main result: -;;; ···················· +;;; .................... (defthm transform-subs-sel-decreases-length-of-first-system (implies (not (normal-form-syst S-match)) @@ -458,7 +458,7 @@ ;;; Three lemmas to state that the set of matchers is preserved by ;;; subs-system-sel -;;; ·········································································· +;;; .......................................................................... (local (defthm subs-system-sel-preserves-matchers-1 @@ -486,7 +486,7 @@ (in-theory (enable union-systems)) ;;; subs-system-sel preserves the property of being a system-substitution. -;;; ·································································· +;;; .................................................................. (local (defthm subs-system-sel-preserves-system-substitution @@ -494,7 +494,7 @@ (system-substitution (cdr (subs-system-sel S-match)))))) ;;; Guard verification: a substitution-s-p is returned -;;; ··················································· +;;; ................................................... (local (defthm @@ -602,7 +602,7 @@ ;;; ---------------------------------------------------------------------------- ;;; Soundness -;;; ········· +;;; ......... (defthm subs-sel-soundness @@ -616,7 +616,7 @@ ;;; Completeness -;;; ············ +;;; ............ (defthm subs-sel-completeness @@ -630,7 +630,7 @@ ;;; Closure property: ;;; (the following theorem is needed for guard verification) -;;; ························································ +;;; ........................................................ (defthm matching-sel-substitution-s-p diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/renamings.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/renamings.lisp index 7bf9152c1ab..dc706d4b458 100644 --- a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/renamings.lisp +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/renamings.lisp @@ -101,9 +101,9 @@ ;;; ---------------------------------------------------------------------------- -;;; ············································································ +;;; ............................................................................ ;;; 2.2.1 An important lemma -;;; ············································································ +;;; ............................................................................ ;;; We will show that the inverse substitution of a renaming is its ;;; inverse function, in some sense. @@ -145,9 +145,9 @@ term)))) -;;; ············································································ +;;; ............................................................................ ;;; 2.2.2 And the intended property -;;; ············································································ +;;; ............................................................................ (defthm renaming-implies-renamed @@ -180,9 +180,9 @@ ;;; * (co-domain sigmar) is a setp. -;;; ············································································ +;;; ............................................................................ ;;; 2.3.1 sigmar is a variable-substitution -;;; ············································································ +;;; ............................................................................ (local (encapsulate @@ -222,9 +222,9 @@ (:instance renamed-implies-variable-substitution-main-lemma (l (make-set (variables flg term))))))))) -;;; ············································································ +;;; ............................................................................ ;;; 2.3.2 An important lemma -;;; ············································································ +;;; ............................................................................ ;;; When (equal (apply-subst flg delta (apply-subst flg sigma term)) ;;; term) then two different variables of term cannot have the the value @@ -267,9 +267,9 @@ (x y)))))))) -;;; ············································································ +;;; ............................................................................ ;;; 2.3.2 co-domain of sigmar is a setp -;;; ············································································ +;;; ............................................................................ @@ -298,9 +298,9 @@ (:instance renamed-implies-setp-codomain-main-lemma (l (make-set (variables flg term))))))))) -;;; ············································································ +;;; ............................................................................ ;;; 2.3.3 sigmar is a renaming -;;; ············································································ +;;; ............................................................................ (local (defthm renamed-implies-renaming-main-lemma @@ -436,9 +436,9 @@ ;;; 3.3 Number-rename-aux: main properties. ;;; ---------------------------------------------------------------------------- -;;; ············································································ +;;; ............................................................................ ;;; 3.3.1 Previous (local) lemmas about coincide. -;;; ············································································ +;;; ............................................................................ ;;; We will need these lemmas because we are going to talk about ;;; extensions (see the definition in terms.lisp, subsection 2.3) @@ -483,9 +483,9 @@ (in-theory (disable coincide-subsetp-transitive)))) -;;; ············································································ +;;; ............................................................................ ;;; 3.3.2 Previous (local) lemmas about acl2-numberp-list-increment -;;; ············································································ +;;; ............................................................................ ;;; We will define and prove some local properties of the concept of ;;; being a list of numbers l such that each of its elements is obtained @@ -542,9 +542,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 3.3.3 number-rename-aux: properties of the variables of the returned term -;;; ············································································ +;;; ............................................................................ ;;; We will prove that (first (number-rename-aux flg term sigma x y) is a ;;; term having numeric variables, and: @@ -611,10 +611,10 @@ (second (number-rename-aux flg term sigma x y))) x)))))) -;;; ············································································ +;;; ............................................................................ ;;; 3.3.4 number-rename-aux: Main property of the co-domain of the ;;; returned substitution. -;;; ············································································ +;;; ............................................................................ (local @@ -625,9 +625,9 @@ (acl2-numberp-list-increment (co-domain (second (number-rename-aux flg term sigma x y))) y)))) -;;; ············································································ +;;; ............................................................................ ;;; 3.3.5 number-rename-aux: the substitution returned is a renaming -;;; ············································································ +;;; ............................................................................ (local @@ -659,16 +659,16 @@ -;;; ············································································ +;;; ............................................................................ ;;; 3.3.3 Subsumption properties of number-rename-aux -;;; ············································································ +;;; ............................................................................ ;;; 3.3.3.1 ;;; The substituion returned by number-rename-aux, applied to the input ;;; term returns the returned term (i.e term subsumes the ;;; number-rename-aux term) -;;; ·········································································· +;;; .......................................................................... ;;; Two previos lemmas: @@ -735,7 +735,7 @@ ;;; 3.3.3.2 ;;; The term returned by number-rename-aux subsumes the input term -;;; ··································································· +;;; ................................................................... (local (encapsulate diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp index 6eefb93b664..376e8836953 100644 --- a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp @@ -26,15 +26,15 @@ ;;; Our goal is to define the subsumption relation between ;;; substitutions. In the literature, this relation is defined in this ;;; way: -;;; sigma <= delta iff (exists gamma) gamma·sigma = delta -;;; where "·" stands for composition. +;;; sigma <= delta iff (exists gamma) gamma.sigma = delta +;;; where "." stands for composition. ;;; Note that equality between substitutions is functional equality (we cannot ;;; use equal), so we reformulate this property as: ;;; (*) sigma <= delta iff (exists gamma) ;;; s.t. for all term -;;; gamma·sigma(term) = delta(term) +;;; gamma.sigma(term) = delta(term) ;;; Our goal in this book is to define the subsumption relation between @@ -285,9 +285,9 @@ ;;; if (subs-sust sigma delta) ;;; WE DISTINGUISH THREE CASES. -;;; ············································································ +;;; ............................................................................ ;;; 3.1.1 Case 1: x is a variable outside V -;;; ············································································ +;;; ............................................................................ @@ -303,14 +303,14 @@ :hints (("Goal" :in-theory (enable x-not-in-domain-remains-the-same))))) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.2. Case 2: x is a variable of (domain-var sigma) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.2.1 A lemma for this case 2: ;;; subs-subst composed with sigma is equal to delta in V. -;;; ······················································ +;;; ...................................................... (local (encapsulate @@ -373,7 +373,7 @@ (local (in-theory (disable subs-subst matching-subst))) ;;; 3.1.2.2 Another lemma for case 2: -;;; ······························· +;;; ............................... (local (defthm variables-co-domain-var @@ -383,7 +383,7 @@ ;;; 3.1.2.3 The main result for Case 2 -;;; ································ +;;; ................................ (local (defthm @@ -396,14 +396,14 @@ (val x delta))))) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.3. Case 3: x in V but not in (domain-var sigma) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.3.1 A lemma for Case 3 ;;; In this case, matching and matching-subst-r take the same values. -;;; ································································· +;;; ................................................................. (local (defthm @@ -472,7 +472,7 @@ ;;; With terms and list of terms (not only with variables) -;;; ······················································ +;;; ...................................................... (local (defthm @@ -512,7 +512,7 @@ ;;; following version will be used as a rewrite rule. ;;; With terms but without using composition -;;; ········································ +;;; ........................................ (defthm subs-subst-implies-matching-subst-r-appplied-to-sigma-term-is-delta-term @@ -526,7 +526,7 @@ ;;; With respect to subsumption between terms -;;; ········································· +;;; ......................................... ;;; Trivial consequence of completeness of subsumption and the previous @@ -563,7 +563,7 @@ ;;; existence of two substitutions, called sigma-w and delta-w and the ;;; only property we will assume about them is that sigma-w <= ;;; delta-w. That is, exists another substitution gamma-w such that -;;; delta-w = gamma-w·sigma-w. +;;; delta-w = gamma-w.sigma-w. ;;; We will use encapsulate for that purpose. Let sigma-w, delta-w and ;;; gamma-w three susbtitutions such that delta-w is functionally equal diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp index 4a36b0f2470..99eb37ed83c 100644 --- a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp @@ -289,7 +289,7 @@ ;;; Most of these properties are obtained by functional instantiation. ;;; Soundness -;;; ········· +;;; ......... (defthm subs-soundness (implies (subs t1 t2) @@ -300,7 +300,7 @@ ;;; Completeness -;;; ············· +;;; ............. (defthm subs-completeness (implies (equal (instance t1 sigma) t2) @@ -310,7 +310,7 @@ (:instance match-mv-completeness (S (list (cons t1 t2))))))) ;;; Substitution-s-p (closure property) -;;; ··································· +;;; ................................... (defthm matching-substitution-s-p @@ -320,7 +320,7 @@ (:instance match-mv-substitution-s-p (S (list (cons t1 t2))))))) ;;; Substitution-p (needed for guard verification) -;;; ·············································· +;;; .............................................. (defthm matching-substitution-p @@ -411,7 +411,7 @@ (second (pair-args l1 (apply-subst nil sigma l1))))) ;;; Soundness -;;; ········· +;;; ......... (defthm subs-list-soundness @@ -423,7 +423,7 @@ ;;; Completeness -;;; ············· +;;; ............. (defthm subs-list-completeness (implies (equal (apply-subst nil sigma l1) l2) @@ -433,7 +433,7 @@ (:instance match-mv-completeness (S (first (pair-args l1 l2))))))) ;;; Substitution-s-p (closure property) -;;; ··································· +;;; ................................... (defthm matching-list-substitution-s-p @@ -446,7 +446,7 @@ ;;; Substitution-p (needed for guard verification) -;;; ·············································· +;;; .............................................. (defthm matching-list-substitution-p @@ -500,7 +500,7 @@ ;;; ---------------------------------------------------------------------------- ;;;; Subsumption reflexive -;;;; ····················· +;;;; ..................... (defthm subsumption-reflexive (subs t1 t1) @@ -510,7 +510,7 @@ ;;;; Subsumption transitive -;;;; ······················ +;;;; ...................... (defthm subsumption-transitive @@ -530,7 +530,7 @@ ;;; ---------------------------------------------------------------------------- ;;; An useful rule: -;;; ··············· +;;; ............... (defthm subsumption-apply-subst (subs term (instance term sigma)) @@ -538,7 +538,7 @@ (t1 term) (t2 (instance term sigma)))))) ;;; Variables are minimum elements in this quasi-order -;;; ·················································· +;;; .................................................. (defthm variable-minimum-subsumption (implies (variable-p x) diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/terms.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/terms.lisp index 95af93cb4cd..52c02ff9fb2 100644 --- a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/terms.lisp +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/terms.lisp @@ -927,7 +927,7 @@ (disjointp (variables nil (co-domain S)) (domain S)))) ;;; REMARK: In the literature, idempotent substitutions are defined as -;;; substitutions sigma such that sigma·sigma = sigma. But this +;;; substitutions sigma such that sigma.sigma = sigma. But this ;;; definition involves functional equality. We will see that the above ;;; definition implies this property (see main-property-mgs in the book ;;; unification-definition.lisp) Nevertheless, the definition does not @@ -937,9 +937,9 @@ ;;; functionally equivalent idempotent (in our sense) substitution, ((x ;;; . y)) in this case. -;;; ············································································ +;;; ............................................................................ ;;; 3.3.1 The main property of idempotent substitutions. -;;; ············································································ +;;; ............................................................................ ;;; .... PROOF PLAN: @@ -1091,9 +1091,9 @@ ;;; 4.2 Some results concerning the tree structure of a term ;;; ---------------------------------------------------------------------------- -;;; ············································································ +;;; ............................................................................ ;;; 4.2.1 Concatenation of positions -;;; ············································································ +;;; ............................................................................ (defthm position-p-append (implies (position-p p1 term) @@ -1116,9 +1116,9 @@ q x))))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.2 Substitutions and positions -;;; ············································································ +;;; ............................................................................ (defthm nth-apply-subst (implies (and (integerp i) @@ -1153,9 +1153,9 @@ (instance (replace-term term pos t1) sigma)))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.3 Prefix positions -;;; ············································································ +;;; ............................................................................ (local (defthm equal-len-replace-list @@ -1190,9 +1190,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 4.2.4 Disjoint positions -;;; ············································································ +;;; ............................................................................ (local (defun induct-position-p-disjoint (pos1 pos2 term) @@ -1255,9 +1255,9 @@ (position-p (cons i pos) (cons fn args))))))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.5 Disabling the theory -;;; ············································································ +;;; ............................................................................ (defconst *tree-structure-of-terms* '(position-p-append occurrence-append replace-term-append diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification-pattern.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification-pattern.lisp index f0b352593ef..3015adb1043 100644 --- a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification-pattern.lisp +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification-pattern.lisp @@ -216,12 +216,12 @@ ;;; Equivalence for each rule (some rules do not need auxiliary lemmas) -;;; ··································································· +;;; ................................................................... -;;; ···················· +;;; .................... ;;; 2.1.1 rule DECOMPOSE -;;; ···················· +;;; .................... (local (defun induction-transform-sel-decompose-rule (l1 l2) (if (or (atom l1) (atom l2)) @@ -241,9 +241,9 @@ -;;; ····················· +;;; ..................... ;;; 2.1.2 rule ELIMINATE -;;; ····················· +;;; ..................... ;;; If sigma is a solution of sol, and x is a variable, then ;;; sigma(sol(x)) = sol(x). @@ -258,7 +258,7 @@ (apply-subst flg sigma (val x sol)) (val x sigma))))) -;;; If sigma is a solution of S, sigma = sigma · S +;;; If sigma is a solution of S, sigma = sigma . S (defthm substitutions-solution-system (implies (solution sigma S) @@ -287,9 +287,9 @@ (solution sigma s))))) -;;; ················ +;;; ................ ;;; 2.1.3 rule CHECK -;;; ················ +;;; ................ ;;; GOAL: ;;; Prove that x = term, when x is not in term and is not term, has no @@ -377,9 +377,9 @@ :use ((:instance transform-sel-check-rule-not-equal-size)))))) -;;; ··················· +;;; ................... ;;; 2.1.4 rule CONFLICT -;;; ··················· +;;; ................... ;;; The equation (f t1 ... tn) = (g s1 ... sm), with f/=g has no ;;; solution: @@ -392,9 +392,9 @@ (not (equal (apply-subst t sigma t1) (apply-subst t sigma t2)))))) -;;; ···················· +;;; .................... ;;; 2.1.5 rule NOT-PAIR -;;; ···················· +;;; .................... ;;; If sigma(t1...tn . a) = sigma(s1...sm . b), then n=m and a=b: ;;; ======= Corolary: The equation (f t1 ... tn . a) = (g s1 ... sm . b) @@ -417,9 +417,9 @@ (apply-subst t sigma t2))))))) -;;; ·················· +;;; .................. ;;; 2.1.6 And finally: -;;; ·················· +;;; .................. ;;; Three lemmas to state that transform-mm-sel preserves the set of ;;; solutions: @@ -498,9 +498,9 @@ ;;; ELIMINATE needs help form the user -;;; ···················· +;;; .................... ;;; 2.2.1 rule DECOMPOSE -;;; ···················· +;;; .................... ;;; Properties to prove that, for the rule decompose, the variables of ;;; the system S are disjoint from the domain of sol. @@ -529,9 +529,9 @@ (variables nil l2))))))) -;;; ···················· +;;; .................... ;;; 2.2.2 rule ELIMINATE -;;; ···················· +;;; .................... ;;; Properties to prove that, for the rule eliminate, the variables of ;;; the system S and the co-domain of sol are disjoint from the domain @@ -634,9 +634,9 @@ (a (system-var (apply-syst sigma S))))))))) -;;; ···················· +;;; .................... ;;; 2.2.3 And finally -;;; ···················· +;;; .................... (local (defthm transform-mm-sel-preserves-idempotency @@ -662,9 +662,9 @@ ;;; This section is needed for guard verification. -;;; ············································································ +;;; ............................................................................ ;;; 2.3.1 preservation of the system-p property -;;; ············································································ +;;; ............................................................................ (local (encapsulate @@ -723,9 +723,9 @@ :hints (("Goal" :in-theory (disable substitution-s-p)))))) -;;; ············································································ +;;; ............................................................................ ;;; 2.3.2 preservation of the system-p property -;;; ············································································ +;;; ............................................................................ (local (encapsulate @@ -814,16 +814,16 @@ -;;; ············································································ +;;; ............................................................................ ;;; 2.4.1 transform-mm-sel does not add new variables -;;; ············································································ +;;; ............................................................................ ;;; Goal: ;;; We will prove that the variables of S are a subset of ;;; the variables of the transformed, for every rule. ;;; Some lemmas about eliminate -;;; ··························· +;;; ........................... (local (defthm subsetp-variables-delete @@ -855,7 +855,7 @@ (S (eliminate ecu S)))))))) ;;; Lemmas dealing with length, setps and subsetps -;;; ·············································· +;;; .............................................. (local (defthm len-subsetp-setp @@ -874,7 +874,7 @@ () ;;; Main lemma (in terms of subsetp) -;;; ································ +;;; ................................ (local (defthm transform-sel-does-not-add-new-variables @@ -890,7 +890,7 @@ (S (car S-sol))))))) ;;; The main lemma (the previous lemma in terms of n-system-var) -;;; ···························································· +;;; ............................................................ (defthm transform-does-not-increases-n-variables @@ -902,9 +902,9 @@ (disable system-var transform-mm-sel)))))) -;;; ············································································ +;;; ............................................................................ ;;; 2.4.2 The rule eliminate eliminates one variable from S -;;; ············································································ +;;; ............................................................................ ;;; This subsection is needed to show that when n-system-var does not ;;; change after one step of transformation, then the rule ELIMNATE has @@ -978,9 +978,9 @@ ;;; complicated. -;;; ············································································ +;;; ............................................................................ ;;; 2.4.3 How we deal with selection (second part). -;;; ············································································ +;;; ............................................................................ ;;; equal-set is not a congruence w.r.t. size-system and ;;; n-variables-right-hand-side. See observaciones.txt to understand why @@ -1069,9 +1069,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 2.4.4 Size-system does not increase (when n-variables remains the same) -;;; ············································································ +;;; ............................................................................ ;;; Technical lemma: @@ -1109,10 +1109,10 @@ -;;; ············································································ +;;; ............................................................................ ;;; 2.4.5 n-variables-right-hand-side does not increase (when the two above ;;; quantities remain the same) -;;; ············································································ +;;; ............................................................................ ;;; Lemmas: @@ -1198,9 +1198,9 @@ (local (in-theory (disable n-variables-rhs-cons-select-and-delete-one))) -;;; ············································································ +;;; ............................................................................ ;;; 2.4.6 Compiling the previous results: the main termination property -;;; ············································································ +;;; ............................................................................ ;;; We disable some definition and lemmas @@ -1218,7 +1218,7 @@ ;;; AND THE MAIN TERMINATION THEOREMS -;;; ································· +;;; ................................. (defthm ordinalp-unification-measure (e0-ordinalp (unification-measure S-sol))) @@ -1267,9 +1267,9 @@ ;;; ---------------------------------------------------------------------------- -;;; ·········································· +;;; .......................................... ;;; 3.2.1 solve-system-sel preserves solutions -;;; ·········································· +;;; .......................................... ;;; A technical lemma @@ -1313,9 +1313,9 @@ (local (in-theory (enable union-systems))) -;;; ············································· +;;; ............................................. ;;; 3.2.2 solve-system-sel preserves idempotence -;;; ············································· +;;; ............................................. (local (in-theory (disable disjointp-conmutative))) @@ -1336,9 +1336,9 @@ :hints (("Goal" :induct (solve-system-sel S-sol))))) -;;; ···························································· +;;; ............................................................ ;;; 3.2.3 solve-system-sel preserves system-p and substitution-p -;;; ···························································· +;;; ............................................................ ;;; Closure property @@ -1380,9 +1380,9 @@ ;;; 4.2 Main properties of mgs-sel ;;; ---------------------------------------------------------------------------- -;;; ······························································ +;;; .............................................................. ;;; THEOREM 4.2.1. If S is solvable, then (mgs-sel S) succeeds. -;;; ······························································ +;;; .............................................................. (defthm mgs-sel-completeness (implies (solution sigma S) @@ -1400,10 +1400,10 @@ (solution sigma (first (solve-system-sel S-sol))))) -;;; ······································································· +;;; ....................................................................... ;;; THEOREM 4.2.2: If (mgs-sel S) succeeds, then the system is solvable ;;; (and a solution is (first (mgs-sel S)) -;;; ······································································· +;;; ....................................................................... (local (defthm mgs-sel-soundness @@ -1415,9 +1415,9 @@ (S-sol (cons S nil)) (sigma (first (mgs-sel S))))))))) -;;; ···················································· +;;; .................................................... ;;; THEOREM 4.2.3: (first (mgs-sel S)) is idempotent. -;;; ····················································· +;;; ..................................................... (local @@ -1428,10 +1428,10 @@ ;;; REMARK: This is true even if (mgs-sel S) fails -;;; ··························································· +;;; ........................................................... ;;; THEOREM 4.2.4: The substitution returned by mgs-sel is ;;; substitution-p, whenever its input system is system-p -;;; ···························································· +;;; ............................................................ ;;; This theorem is needed for guard verification. @@ -1449,10 +1449,10 @@ -;;; ·································································· +;;; .................................................................. ;;; THEOREM 4.2.5: If sigma is a solution of S, (first (mgs-sel S)) ;;; subsumes sigma. (thus, (first (mgs-sel S)) is a mgs of S) -;;; ··································································· +;;; ................................................................... ;;; Lemma: If sigma is a solution of S, then for all term, (first ;;; (mgs-sel S))(term) subsumes sigma(term), with the matching @@ -1524,9 +1524,9 @@ ;;; t1 t2))) -;;; ······································································ +;;; ...................................................................... ;;; THEOREM 5.2.1: If t1 and t2 are unifiable, then (unifiable-sel t1 t2). -;;; ······································································ +;;; ...................................................................... (defthm unifiable-sel-completeness (implies (equal (instance t1 sigma) @@ -1538,10 +1538,10 @@ (S (list (cons t1 t2))))))) -;;; ········································································ +;;; ........................................................................ ;;; THEOREM 5.2.2: If (unifiable-sel t1 t2), t1 and t2 are unifiable ;;; (and (mgu-sel t1 t2) is an unifier). -;;; ········································································ +;;; ........................................................................ (defthm unifiable-sel-soundness @@ -1553,17 +1553,17 @@ (S (list (cons t1 t2)))))))) -;;; ········································································ +;;; ........................................................................ ;;; THEOREM 5.2.3: (mgu-sel t1 t2) is idempotent. -;;; ········································································ +;;; ........................................................................ (defthm mgu-sel-idempotent (idempotent (mgu-sel t1 t2))) -;;; ········································································ +;;; ........................................................................ ;;; THEOREM 5.2.4: If t1 and t2 are terms of a given signature, then mgu-sel ;;; returns a substitution of that signature -;;; ········································································ +;;; ........................................................................ @@ -1573,10 +1573,10 @@ -;;; ········································································ +;;; ........................................................................ ;;; THEOREM 5.2.5: If sigma is an unifier of t1 and t2, then (mgu-sel t1 t2) ;;; subsumes sigma (thus, (mgu-sel t1 t2) is a mgu of t1 and t2). -;;; ········································································ +;;; ........................................................................ (defthm mgu-sel-most-general-unifier (implies (equal (instance t1 sigma) diff --git a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp index aa724aa02af..282a33066a9 100644 --- a/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp +++ b/books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp @@ -43,10 +43,10 @@ ;;; 1.1 A particular version of transform-mm-sel ;;; ---------------------------------------------------------------------------- -;;; ············································································ +;;; ............................................................................ ;;; 1.1.1 A particular "selection" function. If we detect an inmediate fail, ;;; we select it. -;;; ············································································ +;;; ............................................................................ (defun sel-unif (S) (declare (xargs :guard (and (consp S) (system-p S)))) @@ -69,9 +69,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 1.1.2 Some lemmas needed for guard verification: -;;; ············································································ +;;; ............................................................................ (encapsulate () @@ -108,9 +108,9 @@ (variable-p (car (sel-unif S)))) (eqlablep (car (sel-unif S))))) -;;; ············································································ +;;; ............................................................................ ;;; 1.1.3 The function transform-mm -;;; ············································································ +;;; ............................................................................ (defun transform-mm (S sol) @@ -354,7 +354,7 @@ ;;; Most of these properties are obtained by functional instantiation. ;;; Completeness -;;; ············ +;;; ............ (defthm mgu-completeness (implies (equal (instance t1 sigma) @@ -376,7 +376,7 @@ ;;; The hint is not necessary, but makes the proof shorter. ;;; Soundness -;;; ········· +;;; ......... (defthm mgu-soundness @@ -397,7 +397,7 @@ ;;; Idempotence -;;; ··········· +;;; ........... (defthm mgu-idempotent (idempotent (mgu t1 t2)) @@ -416,7 +416,7 @@ ;;; Generality of the unifier -;;; ························· +;;; ......................... (defthm mgu-most-general-unifier (implies (equal (instance t1 sigma) @@ -437,7 +437,7 @@ ;;; Substitution-s-p (closure property of mgu) -;;; ·············································· +;;; .............................................. (defthm mgu-substitution-s-p @@ -458,7 +458,7 @@ ;;; Substitution-p (needed for guard verification) -;;; ·············································· +;;; .............................................. (defthm mgu-substitution-p diff --git a/books/workshops/2004/ruiz-et-al/support/basic.lisp b/books/workshops/2004/ruiz-et-al/support/basic.lisp index 712e934e0ee..66b7b086c77 100644 --- a/books/workshops/2004/ruiz-et-al/support/basic.lisp +++ b/books/workshops/2004/ruiz-et-al/support/basic.lisp @@ -753,7 +753,7 @@ ;;; ;;;============================================================================ -;; Ya incluido en la versión 2-8 +;; Ya incluido en la versión 2-8 ;; (defun natp (n) ;; (declare (xargs :guard t)) ;; (and (integerp n) diff --git a/books/workshops/2004/ruiz-et-al/support/dag-unification-rules.lisp b/books/workshops/2004/ruiz-et-al/support/dag-unification-rules.lisp index eb47d7f4d07..f04bb55259d 100644 --- a/books/workshops/2004/ruiz-et-al/support/dag-unification-rules.lisp +++ b/books/workshops/2004/ruiz-et-al/support/dag-unification-rules.lisp @@ -1,6 +1,6 @@ ;;; ============================================================================ ;;; dag-unification-rules.lisp -;;; Título: Unification rules on term dags +;;; Título: Unification rules on term dags ;;; ============================================================================ #| To certify this book: @@ -22,7 +22,7 @@ ;;; ============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;; ============================================================================ @@ -211,12 +211,12 @@ ;;; variables. We define the "bounded" version and the "relaxed" ;;; version. -;;; NOTA: La guarda de esta función sería muy rara, ya que dag-p +;;; NOTA: La guarda de esta función sería muy rara, ya que dag-p ;;; necesita term-graph-p, que es como bounded-term-graph-p pero para -;;; n=(len g). Así que ha optado por no ponerle guarda( creo que esta no +;;; n=(len g). Así que ha optado por no ponerle guarda( creo que esta no ;;; tinene ni que ejecutarse ni que usarse en una guarda) y luego ;;; definir well-formed-term-dag-p igual que esto pero con n=(len g) y -;;; esa si ponerle guarda. Además, pongo una regla de reescritura que +;;; esa si ponerle guarda. Además, pongo una regla de reescritura que ;;; relacione ambas cosas. (defun bounded-well-formed-term-dag-p (g n) (and (bounded-term-graph-p g n) @@ -281,7 +281,7 @@ ;;; system and the substitution. -;;; NOTA: aquí se aplica el mismo comentario que antes +;;; NOTA: aquí se aplica el mismo comentario que antes (defun bounded-well-formed-upl (upl n) (and (bounded-nat-pairs-true-listp (first upl) n) (bounded-nat-substitution-p (second upl) n) diff --git a/books/workshops/2004/ruiz-et-al/support/dags.lisp b/books/workshops/2004/ruiz-et-al/support/dags.lisp index 542d43ec705..288c1d05696 100644 --- a/books/workshops/2004/ruiz-et-al/support/dags.lisp +++ b/books/workshops/2004/ruiz-et-al/support/dags.lisp @@ -1,6 +1,6 @@ ;;;============================================================================ ;;; dags.lisp -;;; Título: Term dags in ACL2 +;;; Título: Term dags in ACL2 ;;;============================================================================ #| To certify this book: @@ -20,7 +20,7 @@ ;;;============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;;============================================================================ @@ -589,7 +589,7 @@ (not (dag-p-aux hs rp g))))) ;;; Finally, the soundness theorem: -;;; ······························· +;;; ............................... (defthm dag-p-soundness (implies (not (dag-p g)) @@ -633,7 +633,7 @@ ;;; The main lemma for completeness: -;;; ································ +;;; ................................ (local (defthm dag-p-aux-completeness-main-lemma @@ -1680,7 +1680,7 @@ ;;; RECALL: These two theorems would allow us to define functions like these: -;;; ········································································· +;;; ......................................................................... ; (defun occur-check-l (flg x h g) diff --git a/books/workshops/2004/ruiz-et-al/support/matching.lisp b/books/workshops/2004/ruiz-et-al/support/matching.lisp index 2e12bf7beb8..c6882440d29 100644 --- a/books/workshops/2004/ruiz-et-al/support/matching.lisp +++ b/books/workshops/2004/ruiz-et-al/support/matching.lisp @@ -89,9 +89,9 @@ ;;; ---------------------------------------------------------------------------- -;;; ············································································ +;;; ............................................................................ ;;; 1.2.1 How we deal with selection. -;;; ············································································ +;;; ............................................................................ ;;; Firs we prove that equal-set is a congruence w.r.t. the second @@ -139,9 +139,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 1.2.2 transform-subs-sel preserves the set of matchers. -;;; ············································································ +;;; ............................................................................ (local @@ -211,7 +211,7 @@ (not (matcher sigma S))))) ;;; The three main theorems of this subsubsection -;;; ············································· +;;; ............................................. (defthm transform-subs-sel-preserves-matchers-1 (implies @@ -235,10 +235,10 @@ -;;; ············································································ +;;; ............................................................................ ;;; 1.2.3 (system-substitution (cdr S-match)) is an invariant in the rules ;;; of transformation. -;;; ············································································ +;;; ............................................................................ @@ -261,9 +261,9 @@ (system-substitution (cdr (transform-subs-sel S-match))))))) -;;; ············································································ +;;; ............................................................................ ;;; 1.2.4 Main property of the property system-substitution -;;; ············································································ +;;; ............................................................................ (local @@ -362,7 +362,7 @@ (length-term nil args2)))))) ;;; And the main result: -;;; ···················· +;;; .................... (defthm transform-subs-sel-decreases-length-of-first-system (implies (not (normal-form-syst S-match)) @@ -460,7 +460,7 @@ ;;; Three lemmas to state that the set of matchers is preserved by ;;; subs-system-sel -;;; ·········································································· +;;; .......................................................................... (local (defthm subs-system-sel-preserves-matchers-1 @@ -488,7 +488,7 @@ (in-theory (enable union-systems)) ;;; subs-system-sel preserves the property of being a system-substitution. -;;; ·································································· +;;; .................................................................. (local (defthm subs-system-sel-preserves-system-substitution @@ -496,7 +496,7 @@ (system-substitution (cdr (subs-system-sel S-match)))))) ;;; Guard verification: a substitution-s-p is returned -;;; ··················································· +;;; ................................................... (local (defthm @@ -604,7 +604,7 @@ ;;; ---------------------------------------------------------------------------- ;;; Soundness -;;; ········· +;;; ......... (defthm subs-sel-soundness @@ -618,7 +618,7 @@ ;;; Completeness -;;; ············ +;;; ............ (defthm subs-sel-completeness @@ -632,7 +632,7 @@ ;;; Closure property: ;;; (the following theorem is needed for guard verification) -;;; ························································ +;;; ........................................................ (defthm matching-sel-substitution-s-p diff --git a/books/workshops/2004/ruiz-et-al/support/prefix-unification-rules.lisp b/books/workshops/2004/ruiz-et-al/support/prefix-unification-rules.lisp index 871b5bc57fb..f701ec5e02b 100644 --- a/books/workshops/2004/ruiz-et-al/support/prefix-unification-rules.lisp +++ b/books/workshops/2004/ruiz-et-al/support/prefix-unification-rules.lisp @@ -1,6 +1,6 @@ ;;; ============================================================================ ;;; prefix-unification-rules.lisp -;;; Título: Unification as transformation rules (using a prefix representation of terms) +;;; Título: Unification as transformation rules (using a prefix representation of terms) ;;; ============================================================================ @@ -20,7 +20,7 @@ ;;; ============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;; ============================================================================ diff --git a/books/workshops/2004/ruiz-et-al/support/q-dag-unification-rules.lisp b/books/workshops/2004/ruiz-et-al/support/q-dag-unification-rules.lisp index 6e67ac2065d..bd2b83932e7 100644 --- a/books/workshops/2004/ruiz-et-al/support/q-dag-unification-rules.lisp +++ b/books/workshops/2004/ruiz-et-al/support/q-dag-unification-rules.lisp @@ -1,6 +1,6 @@ ;;; ============================================================================ ;;; q-dag-unification-rules.lisp -;;; Título: Unification rules on term dags for the quadratic algorithm +;;; Título: Unification rules on term dags for the quadratic algorithm ;;; 12-03-03 ;;; ============================================================================ @@ -21,7 +21,7 @@ ;;; ============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;; ============================================================================ diff --git a/books/workshops/2004/ruiz-et-al/support/q-dag-unification-st.lisp b/books/workshops/2004/ruiz-et-al/support/q-dag-unification-st.lisp index b3fea462a3c..ef1946973f8 100644 --- a/books/workshops/2004/ruiz-et-al/support/q-dag-unification-st.lisp +++ b/books/workshops/2004/ruiz-et-al/support/q-dag-unification-st.lisp @@ -1,6 +1,6 @@ ;;;============================================================================ ;;; q-dag-unification-st.lisp -;;; Título: A quadratic unification algorithm using stobjs +;;; Título: A quadratic unification algorithm using stobjs ;;;============================================================================ #| To be certified: @@ -15,7 +15,7 @@ ;;;============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;;============================================================================ @@ -743,7 +743,7 @@ ;;; Este disable es importante, puesto que todas las reglas anteriores ;;; (y las que siguen) -;;; llevan nth en su lado izquierdo. Por tanto, sólo habilitaremos nth +;;; llevan nth en su lado izquierdo. Por tanto, sólo habilitaremos nth ;;; en caso de que sea estrictamente necesario. (local (in-theory (disable nth))) @@ -1129,7 +1129,7 @@ (in-theory (disable tbs-as-system-st solved-as-system-st)) -;; Este función es solo para evitarme escribir: +;; Este función es solo para evitarme escribir: (local (defun well-formed-dag-system-st-bis (S td) diff --git a/books/workshops/2004/ruiz-et-al/support/q-dag-unification.lisp b/books/workshops/2004/ruiz-et-al/support/q-dag-unification.lisp index 4f4dd517ba0..ff0949288fc 100644 --- a/books/workshops/2004/ruiz-et-al/support/q-dag-unification.lisp +++ b/books/workshops/2004/ruiz-et-al/support/q-dag-unification.lisp @@ -1,6 +1,6 @@ ;; ============================================================================ ;;; q-dag-unification.lisp -;;; Título: A quadratic dag based unification algorithm +;;; Título: A quadratic dag based unification algorithm ;;; ============================================================================ #| To certify this book: @@ -20,7 +20,7 @@ ;;;============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;;============================================================================ @@ -356,7 +356,7 @@ (term-dag-non-variable-p (cdr (first requations)) g) (not (term-dag-is-p (car (first requations)) g)) -;;; la anterior condición es redundante, pero necesaria para la guarda +;;; la anterior condición es redundante, pero necesaria para la guarda (term-dag-variable-p (car (first requations)) g) (equation-justify-equality (car rargs1) (car rargs2) @@ -419,8 +419,8 @@ (idc (first id-equ))) (and (equal idc 'id) - (let* ((id1 (second id-equ)) ;;; Este let* está aquí por la - ;;; verificación de guardas + (let* ((id1 (second id-equ)) ;;; Este let* está aquí por la + ;;; verificación de guardas (id2 (third id-equ)) (p1 (dagi-l id1 g)) (p2 (dagi-l id2 g))) diff --git a/books/workshops/2004/ruiz-et-al/support/subsumption-subst.lisp b/books/workshops/2004/ruiz-et-al/support/subsumption-subst.lisp index 6eefb93b664..376e8836953 100644 --- a/books/workshops/2004/ruiz-et-al/support/subsumption-subst.lisp +++ b/books/workshops/2004/ruiz-et-al/support/subsumption-subst.lisp @@ -26,15 +26,15 @@ ;;; Our goal is to define the subsumption relation between ;;; substitutions. In the literature, this relation is defined in this ;;; way: -;;; sigma <= delta iff (exists gamma) gamma·sigma = delta -;;; where "·" stands for composition. +;;; sigma <= delta iff (exists gamma) gamma.sigma = delta +;;; where "." stands for composition. ;;; Note that equality between substitutions is functional equality (we cannot ;;; use equal), so we reformulate this property as: ;;; (*) sigma <= delta iff (exists gamma) ;;; s.t. for all term -;;; gamma·sigma(term) = delta(term) +;;; gamma.sigma(term) = delta(term) ;;; Our goal in this book is to define the subsumption relation between @@ -285,9 +285,9 @@ ;;; if (subs-sust sigma delta) ;;; WE DISTINGUISH THREE CASES. -;;; ············································································ +;;; ............................................................................ ;;; 3.1.1 Case 1: x is a variable outside V -;;; ············································································ +;;; ............................................................................ @@ -303,14 +303,14 @@ :hints (("Goal" :in-theory (enable x-not-in-domain-remains-the-same))))) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.2. Case 2: x is a variable of (domain-var sigma) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.2.1 A lemma for this case 2: ;;; subs-subst composed with sigma is equal to delta in V. -;;; ······················································ +;;; ...................................................... (local (encapsulate @@ -373,7 +373,7 @@ (local (in-theory (disable subs-subst matching-subst))) ;;; 3.1.2.2 Another lemma for case 2: -;;; ······························· +;;; ............................... (local (defthm variables-co-domain-var @@ -383,7 +383,7 @@ ;;; 3.1.2.3 The main result for Case 2 -;;; ································ +;;; ................................ (local (defthm @@ -396,14 +396,14 @@ (val x delta))))) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.3. Case 3: x in V but not in (domain-var sigma) -;;; ············································································ +;;; ............................................................................ ;;; 3.1.3.1 A lemma for Case 3 ;;; In this case, matching and matching-subst-r take the same values. -;;; ································································· +;;; ................................................................. (local (defthm @@ -472,7 +472,7 @@ ;;; With terms and list of terms (not only with variables) -;;; ······················································ +;;; ...................................................... (local (defthm @@ -512,7 +512,7 @@ ;;; following version will be used as a rewrite rule. ;;; With terms but without using composition -;;; ········································ +;;; ........................................ (defthm subs-subst-implies-matching-subst-r-appplied-to-sigma-term-is-delta-term @@ -526,7 +526,7 @@ ;;; With respect to subsumption between terms -;;; ········································· +;;; ......................................... ;;; Trivial consequence of completeness of subsumption and the previous @@ -563,7 +563,7 @@ ;;; existence of two substitutions, called sigma-w and delta-w and the ;;; only property we will assume about them is that sigma-w <= ;;; delta-w. That is, exists another substitution gamma-w such that -;;; delta-w = gamma-w·sigma-w. +;;; delta-w = gamma-w.sigma-w. ;;; We will use encapsulate for that purpose. Let sigma-w, delta-w and ;;; gamma-w three susbtitutions such that delta-w is functionally equal diff --git a/books/workshops/2004/ruiz-et-al/support/subsumption.lisp b/books/workshops/2004/ruiz-et-al/support/subsumption.lisp index 74fdaf726d8..938bbc3237b 100644 --- a/books/workshops/2004/ruiz-et-al/support/subsumption.lisp +++ b/books/workshops/2004/ruiz-et-al/support/subsumption.lisp @@ -1,7 +1,7 @@ ;;; subsumption.lisp Definition of a particular RULE-BASED matching ;;; algorithm between terms. We use functional instantion of the ;;; pattern given in matching.lisp Using this algorithm, we define the -;;; subsumption relñation between terms and lists of terms in a +;;; subsumption relñation between terms and lists of terms in a ;;; constructive way, and we prove that subsumption is a preorder. ;;; Created: 11-10-99 Last revison: 07-12-2000 ;;; ============================================================================= @@ -287,7 +287,7 @@ ;;; Most of these properties are obtained by functional instantiation. ;;; Soundness -;;; ········· +;;; ......... (defthm subs-soundness (implies (subs t1 t2) @@ -298,7 +298,7 @@ ;;; Completeness -;;; ············· +;;; ............. (defthm subs-completeness (implies (equal (instance t1 sigma) t2) @@ -308,7 +308,7 @@ (:instance match-mv-completeness (S (list (cons t1 t2))))))) ;;; Substitution-s-p (closure property) -;;; ··································· +;;; ................................... (defthm matching-substitution-s-p @@ -318,7 +318,7 @@ (:instance match-mv-substitution-s-p (S (list (cons t1 t2))))))) ;;; Substitution-p (needed for guard verification) -;;; ·············································· +;;; .............................................. (defthm matching-substitution-p @@ -409,7 +409,7 @@ (second (pair-args l1 (apply-subst nil sigma l1))))) ;;; Soundness -;;; ········· +;;; ......... (defthm subs-list-soundness @@ -421,7 +421,7 @@ ;;; Completeness -;;; ············· +;;; ............. (defthm subs-list-completeness (implies (equal (apply-subst nil sigma l1) l2) @@ -431,7 +431,7 @@ (:instance match-mv-completeness (S (first (pair-args l1 l2))))))) ;;; Substitution-s-p (closure property) -;;; ··································· +;;; ................................... (defthm matching-list-substitution-s-p @@ -444,7 +444,7 @@ ;;; Substitution-p (needed for guard verification) -;;; ·············································· +;;; .............................................. (defthm matching-list-substitution-p @@ -498,7 +498,7 @@ ;;; ---------------------------------------------------------------------------- ;;;; Subsumption reflexive -;;;; ····················· +;;;; ..................... (defthm subsumption-reflexive (subs t1 t1) @@ -508,7 +508,7 @@ ;;;; Subsumption transitive -;;;; ······················ +;;;; ...................... (defthm subsumption-transitive @@ -528,7 +528,7 @@ ;;; ---------------------------------------------------------------------------- ;;; An useful rule: -;;; ··············· +;;; ............... (defthm subsumption-apply-subst (subs term (instance term sigma)) @@ -536,7 +536,7 @@ (t1 term) (t2 (instance term sigma)))))) ;;; Variables are minimum elements in this quasi-order -;;; ·················································· +;;; .................................................. (defthm variable-minimum-subsumption (implies (variable-p x) diff --git a/books/workshops/2004/ruiz-et-al/support/terms-as-dag.lisp b/books/workshops/2004/ruiz-et-al/support/terms-as-dag.lisp index 705a4f2189d..6b00583c768 100644 --- a/books/workshops/2004/ruiz-et-al/support/terms-as-dag.lisp +++ b/books/workshops/2004/ruiz-et-al/support/terms-as-dag.lisp @@ -1,6 +1,6 @@ ;;; ============================================================================ ;;; terms-as-dag.lisp -;;; Título: Storing first--order terms as dags +;;; Título: Storing first--order terms as dags ;;; ============================================================================ #| To certify this book: @@ -20,7 +20,7 @@ ;;; ============================================================================ ;;; -;;; 0) Introducción +;;; 0) Introducción ;;; ;;; ============================================================================ diff --git a/books/workshops/2004/ruiz-et-al/support/terms.lisp b/books/workshops/2004/ruiz-et-al/support/terms.lisp index 391e9d22f6f..fc721089650 100644 --- a/books/workshops/2004/ruiz-et-al/support/terms.lisp +++ b/books/workshops/2004/ruiz-et-al/support/terms.lisp @@ -939,7 +939,7 @@ (disjointp (variables nil (co-domain S)) (domain S)))) ;;; REMARK: In the literature, idempotent substitutions are defined as -;;; substitutions sigma such that sigma·sigma = sigma. But this +;;; substitutions sigma such that sigma.sigma = sigma. But this ;;; definition involves functional equality. We will see that the above ;;; definition implies this property (see main-property-mgs in the book ;;; unification-definition.lisp) Nevertheless, the definition does not @@ -949,9 +949,9 @@ ;;; functionally equivalent idempotent (in our sense) substitution, ((x ;;; . y)) in this case. -;;; ············································································ +;;; ............................................................................ ;;; 3.3.1 The main property of idempotent substitutions. -;;; ············································································ +;;; ............................................................................ ;;; .... PROOF PLAN: @@ -1103,9 +1103,9 @@ ;;; 4.2 Some results concerning the tree structure of a term ;;; ---------------------------------------------------------------------------- -;;; ············································································ +;;; ............................................................................ ;;; 4.2.1 Concatenation of positions -;;; ············································································ +;;; ............................................................................ (defthm position-p-append (implies (position-p p1 term) @@ -1128,9 +1128,9 @@ q x))))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.2 Substitutions and positions -;;; ············································································ +;;; ............................................................................ (defthm nth-apply-subst (implies (and (integerp i) @@ -1165,9 +1165,9 @@ (instance (replace-term term pos t1) sigma)))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.3 Prefix positions -;;; ············································································ +;;; ............................................................................ (local (defthm equal-len-replace-list @@ -1202,9 +1202,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 4.2.4 Disjoint positions -;;; ············································································ +;;; ............................................................................ (local (defun induct-position-p-disjoint (pos1 pos2 term) @@ -1267,9 +1267,9 @@ (position-p (cons i pos) (cons fn args))))))) -;;; ············································································ +;;; ............................................................................ ;;; 4.2.5 Disabling the theory -;;; ············································································ +;;; ............................................................................ (defconst *tree-structure-of-terms* '(position-p-append occurrence-append replace-term-append diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/coe-fld.lisp b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/coe-fld.lisp index cc8c33645a9..f646eff259a 100644 --- a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/coe-fld.lisp +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/coe-fld.lisp @@ -42,22 +42,22 @@ ;;; Inmaculada Medina Bulo ;;; Francisco Palomo Lozano ;;; -;;; Descripción: +;;; Descripción: ;;; ;;; Anillo abeliano de coeficientes. El conjunto de los coeficientes ;;; se representa como un anillo abeliano abstracto mediante un -;;; encapsulado. El conjunto de los números de ACL2 con su -;;; interpretación habitual sirve como modelo de la teoría generada. +;;; encapsulado. El conjunto de los números de ACL2 con su +;;; interpretación habitual sirve como modelo de la teoría generada. ;;; ;;; Notas generales: ;;; -;;; Puede ser interesante comparar esta formalización con la que -;;; aparece en los libros sobre aritmética de Kaufmann, Brock y +;;; Puede ser interesante comparar esta formalización con la que +;;; aparece en los libros sobre aritmética de Kaufmann, Brock y ;;; Cowles. ;;; ;;; Se han incluido algunos teoremas que se deducen inmediatamente de -;;; otros por aplicación directa de la conmutatividad. Estos teoremas -;;; son innecesarios desde un punto de vista lógico, pero evitan el +;;; otros por aplicación directa de la conmutatividad. Estos teoremas +;;; son innecesarios desde un punto de vista lógico, pero evitan el ;;; abuso de la conmutatividad. ;;; ------------------------------------------------------------------ #| @@ -140,21 +140,21 @@ To certify this book, first, create a world with the following package: fdp (a) (acl2-numberp a))) - ;;; Primera operación + ;;; Primera operación (local (defun + (a b) ; (declare (xargs :guard (and (coeficientep a) (coeficientep b)))) (ACL2::+ a b))) - ;;; Segunda operación + ;;; Segunda operación (local (defun * (a b) ; (declare (xargs :guard (and (coeficientep a) (coeficientep b)))) (ACL2::* a b))) - ;;; Inverso de la primera operación + ;;; Inverso de la primera operación (local (defun - (a) @@ -166,7 +166,7 @@ To certify this book, first, create a world with the following package: ; (declare (xargs :guard (coeficientep a))) (ACL2::/ a))) - ;;; Neutro de la primera operación + ;;; Neutro de la primera operación ;; (local ;; (defun nulo () @@ -175,7 +175,7 @@ To certify this book, first, create a world with the following package: (local (defun 0_f () 0)) - ;;; Neutro de la segunda operación + ;;; Neutro de la segunda operación ;; (local ;; (defun identidad () @@ -184,7 +184,7 @@ To certify this book, first, create a world with the following package: (local (defun 1_f () 1)) - ;;; Igualdad sintáctica + ;;; Igualdad sintáctica ;; (defmacro = (a b) ;; `(equal ,a ,b)) @@ -200,7 +200,7 @@ To certify this book, first, create a world with the following package: ;;; ------- ;;; Field Axioms: - ;;; El reconocedor es una función booleana + ;;; El reconocedor es una función booleana ;; (defthm booleanp-coeficientep ;; (booleanp (coeficientep a)) @@ -463,7 +463,7 @@ To certify this book, first, create a world with the following package: :hints (("Goal" :use Congruence-Laws))) - ;;; Conmutatividad de la primera operación + ;;; Conmutatividad de la primera operación ;; (defthm |a + b = b + a| ;; (implies (and (coeficientep a) (coeficientep b)) @@ -476,7 +476,7 @@ To certify this book, first, create a world with the following package: :hints (("Goal" :use Commutativity-Laws))) - ;;; Asociatividad de la primera operación + ;;; Asociatividad de la primera operación ;; (defthm |(a + b) + c = a + (b + c)| ;; (implies (and (coeficientep a) (coeficientep b) (coeficientep c)) @@ -490,7 +490,7 @@ To certify this book, first, create a world with the following package: :hints (("Goal" :use Associativity-Laws))) - ;;; Neutro de la primera operación + ;;; Neutro de la primera operación ;; (defthm |0 + a = a| ;; (implies (coeficientep a) @@ -502,7 +502,7 @@ To certify this book, first, create a world with the following package: :hints (("Goal" :use Left-Unicity-Laws))) - ;;; Conmutatividad de la segunda operación + ;;; Conmutatividad de la segunda operación ;; (defthm |a * b = b * a| ;; (implies (and (coeficientep a) (coeficientep b)) @@ -515,7 +515,7 @@ To certify this book, first, create a world with the following package: :hints (("Goal" :use Commutativity-Laws))) - ;;; Asociatividad de la segunda operación + ;;; Asociatividad de la segunda operación ;; (defthm |(a * b) * c = a * (b * c)| ;; (implies (and (coeficientep a) (coeficientep b) (coeficientep c)) @@ -529,7 +529,7 @@ To certify this book, first, create a world with the following package: :hints (("Goal" :use Associativity-Laws))) - ;;; Neutro de la segunda operación + ;;; Neutro de la segunda operación ;; (defthm |1 * a = a| ;; (implies (coeficientep a) @@ -541,7 +541,7 @@ To certify this book, first, create a world with the following package: :hints (("Goal" :use Left-Unicity-Laws))) - ;;; Inverso de la primera operación + ;;; Inverso de la primera operación ;; (defthm |a + (- a) = 0| ;; (implies (coeficientep a) @@ -560,7 +560,7 @@ To certify this book, first, create a world with the following package: :hints (("Goal" :use Right-Inverse-Laws))) - ;;; Distributividad de la segunda operación respecto a la primera + ;;; Distributividad de la segunda operación respecto a la primera ;; (defthm |a * (b + c) = (a * b) + (a * c)| ;; (implies (and (coeficientep a) (coeficientep b) (coeficientep c)) @@ -575,7 +575,7 @@ To certify this book, first, create a world with the following package: :use Left-Distributivity-Law))) ;;; ----------------------------------------------------------------------- -;;; El inverso debe ser invisible para la primera operación y para sí mismo +;;; El inverso debe ser invisible para la primera operación y para sí mismo ;;; ----------------------------------------------------------------------- ;; (ACL2::set-invisible-fns-table ((+ -) (- -))) @@ -642,7 +642,7 @@ To certify this book, first, create a world with the following package: (fdp (double-rewrite c))) (= (* (+ a b) c) (+ (* a c) (* b c))))) -;;; Teorema de cancelación +;;; Teorema de cancelación ;; (defthm |a + c = b + c <=> a = b| ;; (implies (and (coeficientep a) (coeficientep b) (coeficientep c)) @@ -666,8 +666,8 @@ To certify this book, first, create a world with the following package: ;;; NOTA: ;;; -;;; Estos teoremas son innecesarios desde un punto de vista lógico -;;; pero son útiles en las subsecuentes demostraciones. +;;; Estos teoremas son innecesarios desde un punto de vista lógico +;;; pero son útiles en las subsecuentes demostraciones. ;; (local ;; (defthm |a + b = b <=> a = 0| @@ -701,16 +701,16 @@ To certify this book, first, create a world with the following package: :in-theory (disable |a + c = b + c <=> a = b|) :use (:instance |a + c = b + c <=> a = b| (a b) (b (- a)) (c a)))))) -;;; Complemento a la conmutatividad y la asociatividad de la primera operación +;;; Complemento a la conmutatividad y la asociatividad de la primera operación ;;; NOTA: ;;; -;;; Dada una operación, las reglas generadas por este teorema y los +;;; Dada una operación, las reglas generadas por este teorema y los ;;; axiomas de conmutatividad y asociatividad permiten decidir una -;;; igualdad de dos términos en los que sólo intervienen símbolos sin -;;; interpretación y dicha operación. Esto se debe a que ACL2 emplea -;;; un sistema de reescritura ordenada. Véase «Ordered Rewriting and -;;; Confluence», por Martin y Nipkow. +;;; igualdad de dos términos en los que sólo intervienen símbolos sin +;;; interpretación y dicha operación. Esto se debe a que ACL2 emplea +;;; un sistema de reescritura ordenada. Véase «Ordered Rewriting and +;;; Confluence», por Martin y Nipkow. ;; (defthm |a + (b + c) = b + (a + c)| ;; (implies (and (coeficientep a) (coeficientep b) (coeficientep c)) @@ -730,11 +730,11 @@ To certify this book, first, create a world with the following package: :use (|(a + b) + c = a + (b + c)| (:instance |(a + b) + c = a + (b + c)| (a b) (b a)))))) -;;; Complemento a la conmutatividad y la asociatividad de la segunda operación +;;; Complemento a la conmutatividad y la asociatividad de la segunda operación ;;; NOTA: ;;; -;;; Se aplican comentarios análogos a los del caso anterior. +;;; Se aplican comentarios análogos a los del caso anterior. ;; (defthm |a * (b * c) = b * (a * c)| ;; (implies (and (coeficientep a) (coeficientep b) (coeficientep c)) @@ -770,7 +770,7 @@ To certify this book, first, create a world with the following package: :in-theory (disable |a + b = 0 <=> b = - a|) :use (:instance |a + b = 0 <=> b = - a| (a (- a)) (b a))))) -;;; Distributividad de la inversa sobre la primera operación +;;; Distributividad de la inversa sobre la primera operación ;; (defthm |- (a + b) = (- a) + (- b)| ;; (implies (and (coeficientep a) (coeficientep b)) @@ -788,7 +788,7 @@ To certify this book, first, create a world with the following package: :use (:instance |a + b = 0 <=> b = - a| (a (+ a b)) (b (+ (- a) (- b))))))) -;;; Inverso del neutro de la primera operación +;;; Inverso del neutro de la primera operación ;; (defthm |- 0 = 0| ;; (= (- (nulo)) (nulo)) @@ -802,7 +802,7 @@ To certify this book, first, create a world with the following package: :in-theory (disable |a + b = 0 <=> b = - a|) :use (:instance |a + b = 0 <=> b = - a| (a (0_f)) (b (0_f)))))) -;;; Generalización de |a + (- a) = 0| +;;; Generalización de |a + (- a) = 0| ;; (defthm |a + ((- a) + b) = b| ;; (implies (and (coeficientep a) (coeficientep b)) @@ -828,7 +828,7 @@ To certify this book, first, create a world with the following package: (fdp (double-rewrite b))) (= (+ a (+ b (- a))) b))) -;;; Elemento cancelador de la segunda operación +;;; Elemento cancelador de la segunda operación ;; (defthm |0 * a = 0| ;; (implies (coeficientep a) @@ -857,7 +857,7 @@ To certify this book, first, create a world with the following package: (implies (fdp (double-rewrite a)) (= (* a (0_f)) (0_f)))) -;;; Extracción del inverso +;;; Extracción del inverso ;; (defthm |a * (- b) = - (a * b)| ;; (implies (and (coeficientep a) (coeficientep b)) @@ -885,7 +885,7 @@ To certify this book, first, create a world with the following package: (fdp (double-rewrite b))) (= (* (- a) b) (- (* a b))))) -;;; Generalización de |- 0 = 0| +;;; Generalización de |- 0 = 0| ;; (defthm |- a = 0 <=> a = 0| ;; (implies (coeficientep a) @@ -1027,10 +1027,10 @@ To certify this book, first, create a world with the following package: ;;; NOTA: ;;; ;;; El lado izquierdo puede aparecer por varias razones, sin -;;; descartar una aplicación de |- (a + b) = (- a) + (- b)| en un +;;; descartar una aplicación de |- (a + b) = (- a) + (- b)| en un ;;; contexto en el que aparece |- (a + b) = c| y posteriormente se -;;; establece que |c = 0|. Esto podría evitarse postponiendo la -;;; definición de dicha regla. +;;; establece que |c = 0|. Esto podría evitarse postponiendo la +;;; definición de dicha regla. ;; (defthm |(- a) + (- b) = 0 <=> a + b = 0| ;; (implies (and (coeficientep a) (coeficientep b)) @@ -1049,7 +1049,7 @@ To certify this book, first, create a world with the following package: ;;; NOTA: ;;; -;;; En un anillo el recíproco no es, en general, cierto. +;;; En un anillo el recíproco no es, en general, cierto. ;; (defthm |b + c = 0 => (a * b) + (a * c) = 0| ;; (implies (and (coeficientep a) (coeficientep b) (coeficientep c) diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-producto.lisp b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-producto.lisp index eff8fac98b0..bb87da82faf 100644 --- a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-producto.lisp +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-producto.lisp @@ -30,9 +30,9 @@ ;;; Inmaculada Medina Bulo ;;; Francisco Palomo Lozano ;;; -;;; Descripción: +;;; Descripción: ;;; -;;; Demostración de las congruencias de la igualdad de polinomios con +;;; Demostración de las congruencias de la igualdad de polinomios con ;;; el producto externo y el producto. ;;; ----------------------------------------------------------------- #| @@ -74,7 +74,7 @@ To certify this book, first, create a world with the following packages: :load-compiled-file nil) ;;; -------------------------------------------------------- -;;; Éstas son las propiedades de "polinomio" que lo abstraen +;;; Éstas son las propiedades de "polinomio" que lo abstraen ;;; -------------------------------------------------------- (defthm |m +M p != 0| @@ -92,7 +92,7 @@ To certify this book, first, create a world with the following packages: (equal (resto (+M m p)) p))) ;;; ++++++++++++++++++++++++++ -;;; + Barrera de abstracción + +;;; + Barrera de abstracción + ;;; ++++++++++++++++++++++++++ (in-theory (disable +M)) @@ -101,8 +101,8 @@ To certify this book, first, create a world with the following packages: ;;; Distributividad del producto externo respecto a la suma externa ;;; --------------------------------------------------------------- -;;; Propiedades sintácticas de la suma de monomio y polinomio y la -;;; normalización. +;;; Propiedades sintácticas de la suma de monomio y polinomio y la +;;; normalización. ;; (defthm |fn(m +Mo fn(p)) = fn(m +Mo p)| ;; (equal (fn (+-monomio m (fn p))) @@ -124,7 +124,7 @@ To certify this book, first, create a world with the following packages: :hints (("Subgoal *1/8" :in-theory (enable +M)))) -;;; Este es un caso particular de la definición de "+-monomio". +;;; Este es un caso particular de la definición de "+-monomio". (defthm |n +Mo p = p_p +M (n +Mo p_r)| (implies (and (monomiop (double-rewrite n)) @@ -135,9 +135,9 @@ To certify this book, first, create a world with the following packages: (+M (primero p) (+-monomio n (resto p))))) :hints (("Goal" :do-not '(generalize)))) -;;; Esta propiedad sintáctica establece la relación entre La suma de +;;; Esta propiedad sintáctica establece la relación entre La suma de ;;; monomios y polinomios, el constructor de los polinomios y la -;;; función de normalización. +;;; función de normalización. (defthm |m +Mo fn(p) = fn(m +M p)| (implies (and (monomiop (double-rewrite m)) @@ -150,14 +150,14 @@ To certify this book, first, create a world with the following packages: ;;; NOTA: ;;; -;;; Este teorema es tremendamente complicado. Nótese que la igualdad a -;;; la que apela es sintáctica. El problema es una explosión -;;; combinatoria en el número de casos debido, principalmente, a la -;;; gran cantidad de casos existente en la definición de +;;; Este teorema es tremendamente complicado. Nótese que la igualdad a +;;; la que apela es sintáctica. El problema es una explosión +;;; combinatoria en el número de casos debido, principalmente, a la +;;; gran cantidad de casos existente en la definición de ;;; "+-monomio". Por otro lado, no parece factible simplificar dicha -;;; definición, ya que esto obligaría a añadir hipótesis a muchos +;;; definición, ya que esto obligaría a añadir hipótesis a muchos ;;; teoremas que son necesarios para demostrar la congruencia -;;; (recuérdese que las congruencias son incondicionales). La +;;; (recuérdese que las congruencias son incondicionales). La ;;; consecuencia es una prueba muy extensa, poco automatizada y muy ;;; sensible al entorno. @@ -289,7 +289,7 @@ To certify this book, first, create a world with the following packages: ;;; ;;; En realidad, este es el teorema que realmente queremos demostrar ;;; pero, para ello, hemos necesitado el anterior. Se emplea en la -;;; demostración de que "m *M p = m *M fn(p)", que permite establecer +;;; demostración de que "m *M p = m *M fn(p)", que permite establecer ;;; la congruencia con el producto externo. (in-theory (disable |fn(m *M (n +Mo p)) =P fn((m * n) +Mo (m *M p))|)) @@ -306,7 +306,7 @@ To certify this book, first, create a world with the following packages: ;; (in-theory (disable |fn(m *M (n +Mo p)) = fn((m * n) +Mo (m *M p))|)) ;;; ++++++++++++++++++++++++++ -;;; + Barrera de abstracción + +;;; + Barrera de abstracción + ;;; ++++++++++++++++++++++++++ (in-theory (disable = (=))) @@ -315,7 +315,7 @@ To certify this book, first, create a world with the following packages: ;;; Congruencias de la igualdad de polinomios con el producto externo ;;; ----------------------------------------------------------------- -;;; Primer parámetro +;;; Primer parámetro ;; (defcong MON::= = (*-monomio m p) 1 ;; :hints (("Goal" :in-theory (enable MON::=)))) @@ -327,11 +327,11 @@ To certify this book, first, create a world with the following packages: (*-monomio m2 p))) :rule-classes :congruence) -;;; Segundo parámetro +;;; Segundo parámetro ;;; NOTA: ;;; -;;; Esta propiedad es expansiva; restringimos su aplicación sintácticamente +;;; Esta propiedad es expansiva; restringimos su aplicación sintácticamente (local (defthm |m +M p = m +Mo p| @@ -383,7 +383,7 @@ To certify this book, first, create a world with the following packages: ;;; Congruencia de la igualdad de polinomios con el producto ;;; -------------------------------------------------------- -;;; Segundo parámetro +;;; Segundo parámetro (defthm |p * fn(q) = p * q| (= (* p (fn q)) (* p q))) @@ -396,7 +396,7 @@ To certify this book, first, create a world with the following packages: (* p q2))) :rule-classes :congruence) -;;; Primer parámetro +;;; Primer parámetro (defthm |fn(p) * q = p * q| (= (* (fn p) q) (* p q))) diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-suma.lisp b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-suma.lisp index 11ff0555958..06cb30c3f1f 100644 --- a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-suma.lisp +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-suma.lisp @@ -30,23 +30,23 @@ ;;; Inmaculada Medina Bulo ;;; Francisco Palomo Lozano ;;; -;;; Descripción: +;;; Descripción: ;;; -;;; Aquí se demuestran las congruencias de la igualdad de polinomios +;;; Aquí se demuestran las congruencias de la igualdad de polinomios ;;; con la suma. Las demostraciones son complejas debido a que ;;; necesitan reglas expansivas. Estas reglas son peligrosas, ya que -;;; pueden producir fácilmente ciclos en el demostrador. Para -;;; restringir su aplicación caben dos opciones: +;;; pueden producir fácilmente ciclos en el demostrador. Para +;;; restringir su aplicación caben dos opciones: ;;; -;;; 1. Desactivarlas y usarlas explícitamente donde sea necesario. Una +;;; 1. Desactivarlas y usarlas explícitamente donde sea necesario. Una ;;; variante es no generar la regla en absoluto (es decir, introducir -;;; el teorema con la clases de reglas vacía). +;;; el teorema con la clases de reglas vacía). ;;; -;;; 2. Restringir su aplicación sintácticamente para prevenir +;;; 2. Restringir su aplicación sintácticamente para prevenir ;;; expansiones en cadena. Esto se puede lograr graciasa syntaxp. ;;; -;;; Elegimos la segunda opción porque se consigue un mayor grado de -;;; automatización y hace a las demostraciones menos sensibles a los +;;; Elegimos la segunda opción porque se consigue un mayor grado de +;;; automatización y hace a las demostraciones menos sensibles a los ;;; cambios. ;;; ------------------------------------------------------------------ #| @@ -91,11 +91,11 @@ To certify this book, first, create a world with the following packages: ;;; Congruencia de la igualdad de polinomios con la suma ;;; ---------------------------------------------------- -;;; Segundo parámetro +;;; Segundo parámetro ;;; NOTA: ;;; -;;; Esta propiedad es expansiva; restringimos su aplicación sintácticamente +;;; Esta propiedad es expansiva; restringimos su aplicación sintácticamente (defthm polinomiop-implies-true-listp @@ -141,7 +141,7 @@ To certify this book, first, create a world with the following packages: (+ p q2))) :rule-classes :congruence) -;;; Primer parámetro +;;; Primer parámetro ;; (defcong = = (+ p q) 1 ;; :hints (("Goal" @@ -165,7 +165,7 @@ To certify this book, first, create a world with the following packages: ;;; NOTA: ;;; -;;; Esta propiedad es expansiva; restringimos su aplicación sintácticamente +;;; Esta propiedad es expansiva; restringimos su aplicación sintácticamente (defthm |p + q = fn(p) + q| (implies (syntaxp (not (and (consp p) (eq (primero p) 'fn)))) diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuforma-normal.lisp b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuforma-normal.lisp index 7e1d77fe45b..2c1c5c03f6f 100644 --- a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuforma-normal.lisp +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuforma-normal.lisp @@ -30,16 +30,16 @@ ;;; Inmaculada Medina Bulo ;;; Francisco Palomo Lozano ;;; -;;; Descripción: +;;; Descripción: ;;; -;;; Desarrollo de la función de normalización que permite reducir la -;;; comprobación de la igualdad semántica de dos polinomios a la de -;;; una igualdad sintáctica de sus formas normales. Se define primero +;;; Desarrollo de la función de normalización que permite reducir la +;;; comprobación de la igualdad semántica de dos polinomios a la de +;;; una igualdad sintáctica de sus formas normales. Se define primero ;;; una suma externa de un monomio con un polinomio ordenado, teniendo -;;; en cuenta una posible cancelación. A partir de aquí se define la -;;; forma normal y su relación de equivalencia inducida. Se demuestran +;;; en cuenta una posible cancelación. A partir de aquí se define la +;;; forma normal y su relación de equivalencia inducida. Se demuestran ;;; algunas propiedades importantes como la idempotencia de la -;;; normalización. +;;; normalización. ;;; ------------------------------------------------------------------ #| To certify this book, first, create a world with the following packages: @@ -83,7 +83,7 @@ To certify this book, first, create a world with the following packages: ;;; Polinomios ordenados ;;; -------------------- -;;; Esta función permite averiguar si un monomio debe preceder al +;;; Esta función permite averiguar si un monomio debe preceder al ;;; monomio principal de un polinomio ordenado (defmacro termino-mayor-termino-principal (m p) @@ -91,7 +91,7 @@ To certify this book, first, create a world with the following packages: (FUTER::< (termino (primero ,p)) (termino ,m)))) ;;; Reconocedor de polinomios estrictamente ordenado mediante un orden -;;; de términos decreciente y que no poseen monomios nulos +;;; de términos decreciente y que no poseen monomios nulos (defun ordenadop (p) (and (polinomiop p) @@ -101,7 +101,7 @@ To certify this book, first, create a world with the following packages: (ordenadop (resto p)))))) ;;; ------------------------------------ -;;; Adición de un monomio y un polinomio +;;; Adición de un monomio y un polinomio ;;; ------------------------------------ ;;; Suma un monomio a un polinomio @@ -125,7 +125,7 @@ To certify this book, first, create a world with the following packages: ;;; NOTA: ;;; ;;; Hay que garantizar (cosa que probaremos en breve) que si el -;;; polinomio está normalizado, el resultado también. +;;; polinomio está normalizado, el resultado también. ;; (defun +-monomio (m p) ;; (cond ((and (not (monomiop m)) (not (polinomiop p))) @@ -404,18 +404,18 @@ To certify this book, first, create a world with the following packages: ;;; Forma normal ;;; ------------ -;;; Normalización de un polinomio meidante adición de monomios. +;;; Normalización de un polinomio meidante adición de monomios. ;;; NOTA: ;;; -;;; Este es un punto en el que en un futuro se podría trabajar para -;;; mejorar la eficiencia de los algoritmos. Básicamente podemos -;;; entender la normalización de un polinomio como un proceso de -;;; ordenación (con algunas diferencias importantes) y, con éste -;;; símil, el algoritmo que se presenta a continuación correspondería -;;; con un método directo (inserción directa). Cabría la posibilidad -;;; de adaptar algoritmos de ordenación más eficientes (los de Hoare y -;;; Williams serían buenas opciones) para normalizar polinomios. +;;; Este es un punto en el que en un futuro se podría trabajar para +;;; mejorar la eficiencia de los algoritmos. Básicamente podemos +;;; entender la normalización de un polinomio como un proceso de +;;; ordenación (con algunas diferencias importantes) y, con éste +;;; símil, el algoritmo que se presenta a continuación correspondería +;;; con un método directo (inserción directa). Cabría la posibilidad +;;; de adaptar algoritmos de ordenación más eficientes (los de Hoare y +;;; Williams serían buenas opciones) para normalizar polinomios. (defun fn (p) (cond ((or (not (polinomiop p)) (nulop p)) @@ -433,7 +433,7 @@ To certify this book, first, create a world with the following packages: ;;; ;;; NOTA: ;;; -;;; Un polinomio normalizado coincide sintácticamente con su forma +;;; Un polinomio normalizado coincide sintácticamente con su forma ;;; normal. (defmacro fnp (p) @@ -445,22 +445,22 @@ To certify this book, first, create a world with the following packages: (ordenadop (fn p)) :rule-classes (:type-prescription :rewrite)) -;;; Si un polinomio está ordenado entonces está en forma normal +;;; Si un polinomio está ordenado entonces está en forma normal (defthm fn-ordenado (implies (ordenadop (double-rewrite p)) (equal (fn p) p))) -;;; Un polinomio está en forma normal si, y sólo si, está ordenado +;;; Un polinomio está en forma normal si, y sólo si, está ordenado ;;; NOTA: ;;; -;;; Este teorema establece la corrección de la función de -;;; normalización frente a la especificación dada por el hecho de que +;;; Este teorema establece la corrección de la función de +;;; normalización frente a la especificación dada por el hecho de que ;;; un polinomio en forma normal debe tener sus monomios ordenados ;;; decrecientemente y no puede poseer monomios nulos. Al ser la -;;; ordenación estricta, se evita la posibilidad de que aparezcan -;;; monomios con el mismo término. +;;; ordenación estricta, se evita la posibilidad de que aparezcan +;;; monomios con el mismo término. (defthm fnp-iff-ordenadop (iff (fnp p) (ordenadop p))) @@ -472,15 +472,15 @@ To certify this book, first, create a world with the following packages: (fnp (fn p))) ;;; ------------------ -;;; Igualdad semántica +;;; Igualdad semántica ;;; ------------------ -;;; Igualdad semántica +;;; Igualdad semántica ;;; NOTA: ;;; -;;; Aquí radica una de las aplicaciones de la forma normal: permitir -;;; comprobar si dos polinomios son iguales módulo formas normales. +;;; Aquí radica una de las aplicaciones de la forma normal: permitir +;;; comprobar si dos polinomios son iguales módulo formas normales. ;; (defun = (p1 p2) ;; (equal (fn p1) (fn p2))) @@ -488,12 +488,12 @@ To certify this book, first, create a world with the following packages: (defun = (p1 p2) (=P (fn p1) (fn p2))) -;;; La igualdad semántica es una relación de equivalencia +;;; La igualdad semántica es una relación de equivalencia ;;; NOTA: ;;; ;;; Esto abre paso al establecimiento de las congruencias entre la -;;; igualdad semántica y las operaciones. +;;; igualdad semántica y las operaciones. (defthm =-is-an-equivalence @@ -558,7 +558,7 @@ To certify this book, first, create a world with the following packages: (FLD::a a) (FLD::b b) (FLD::c (coeficiente (primero p))))))) -;; (defthm |¬(a + b) = 0 => a +Mo (b +Mo p) = (a + b) +Mo p| +;; (defthm |¬(a + b) = 0 => a +Mo (b +Mo p) = (a + b) +Mo p| ;; (implies (and (COE::coeficientep a) ;; (COE::coeficientep b) ;; (TER::terminop te) @@ -584,7 +584,7 @@ To certify this book, first, create a world with the following packages: ;;; polinomio ;;; ----------------------------------------------------------------- -;;; Primer parámetro +;;; Primer parámetro ;; (defcong MON::= = (+M m p) 1 ;; :hints (("Goal" :in-theory (enable MON::=)))) @@ -596,7 +596,7 @@ To certify this book, first, create a world with the following packages: (+M m2 p))) :rule-classes :congruence) -;;; Segundo parámetro +;;; Segundo parámetro ;; (defcong = = (+M m p) 2) @@ -624,7 +624,7 @@ To certify this book, first, create a world with the following packages: ;;; Congruencia de la igualdad de polinomios con la suma externa ;;; ------------------------------------------------------------ -;;; Primer parámetro +;;; Primer parámetro ;; (defcong MON::= equal (+-monomio m p) 1 ;; :hints (("Goal" :in-theory (enable MON::=)))) @@ -640,14 +640,14 @@ To certify this book, first, create a world with the following packages: ;;; NOTA: ;;; -;;; Esta propiedad es expansiva; restringimos su aplicación sintácticamente +;;; Esta propiedad es expansiva; restringimos su aplicación sintácticamente (local (defthm +-monomio-fn (implies (syntaxp (not (and (consp p) (eq (primero p) 'fn)))) (= (+-monomio m p) (+-monomio m (fn p)))))) -;;; Segundo parámetro +;;; Segundo parámetro ;; (defcong = = (+-monomio m p) 2) diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fumonomio.lisp b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fumonomio.lisp index a13a825be06..fe809b318ad 100644 --- a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fumonomio.lisp +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fumonomio.lisp @@ -23,19 +23,19 @@ ;; Based on ;;; ------------------------------------------------------------------ -;;; Monomios con coeficientes y términos abstractos +;;; Monomios con coeficientes y términos abstractos ;;; ;;; Autores: ;;; ;;; Inmaculada Medina Bulo ;;; Francisco Palomo Lozano ;;; -;;; Descripción: +;;; Descripción: ;;; -;;; Pares coeficiente-término. Se define una igualdad semántica, ya +;;; Pares coeficiente-término. Se define una igualdad semántica, ya ;;; que dos monomios con coeficiente nulo han de ser interpretados -;;; como el mismo, aunque tengan distinto término. Orden de monomios -;;; heredado de los términos. +;;; como el mismo, aunque tengan distinto término. Orden de monomios +;;; heredado de los términos. ;;; ------------------------------------------------------------------ #| To certify this book, first, create a world with the following packages: @@ -131,7 +131,7 @@ To certify this book, first, create a world with the following packages: (defun nulop (a) (FLD::= (coeficiente a) (FLD::0_f))) -;;; Neutro de la operación +;;; Neutro de la operación ;; (defun identidad () ;; (monomio (COE::identidad) (TER::uno))) @@ -139,7 +139,7 @@ To certify this book, first, create a world with the following packages: (defun identidad () (monomio (FLD::1_f) (FUTER::uno))) -;;; Operación +;;; Operación ;; (defun * (a b) ;; (monomio (COE::* (coeficiente a) (coeficiente b)) @@ -149,7 +149,7 @@ To certify this book, first, create a world with the following packages: (monomio (FLD::* (coeficiente a) (coeficiente b)) (FUTER::* (termino a) (termino b)))) -;;; Igualdad semántica +;;; Igualdad semántica ;; (defun = (a b) ;; (or (and (not (monomiop a)) (not (monomiop b))) @@ -167,7 +167,7 @@ To certify this book, first, create a world with the following packages: (FLD::= (coeficiente a) (coeficiente b)) (FUTER::= (termino a) (termino b))))) -;;; Igualdad de los términos subyacentes +;;; Igualdad de los términos subyacentes (defmacro =T (a b) `(FUTER::= (termino ,a) (termino ,b))) @@ -177,13 +177,13 @@ To certify this book, first, create a world with the following packages: (defmacro < (a b) `(FUTER::< (termino ,a) (termino ,b))) -;;; Inmersión en los ordinales +;;; Inmersión en los ordinales (defmacro monomio->ordinal (a) `(FUTER::termino->ordinal (termino ,a))) ;;; ----------------------- -;;; Teoría de las funciones +;;; Teoría de las funciones ;;; ----------------------- (deftheory funciones @@ -287,13 +287,13 @@ To certify this book, first, create a world with the following packages: (* x y2))) :rule-classes :congruence) -;;; Conmutatividad de la operación +;;; Conmutatividad de la operación (defthm |a * b = b * a| (implies (and (monomiop a) (monomiop b)) (= (* a b) (* b a)))) -;;; Asociatividad de la operación +;;; Asociatividad de la operación ;; (defthm |(a * b) * c = a * (b * c)| ;; (implies (and (monomiop a) (monomiop b) (monomiop c)) @@ -307,21 +307,21 @@ To certify this book, first, create a world with the following packages: :hints (("Goal" :in-theory (disable (nulo) FLD::|a + b = b + a|)))) -;;; Neutro de la operación +;;; Neutro de la operación (defthm |1 * b = b| (implies (monomiop b) (= (* (identidad) b) b)) :hints (("Goal" :in-theory (disable (identidad))))) -;;; Cancelativo de la operación +;;; Cancelativo de la operación (defthm |a = 0 => a * b = 0| (implies (and (monomiop a) (monomiop b) (nulop a)) (nulop (* a b))) :hints (("Goal" :in-theory (disable (nulo))))) -;;; Coeficiente y término del constructor +;;; Coeficiente y término del constructor ;; (defthm coeficiente-monomio ;; (implies (and (coeficientep c) (terminop e)) @@ -339,14 +339,14 @@ To certify this book, first, create a world with the following packages: (implies (and (fdp (double-rewrite c)) (terminop e)) (FUTER::= (termino (monomio c e)) e))) -;;; Eliminación de destructores +;;; Eliminación de destructores (defthm monomio-coeficiente-termino (implies (monomiop m) (equal (monomio (coeficiente m) (termino m)) m)) :rule-classes (:rewrite :elim)) -;;; Coeficiente y término de la operación +;;; Coeficiente y término de la operación ;; (defthm coeficiente-* ;; (COE::= (coeficiente (* a b)) @@ -362,7 +362,7 @@ To certify this book, first, create a world with the following packages: (FUTER::= (termino (* a b)) (FUTER::* (termino a) (termino b)))) -;;; Buena fundamentación +;;; Buena fundamentación (defthm buena-fundamentacion-<-M (and (implies (monomiop a) @@ -437,7 +437,7 @@ To certify this book, first, create a world with the following packages: (monomio (FLD::+ (coeficiente a) (coeficiente b)) (termino a))) -;;; Negación +;;; Negación ;; (defun - (a) ;; (monomio (COE::- (coeficiente a)) (termino a))) @@ -467,7 +467,7 @@ To certify this book, first, create a world with the following packages: (implies (nulop a) (nulop (* b a)))) -;;; Complemento a la conmutatividad y la asociatividad de la operación +;;; Complemento a la conmutatividad y la asociatividad de la operación (defthm |a * (b * c) = b * (a * c)| (implies (and (monomiop a) (monomiop b) (monomiop c)) @@ -562,12 +562,12 @@ To certify this book, first, create a world with the following packages: ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; ++++++++++++++++++++++++++ -;;; + Barrera de abstracción + +;;; + Barrera de abstracción + ;;; ++++++++++++++++++++++++++ ;;; NOTA: ;;; -;;; A partir de aquí se procederá por aplicación de las propiedades +;;; A partir de aquí se procederá por aplicación de las propiedades (in-theory (disable funciones)) (in-theory (enable nulop (nulop) (:type-prescription nulop))) diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuopuesto.lisp b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuopuesto.lisp index 790f562df57..00119638cd3 100644 --- a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuopuesto.lisp +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuopuesto.lisp @@ -30,13 +30,13 @@ ;;; Inmaculada Medina Bulo ;;; Francisco Palomo Lozano ;;; -;;; Descripción: +;;; Descripción: ;;; ;;; Desarrollo del opuesto de un polinomio, que se define monomio a -;;; monomio. Su corrección se prueba demostrando que la función que lo -;;; calcula produce el inverso aditivo. Para que éstas y otras -;;; propiedades sean incondicionales (carezcan de hipótesis) se -;;; completa cuidadosamente la definición de la función. Se demuestra +;;; monomio. Su corrección se prueba demostrando que la función que lo +;;; calcula produce el inverso aditivo. Para que éstas y otras +;;; propiedades sean incondicionales (carezcan de hipótesis) se +;;; completa cuidadosamente la definición de la función. Se demuestra ;;; que los polinomios con las operaciones de suma y opuesto forman un ;;; grupo conmutativo. ;;; ------------------------------------------------------------------ @@ -82,8 +82,8 @@ To certify this book, first, create a world with the following packages: ;;; Opuesto de polinomios ;;; --------------------- -;;; La siguiente desactivación es necesaria para la verificación de la -;;; protección del opuesto +;;; La siguiente desactivación es necesaria para la verificación de la +;;; protección del opuesto (in-theory (disable FUMON::monomio-coeficiente-termino)) @@ -191,7 +191,7 @@ To certify this book, first, create a world with the following packages: (local (in-theory (disable polinomiop = + -))) ;;; ----------------------------------------------------------------------- -;;; El inverso debe ser invisible para la primera operación y para sí mismo +;;; El inverso debe ser invisible para la primera operación y para sí mismo ;;; ----------------------------------------------------------------------- (ACL2::set-invisible-fns-table ((+ -) (- -))) @@ -245,7 +245,7 @@ To certify this book, first, create a world with the following packages: :in-theory (disable |p + q = 0 <=> q = - p|) :use (:instance |p + q = 0 <=> q = - p| (p (- p)) (q p))))) -;;; Distributividad de la inversa sobre la primera operación +;;; Distributividad de la inversa sobre la primera operación (defthm |- (p + q) = (- p) + (- q)| (= (- (+ p q)) (+ (- p) (- q))) diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio-normalizado.lisp b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio-normalizado.lisp index 61e5666a3e8..fb605c578b8 100644 --- a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio-normalizado.lisp +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio-normalizado.lisp @@ -30,11 +30,11 @@ ;;; Inmaculada Medina Bulo ;;; Francisco Palomo Lozano ;;; -;;; Descripción: +;;; Descripción: ;;; ;;; Polinomios normalizados definidos a partir de los polinomios -;;; desnormalizados y de la operación de normalización. Ascenso de las -;;; propiedades de anillo de la representación desnormalizada a la +;;; desnormalizados y de la operación de normalización. Ascenso de las +;;; propiedades de anillo de la representación desnormalizada a la ;;; normalizada. ;;; ------------------------------------------------------------------ #| @@ -138,7 +138,7 @@ To certify this book, first, create a world with the following packages: :rule-classes :type-prescription) ;;; -------------- -;;; Multiplicación +;;; Multiplicación ;;; -------------- (defun * (p q) @@ -386,13 +386,13 @@ To certify this book, first, create a world with the following packages: (equal (- (nulo)) (nulo))) -;;; Mejor con teorías +;;; Mejor con teorías (in-theory (disable + (+) * (*) - (-) nulo (nulo) identidad (identidad))) (in-theory (disable = (=))) ;;; ----------------------------------------------------------------------- -;;; El inverso debe ser invisible para la primera operación y para sí mismo +;;; El inverso debe ser invisible para la primera operación y para sí mismo ;;; ----------------------------------------------------------------------- ;; (ACL2::set-invisible-fns-table ((+ -) (- -))) @@ -432,7 +432,7 @@ To certify this book, first, create a world with the following packages: (defthm |(p + q) * r = (p * r) + (q * r)| (= (* (+ p q) r) (+ (* p r) (* q r)))) -;;; Teorema de cancelación +;;; Teorema de cancelación ;; (defthm |p + r = q + r <=> p = q| ;; (implies (and (polinomiop p) (polinomiop q)) diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio.lisp b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio.lisp index 37318419401..5bb1353d1db 100644 --- a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio.lisp +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio.lisp @@ -29,11 +29,11 @@ ;;; Inmaculada Medina Bulo ;;; Francisco Palomo Lozano ;;; -;;; Descripción: +;;; Descripción: ;;; -;;; Representación abstracta de los polinomios mediante listas propias +;;; Representación abstracta de los polinomios mediante listas propias ;;; de ACL2 formadas por monomios que contienen coeficientes y -;;; términos abstractos. +;;; términos abstractos. ;;; ------------------------------------------------------------------- #| To certify this book, first, create a world with the following packages: @@ -96,16 +96,16 @@ To certify this book, first, create a world with the following packages: ;;; NOTA: ;;; -;;; Posteriormente definiremos la igualdad semántica entre -;;; polinomios. Entonces, esta definición corresponderá al -;;; representante canónico de la clase de equivalencia formada por los +;;; Posteriormente definiremos la igualdad semántica entre +;;; polinomios. Entonces, esta definición corresponderá al +;;; representante canónico de la clase de equivalencia formada por los ;;; polinomios nulos. (defmacro nulo () nil) ;;; NOTA: ;;; -;;; La siguiente versión se emplea en los casos base de las funciones +;;; La siguiente versión se emplea en los casos base de las funciones ;;; recursivas que trabajan con polinomios. (defmacro nulop (p) diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.lisp b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.lisp index 3639b3dc8b0..cefb7586afb 100644 --- a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.lisp +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.lisp @@ -33,15 +33,15 @@ ;;; Inmaculada Medina Bulo ;;; Francisco Palomo Lozano ;;; -;;; Descripción: +;;; Descripción: ;;; ;;; Desarrollo del producto externo de un monomio por un polinomio y ;;; del producto de polinomios. Las funciones se completan ;;; cuidadosamente, de lo contrario, no es posible establecer las -;;; congruencias, ya que éstas no pueden contener hipótesis. Se +;;; congruencias, ya que éstas no pueden contener hipótesis. Se ;;; demuestra que los polinomios con el producto forman un monoide ;;; conmutativo y que el producto distribuye respecto de la suma, -;;; completándose con esto la demostración de las propiedades del +;;; completándose con esto la demostración de las propiedades del ;;; anillo de polinomios. ;;; ---------------------------------------------------------------- #| @@ -130,12 +130,12 @@ To certify this book, first, create a world with the following packages: (implies (polinomiop (double-rewrite p)) (= (*-monomio (FUMON::identidad) p) p))) -;;; Cancelación +;;; Cancelación ;;; NOTA: ;;; -;;; Primero se demuestra sintácticamente, introduciendo la forma -;;; normal. Luego se extiende a la igualdad semántica. +;;; Primero se demuestra sintácticamente, introduciendo la forma +;;; normal. Luego se extiende a la igualdad semántica. (defthm |m = 0 => fn(m *M p) =e 0| (implies (FUMON::nulop m) @@ -163,7 +163,7 @@ To certify this book, first, create a world with the following packages: ;;; NOTA: ;;; ;;; Esta propiedad permite cambiar un producto externo por otro -;;; más sencillo sobre monomios. +;;; más sencillo sobre monomios. (defthm |m1 *M (m2 *M p) = (m1 * m2) *M p| (implies (and (monomiop (double-rewrite m1)) @@ -246,7 +246,7 @@ To certify this book, first, create a world with the following packages: (defthm |1 * p = p| (= (* (identidad) p) p)) -;;; Cancelación +;;; Cancelación (defthm |0 * p =e 0| (equal (* (nulo) p) (nulo))) @@ -264,8 +264,8 @@ To certify this book, first, create a world with the following packages: ;;; NOTA: ;;; -;;; La inducción apropiada es múltiple. Unas veces se requiere una -;;; hipótesis de inducción sobre uno de los parámetros, otras veces +;;; La inducción apropiada es múltiple. Unas veces se requiere una +;;; hipótesis de inducción sobre uno de los parámetros, otras veces ;;; sobre el otro y otras sobre ambos. Hemos de suministrar el ;;; esquema. diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fusuma.lisp b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fusuma.lisp index 2c551ef4491..dded427a082 100644 --- a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fusuma.lisp +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fusuma.lisp @@ -30,14 +30,14 @@ ;;; Inmaculada Medina Bulo ;;; Francisco Palomo Lozano ;;; -;;; Descripción: +;;; Descripción: ;;; ;;; Desarrollo de la suma de polinomios definida simplemente como la -;;; concatenación de las listas de monomios que los integran. Las -;;; propiedades de la concatenación de listas permiten establecer la +;;; concatenación de las listas de monomios que los integran. Las +;;; propiedades de la concatenación de listas permiten establecer la ;;; base para realizar demostraciones de propiedades sobre los -;;; polinomios más complicadas que incorporan la igualdad -;;; semántica. Se demuestra que los polinomios con la operación de +;;; polinomios más complicadas que incorporan la igualdad +;;; semántica. Se demuestra que los polinomios con la operación de ;;; suma forman un monoide conmutativo. ;;; ---------------------------------------------------------------- #| diff --git a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/futermino.lisp b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/futermino.lisp index 5585ef8075b..6ca38686a17 100644 --- a/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/futermino.lisp +++ b/books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/futermino.lisp @@ -26,29 +26,29 @@ ;; Based on ;;; ------------------------------------------------------------------ -;;; Términos abstractos +;;; Términos abstractos ;;; ;;; Autores: ;;; ;;; Inmaculada Medina Bulo ;;; Francisco Palomo Lozano ;;; -;;; Descripción: +;;; Descripción: ;;; -;;; Un monoide conmutativo de términos con un orden bien fundamentado -;;; cuya representación se abstrae mediante un encapsulado. Las listas -;;; propias de números naturales de ACL2 con la suma elemento a -;;; elemento y el orden lexicográfico sirven como modelo de la teoría -;;; generada. La buena fundamentación del orden se establece por -;;; inmersión en los ordinales ACL2. +;;; Un monoide conmutativo de términos con un orden bien fundamentado +;;; cuya representación se abstrae mediante un encapsulado. Las listas +;;; propias de números naturales de ACL2 con la suma elemento a +;;; elemento y el orden lexicográfico sirven como modelo de la teoría +;;; generada. La buena fundamentación del orden se establece por +;;; inmersión en los ordinales ACL2. ;;; ;;; Notas generales: ;;; -;;; La parte más complicada es la inmersión y la buena fundamentación +;;; La parte más complicada es la inmersión y la buena fundamentación ;;; del orden. Es curioso que los ordinales obtenidos son bastante -;;; pequeños en relación a, por ejemplo, los propuestos por Kaufmann, -;;; Manolios y Moore como solución al ejercicio 6.8 de su libro -;;; «Computer-Aided Reasoning. An Approach». Véase el trabajo +;;; pequeños en relación a, por ejemplo, los propuestos por Kaufmann, +;;; Manolios y Moore como solución al ejercicio 6.8 de su libro +;;; «Computer-Aided Reasoning. An Approach». Véase el trabajo ;;; presentado en Austin. ;;; ------------------------------------------------------------------ #| @@ -100,7 +100,7 @@ To certify this book, first, create a world with the following package: (and (integerp a) (>= a 0))) - ;;; Neutro de la operación + ;;; Neutro de la operación ;; (local ;; (defun uno () @@ -112,7 +112,7 @@ To certify this book, first, create a world with the following package: (defun uno () (hide 0)) - ;;; Operación + ;;; Operación ;; (local ;; (defun * (a b) @@ -132,12 +132,12 @@ To certify this book, first, create a world with the following package: * (a b) (ACL2::+ a b)) - ;;; Igualdad sintáctica entre términos + ;;; Igualdad sintáctica entre términos (defmacro = (a b) `(equal ,a ,b)) - ;;; Inmersión en los ordinales + ;;; Inmersión en los ordinales ;; (local ;; (defun termino->e0-ordinal (a) @@ -155,7 +155,7 @@ To certify this book, first, create a world with the following package: termino->ordinal (a) (ACL2::+ 1 a)) - ;;; Orden lexicográfico estricto + ;;; Orden lexicográfico estricto ;; (local ;; (defun < (a b) @@ -178,7 +178,7 @@ To certify this book, first, create a world with the following package: ;;; Axiomas ;;; ------- - ;;; El reconocedor es una función booleana + ;;; El reconocedor es una función booleana (defthm booleanp-terminop (booleanp (terminop a)) @@ -195,29 +195,29 @@ To certify this book, first, create a world with the following package: (terminop (uno)) :rule-classes :type-prescription) - ;;; Conmutatividad de la operación + ;;; Conmutatividad de la operación (defthm |a * b = b * a| (implies (and (terminop a) (terminop b)) (= (* a b) (* b a)))) - ;;; Asociatividad de la operación + ;;; Asociatividad de la operación (defthm |(a * b) * c = a * (b * c)| (implies (and (terminop a) (terminop b) (terminop c)) (= (* (* a b) c) (* a (* b c))))) - ;;; Neutro de la operación + ;;; Neutro de la operación (defthm |1 * a = a| (implies (terminop a) (= (* (uno) a) a))) ;;; -------------------- - ;;; Buena fundamentación + ;;; Buena fundamentación ;;; -------------------- - ;;; Extensión de la corrección de la inmersión + ;;; Extensión de la corrección de la inmersión ;; (local ;; (defthm extension-correccion @@ -226,7 +226,7 @@ To certify this book, first, create a world with the following package: ;; (o-p (termino->ordinal a))) ;; :otf-flg t)) - ;;; Corrección de la inmersión + ;;; Corrección de la inmersión ;; (local ;; (defthm o-p-termino->ordinal @@ -235,12 +235,12 @@ To certify this book, first, create a world with the following package: ;; :hints (("Goal" ;; :in-theory (disable o-p termino->ordinal))))) - ;;; Buena fundamentación + ;;; Buena fundamentación ;;; NOTA: ;;; - ;;; Este teorema es útil como regla de reescritura para extender el - ;;; orden de términos a polinomios. + ;;; Este teorema es útil como regla de reescritura para extender el + ;;; orden de términos a polinomios. (defthm buena-fundamentacion-< (and (implies (terminop a) @@ -250,11 +250,11 @@ To certify this book, first, create a world with the following package: (o< (termino->ordinal a) (termino->ordinal b)))) :rule-classes (:rewrite :well-founded-relation)) - ;;; La inmersión no produce 0 + ;;; La inmersión no produce 0 ;;; NOTA: ;;; - ;;; Estos teoremas facilitan la extensión del orden de términos a + ;;; Estos teoremas facilitan la extensión del orden de términos a ;;; polinomios. (defthm |~(termino->ordinal(a) = 0)| @@ -272,13 +272,13 @@ To certify this book, first, create a world with the following package: ;;; NOTA: ;;; ;;; En realidad estas propiedades no son independientes de los - ;;; axiomas. Se podrían deducir de la inmersión. + ;;; axiomas. Se podrían deducir de la inmersión. ;;; Irreflexividad (defthm |~(a < a)| (not (< a a))) - ;;; Antisimetría + ;;; Antisimetría (defthm |a < b => ~(b < a)| (implies (< a b) (not (< b a)))) @@ -288,7 +288,7 @@ To certify this book, first, create a world with the following package: (defthm |a < b & b < c => a < c| (implies (and (< a b) (< b c)) (< a c))) - ;;; Tricotomía + ;;; Tricotomía (defthm |a < b or b < a or a = b| (implies (and (terminop a) (terminop b)) @@ -324,7 +324,7 @@ To certify this book, first, create a world with the following package: (implies (terminop a) (= (* a (uno)) a))) -;;; Complemento a la conmutatividad y la asociatividad de la operación +;;; Complemento a la conmutatividad y la asociatividad de la operación (defthm |a * (b * c) = b * (a * c)| (implies (and (terminop a) (terminop b) (terminop c)) diff --git a/books/workshops/2007/cowles-et-al/support/greve/ack.lisp b/books/workshops/2007/cowles-et-al/support/greve/ack.lisp index 740e1d9c9a0..0df109fb9b2 100644 --- a/books/workshops/2007/cowles-et-al/support/greve/ack.lisp +++ b/books/workshops/2007/cowles-et-al/support/greve/ack.lisp @@ -1,6 +1,6 @@ #|-*-Lisp-*-=================================================================|# #| |# -#| Copyright © 2005-7 Rockwell Collins, Inc. All Rights Reserved. |# +#| Copyright © 2005-7 Rockwell Collins, Inc. All Rights Reserved. |# #| |# #|===========================================================================|# (in-package "ACL2") diff --git a/books/workshops/2007/cowles-et-al/support/greve/defminterm.lisp b/books/workshops/2007/cowles-et-al/support/greve/defminterm.lisp index 3c06cd7fa70..8411cf8a217 100644 --- a/books/workshops/2007/cowles-et-al/support/greve/defminterm.lisp +++ b/books/workshops/2007/cowles-et-al/support/greve/defminterm.lisp @@ -1,6 +1,6 @@ #|-*-Lisp-*-=================================================================|# #| |# -#| Copyright © 2005-7 Rockwell Collins, Inc. All Rights Reserved. |# +#| Copyright © 2005-7 Rockwell Collins, Inc. All Rights Reserved. |# #| |# #|===========================================================================|# (in-package "ACL2") diff --git a/books/workshops/2007/cowles-et-al/support/greve/defxch.lisp b/books/workshops/2007/cowles-et-al/support/greve/defxch.lisp index 32bdd0d2950..2a21c47ab08 100644 --- a/books/workshops/2007/cowles-et-al/support/greve/defxch.lisp +++ b/books/workshops/2007/cowles-et-al/support/greve/defxch.lisp @@ -1,6 +1,6 @@ #|-*-Lisp-*-=================================================================|# #| |# -#| Copyright © 2005-7 Rockwell Collins, Inc. All Rights Reserved. |# +#| Copyright © 2005-7 Rockwell Collins, Inc. All Rights Reserved. |# #| |# #|===========================================================================|# (in-package "ACL2") diff --git a/books/workshops/2007/rubio/support/abstract-reductions/confluence.lisp b/books/workshops/2007/rubio/support/abstract-reductions/confluence.lisp index 1b1612e3981..4fa8ab317ca 100644 --- a/books/workshops/2007/rubio/support/abstract-reductions/confluence.lisp +++ b/books/workshops/2007/rubio/support/abstract-reductions/confluence.lisp @@ -216,7 +216,7 @@ (equiv-p z y p2)))))) ;;; 1.2.1. equiv-p is an equivalence relation -;;; ········································· +;;; ......................................... ;;; The properties of equivalence relations (in q) are met by equiv-p: @@ -241,7 +241,7 @@ ;;; 1.2.2. equiv-p contains the reduction relation -;;; ·············································· +;;; .............................................. (defthm equiv-p-contains-reduction (implies (and (q x) @@ -258,7 +258,7 @@ ;;; 1.2.3. equiv-p is the least equivalence relation with the above ;;; properties -;;; ································································ +;;; ................................................................ ;;; Let us assume that we have a relation eqv of equivalence in the set ;;; defined by q, containing the reduction steps, and let us show that @@ -401,9 +401,9 @@ (defun r-equiv (x y) (equal (normal-form x) (normal-form y))) -;;; ············································································ +;;; ............................................................................ ;;; 2.2.1 Completeness -;;; ············································································ +;;; ............................................................................ ;;; We want to show that if (equiv-p x y p) the the normal forms of x ;;; and y are the same. The idea is the following: if we have a proof @@ -471,9 +471,9 @@ (p (make-proof-between-normal-forms x y p))))))) -;;; ············································································ +;;; ............................................................................ ;;; 2.2.1 Soundness -;;; ············································································ +;;; ............................................................................ ;;; We want to prove that if x and y have common normal forms then there ;;; is a proof between x and y. diff --git a/books/workshops/2007/rubio/support/abstract-reductions/convergent.lisp b/books/workshops/2007/rubio/support/abstract-reductions/convergent.lisp index 6229eed08cb..9c3d02faa38 100644 --- a/books/workshops/2007/rubio/support/abstract-reductions/convergent.lisp +++ b/books/workshops/2007/rubio/support/abstract-reductions/convergent.lisp @@ -304,7 +304,7 @@ ;;; See newman.lisp for details. ;;; Well-founded multiset extension of rel -;;; ······································ +;;; ...................................... ;(acl2::defmul-components rel) ;The list of components is: @@ -314,7 +314,7 @@ ;;; Auxiliary functions in the definition of transform-to-valley -;;; ···························································· +;;; ............................................................ (local (defun exists-local-peak (p) @@ -356,7 +356,7 @@ ;;; transform-to-valley terminates -;;; ······························ +;;; .............................. ;;; By functional instantiation of the same result in newman.lisp @@ -392,7 +392,7 @@ ;;; Definition of transform-to-valley -;;; ································· +;;; ................................. (local (defun transform-to-valley (p) (declare (xargs :measure (if (steps-q p) (proof-measure p) nil) @@ -404,7 +404,7 @@ ;;; Properties of transform-to-valley: the Church-Rosser property -;;; ····························································· +;;; ............................................................. ;;; By functional instantiation of the same results in newman.lisp @@ -453,7 +453,7 @@ ;;; w.r.t. it). ;;; Definition of proof-irreducible -;;; ······························· +;;; ............................... ;;; REMARK: Iteratively apply reduction steps until an irreducible ;;; element is found, and collect all those proof steps. @@ -490,7 +490,7 @@ ;;; Main property of proof-irreducible (normalizing property) -;;; ························································· +;;; ......................................................... ;;; REMARK: This is the assumed property of proof-irreducible in ;;; confluence.lisp. @@ -566,7 +566,7 @@ ;;; This is the same function as r-equiv in confluence.lisp -;;; ······················································· +;;; ....................................................... ;;; REMARK: normal-form-aux is analogue NWM::normal-form, but ;;; normal-form is more "eficcient". The same for r-equiv. @@ -592,7 +592,7 @@ ;;; ---------------------------------------------------------------------------- ;;; Completeness -;;; ············ +;;; ............ ;;; By functional instantiation of the same results in confluence.lisp @@ -612,7 +612,7 @@ ;;; Soundness -;;; ········· +;;; ......... ;;; By functional instantiation of the same results in confluence.lisp diff --git a/books/workshops/2007/rubio/support/abstract-reductions/newman.lisp b/books/workshops/2007/rubio/support/abstract-reductions/newman.lisp index 80ca739f653..1bfc374d618 100644 --- a/books/workshops/2007/rubio/support/abstract-reductions/newman.lisp +++ b/books/workshops/2007/rubio/support/abstract-reductions/newman.lisp @@ -165,7 +165,7 @@ ;;; A first theorem: irreflexivity of rel -;; Añadido para la 2.8 +;; Añadido para la 2.8 (defthm o<-irreflexive (not (o< x x))) @@ -399,9 +399,9 @@ ;;; In the sequel, we build a collection of rules to prove these two goals. -;;; ············································································ +;;; ............................................................................ ;;; 3.2.1 Removing initial and final common parts -;;; ············································································ +;;; ............................................................................ (local @@ -474,9 +474,9 @@ -;;; ············································································ +;;; ............................................................................ ;;; 3.2.2 Removing the first element of the local peak -;;; ············································································ +;;; ............................................................................ ;;; First, let's prove that the local peak and the transformed are ;;; proofs with the same endpoints, so their proof measures have the @@ -611,13 +611,13 @@ ;;; (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))). -;;; ············································································ +;;; ............................................................................ ;;; 3.2.3 An explicit reference to the peak-element -;;; ············································································ +;;; ............................................................................ ;;; Definition and properties of peak-element -;;; ········································· +;;; ......................................... ;;; See the definition in abstract-proofs.lisp @@ -675,13 +675,13 @@ ;;; (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))). -;;; ············································································ +;;; ............................................................................ ;;; 3.2.4 The peak element is bigger than any element of ;;; (transform-local-peak (local-peak p)) -;;; ············································································ +;;; ............................................................................ ;;; Definition of being bigger (w.r.t rel) than every element of a list -;;; ··································································· +;;; ................................................................... (local (defun rel-bigger-than-list (x l) @@ -693,7 +693,7 @@ ;;; Conditions assuring that an element m is rel-bigger-than-list than ;;; the elements of the proof-measure of a proof, when the proof is, ;;; respectively, steps-up or steps-down: -;;; ··································································· +;;; ................................................................... ;;; A previous lemma: transitivity of rel is needed here @@ -737,7 +737,7 @@ ;;; (transform-local-peak (local-peak p)) in two proofs: the proof ;;; before the valley (steps-up) and the proof after the valley ;;; (steps-down). The following lemmas are needed for that purpose. -;;; ···································································· +;;; .................................................................... ;;; If p is a proof, so they are the proofs after and before the ;;; valley. @@ -766,7 +766,7 @@ ;;; The transformed proof is a valley -;;; ································· +;;; ................................. (local (defthm local-peak-local-peak-p @@ -791,7 +791,7 @@ ;;; steps-up-proof-measure-w-f-v (and then prove that the peak-element ;;; is bigger than every element of the complexities of the ;;; proof-after-valley and the proof-before-valley, respectively. -;;; ···································································· +;;; .................................................................... @@ -818,7 +818,7 @@ ;;; Some technical lemmas -;;; ····················· +;;; ..................... (local (defthm consp-proof-after-proof-instance @@ -834,7 +834,7 @@ ;;; And finally, the intended lemma -;;; ······························· +;;; ............................... (local (defthm valley-rel-bigger-peak-lemma @@ -847,9 +847,9 @@ (transform-local-peak (local-peak p)))))))) -;;; ············································································ +;;; ............................................................................ ;;; 3.2.5 Using valley-rel-bigger-peak-lemma to simplify the goals -;;; ············································································ +;;; ............................................................................ ;;; The two unresolved goals, as stated at the end of 3.2.3, can be ;;; simplified to t by using the previously proved @@ -860,7 +860,7 @@ ;;; following lemma (stating that the peak-element is not a member of ;;; the proof-meassure of the transformed proof), ;;; the calls to multiset-diff in the goals now disappear. -;;; ··································································· +;;; ................................................................... (local (encapsulate @@ -897,7 +897,7 @@ ;;; in the unresolved goal above, is reduced to a call to ;;; rel-bigger-than-list (and then valley-rel-bigger-peak-lemma will be ;;; applied) -;;; ··································································· +;;; ................................................................... (local @@ -914,18 +914,18 @@ ;;; With this two rules altogether with valley-rel-bigger-peak-lemma our ;;; unresolved goal becomes T, so we have: -;;; ············································································ +;;; ............................................................................ ;;; 3.2.6 The main lemma of this book -;;; ············································································ +;;; ............................................................................ (defthm transform-to-valley-admission (implies (exists-local-peak p) (mul-rel (proof-measure (replace-local-peak p)) (proof-measure p)))) -;;; ············································································ +;;; ............................................................................ ;;; 3.2.7 Some final technical events -;;; ············································································ +;;; ............................................................................ ;;; Needed in the admission proof of transform-to-valley @@ -967,13 +967,13 @@ ;;; 4.1 Some previous events ;;; ---------------------------------------------------------------------------- -;;; ············································································· +;;; ............................................................................. ;;; 4.1.1 Previous rules needed to show that (transform-to-valley p) is eqv. to p -;;; ············································································· +;;; ............................................................................. ;;; We have to see that (replace-local-peak p) is equivalent to p -;;; ····························································· +;;; ............................................................. ;;; An useful rule to deal with concatenation of proofs (local @@ -1037,9 +1037,9 @@ ;;; three pieces of p (before, at and after the peak), using the ;;; previous bridge lemma. -;;; ············································································· +;;; ............................................................................. ;;; 4.1.2 A rule needed to show that (transform-to-valley p) is a valley -;;; ············································································· +;;; ............................................................................. @@ -1050,9 +1050,9 @@ (implies (equiv-p x y p) (equal (steps-valley p) (not (exists-local-peak p)))))) -;;; ············································································· +;;; ............................................................................. ;;; 4.1.3 If equiv-p, then steps-q -;;; ············································································· +;;; ............................................................................. (local (defthm equiv-p-implies-stetps-q @@ -1060,9 +1060,9 @@ (steps-q p)) :rule-classes :forward-chaining)) -;;; ············································································· +;;; ............................................................................. ;;; 4.1.4 Disabling the induction rule for equiv-p -;;; ············································································· +;;; ............................................................................. (local (in-theory (disable equiv-p-induct))) @@ -1079,7 +1079,7 @@ ;;; It returns an equivalent proof -;;; ······························ +;;; .............................. (defthm equiv-p-x-y-transform-to-valley @@ -1090,7 +1090,7 @@ ;;; It returns a valley proof -;;; ························· +;;; ......................... (defthm valley-transform-to-valley diff --git a/books/workshops/2007/rubio/support/multisets/multiset.lisp b/books/workshops/2007/rubio/support/multisets/multiset.lisp index 72fe57765e8..15b5d196524 100644 --- a/books/workshops/2007/rubio/support/multisets/multiset.lisp +++ b/books/workshops/2007/rubio/support/multisets/multiset.lisp @@ -14,7 +14,7 @@ (union-eq *common-lisp-symbols-from-main-lisp-package* '(remove-one multiset-diff ctoa atoc)))) -;;; Con la nueva representación, añadimos ctoa y atoc al paquete MUL +;;; Con la nueva representación, añadimos ctoa y atoc al paquete MUL (certify-book "multiset" 1) @@ -342,7 +342,7 @@ ;;; Conviene tenerlo separado, por que hace falta. PERO NO DENTRO DEL -;;; ENCAPSULADO. Como alternativa, yo la he puesto además como regla de +;;; ENCAPSULADO. Como alternativa, yo la he puesto además como regla de ;;; reescritura. Preguntar a CK si esto afecta a defmul. @@ -350,9 +350,9 @@ ;;; values must be greater than 0. Thus, we define a new measure ;;; function "fn1" equal to "fn" except for integers, where 1 is added. -;;; Nota: hace falta probar que la relación es b.f. "respecto" a +;;; Nota: hace falta probar que la relación es b.f. "respecto" a ;;; e0-ordinalp, porque la prueba esta hecha para los ordinales -;;; antiguos. Así que ahora también introducimos "ctoa" +;;; antiguos. Así que ahora también introducimos "ctoa" (defun add1-if-integer (x) (if (integerp x) (1+ x) x)) @@ -416,10 +416,10 @@ ;;; - The embedding justifying well-foundedness: mp-fn-o-p. ;;; Como originalmente hicimos la prueba con e0-ordinal, habiamos construido una -;;; inmersión en los ordinales, llamada map-fn-e0-ordinal y toda la -;;; prueba la habíamos hecho probando que era una inmersión en los +;;; inmersión en los ordinales, llamada map-fn-e0-ordinal y toda la +;;; prueba la habíamos hecho probando que era una inmersión en los ;;; e0 ordinales. Para aprovechar eso en la 2-8, definimos map-fn-o-p -;;; simplemente aplicando atoc en un último paso. +;;; simplemente aplicando atoc en un último paso. ;;; Measure property @@ -459,9 +459,9 @@ (map-fn-e0-ord (cdr l))) 0)) -;;; Nuevo para la 2.8: má adelante tendremos que definir esto y +;;; Nuevo para la 2.8: má adelante tendremos que definir esto y ;;; demostrar que se trata de una inmersion en los nuevos ordinales de -;;; la versión 2.8: +;;; la versión 2.8: ;; (defun map-fn-o-p (x) ;; (declare (xargs :guard (mp-true-listp x))) ;; (atoc (map-fn-e0-ord x))) @@ -559,9 +559,9 @@ ;;; (e0-ord-< (map-fn-e0-ord n) (map-fn-e0-ord m)) -;;; ············································································ +;;; ............................................................................ ;;; 2.5.1 The measure is an e0-ordinal. -;;; ············································································ +;;; ............................................................................ (local (defthm e0-ordinalp-insert-e0-ord-< @@ -577,9 +577,9 @@ (e0-ordinalp (map-fn-e0-ord m))))) -;;; ············································································ +;;; ............................................................................ ;;; 2.5.2 The measure is an embedding -;;; ············································································ +;;; ............................................................................ @@ -613,7 +613,7 @@ ;;; max-fn1-list (an element in l with maximal (fn1 ..)) and properties. -;;; ······································································ +;;; ...................................................................... (local (defun max-fn1-list (l) @@ -652,7 +652,7 @@ ;;; An "alternative definition" of "map-fn-e0-ord". -;;; ··············································· +;;; ............................................... (local (encapsulate @@ -779,7 +779,7 @@ ;;; Needed for forall-exists-rel-bigger-max-fn1-list -;;; ················································ +;;; ................................................ ;;; We prove forall-exists-rel-bigger-max-fn1-list-lemma, establishing ;;; that if (mul-rel n m), and x is in n and not in m, then (fn1 x) is @@ -875,7 +875,7 @@ ;;; Previous lemmas to map-fn-e0-ord-measure, handling every subgoal -;;; ································································ +;;; ................................................................ ;;; Needed for "Subgoal *1/8": @@ -957,7 +957,7 @@ ;;; At last: map-fn-e0-ord-measure. -;;; ······························· +;;; ............................... (local (encapsulate @@ -1012,9 +1012,9 @@ ;;; Pero con los nuevos ordinales no nos basta con esto, hay que demostrar -;;; una inmersión en los ordinales con la nueva representación. Esta -;;; inmersión la dá map-fn-o-p, definida simplemente -;;; como la aplicación de atoc a map-fn-e0-ord +;;; una inmersión en los ordinales con la nueva representación. Esta +;;; inmersión la dá map-fn-o-p, definida simplemente +;;; como la aplicación de atoc a map-fn-e0-ord (defun map-fn-o-p (x) diff --git a/books/workshops/2007/rubio/support/simplicial-topology/generate-degenerate.lisp b/books/workshops/2007/rubio/support/simplicial-topology/generate-degenerate.lisp index 06a07c8b30f..5b372ab6095 100644 --- a/books/workshops/2007/rubio/support/simplicial-topology/generate-degenerate.lisp +++ b/books/workshops/2007/rubio/support/simplicial-topology/generate-degenerate.lisp @@ -2,7 +2,7 @@ ;;; An elementary example about simplicial topology ;;; Supporting material for the paper "Formalizing simplicial topology ;;; in ACL2" -;;; Authors: J.L. Ruiz-Reina, J. Rubio, M. Andrés, L. Lambán +;;; Authors: J.L. Ruiz-Reina, J. Rubio, M. Andrés, L. Lambán ;;; Created: July, 2007 ;;; Last modified: July 9th, 2007 ;;; ==========================================================