1 (*<*) |
|
2 theory Aufgabe5 = Main: |
|
3 (*>*) |
|
4 |
|
5 subsection {* Interval lists *} |
|
6 |
|
7 |
|
8 text {* Sets of natural numbers can be implemented as lists of |
|
9 intervals, where an interval is simply a pair of numbers. For example |
|
10 the set @{term "{2, 3, 5, 7, 8, 9::nat}"} can be represented by the |
|
11 list @{term "[(2, 3), (5, 5), (7::nat,9::nat)]"}. A typical application |
|
12 is the list of free blocks of dynamically allocated memory. *} |
|
13 |
|
14 subsubsection {* Definitions *} |
|
15 |
|
16 text {* We introduce the type *} |
|
17 |
|
18 types intervals = "(nat*nat) list" |
|
19 |
|
20 text {* This type contains all possible lists of pairs of natural |
|
21 numbers, even those that we may not recognize as meaningful |
|
22 representations of sets. Thus you should introduce an \emph{invariant} *} |
|
23 |
|
24 consts inv :: "intervals => bool" |
|
25 |
|
26 text {* that characterizes exactly those interval lists representing |
|
27 sets. (The reason why we call this an invariant will become clear |
|
28 below.) For efficiency reasons intervals should be sorted in |
|
29 ascending order, the lower bound of each interval should be less or |
|
30 equal the upper bound, and the intervals should be chosen as large as |
|
31 possible, i.e.\ no two adjecent intervals should overlap or even touch |
|
32 each other. It turns out to be convenient to define @{term inv} in |
|
33 terms of a more general function *} |
|
34 |
|
35 consts inv2 :: "nat => intervals => bool" |
|
36 |
|
37 text {* such that the additional argument is a lower bound for the |
|
38 intervals in the list. |
|
39 |
|
40 To relate intervals back to sets define an \emph{abstraktion funktion} *} |
|
41 |
|
42 consts set_of :: "intervals => nat set" |
|
43 |
|
44 text {* that yields the set corresponding to an interval list (that |
|
45 satisfies the invariant). |
|
46 |
|
47 Finally, define two primitive recursive functions |
|
48 *} |
|
49 |
|
50 consts add :: "(nat*nat) => intervals => intervals" |
|
51 rem :: "(nat*nat) => intervals => intervals" |
|
52 |
|
53 text {* for inserting and deleting an interval from an interval |
|
54 list. The result should again satisfies the invariant. Hence the name: |
|
55 @{text inv} is invariant under the application of the operations |
|
56 @{term add} and @{term rem} --- if @{text inv} holds for the input, it |
|
57 must also hold for the output. |
|
58 *} |
|
59 |
|
60 subsubsection {* Proving the invariant *} |
|
61 |
|
62 declare Let_def [simp] |
|
63 declare split_split [split] |
|
64 |
|
65 text {* Start off by proving the monotonicity of @{term inv2}: *} |
|
66 |
|
67 lemma inv2_monotone: "inv2 m ins \<Longrightarrow> n\<le>m \<Longrightarrow> inv2 n ins" |
|
68 (*<*)oops(*>*) |
|
69 |
|
70 text {* |
|
71 Now show that @{term add} and @{term rem} preserve the invariant: |
|
72 *} |
|
73 |
|
74 theorem inv_add: "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> inv (add (i,j) ins)" |
|
75 (*<*)oops(*>*) |
|
76 |
|
77 theorem inv_rem: "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> inv (rem (i,j) ins)" |
|
78 (*<*)oops(*>*) |
|
79 |
|
80 text {* Hint: you should first prove a more general statement |
|
81 (involving @{term inv2}). This will probably involve some advanced |
|
82 forms of induction discussed in section~9.3.1 of |
|
83 \cite{isabelle-tutorial}. *} |
|
84 |
|
85 |
|
86 subsubsection {* Proving correctness of the implementation *} |
|
87 |
|
88 text {* Show the correctness of @{term add} and @{term rem} wrt.\ |
|
89 their counterparts @{text"\<union>"} and @{text"-"} on sets: *} |
|
90 |
|
91 theorem set_of_add: |
|
92 "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> set_of (add (i,j) ins) = set_of [(i,j)] \<union> set_of ins" |
|
93 (*<*)oops(*>*) |
|
94 |
|
95 theorem set_of_rem: |
|
96 "\<lbrakk> i \<le> j; inv ins \<rbrakk> \<Longrightarrow> set_of (rem (i,j) ins) = set_of ins - set_of [(i,j)]" |
|
97 (*<*)oops(*>*) |
|
98 |
|
99 text {* Hints: in addition to the hints above, you may also find it |
|
100 useful to prove some relationship between @{term inv2} and @{term |
|
101 set_of} as a lemma. *} |
|
102 |
|
103 subsubsection{* General hints *} |
|
104 |
|
105 text {* |
|
106 \begin{itemize} |
|
107 |
|
108 \item You should be familiar both with simplification and predicate |
|
109 calculus reasoning. Automatic tactics like @{text blast} and @{text |
|
110 force} can simplify the proof. |
|
111 |
|
112 \item |
|
113 Equality of two sets can often be proved via the rule @{text set_ext}: |
|
114 @{thm[display] set_ext[of A B,no_vars]} |
|
115 |
|
116 \item |
|
117 Potentially useful theorems for the simplification of sets include \\ |
|
118 @{text "Un_Diff:"}~@{thm Un_Diff [no_vars]} \\ |
|
119 @{text "Diff_triv:"}~@{thm Diff_triv [no_vars]}. |
|
120 |
|
121 \item |
|
122 Theorems can be instantiated and simplified via @{text of} and |
|
123 @{text "[simplified]"} (see \cite{isabelle-tutorial}). |
|
124 \end{itemize} |
|
125 *}(*<*) |
|
126 end |
|
127 (*>*) |
|