1 (*<*)theory FP1 = Main:(*>*) |
|
2 |
|
3 lemma "if xs = ys |
|
4 then rev xs = rev ys |
|
5 else rev xs \<noteq> rev ys" |
|
6 by auto |
|
7 |
|
8 lemma "case xs of |
|
9 [] \<Rightarrow> tl xs = xs |
|
10 | y#ys \<Rightarrow> tl xs \<noteq> xs" |
|
11 apply(case_tac xs) |
|
12 by auto |
|
13 |
|
14 |
|
15 subsection{*More Types*} |
|
16 |
|
17 |
|
18 subsubsection{*Natural Numbers*} |
|
19 |
|
20 consts sum :: "nat \<Rightarrow> nat" |
|
21 primrec "sum 0 = 0" |
|
22 "sum (Suc n) = Suc n + sum n" |
|
23 |
|
24 lemma "sum n + sum n = n*(Suc n)" |
|
25 apply(induct_tac n) |
|
26 apply(auto) |
|
27 done |
|
28 |
|
29 text{*Some examples of linear arithmetic:*} |
|
30 |
|
31 lemma "\<lbrakk> \<not> m < n; m < n+(1::int) \<rbrakk> \<Longrightarrow> m = n" |
|
32 by(auto) |
|
33 |
|
34 lemma "min i (max j k) = max (min k i) (min i (j::nat))" |
|
35 by(arith) |
|
36 |
|
37 text{*Not proved automatically because it involves multiplication:*} |
|
38 |
|
39 lemma "n*n = n \<Longrightarrow> n=0 \<or> n=(1::int)" |
|
40 (*<*)oops(*>*) |
|
41 |
|
42 |
|
43 subsubsection{*Pairs*} |
|
44 |
|
45 lemma "fst(x,y) = snd(z,x)" |
|
46 by auto |
|
47 |
|
48 |
|
49 |
|
50 subsection{*Definitions*} |
|
51 |
|
52 consts xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
|
53 defs xor_def: "xor x y \<equiv> x \<and> \<not>y \<or> \<not>x \<and> y" |
|
54 |
|
55 constdefs nand :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
|
56 "nand x y \<equiv> \<not>(x \<and> y)" |
|
57 |
|
58 lemma "\<not> xor x x" |
|
59 apply(unfold xor_def) |
|
60 by auto |
|
61 |
|
62 |
|
63 |
|
64 subsection{*Simplification*} |
|
65 |
|
66 |
|
67 subsubsection{*Simplification Rules*} |
|
68 |
|
69 lemma fst_conv[simp]: "fst(x,y) = x" |
|
70 by auto |
|
71 |
|
72 text{*Setting and resetting the @{text simp} attribute:*} |
|
73 |
|
74 declare fst_conv[simp] |
|
75 declare fst_conv[simp del] |
|
76 |
|
77 |
|
78 subsubsection{*The Simplification Method*} |
|
79 |
|
80 lemma "x*(y+1) = y*(x+1::nat)" |
|
81 apply simp |
|
82 (*<*)oops(*>*) |
|
83 |
|
84 |
|
85 subsubsection{*Adding and Deleting Simplification Rules*} |
|
86 |
|
87 lemma "\<forall>x::nat. x*(y+z) = r" |
|
88 apply (simp add: add_mult_distrib2) |
|
89 (*<*)oops(*>*)text_raw{* \isanewline\isanewline *} |
|
90 |
|
91 lemma "rev(rev(xs @ [])) = xs" |
|
92 apply (simp del: rev_rev_ident) |
|
93 (*<*)oops(*>*) |
|
94 |
|
95 subsubsection{*Assumptions*} |
|
96 |
|
97 lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs" |
|
98 by simp |
|
99 |
|
100 lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []" |
|
101 by(simp (no_asm)) |
|
102 |
|
103 subsubsection{*Rewriting with Definitions*} |
|
104 |
|
105 lemma "xor A (\<not>A)" |
|
106 apply(simp only: xor_def) |
|
107 apply simp |
|
108 done |
|
109 |
|
110 |
|
111 subsubsection{*Conditional Equations*} |
|
112 |
|
113 lemma hd_Cons_tl[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs" |
|
114 by(case_tac xs, simp_all) |
|
115 |
|
116 lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs" |
|
117 by simp |
|
118 |
|
119 |
|
120 subsubsection{*Automatic Case Splits*} |
|
121 |
|
122 lemma "\<forall>xs. if xs = [] then A else B" |
|
123 apply simp |
|
124 (*<*)oops(*>*)text_raw{* \isanewline\isanewline *} |
|
125 |
|
126 lemma "case xs @ [] of [] \<Rightarrow> P | y#ys \<Rightarrow> Q ys y" |
|
127 apply simp |
|
128 apply(simp split: list.split) |
|
129 (*<*)oops(*>*) |
|
130 |
|
131 |
|
132 subsubsection{*Arithmetic*} |
|
133 |
|
134 text{*Is simple enough for the default arithmetic:*} |
|
135 lemma "\<lbrakk> \<not> m < n; m < n+(1::nat) \<rbrakk> \<Longrightarrow> m = n" |
|
136 by simp |
|
137 |
|
138 text{*Contains boolean combinations and needs full arithmetic:*} |
|
139 lemma "\<not> m < n \<and> m < n+(1::nat) \<Longrightarrow> m = n" |
|
140 apply simp |
|
141 by(arith) |
|
142 |
|
143 (*<*) |
|
144 subsubsection{*Tracing*} |
|
145 |
|
146 lemma "rev [a] = []" |
|
147 apply(simp) |
|
148 oops |
|
149 (*>*) |
|
150 |
|
151 |
|
152 subsection{*Case Study: Compiling Expressions*} |
|
153 |
|
154 |
|
155 subsubsection{*Expressions*} |
|
156 |
|
157 types 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v" |
|
158 |
|
159 datatype ('a,'v)expr = Cex 'v |
|
160 | Vex 'a |
|
161 | Bex "'v binop" "('a,'v)expr" "('a,'v)expr" |
|
162 |
|
163 consts value :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v" |
|
164 primrec |
|
165 "value (Cex v) env = v" |
|
166 "value (Vex a) env = env a" |
|
167 "value (Bex f e1 e2) env = f (value e1 env) (value e2 env)" |
|
168 |
|
169 |
|
170 subsubsection{*The Stack Machine*} |
|
171 |
|
172 datatype ('a,'v) instr = Const 'v |
|
173 | Load 'a |
|
174 | Apply "'v binop" |
|
175 |
|
176 consts exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list" |
|
177 primrec |
|
178 "exec [] s vs = vs" |
|
179 "exec (i#is) s vs = (case i of |
|
180 Const v \<Rightarrow> exec is s (v#vs) |
|
181 | Load a \<Rightarrow> exec is s ((s a)#vs) |
|
182 | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))" |
|
183 |
|
184 |
|
185 subsubsection{*The Compiler*} |
|
186 |
|
187 consts comp :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list" |
|
188 primrec |
|
189 "comp (Cex v) = [Const v]" |
|
190 "comp (Vex a) = [Load a]" |
|
191 "comp (Bex f e1 e2) = (comp e2) @ (comp e1) @ [Apply f]" |
|
192 |
|
193 theorem "exec (comp e) s [] = [value e s]" |
|
194 (*<*)oops(*>*) |
|
195 |
|
196 |
|
197 |
|
198 subsection{*Advanced Datatypes*} |
|
199 |
|
200 |
|
201 subsubsection{*Mutual Recursion*} |
|
202 |
|
203 datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" |
|
204 | Sum "'a aexp" "'a aexp" |
|
205 | Var 'a |
|
206 | Num nat |
|
207 and 'a bexp = Less "'a aexp" "'a aexp" |
|
208 | And "'a bexp" "'a bexp" |
|
209 | Neg "'a bexp" |
|
210 |
|
211 |
|
212 consts evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" |
|
213 evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool" |
|
214 |
|
215 primrec |
|
216 "evala (IF b a1 a2) env = |
|
217 (if evalb b env then evala a1 env else evala a2 env)" |
|
218 "evala (Sum a1 a2) env = evala a1 env + evala a2 env" |
|
219 "evala (Var v) env = env v" |
|
220 "evala (Num n) env = n" |
|
221 |
|
222 "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)" |
|
223 "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)" |
|
224 "evalb (Neg b) env = (\<not> evalb b env)" |
|
225 |
|
226 consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp" |
|
227 substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp" |
|
228 |
|
229 primrec |
|
230 "substa s (IF b a1 a2) = |
|
231 IF (substb s b) (substa s a1) (substa s a2)" |
|
232 "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)" |
|
233 "substa s (Var v) = s v" |
|
234 "substa s (Num n) = Num n" |
|
235 |
|
236 "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)" |
|
237 "substb s (And b1 b2) = And (substb s b1) (substb s b2)" |
|
238 "substb s (Neg b) = Neg (substb s b)" |
|
239 |
|
240 lemma substitution_lemma: |
|
241 "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and> |
|
242 evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)" |
|
243 apply(induct_tac a and b) |
|
244 by simp_all |
|
245 |
|
246 |
|
247 subsubsection{*Nested Recursion*} |
|
248 |
|
249 datatype tree = C "tree list" |
|
250 |
|
251 text{*Some trees:*} |
|
252 term "C []" |
|
253 term "C [C [C []], C []]" |
|
254 |
|
255 consts |
|
256 mirror :: "tree \<Rightarrow> tree" |
|
257 mirrors:: "tree list \<Rightarrow> tree list" |
|
258 |
|
259 primrec |
|
260 "mirror(C ts) = C(mirrors ts)" |
|
261 |
|
262 "mirrors [] = []" |
|
263 "mirrors (t # ts) = mirrors ts @ [mirror t]" |
|
264 |
|
265 lemma "mirror(mirror t) = t \<and> mirrors(mirrors ts) = ts" |
|
266 apply(induct_tac t and ts) |
|
267 apply simp_all |
|
268 (*<*)oops(*>*) |
|
269 |
|
270 text{* |
|
271 \begin{exercise} |
|
272 Complete the above proof. |
|
273 \end{exercise} |
|
274 *} |
|
275 |
|
276 subsubsection{*Datatypes Involving Functions*} |
|
277 |
|
278 datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree" |
|
279 |
|
280 text{*A big tree:*} |
|
281 term "Br 0 (\<lambda>i. Br i (\<lambda>n. Tip))" |
|
282 |
|
283 consts map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree" |
|
284 primrec |
|
285 "map_bt f Tip = Tip" |
|
286 "map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))" |
|
287 |
|
288 lemma "map_bt (g o f) T = map_bt g (map_bt f T)" |
|
289 apply(induct_tac T, rename_tac[2] F) |
|
290 apply simp_all |
|
291 done |
|
292 |
|
293 text{* This is \emph{not} allowed: |
|
294 \begin{verbatim} |
|
295 datatype lambda = C "lambda => lambda" |
|
296 \end{verbatim} |
|
297 |
|
298 \begin{exercise} |
|
299 Define a datatype of ordinals and the ordinal $\Gamma_0$. |
|
300 \end{exercise} |
|
301 *} |
|
302 (*<*)end(*>*) |
|