← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2003/greve-wilding-vanfleet/support/compatible.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/2003/greve-wilding-vanfleet/support/compatible.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;; This file demonstrates that our notion of separation implies the
 
4
;; "standard" notion presented to us by Vanfleet and derived from
 
5
;; previous work.  These separation notions are: infiltration,
 
6
;; exfiltration, and mediation.
 
7
;;
 
8
;; Matt July 2002
 
9
 
 
10
;; Requires:
 
11
;; (include-book "separation")
 
12
 
 
13
(defthm subsetp-intersection-equal
 
14
  (and
 
15
   (subsetp (intersection-equal a b) a)
 
16
   (subsetp (intersection-equal a b) b)))
 
17
 
 
18
(defthm member-selectlist-means
 
19
  (implies
 
20
   (and 
 
21
    (equal (selectlist l l1) (selectlist l l2))
 
22
    (member x l))
 
23
   (iff (equal (select x l1) (select x l2)) t))
 
24
  :rule-classes :forward-chaining)
 
25
 
 
26
(defthm selectlist-subset
 
27
  (implies
 
28
   (and
 
29
    (equal (selectlist y l1) (selectlist y l2))
 
30
    (subsetp x y))
 
31
   (iff (equal (selectlist x l1) (selectlist x l2)) t)))
 
32
   
 
33
(defthm infiltration
 
34
  (implies
 
35
   (and
 
36
    (equal (current st1) (current st2))
 
37
    (equal (selectlist (segs (current st1)) st1)
 
38
           (selectlist (segs (current st2)) st2))
 
39
    (member x (segs (current st1))))
 
40
   (equal (select x (next st1))
 
41
          (select x (next st2))))
 
42
  :hints (("goal" :use (:instance separation (seg x)))))
 
43
 
 
44
;; Our initial version of exfiltration was quite strong: the segment
 
45
;; in question was unchanged assuming that the current partition had
 
46
;; no dia segments.  This version using these functions would be
 
47
;; something like:
 
48
 
 
49
;(defthm exfiltration 
 
50
;  (implies
 
51
;   (not (intersection-equal (dia y) (segs (current st))))
 
52
;   (equal (select y (next st))
 
53
;         (select y st)))
 
54
;  :hints (("goal" :use (:instance separation (seg y)))))
 
55
 
 
56
;; Unfortunately, this formulation forecloses the possibility of
 
57
;; free-running counters, interrupt handlers, etc. that change the
 
58
;; state of y in a way not dependant on the current partition.  This
 
59
;; kind of behavior ought to be allowed by this formalization, so we
 
60
;; weaken it somewhat.
 
61
 
 
62
; Matt K., after v4-2:
 
63
; Commenting out the following rule, which rewrites a term to itself!
 
64
#||
 
65
(defthm exfiltration 
 
66
  (implies
 
67
   (and
 
68
    (equal (current st1) (current st2))
 
69
    (not (intersection-equal (dia y) (segs (current st1)))))
 
70
   (equal (select y (next st2))
 
71
          (select y (next st2))))
 
72
  :hints (("goal" :use (:instance separation (seg y)))))
 
73
||#
 
74
 
 
75
(defthm mediation 
 
76
  (implies
 
77
   (and
 
78
    (equal (current st1) (current st2))
 
79
    (equal (selectlist (segs (current st1)) st1)
 
80
           (selectlist (segs (current st2)) st2))
 
81
    (equal (select x st1) (select x st2)))
 
82
   (equal (select x (next st1)) (select x (next st2))))
 
83
  :hints (("goal" :use (:instance separation (seg x)))))
 
84
 
 
85
  
 
86
 
 
87