|
1 theory FP1 = Main: |
|
2 |
|
3 subsection{*More Constructs*} |
|
4 |
|
5 lemma "if xs = ys |
|
6 then rev xs = rev ys |
|
7 else rev xs \<noteq> rev ys" |
|
8 by auto |
|
9 |
|
10 lemma "case xs of |
|
11 [] \<Rightarrow> tl xs = xs |
|
12 | y#ys \<Rightarrow> tl xs \<noteq> xs" |
|
13 apply(case_tac xs) |
|
14 by auto |
|
15 |
|
16 |
|
17 subsection{*More Types*} |
|
18 |
|
19 |
|
20 subsubsection{*Natural Numbers*} |
|
21 |
|
22 consts sum :: "nat \<Rightarrow> nat" |
|
23 primrec "sum 0 = 0" |
|
24 "sum (Suc n) = Suc n + sum n" |
|
25 |
|
26 lemma "sum n + sum n = n*(Suc n)"; |
|
27 apply(induct_tac n); |
|
28 apply(auto); |
|
29 done |
|
30 |
|
31 lemma "\<lbrakk> \<not> m < n; m < n+1 \<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 lemma "n*n = n \<Longrightarrow> n=0 \<or> n=1" |
|
38 oops |
|
39 |
|
40 |
|
41 subsubsection{*Pairs*} |
|
42 |
|
43 lemma "fst(x,y) = snd(z,x)" |
|
44 by auto |
|
45 |
|
46 |
|
47 |
|
48 subsection{*Definitions*} |
|
49 |
|
50 consts xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
|
51 defs xor_def: "xor x y \<equiv> x \<and> \<not>y \<or> \<not>x \<and> y" |
|
52 |
|
53 constdefs nand :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
|
54 "nand x y \<equiv> \<not>(x \<and> y)" |
|
55 |
|
56 lemma "\<not> xor x x" |
|
57 apply(unfold xor_def) |
|
58 by auto |
|
59 |
|
60 |
|
61 |
|
62 subsection{*Simplification*} |
|
63 |
|
64 |
|
65 subsubsection{*Simplification Rules*} |
|
66 |
|
67 lemma fst_conv[simp]: "fst(x,y) = x" |
|
68 by auto |
|
69 |
|
70 declare fst_conv[simp] |
|
71 declare fst_conv[simp del] |
|
72 |
|
73 |
|
74 subsubsection{*The Simplification Method*} |
|
75 |
|
76 lemma "x*(y+1) = y*(x+1)" |
|
77 apply simp |
|
78 oops |
|
79 |
|
80 |
|
81 subsubsection{*Adding and Deleting Simplification Rules*} |
|
82 |
|
83 lemma "\<forall>x::nat. x*(y+z) = r" |
|
84 apply (simp add: add_mult_distrib2) |
|
85 oops |
|
86 |
|
87 lemma "rev(rev(xs @ [])) = xs" |
|
88 apply (simp del: rev_rev_ident) |
|
89 oops |
|
90 |
|
91 |
|
92 subsubsection{*Assumptions*} |
|
93 |
|
94 lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"; |
|
95 apply simp; |
|
96 done |
|
97 |
|
98 lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []"; |
|
99 apply(simp (no_asm)); |
|
100 done |
|
101 |
|
102 |
|
103 subsubsection{*Rewriting with Definitions*} |
|
104 |
|
105 lemma "xor A (\<not>A)"; |
|
106 apply(simp only:xor_def); |
|
107 by simp |
|
108 |
|
109 |
|
110 subsubsection{*Conditional Equations*} |
|
111 |
|
112 lemma hd_Cons_tl[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs" |
|
113 apply(case_tac xs, simp, simp) |
|
114 done |
|
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 |
|
125 |
|
126 lemma "case xs @ [] of [] \<Rightarrow> A | y#ys \<Rightarrow> B"; |
|
127 apply simp |
|
128 apply(simp split: list.split) |
|
129 oops |
|
130 |
|
131 |
|
132 subsubsection{*Arithmetic*} |
|
133 |
|
134 lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n" |
|
135 by simp |
|
136 |
|
137 lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n"; |
|
138 apply simp |
|
139 by(arith) |
|
140 |
|
141 |
|
142 subsubsection{*Tracing*} |
|
143 |
|
144 ML "set trace_simp" |
|
145 lemma "rev [a] = []" |
|
146 apply(simp) |
|
147 oops |
|
148 ML "reset trace_simp" |
|
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 theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs"; |
|
197 oops |
|
198 |
|
199 lemma exec_app[simp]: |
|
200 "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; |
|
201 apply(induct_tac xs) |
|
202 apply(simp) |
|
203 apply(simp split: instr.split) |
|
204 done |
|
205 |
|
206 theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs"; |
|
207 by(induct_tac e, auto) |
|
208 |
|
209 |
|
210 |
|
211 subsection{*Advanced Datatupes*} |
|
212 |
|
213 |
|
214 subsubsection{*Mutual Recursion*} |
|
215 |
|
216 datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" |
|
217 | Sum "'a aexp" "'a aexp" |
|
218 | Var 'a |
|
219 | Num nat |
|
220 and 'a bexp = Less "'a aexp" "'a aexp" |
|
221 | And "'a bexp" "'a bexp" |
|
222 | Neg "'a bexp"; |
|
223 |
|
224 |
|
225 consts evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" |
|
226 evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"; |
|
227 |
|
228 primrec |
|
229 "evala (IF b a1 a2) env = |
|
230 (if evalb b env then evala a1 env else evala a2 env)" |
|
231 "evala (Sum a1 a2) env = evala a1 env + evala a2 env" |
|
232 "evala (Var v) env = env v" |
|
233 "evala (Num n) env = n" |
|
234 |
|
235 "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)" |
|
236 "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)" |
|
237 "evalb (Neg b) env = (\<not> evalb b env)" |
|
238 |
|
239 consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp" |
|
240 substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp" |
|
241 |
|
242 primrec |
|
243 "substa s (IF b a1 a2) = |
|
244 IF (substb s b) (substa s a1) (substa s a2)" |
|
245 "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)" |
|
246 "substa s (Var v) = s v" |
|
247 "substa s (Num n) = Num n" |
|
248 |
|
249 "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)" |
|
250 "substb s (And b1 b2) = And (substb s b1) (substb s b2)" |
|
251 "substb s (Neg b) = Neg (substb s b)" |
|
252 |
|
253 lemma substitution_lemma: |
|
254 "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and> |
|
255 evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)"; |
|
256 apply(induct_tac a and b); |
|
257 by simp_all |
|
258 |
|
259 |
|
260 subsubsection{*Nested Recursion*} |
|
261 |
|
262 datatype tree = C "tree list" |
|
263 |
|
264 term "C[]" |
|
265 term "C[C[C[]],C[]]" |
|
266 |
|
267 consts |
|
268 mirror :: "tree \<Rightarrow> tree" |
|
269 mirrors:: "tree list \<Rightarrow> tree list"; |
|
270 |
|
271 primrec |
|
272 "mirror(C ts) = C(mirrors ts)" |
|
273 |
|
274 "mirrors [] = []" |
|
275 "mirrors (t # ts) = mirrors ts @ [mirror t]" |
|
276 |
|
277 lemma "mirror(mirror t) = t \<and> mirrors(mirrors ts) = ts" |
|
278 apply(induct_tac t and ts) |
|
279 apply simp_all |
|
280 oops |
|
281 |
|
282 lemma "mirrors ts = rev(map mirror ts)" |
|
283 by(induct ts, simp_all) |
|
284 |
|
285 |
|
286 subsubsection{*Datatypes Involving Functions*} |
|
287 |
|
288 datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree" |
|
289 |
|
290 term "Br 0 (\<lambda>i. Br i (\<lambda>n. Tip))" |
|
291 |
|
292 consts map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree" |
|
293 primrec |
|
294 "map_bt f Tip = Tip" |
|
295 "map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))" |
|
296 |
|
297 lemma "map_bt (g o f) T = map_bt g (map_bt f T)" |
|
298 apply(induct_tac T, rename_tac[2] F) |
|
299 apply simp_all |
|
300 done |
|
301 |
|
302 (* This is NOT allowed: |
|
303 datatype lambda = C "lambda \<Rightarrow> lambda" |
|
304 *) |
|
305 |
|
306 end |