1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Trie}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 To minimize running time, each node of a trie should contain an array that maps |
|
20 letters to subtries. We have chosen a |
|
21 representation where the subtries are held in an association list, i.e.\ a |
|
22 list of (letter,trie) pairs. Abstracting over the alphabet \isa{{\isaliteral{27}{\isacharprime}}a} and the |
|
23 values \isa{{\isaliteral{27}{\isacharprime}}v} we define a trie as follows:% |
|
24 \end{isamarkuptext}% |
|
25 \isamarkuptrue% |
|
26 \isacommand{datatype}\isamarkupfalse% |
|
27 \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}trie\ {\isaliteral{3D}{\isacharequal}}\ Trie\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}v\ option{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}trie{\isaliteral{29}{\isacharparenright}}list{\isaliteral{22}{\isachardoublequoteclose}}% |
|
28 \begin{isamarkuptext}% |
|
29 \noindent |
|
30 \index{datatypes!and nested recursion}% |
|
31 The first component is the optional value, the second component the |
|
32 association list of subtries. This is an example of nested recursion involving products, |
|
33 which is fine because products are datatypes as well. |
|
34 We define two selector functions:% |
|
35 \end{isamarkuptext}% |
|
36 \isamarkuptrue% |
|
37 \isacommand{primrec}\isamarkupfalse% |
|
38 \ {\isaliteral{22}{\isachardoublequoteopen}}value{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}trie\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}v\ option{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
39 {\isaliteral{22}{\isachardoublequoteopen}}value{\isaliteral{28}{\isacharparenleft}}Trie\ ov\ al{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ov{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
40 \isacommand{primrec}\isamarkupfalse% |
|
41 \ alist\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}trie\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}trie{\isaliteral{29}{\isacharparenright}}list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
42 {\isaliteral{22}{\isachardoublequoteopen}}alist{\isaliteral{28}{\isacharparenleft}}Trie\ ov\ al{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ al{\isaliteral{22}{\isachardoublequoteclose}}% |
|
43 \begin{isamarkuptext}% |
|
44 \noindent |
|
45 Association lists come with a generic lookup function. Its result |
|
46 involves type \isa{option} because a lookup can fail:% |
|
47 \end{isamarkuptext}% |
|
48 \isamarkuptrue% |
|
49 \isacommand{primrec}\isamarkupfalse% |
|
50 \ assoc\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}key\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}val{\isaliteral{29}{\isacharparenright}}list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}key\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}val\ option{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
51 {\isaliteral{22}{\isachardoublequoteopen}}assoc\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ None{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
52 {\isaliteral{22}{\isachardoublequoteopen}}assoc\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{23}{\isacharhash}}ps{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
53 \ \ \ {\isaliteral{28}{\isacharparenleft}}let\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ p\ in\ if\ a{\isaliteral{3D}{\isacharequal}}x\ then\ Some\ b\ else\ assoc\ ps\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
54 \begin{isamarkuptext}% |
|
55 Now we can define the lookup function for tries. It descends into the trie |
|
56 examining the letters of the search string one by one. As |
|
57 recursion on lists is simpler than on tries, let us express this as primitive |
|
58 recursion on the search string argument:% |
|
59 \end{isamarkuptext}% |
|
60 \isamarkuptrue% |
|
61 \isacommand{primrec}\isamarkupfalse% |
|
62 \ lookup\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}trie\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}v\ option{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
63 {\isaliteral{22}{\isachardoublequoteopen}}lookup\ t\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ value\ t{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
64 {\isaliteral{22}{\isachardoublequoteopen}}lookup\ t\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{23}{\isacharhash}}as{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}case\ assoc\ {\isaliteral{28}{\isacharparenleft}}alist\ t{\isaliteral{29}{\isacharparenright}}\ a\ of\isanewline |
|
65 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ None\isanewline |
|
66 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Some\ at\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ lookup\ at\ as{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
67 \begin{isamarkuptext}% |
|
68 As a first simple property we prove that looking up a string in the empty |
|
69 trie \isa{Trie\ None\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} always returns \isa{None}. The proof merely |
|
70 distinguishes the two cases whether the search string is empty or not:% |
|
71 \end{isamarkuptext}% |
|
72 \isamarkuptrue% |
|
73 \isacommand{lemma}\isamarkupfalse% |
|
74 \ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{28}{\isacharparenleft}}Trie\ None\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ as\ {\isaliteral{3D}{\isacharequal}}\ None{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
75 % |
|
76 \isadelimproof |
|
77 % |
|
78 \endisadelimproof |
|
79 % |
|
80 \isatagproof |
|
81 \isacommand{apply}\isamarkupfalse% |
|
82 {\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ as{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}\isanewline |
|
83 \isacommand{done}\isamarkupfalse% |
|
84 % |
|
85 \endisatagproof |
|
86 {\isafoldproof}% |
|
87 % |
|
88 \isadelimproof |
|
89 % |
|
90 \endisadelimproof |
|
91 % |
|
92 \begin{isamarkuptext}% |
|
93 Things begin to get interesting with the definition of an update function |
|
94 that adds a new (string, value) pair to a trie, overwriting the old value |
|
95 associated with that string:% |
|
96 \end{isamarkuptext}% |
|
97 \isamarkuptrue% |
|
98 \isacommand{primrec}\isamarkupfalse% |
|
99 \ update{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}trie\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}v\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}trie{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
100 {\isaliteral{22}{\isachardoublequoteopen}}update\ t\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ v\ {\isaliteral{3D}{\isacharequal}}\ Trie\ {\isaliteral{28}{\isacharparenleft}}Some\ v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}alist\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
101 {\isaliteral{22}{\isachardoublequoteopen}}update\ t\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{23}{\isacharhash}}as{\isaliteral{29}{\isacharparenright}}\ v\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
102 \ \ \ {\isaliteral{28}{\isacharparenleft}}let\ tt\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}case\ assoc\ {\isaliteral{28}{\isacharparenleft}}alist\ t{\isaliteral{29}{\isacharparenright}}\ a\ of\isanewline |
|
103 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ Trie\ None\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ Some\ at\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ at{\isaliteral{29}{\isacharparenright}}\isanewline |
|
104 \ \ \ \ in\ Trie\ {\isaliteral{28}{\isacharparenleft}}value\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}update\ tt\ as\ v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ alist\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
105 \begin{isamarkuptext}% |
|
106 \noindent |
|
107 The base case is obvious. In the recursive case the subtrie |
|
108 \isa{tt} associated with the first letter \isa{a} is extracted, |
|
109 recursively updated, and then placed in front of the association list. |
|
110 The old subtrie associated with \isa{a} is still in the association list |
|
111 but no longer accessible via \isa{assoc}. Clearly, there is room here for |
|
112 optimizations! |
|
113 |
|
114 Before we start on any proofs about \isa{update} we tell the simplifier to |
|
115 expand all \isa{let}s and to split all \isa{case}-constructs over |
|
116 options:% |
|
117 \end{isamarkuptext}% |
|
118 \isamarkuptrue% |
|
119 \isacommand{declare}\isamarkupfalse% |
|
120 \ Let{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}\ option{\isaliteral{2E}{\isachardot}}split{\isaliteral{5B}{\isacharbrackleft}}split{\isaliteral{5D}{\isacharbrackright}}% |
|
121 \begin{isamarkuptext}% |
|
122 \noindent |
|
123 The reason becomes clear when looking (probably after a failed proof |
|
124 attempt) at the body of \isa{update}: it contains both |
|
125 \isa{let} and a case distinction over type \isa{option}. |
|
126 |
|
127 Our main goal is to prove the correct interaction of \isa{update} and |
|
128 \isa{lookup}:% |
|
129 \end{isamarkuptext}% |
|
130 \isamarkuptrue% |
|
131 \isacommand{theorem}\isamarkupfalse% |
|
132 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ v\ bs{\isaliteral{2E}{\isachardot}}\ lookup\ {\isaliteral{28}{\isacharparenleft}}update\ t\ as\ v{\isaliteral{29}{\isacharparenright}}\ bs\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
133 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ as{\isaliteral{3D}{\isacharequal}}bs\ then\ Some\ v\ else\ lookup\ t\ bs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
134 \isadelimproof |
|
135 % |
|
136 \endisadelimproof |
|
137 % |
|
138 \isatagproof |
|
139 % |
|
140 \begin{isamarkuptxt}% |
|
141 \noindent |
|
142 Our plan is to induct on \isa{as}; hence the remaining variables are |
|
143 quantified. From the definitions it is clear that induction on either |
|
144 \isa{as} or \isa{bs} is required. The choice of \isa{as} is |
|
145 guided by the intuition that simplification of \isa{lookup} might be easier |
|
146 if \isa{update} has already been simplified, which can only happen if |
|
147 \isa{as} is instantiated. |
|
148 The start of the proof is conventional:% |
|
149 \end{isamarkuptxt}% |
|
150 \isamarkuptrue% |
|
151 \isacommand{apply}\isamarkupfalse% |
|
152 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ as{\isaliteral{2C}{\isacharcomma}}\ auto{\isaliteral{29}{\isacharparenright}}% |
|
153 \begin{isamarkuptxt}% |
|
154 \noindent |
|
155 Unfortunately, this time we are left with three intimidating looking subgoals: |
|
156 \begin{isabelle} |
|
157 ~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline |
|
158 ~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline |
|
159 ~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs |
|
160 \end{isabelle} |
|
161 Clearly, if we want to make headway we have to instantiate \isa{bs} as |
|
162 well now. It turns out that instead of induction, case distinction |
|
163 suffices:% |
|
164 \end{isamarkuptxt}% |
|
165 \isamarkuptrue% |
|
166 \isacommand{apply}\isamarkupfalse% |
|
167 {\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}\ bs{\isaliteral{2C}{\isacharcomma}}\ auto{\isaliteral{29}{\isacharparenright}}\isanewline |
|
168 \isacommand{done}\isamarkupfalse% |
|
169 % |
|
170 \endisatagproof |
|
171 {\isafoldproof}% |
|
172 % |
|
173 \isadelimproof |
|
174 % |
|
175 \endisadelimproof |
|
176 % |
|
177 \begin{isamarkuptext}% |
|
178 \noindent |
|
179 \index{subgoal numbering}% |
|
180 All methods ending in \isa{tac} take an optional first argument that |
|
181 specifies the range of subgoals they are applied to, where \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}} means |
|
182 all subgoals, i.e.\ \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isaliteral{2D}{\isacharminus}}{\isadigit{3}}{\isaliteral{5D}{\isacharbrackright}}} in our case. Individual subgoal numbers, |
|
183 e.g. \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}} are also allowed. |
|
184 |
|
185 This proof may look surprisingly straightforward. However, note that this |
|
186 comes at a cost: the proof script is unreadable because the intermediate |
|
187 proof states are invisible, and we rely on the (possibly brittle) magic of |
|
188 \isa{auto} (\isa{simp{\isaliteral{5F}{\isacharunderscore}}all} will not do --- try it) to split the subgoals |
|
189 of the induction up in such a way that case distinction on \isa{bs} makes |
|
190 sense and solves the proof. |
|
191 |
|
192 \begin{exercise} |
|
193 Modify \isa{update} (and its type) such that it allows both insertion and |
|
194 deletion of entries with a single function. Prove the corresponding version |
|
195 of the main theorem above. |
|
196 Optimize your function such that it shrinks tries after |
|
197 deletion if possible. |
|
198 \end{exercise} |
|
199 |
|
200 \begin{exercise} |
|
201 Write an improved version of \isa{update} that does not suffer from the |
|
202 space leak (pointed out above) caused by not deleting overwritten entries |
|
203 from the association list. Prove the main theorem for your improved |
|
204 \isa{update}. |
|
205 \end{exercise} |
|
206 |
|
207 \begin{exercise} |
|
208 Conceptually, each node contains a mapping from letters to optional |
|
209 subtries. Above we have implemented this by means of an association |
|
210 list. Replay the development replacing \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}\ trie{\isaliteral{29}{\isacharparenright}}\ list} |
|
211 with \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}\ trie\ option}. |
|
212 \end{exercise}% |
|
213 \end{isamarkuptext}% |
|
214 \isamarkuptrue% |
|
215 % |
|
216 \isadelimproof |
|
217 % |
|
218 \endisadelimproof |
|
219 % |
|
220 \isatagproof |
|
221 % |
|
222 \endisatagproof |
|
223 {\isafoldproof}% |
|
224 % |
|
225 \isadelimproof |
|
226 % |
|
227 \endisadelimproof |
|
228 % |
|
229 \isadelimproof |
|
230 % |
|
231 \endisadelimproof |
|
232 % |
|
233 \isatagproof |
|
234 % |
|
235 \endisatagproof |
|
236 {\isafoldproof}% |
|
237 % |
|
238 \isadelimproof |
|
239 % |
|
240 \endisadelimproof |
|
241 % |
|
242 \isadelimproof |
|
243 % |
|
244 \endisadelimproof |
|
245 % |
|
246 \isatagproof |
|
247 % |
|
248 \endisatagproof |
|
249 {\isafoldproof}% |
|
250 % |
|
251 \isadelimproof |
|
252 % |
|
253 \endisadelimproof |
|
254 % |
|
255 \isadelimproof |
|
256 % |
|
257 \endisadelimproof |
|
258 % |
|
259 \isatagproof |
|
260 % |
|
261 \endisatagproof |
|
262 {\isafoldproof}% |
|
263 % |
|
264 \isadelimproof |
|
265 % |
|
266 \endisadelimproof |
|
267 % |
|
268 \isadelimproof |
|
269 % |
|
270 \endisadelimproof |
|
271 % |
|
272 \isatagproof |
|
273 % |
|
274 \endisatagproof |
|
275 {\isafoldproof}% |
|
276 % |
|
277 \isadelimproof |
|
278 % |
|
279 \endisadelimproof |
|
280 % |
|
281 \isadelimtheory |
|
282 % |
|
283 \endisadelimtheory |
|
284 % |
|
285 \isatagtheory |
|
286 % |
|
287 \endisatagtheory |
|
288 {\isafoldtheory}% |
|
289 % |
|
290 \isadelimtheory |
|
291 % |
|
292 \endisadelimtheory |
|
293 \end{isabellebody}% |
|
294 %%% Local Variables: |
|
295 %%% mode: latex |
|
296 %%% TeX-master: "root" |
|
297 %%% End: |
|