← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp
 
1
;;; subsumption-subst.lisp 
 
2
;;; The subsumption relation between substitutions
 
3
;;; Created 13-10-99. Last revision: 09-01-2001
 
4
;;; =================================================================
 
5
 
 
6
 
 
7
#| To certify this book:
 
8
 
 
9
(in-package "ACL2")
 
10
 
 
11
(certify-book "subsumption-subst")
 
12
 
 
13
|#
 
14
 
 
15
(in-package "ACL2")
 
16
(include-book "subsumption")
 
17
 
 
18
 
 
19
 
 
20
 
 
21
;;; *******************************************************************
 
22
;;; THE SUBSUMPTION RELATION BETWEEN SUBSTITUTIONS. 
 
23
;;; DEFINITION AND PROPERTIES.
 
24
;;; *******************************************************************
 
25
 
 
26
;;; Our goal is to define the subsumption relation between
 
27
;;; substitutions. In the literature, this relation is defined in this
 
28
;;; way: 
 
29
;;;     sigma <= delta iff (exists gamma) gamma�sigma = delta
 
30
;;; where "�" stands for composition.
 
31
 
 
32
;;; Note that equality between substitutions is functional equality (we cannot
 
33
;;; use equal), so we reformulate this property as:
 
34
 
 
35
;;; (*) sigma <= delta iff (exists gamma) 
 
36
;;;                        s.t. for all term 
 
37
;;;                        gamma�sigma(term) = delta(term) 
 
38
 
 
39
 
 
40
;;; Our goal in this book is to define the subsumption relation between
 
41
;;; substitutions as a function, subs-subst. We will define that
 
42
;;; function paying attention only to a restricted list of
 
43
;;; variables. Then will prove (*) in the ACL2 logic. As subsumption
 
44
;;; between terms (due to existential quantification) we have to give
 
45
;;; the substitution gamma in a constructive way, so our definition of
 
46
;;; the subsumption relation will be based on a algorithm that finds
 
47
;;; such substitution gamma, whenever it exists.
 
48
 
 
49
 
 
50
;;; That is to say, we are going to:
 
51
 
 
52
;;; 1) Define the subsumption relation, (subs-subst sigma delta) as a
 
53
;;;    function and the witness matching substitution, called
 
54
;;;    (matching-subst-r sigma delta). Both functions will be based on a
 
55
;;;    matching algorithm called subs-subst-mv.
 
56
 
 
57
;;; 2) Prove that if (subs-subst sigma delta), then 
 
58
;;;    (matching-subst-r sigma delta) applied to sigma(term) is equal to
 
59
;;;    delta(term), with the same matching substitution, for all
 
60
;;;    term. The reverse implication is trivial.
 
61
 
 
62
 
 
63
;;; ============================================================================
 
64
;;; 1. Definition of subs-subst
 
65
;;; ============================================================================
 
66
 
 
67
;;; ----------------------------------------------------------------------------
 
68
;;; 1.1. Some previous definitions and lemmas
 
69
;;; ----------------------------------------------------------------------------
 
70
 
 
71
;;; ===== TRUE-LIST-OF-VARIABLES
 
72
(local
 
73
 (defun true-list-of-variables (l)
 
74
   (if (atom l)
 
75
       (equal l nil)
 
76
     (and (variable-p (car l))
 
77
          (true-list-of-variables (cdr l))))))
 
78
 
 
79
(local
 
80
 (defthm true-list-of-variables-append
 
81
   (implies (and (true-list-of-variables l)
 
82
                 (true-list-of-variables m))
 
83
            (true-list-of-variables (append l m)))))
 
84
 
 
85
(local
 
86
 (defthm true-list-of-variables-variables
 
87
   (true-list-of-variables (variables flg term))))
 
88
 
 
89
 
 
90
;;; ===== TRUE-LIST-OF-EQLABLEP (needed for guard verification)
 
