equal
deleted
inserted
replaced
53 with prems' show False by auto |
53 with prems' show False by auto |
54 qed |
54 qed |
55 qed |
55 qed |
56 |
56 |
57 definition (in ordered) |
57 definition (in ordered) |
58 min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
58 min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
59 "min x y = (if x \<^loc><<= y then x else y)" |
59 "min x y = (if x \<^loc><<= y then x else y)" |
60 max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
60 |
|
61 definition (in ordered) |
|
62 max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
61 "max x y = (if x \<^loc><<= y then y else x)" |
63 "max x y = (if x \<^loc><<= y then y else x)" |
62 |
64 |
63 definition |
65 definition |
64 min :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" |
66 min :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" where |
65 "min x y = (if x <<= y then x else y)" |
67 "min x y = (if x <<= y then x else y)" |
66 max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" |
68 |
|
69 definition |
|
70 max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" where |
67 "max x y = (if x <<= y then y else x)" |
71 "max x y = (if x <<= y then y else x)" |
68 |
72 |
69 fun abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" |
73 fun abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" |
70 where |
74 where |
71 "abs_sorted cmp [] = True" |
75 "abs_sorted cmp [] = True" |
364 primrec |
368 primrec |
365 "get_index p n [] = None" |
369 "get_index p n [] = None" |
366 "get_index p n (x#xs) = (if p x then Some n else get_index p (Suc n) xs)" |
370 "get_index p n (x#xs) = (if p x then Some n else get_index p (Suc n) xs)" |
367 |
371 |
368 definition |
372 definition |
369 between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option" |
373 between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option" where |
370 "between x y = get_first (\<lambda>z. x << z & z << y) enum" |
374 "between x y = get_first (\<lambda>z. x << z & z << y) enum" |
371 |
375 |
372 definition |
376 definition |
373 index :: "'a::enum \<Rightarrow> nat" |
377 index :: "'a::enum \<Rightarrow> nat" where |
374 "index x = the (get_index (\<lambda>y. y = x) 0 enum)" |
378 "index x = the (get_index (\<lambda>y. y = x) 0 enum)" |
375 |
379 |
376 definition |
380 definition |
377 add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a" |
381 add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a" where |
378 "add x y = |
382 "add x y = |
379 (let |
383 (let |
380 enm = enum |
384 enm = enum |
381 in enm ! ((index x + index y) mod length enm))" |
385 in enm ! ((index x + index y) mod length enm))" |
382 |
386 |
385 |
389 |
386 primrec |
390 primrec |
387 "sum [] = inf" |
391 "sum [] = inf" |
388 "sum (x#xs) = add x (sum xs)" |
392 "sum (x#xs) = add x (sum xs)" |
389 |
393 |
390 definition |
394 definition "test1 = sum [None, Some True, None, Some False]" |
391 "test1 = sum [None, Some True, None, Some False]" |
395 definition "test2 = (inf :: nat \<times> unit)" |
392 "test2 = (inf :: nat \<times> unit)" |
|
393 |
396 |
394 code_gen "op <<=" |
397 code_gen "op <<=" |
395 code_gen "op <<" |
398 code_gen "op <<" |
396 code_gen inf |
399 code_gen inf |
397 code_gen between |
400 code_gen between |