1
#|-*-Lisp-*-=================================================================|#
3
#| coi: Computational Object Inference |#
5
#|===========================================================================|#
1
; Computational Object Inference
2
; Copyright (C) 2005-2014 Kookamara LLC
7
; 11410 Windermere Meadows
8
; Austin, TX 78759, USA
9
; http://www.kookamara.com/
11
; License: (An MIT/X11-style license)
13
; Permission is hereby granted, free of charge, to any person obtaining a
14
; copy of this software and associated documentation files (the "Software"),
15
; to deal in the Software without restriction, including without limitation
16
; the rights to use, copy, modify, merge, publish, distribute, sublicense,
17
; and/or sell copies of the Software, and to permit persons to whom the
18
; Software is furnished to do so, subject to the following conditions:
20
; The above copyright notice and this permission notice shall be included in
21
; all copies or substantial portions of the Software.
23
; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
24
; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
25
; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
26
; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
27
; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
28
; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
29
; DEALINGS IN THE SOFTWARE.
6
31
(in-package "DEFUNG")
8
33
(include-book "coi/generalize/generalize" :dir :system)
22
(defun ,phony-test (,@args)
47
(defun ,phony-test (,@args)
23
48
(declare (ignore ,@args)) nil)
25
50
(local (in-theory (disable (:type-prescription ,phony-test))))
27
52
(defun ,phony-induction (,@args)
28
53
(declare (xargs :measure 0))
29
54
(if (,phony-test ,@args) (,phony-induction ,@args) nil))
31
56
(defthm ,phony-induction-rule t
32
57
:rule-classes ((:induction :pattern (,fn ,@args)
33
58
:scheme (,phony-induction ,@args))))
46
71
(in-theory (disable (:type-prescription goo)))
49
74
(declare (ignore x)) 0)
52
77
(equal (hoo x) (goo (gensym::generalize x)))
54
79
:hints (("Goal" :expand (:free (x) (gensym::generalize x)))))
56
81
(in-theory (disable (:type-prescription hoo) hoo))
58
83
(def::phony-induction hoo (x))
60
85
(defstub arg () nil)
62
87
(acl2::add-generalization-pattern (arg))