91
(local
 
92
 (defun true-list-of-eqlablep (l)
 
93
   (if (atom l)
 
94
       (equal l nil)
 
95
     (and (eqlablep (car l))
 
96
          (true-list-of-eqlablep (cdr l))))))
 
97
 
 
98
(local
 
99
 (defthm true-list-of-eqlablep-append
 
100
   (implies (and (true-list-of-eqlablep l)
 
101
                 (true-list-of-eqlablep m))
 
102
            (true-list-of-eqlablep (append l m)))))
 
103
 
 
104
(local
 
105
 (defthm true-list-of-eqlablep-variables
 
106
   (implies (term-s-p-aux flg term)
 
107
            (true-list-of-eqlablep (variables flg term)))))
 
108
 
 
109
 
 
110
 
 
111
;;; ===== DOMAIN-VAR
 
112
;;; The variables of the domain (to remove anomalies).
 
113
 
 
114
(defun domain-var (sigma)
 
115
  (if (endp sigma)
 
116
      nil  
 
117
    (if (variable-p (caar sigma))
 
118
        (cons (caar sigma) (domain-var (cdr sigma)))
 
119
      (domain-var (cdr sigma)))))
 
120
 
 
121
 
 
122
 
 
123
;;; Its main properties
 
124
 
 
125
(local
 
126
 (defthm domain-var-main-property
 
127
   (iff (member x (domain-var sigma))
 
128
        (and (member x (domain sigma))
 
129
             (variable-p x)))))
 
130
 
 
131
;;; Needed for guard verification
 
132
(local
 
133
 (defthm true-list-of-variables-domain-var
 
134
   (true-list-of-variables (domain-var sigma))))
 
135
 
 
136
(local
 
137
 (defthm true-list-of-eqlablep-domain-var
 
138
   (implies (substitution-s-p sigma)
 
139
            (true-list-of-eqlablep (domain-var sigma)))))
 
140
 
 
141
 
 
142
(local (in-theory (disable domain-var)))
 
143
 
 
144
 
 
145
 
 
146
 
 
147
;;; ====== CO-DOMAIN-VAR
 
148
;;; The "values" of the variables in domain-var
 
149
 
 
150
 
 
151
(defun co-domain-var (sigma)
 
152
  (if (endp sigma)
 
153
      nil  
 
154
    (if (variable-p (caar sigma))
 
155
        (cons (cdar sigma) (co-domain-var (cdr sigma)))
 
156
      (co-domain-var (cdr sigma)))))
 
157
 
 
158
;;; Needed for guard verification
 
159
(local
 
160
 (defthm term-s-p-aux-co-domain-var
 
161
   (implies (substitution-s-p sigma)
 
162
            (term-s-p-aux nil (co-domain-var sigma)))))
 
163
 
 
164
 
 
165
 
 
166
;;; ====== IMPORTANT-VARIABLES
 
167
;;; For subsumption of substitutions, we only pay atention to these
 
168
;;; variables 
 
169
 
 
170
(defun important-variables (sigma delta)
 
171
  (append (domain-var sigma)
 
172
          (append (domain-var delta)
 
173
                  (variables nil (co-domain-var sigma)))))
 
174
 
 
175
 
 
176
 
 
177
;;; ===== SYSTEM-SUBS-SUBST.
 
178
;;; A technical macro definition
 
179
;;; We will prove below that two substitutions are related by
 
180
;;; subsumption iff the following system of equations is matchable.
 
