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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
(in-package "ACL2")
; insert-text.lisp Mihir Mehta
(local (include-book "../file-system-lemmas"))
(defund
insert-text (oldtext start text)
(declare (xargs :guard (and (character-listp oldtext)
(natp start)
(stringp text))))
(let*
((start (mbe :exec start :logic (nfix start)))
(oldtext (mbe :exec oldtext :logic (make-character-list oldtext)))
(end (+ start (length text))))
(append (make-character-list (take start oldtext))
(coerce text 'list)
(nthcdr end oldtext))))
(defthm insert-text-correctness-1
(character-listp (insert-text oldtext start text))
:hints (("goal" :in-theory (enable insert-text))))
(defthm insert-text-correctness-2
(equal (take (+ start (- start)
(len (coerce text 'list)))
(nthcdr start (insert-text oldtext start text)))
(coerce text 'list))
:hints (("goal" :in-theory (enable insert-text)
:use (:theorem (equal (+ start (- start)
(len (coerce text 'list)))
(len (coerce text 'list)))))))
(defthm
insert-text-correctness-3
(<= (+ (nfix start)
(len (coerce text 'list)))
(len (insert-text oldtext start text)))
:hints (("goal" :in-theory (enable insert-text)))
:rule-classes
(:linear
(:linear
:corollary (implies (natp start)
(<= (+ start (len (coerce text 'list)))
(len (insert-text oldtext start text)))))))
(defthmd len-of-insert-text
(implies (stringp text)
(equal (len (insert-text oldtext start text))
(max (+ (nfix start)
(len (coerce text 'list)))
(len oldtext))))
:hints (("goal" :do-not-induct t
:expand (insert-text oldtext start text))))
(defthm insert-text-correctness-4
(implies (stringp text)
(iff (consp (insert-text oldtext start text))
(or (not (zp start))
(> (len (coerce text 'list)) 0)
(consp oldtext))))
:hints (("goal" :do-not-induct t
:use len-of-insert-text
:in-theory (e/d (insert-text len-when-consp)
(len-of-insert-text)))))
(defthm true-listp-of-insert-text
(implies (true-listp oldtext)
(true-listp (insert-text oldtext start text)))
:hints (("goal" :in-theory (enable insert-text)))
:rule-classes :type-prescription)
|
