/usr/share/acl2-8.0dfsg/books/system/case-match.lisp is in acl2-books-source 8.0dfsg-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 | ; Copyright (C) 2017, Regents of the University of Texas
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
(verify-termination equal-x-constant) ; and guards
(verify-termination match-tests-and-bindings
(declare (xargs :verify-guards nil)))
; Start proof for (verify-guards match-tests-and-bindings).
(local
(defthm symbol-doublet-listp--mv-nth-1-match-tests-and-bindings
(implies (symbol-doublet-listp bindings)
(symbol-doublet-listp
(mv-nth 1 (match-tests-and-bindings x pat tests bindings))))))
(local
(defthm cdr-assoc-equal-type-for-symbol-doublet-listp
(implies (symbol-doublet-listp x)
(or (consp (cdr (assoc-equal pat x)))
(null (cdr (assoc-equal pat x)))))
:rule-classes :type-prescription))
(local
(defthm assoc-equal-type-for-symbol-doublet-listp
(implies (symbol-doublet-listp x)
(or (consp (assoc-equal pat x))
(null (assoc-equal pat x))))
:rule-classes :type-prescription))
(local
(defthm symbol-doublet-listp-forward-to-symbol-alistp
(implies (symbol-doublet-listp bindings)
(symbol-alistp bindings))
:rule-classes :forward-chaining))
(local
(defthm cdr-preserves-character-listp
(implies (character-listp x)
(character-listp (cdr x)))))
(verify-guards match-tests-and-bindings)
; Lemma for match-clause guard verification:
(local
(defthm true-listp-car-match-tests-and-bindings
(implies (true-listp tests)
(true-listp (car (match-tests-and-bindings x pat tests bindings))))))
(verify-termination match-clause) ; and guards
(verify-termination match-clause-list) ; and guards
|