181
 
 
182
(local
 
183
 (defmacro system-subs-subst (sigma delta)
 
184
   `(first
 
185
     (pair-args
 
186
      (apply-subst nil ,sigma (important-variables ,sigma ,delta))
 
187
      (apply-subst nil ,delta (important-variables ,sigma ,delta))))))
 
188
 
 
189
 
 
190
;;; ----------------------------------------------------------------------------
 
191
;;; 1.2. Definition of subs-subst
 
192
;;; ----------------------------------------------------------------------------
 
193
 
 
194
 
 
195
;;;; NOTATION:
 
196
;;;; ^^^^^^^^^ 
 
197
;;;; In the followin comments, V will be
 
198
;;;; (important-variables sigma delta))
 
199
 
 
200
;;; ===== SUBS-SUBST-MV
 
201
;;; Subsumption between substitutions.
 
202
;;; To decide wether sigma subsumes delta, then we take the list of
 
203
;;; variables of the domain of sigma, the domain of delta and the
 
204
;;; variables of the terms in the co-domain of sigma (i.e, the list V), and
 
205
;;; test if the list of terms sigma(V) subsumes the list of terms
 
206
;;; delta(V). 
 
207
 
 
208
(defun subs-subst-mv (sigma delta)
 
209
  (let ((V (important-variables sigma delta)))
 
210
    (mv-let (system bool)
 
211
            (pair-args (apply-subst nil sigma V)
 
212
                       (apply-subst nil delta V))
 
213
            (declare (ignore bool))
 
214
            (match-mv system))))
 
215
 
 
216
;;; ====== SUBS-SUBST
 
217
;;; The subsumption relation between substitutions:
 
218
 
 
219
 
 
220
(defun subs-subst (sigma delta)
 
221
  (mv-let (match bool)
 
222
          (subs-subst-mv sigma delta)
 
223
          (declare (ignore match))
 
224
          bool))
 
225
 
 
226
 
 
227
;;; ===== MATCHING-SUBST 
 
228
;;; An important auxiliary definition: when
 
229
;;; (subs-subst sigma delta) returns t, this is the substitution that
 
230
;;; applied to the list (apply-subst nil sigma V) returns
 
231
;;; (apply-subst nil delta V)
 
232
 
 
233
(defun matching-subst (sigma delta)
 
234
  (mv-let (match bool)
 
235
          (subs-subst-mv sigma delta)
 
236
          (declare (ignore bool))
 
237
          match))
 
238
 
 
239
;;; ====== MATCHING-SUBST-R
 
240
;;; Restriction of (subs-sust sigma delta) to V.
 
241
 
 
242
(defun matching-subst-r (sigma delta)
 
243
  (restriction (matching-subst sigma delta)
 
244
               (important-variables sigma delta)))
 
245
 
 
246
 
 
247
;;; REMARKS:
 
248
;;;
 
249
;;; 1) The substitution subs-sust-r is the witness substitution to prove
 
250
;;; subsumption between sigma(term) and delta(term), for all terms, as
 
251
;;; we will prove.
 
252
 
 
253
;;; 2) For our particular implementation of subsumption between terms,
 
254
;;; subs-sust and subs-sust-r are exactly the same (from a functional
 
255
;;; pont of view) (when subs-sust is not nil). But we have to define
 
256
;;; subs-sust-r to assure explicitly that outside V, the substitution is
 
257
;;; the identity, because this is not derived from the soundness and
 
258
;;; completeness theorems of and we forbid ourselves to use particular
 
259
;;; properties of a particular matching algorithms.
 
260
 
 
261
;;; 3) Note that subst-sust-r probably has many repetitions in his
 
262
;;; domain, but this is not a problem for us. We will not use
 
263
;;; subs-sust-r to compute, only as a tool to deduce properties. 
 
264
 
 
265
 
 
266
;;; ============================================================================
 
267
;;; 2. Soundness theorem
 
268
;;; ============================================================================
 
269
 
 
270
;;; We want to prove: if (subs-sust sigma delta), then
 
271
;;; the substitutions 
 
272
;;; delta 
 
273
;;; and 
 
274
;;; (composition (subs-subst-r sigma delta) sigma) 
 
275
;;; are functionally equal.
 
276
 
 
277
;;; ----------------------------------------------------------------------------
 
278
;;; 3.1 The main lemma needed for the soundness theorem
 
279
;;; ----------------------------------------------------------------------------
 
280
 
 
281
 
 
282
;;; The main goal here is to prove that:
 
283
;;; For all variable x,
 
284
;;; (val x (composition (subs-subst-r sigma delta) sigma)) = (val x delta)
 
285
;;; if (subs-sust sigma delta)
 
286
;;; WE DISTINGUISH THREE CASES.
 
287
 
 
288
;;; ����������������������������������������������������������������������������
 
289
;;; 3.1.1 Case 1: x is a variable outside V 
 
290
;;; ����������������������������������������������������������������������������
 
291
 
 
292
 
 
293
 
 
294
(local
 
295
 (defthm subs-subst-main-property-variable-x-not-in-V 
 
296
   (let ((V (important-variables sigma delta)))
 
297
     (implies (and
 
298
               (variable-p x)
 
299
               (not (member x V))
 
300
               (subs-subst sigma delta))
 
301
              (equal (instance (val x sigma) (matching-subst-r sigma delta)) 
 
302
                     (val x delta))))
 
303
   :hints (("Goal" :in-theory (enable x-not-in-domain-remains-the-same)))))
 
304
 
 
305
 
 
306
;;; ����������������������������������������������������������������������������
 
307
;;; 3.1.2. Case 2: x is a variable of (domain-var sigma)
 
308
;;; ����������������������������������������������������������������������������
 
309
 
 
310
 
 
311
;;; 3.1.2.1 A lemma for this case 2: 
 
312
;;; subs-subst composed with sigma is equal to delta in V.
 
313
;;; ������������������������������������������������������
 
314
 
 
315
(local
 
316
 (encapsulate
 
317
  ()
 
318
 
 
319
;;; Two  previous lemmas:
 
320
  (local
 
321
   (defthm pair-args-success
 
322
     (second (pair-args (apply-subst nil sigma l)
 
323
                        (apply-subst nil delta l)))))
 
324
  
 
325
  (local
 
326
   (defthm apply-nil-apply-t 
 
327
     (implies (and (equal (apply-subst nil sigma1 l)
 
328
                          (apply-subst nil sigma2 l))
 
329
                   (member x l))
 
330
              (equal (instance x sigma1)
 
331
                     (instance x sigma2)))
 
332
     :rule-classes nil))
 
333
 
 
334
;;; A technical lemma:
 
335
 
 
336
  (local
 
337
   (defthm apply-subst-from-matchers-to-lists-of-terms
 
338
     (implies (and
 
339
               (second (pair-args l m))
 
340
               (matcher sigma (first (pair-args l m))))
 
341
              (equal (equal (apply-subst nil sigma l) m) t))
 
342
     :hints (("Goal" :induct (pair-args l m)))))
 
343
  
 
344
;;; And the intended lemma:
 
345
 
 
346
  (defthm matching-subst-composed-sigma-coincide-with-delta-in-V
 
347
    (let ((V (important-variables sigma delta)))
 
348
      (implies (and
 
349
                (variable-p x)
 
350
                (member x V)
 
351
                (subs-subst sigma delta))
 
352
               (equal (instance (val x sigma) (matching-subst sigma delta))
 
353
                      (val x delta))))
 
354
    :hints (("Goal" :in-theory (disable important-variables)
 
355
             :use (:instance apply-nil-apply-t
 
356
                             (l (important-variables sigma delta))
 
357
                             (sigma1 (composition
 
358
                                      (matching-subst sigma delta) sigma))
 
359
                             (sigma2 delta)))))))
 
360
 
 
361
 
 
362
 
 
363
;;; REMARKS: 
 
364
;;; 1) If we not disable important-variables the proof is longer.
 
365
;;; 2) The condition (variable-p x) is not necessary, but the proof is
 
366
;;; shorter. 
 
367
 
 
368
 
 
369
;;; The above lemma gives the fundamental property of subs-subst and
 
370
;;; matching-subst . We can forget its definition, so we disable their
 
371
;;; definitions: 
 
372
 
 
373
(local (in-theory (disable subs-subst matching-subst)))
 
374
 
 
375
;;; 3.1.2.2 Another lemma for case 2:
 
376
;;; �������������������������������
 
377
 
 
378
(local
 
379
 (defthm variables-co-domain-var 
 
380
  (implies (member x (domain-var sigma))
 
381
           (subsetp (variables t (val x sigma))
 
382
                    (variables nil (co-domain-var sigma))))))
 
383
 
 
384
 
 
385
;;; 3.1.2.3 The main result for Case 2
 
386
;;; ��������������������������������
 
387
 
 
388
(local
 
389
 (defthm
 
390
   subs-subst-main-property-variable-x-in-domain-var-sigma  
 
391
   (implies (and
 
392
             (variable-p x)
 
393
             (member x (domain-var sigma))
 
394
             (subs-subst sigma delta))
 
395
            (equal (apply-subst t (matching-subst-r sigma delta) (val x sigma))
 
396
                   (val x delta)))))
 
397
 
 
398
 
 
399
;;; ����������������������������������������������������������������������������
 
400
;;; 3.1.3. Case 3: x in V but not in (domain-var sigma) 
 
401
;;; ����������������������������������������������������������������������������
 
402
 
 
403
 
 
404
;;; 3.1.3.1 A lemma for Case 3
 
405
;;; In this case, matching and matching-subst-r take the same values. 
 
406
;;; �����������������������������������������������������������������
 
407
 
 
408
(local
 
409
 (defthm
 
410
   subsumption-subst-main-property-variable-in-V-not-in-domain-var-sigma-lemma 
 
411
   (let ((V (important-variables sigma delta)))
 
412
     (implies (and
 
413
               (variable-p x)
 
414
               (not (member x (domain-var sigma)))
 
415
               (member x V)
 
416
               (subs-subst sigma delta))
 
417
              (equal (apply-subst t (matching-subst-r sigma delta) (val x sigma))
 
418
                     (apply-subst t (matching-subst sigma delta)
 
419
                                  (val x sigma)))))
 
420
   :hints (("Goal" :in-theory (enable x-not-in-domain-remains-the-same)))))
 
421
 
 
422
 
 
423
;;; We disable important-variables and matching-subst-r since we do not
 
424
;;; need to "extract" more properties from the definitions.
 
425
 
 
426
(local (in-theory (disable important-variables matching-subst-r)))
 
427
 
 
428
 
 
429
;;; 3.1.3.2 The main result for this case.
 
430
;;; This result is not strictly needed, bu we include in favour of
 
431
;;; clarity. 
 
432
 
 
433
(local
 
434
 (defthm
 
435
   subs-subst-main-property-variable-x-in-V-not-in-domain-var-sigma
 
436
   (let ((V (important-variables sigma delta)))
 
437
     (implies (and
 
438
               (variable-p x)
 
439
               (not (member x (domain-var sigma)))
 
440
               (member x V)
 
441
               (subs-subst sigma delta))
 
442
              (equal (apply-subst t (matching-subst-r sigma delta) (val x sigma))
 
443
                     (val x delta))))))
 
444
 
 
445
 
 
446
 
 
447
;;; ----------------------------------------------------------------------------
 
448
;;; 3.2 Statements of the soundness theorem
 
449
;;; ----------------------------------------------------------------------------
 
450
 
 
451
;;; Joining the three cases together, we prove 
 
452
;;; functional equality between
 
453
;;; (composition (matching-subst-r sigma delta) sigma) and delta.
 
454
 
 
455
 
 
456
(local
 
457
 (defthm
 
458
   equal-composition-matching-subst-with-sigma-to-delta-variable
 
459
   (implies (and (variable-p x)
 
460
                 (subs-subst sigma delta))
 
461
            (equal (val x (composition (matching-subst-r sigma delta) sigma))
 
462
                   (val x delta)))
 
463
   :hints
 
464
   (("Goal"
 
465
     :cases ((not (member x (important-variables sigma delta)))
 
466
             (member x (domain-var sigma)))))))
 
467
 
 
468
 
 
469
 
 
470
 
 
471
;;; DIFFERENT VERSIONS OF THE SOUNDNESS THEOREM
 
472
 
 
473
 
 
474
;;; With terms and list of terms (not only with variables)
 
475
;;; ������������������������������������������������������
 
476
 
 
477
(local
 
478
 (defthm
 
479
   equal-composition-subs-subst-with-sigma-to-delta
 
480
   (implies (subs-subst sigma delta)
 
481
            (equal (apply-subst
 
482
                    flg
 
483
                    (composition (matching-subst-r sigma delta) sigma)
 
484
                    term)
 
485
                   (apply-subst flg delta term)))
 
486
   :hints (("Goal" :in-theory (disable
 
487
                               composition-of-substitutions-apply)))
 
488
   :rule-classes nil))
 
489
 
 
490
;;; We prefer this formulation to be called the soundness theorem of
 
491
;;; subs-subst 
 
492
 
 
493
(defthm
 
494
  subs-subst-soundness
 
495
  (implies (subs-subst sigma delta)
 
496
           (equal
 
497
            (instance term (composition (matching-subst-r sigma delta)
 
498
                                        sigma)) 
 
499
                      
 
500
            (instance term delta)))
 
501
   :rule-classes nil
 
502
   :hints (("Goal" :use
 
503
            (:instance
 
504
             equal-composition-subs-subst-with-sigma-to-delta
 
505
             (flg t)))))
 
506
 
 
507
 
 
508
 
 
509
 
 
510
;;; REMARK: we do not use the two above lemmas as a rewrite rule to avoid
 
511
;;; conflicts with composition-of-substitutions-appply. Instead, the
 
512
;;; following version will be used as a rewrite rule.
 
513
 
 
514
;;; With terms but without using composition
 
515
;;; ����������������������������������������
 
516
 
 
517
(defthm
 
518
  subs-subst-implies-matching-subst-r-appplied-to-sigma-term-is-delta-term
 
519
  (implies (subs-subst sigma delta)
 
520
           (equal (apply-subst flg (matching-subst-r sigma delta)
 
521
                         (apply-subst flg sigma term))
 
522
                  (apply-subst flg delta term)))
 
523
  :hints
 
524
  (("Goal" :use
 
525
    (:instance equal-composition-subs-subst-with-sigma-to-delta))))
 
526
 
 
527
 
 
528
;;; With respect to subsumption between terms
 
529
;;; �����������������������������������������
 
530
           
 
531
 
 
532
;;; Trivial consequence of completeness of subsumption and the previous
 
533
;;; lemma: 
 
534
 
 
535
 
 
536
(defthm
 
537
  subs-subst-main-property
 
538
  (implies (subs-subst sigma delta)
 
539
           (subs (instance term sigma) (instance term delta)))
 
540
  :hints (("Goal" :use
 
541
           ((:instance subs-completeness
 
542
                       (t1 (instance term sigma))
 
543
                       (t2 (instance term delta))
 
544
                       (sigma (matching-subst-r sigma delta)))))))
 
545
 
 
546
 
 
547
 
 
548
 
 
549
;;; ============================================================================
 
550
;;; 3. Completeness theorem
 
551
;;; ============================================================================
 
552
 
 
553
(local (in-theory (enable subs-subst)))
 
554
 
 
555
 
 
556
;;; We want to prove the following:
 
557
;;; If sigma <= delta, then (subs-subst sigma delta). 
 
558
;;; In fact, it will be more useful to prove 
 
559
 
 
560
 
 
561
;;; The theorem is very easy to prove, but the problem is how we
 
562
;;; formulate the hypothesis sigma <= delta.  We will assume the
 
563
;;; existence of two substitutions, called sigma-w and delta-w and the
 
564
;;; only property we will assume about them is that sigma-w <=
 
565
;;; delta-w. That is, exists another substitution gamma-w such that
 
566
;;; delta-w = gamma-w�sigma-w.
 
567
 
 
568
;;; We will use encapsulate for that purpose. Let sigma-w, delta-w and
 
569
;;; gamma-w three susbtitutions such that delta-w is functionally equal
 
570
;;; to (composition gamma-w sigma-w)
 
571
 
 
572
;;; HYPOTHESIS:
 
573
 
 
574
(encapsulate
 
575
 (((sigma-w) => *)
 
576
  ((delta-w) => *)
 
577
  ((gamma-w) => *))
 
578
 
 
579
 (local (defun sigma-w () nil))
 
580
 (local (defun delta-w () nil))
 
581
 (local (defun gamma-w () nil))
 
582
 
 
583
 (defthm sigma-w-delta-w-subsumption-hypothesis
 
584
   (equal (instance term (composition (gamma-w) (sigma-w)))
 
585
          (instance term (delta-w)))
 
586
   :rule-classes nil))
 
587
 
 
588
;;; Now our goal is to prove (subs-subst (sigma-w) (delta-w)).
 
589
 
 
590
;;; The assumption as a rewrite rule:
 
591
(local
 
592
 (defthm sigma-w-delta-w-subsumption-hypothesis-rewrite-rule
 
593
   (equal (instance (instance term (sigma-w)) (gamma-w))
 
594
          (instance term (delta-w)))
 
595
   :hints (("Goal" :use sigma-w-delta-w-subsumption-hypothesis))))
 
596
    
 
597
;;; The main lemma
 
598
(defthm gamma-w-matcher
 
599
  (matcher (gamma-w)
 
600
           (first (pair-args (apply-subst nil (sigma-w) l)
 
601
                             (apply-subst nil (delta-w) l)))))
 
602
 
 
603
;;; And the completeness theorem:
 
604
 
 
605
(defthm subs-subst-completeness
 
606
  (subs-subst (sigma-w) (delta-w))
 
607
  :rule-classes nil
 
608
  :hints (("Goal" :use
 
609
           (:instance match-mv-completeness
 
610
                      (sigma (gamma-w))
 
611
                      (S (system-subs-subst (sigma-w) (delta-w)))))))
 
612
 
 
613
;;; REMARK: Note that this result can be easily used by functional
 
614
;;; instantiation (see for example unification-definition.lisp).
 
615
 
 
616
 
 
617
;;; ============================================================================
 
618
;;; 4. Closure properties of subs-subst
 
619
;;; ============================================================================
 
620
 
 
621
(local (in-theory (enable matching-subst matching-subst-r 
 
622
                   important-variables)))
 
623
 
 
624
;;; ============================================================================
 
625
;;; 4.1 Closure properties for the soundness theorem
 
626
;;; ============================================================================
 
627
 
 
628
 
 
629
;;; We are going to prove that, provided the two substitutions are in a
 
630
;;; given signature, the witness substitution used for the soundness
 
631
;;; proof above, is also in the given signature.
 
632
 
 
633
(encapsulate
 
634
 ()
 
635
 
 
636
 (local
 
637
  (defthm substitution-s-p--apply-subst-nil-term-s-p-aux
 
638
    (implies (and (substitution-s-p sigma)
 
639
                  (true-list-of-eqlablep l))
 
640
             (term-s-p-aux nil (apply-subst nil sigma l)))))
 
641
 
 
642
 (local
 
643
  (defthm pair-args-system-p
 
644
    (implies (and (term-s-p-aux nil l)
 
645
                  (term-s-p-aux nil m))
 
646
             (system-s-p (first (pair-args l m))))))
 
647
 
 
648
 (defthm matching-subst-substitution-s-p
 
649
   (implies (and (substitution-s-p sigma)
 
650
                 (substitution-s-p delta))
 
651
            (substitution-s-p (matching-subst sigma delta))))
 
652
 
 
653
 (local
 
654
  (defthm restriction-substitution-s-p
 
655
    (implies (and (substitution-s-p sigma)
 
656
                  (true-list-of-eqlablep l))
 
657
             (substitution-s-p (restriction sigma l)))))
 
658
 
 
659
 (defthm matching-subst-r-substitution-s-p
 
660
   (implies (and (substitution-s-p sigma)
 
661
                 (substitution-s-p delta))
 
662
            (substitution-s-p (matching-subst-r sigma delta)))))
 
663
 
 
664
 
 
665
 
 
666
 
 
667
 
 
668
;;; ----------------------------------------------------------------------------
 
669
;;; 4.2 Closure property for the completeness theorem 
 
670
;;; ----------------------------------------------------------------------------
 
671
 
 
672
;;; We can prove a slightly different version of the completeness
 
673
;;; theorem: the closure property of the completeness theorem
 
674
;;; 
 
675
 
 
676
;;; We want to prove the following:
 
677
;;; let us suppose that sigma and gamma are two substitutions IN A GIVEN
 
678
;;; SIGNATURE. Suppose that sigma <= delta, i.e., there exists a
 
679
;;; substitution gamma IN THE SAME SIGNATURE such that sigma(term) =
 
680
;;; gamma.sigma(term), FOR ALL TERM IN THE SIGNATURE. 
 
681
;;; Then (subs-subst sigma delta).  
 
682
 
 
683
;;; Let us formulate the hypothesis using encapsulate:
 
684
 
 
685
 
 
686
(encapsulate
 
687
 (((sigma-w-s) => *)
 
688
  ((delta-w-s) => *)
 
689
  ((gamma-w-s) => *))
 
690
 
 
691
 (local (defun sigma-w-s () nil))
 
692
 (local (defun delta-w-s () nil))
 
693
 (local (defun gamma-w-s () nil))
 
694
 
 
695
 (defthm sigma-w-s-substitution-s-p (substitution-s-p (sigma-w-s)))
 
696
 (defthm delta-w-s-substitution-s-p (substitution-s-p (delta-w-s)))
 
697
 (defthm gamma-w-s-substitution-s-p (substitution-s-p (gamma-w-s)))
 
698
 
 
699
 (defthm sigma-w-s-delta-w-s-subsumption-hypothesis
 
700
   (implies (term-s-p term)
 
701
            (equal (instance term (composition (gamma-w-s) (sigma-w-s)))
 
702
                   (instance term (delta-w-s))))
 
703
   :rule-classes nil))
 
704
 
 
705
;;; Now our goal is to prove (subs-subst (sigma-w-s) (delta-w-s)).
 
706
 
 
707
 
 
708
;;; The assumption as a rewrite rule:
 
709
(local
 
710
 (defthm sigma-w-s-delta-w-s-subsumption-hypothesis-rewrite-rule
 
711
   (implies (variable-s-p x)
 
712
            (equal (instance (val x (sigma-w-s)) (gamma-w-s))
 
713
                   (val x (delta-w-s))))
 
714
   :hints (("Goal"
 
715
            :use (:instance
 
716
                  sigma-w-s-delta-w-s-subsumption-hypothesis
 
717
                  (term x))))))
 
718
 
 
719
;;; The main lemma
 
720
(local
 
721
 (defthm gamma-w-s-matcher
 
722
   (implies (true-list-of-eqlablep l) 
 
723
            (matcher (gamma-w-s)
 
724
                     (first (pair-args (apply-subst nil (sigma-w-s) l)
 
725
                                       (apply-subst nil (delta-w-s)
 
726
                                                    l)))))))
 
727
;;; And the closure property for the completeness theorem 
 
728
 
 
729
(defthm subs-subst-completeness-closure
 
730
  (subs-subst (sigma-w-s) (delta-w-s))
 
731
  :rule-classes nil
 
732
  :hints (("Goal" :use
 
733
           (:instance match-mv-completeness
 
734
                      (sigma (gamma-w-s))
 
735
                      (S (system-subs-subst (sigma-w-s) (delta-w-s)))))))
 
736
 
 
737
;;; REMARK: Note that this result can be easily used by functional
 
738
;;; instantiation.  
 
739
 
 
740
;;; We disable the defintions of subs-subst (the subsumption relation)
 
741
;;; and matching-subst-r (the witness substitution) 
 
742
 
 
743
(in-theory (disable subs-subst matching-subst-r))
 
744
 
 
745
 
 
746
 
 
747
 
 
748