equal
deleted
inserted
replaced
15 max_threads = 1, timeout = 60 s] |
15 max_threads = 1, timeout = 60 s] |
16 |
16 |
17 subsection {* Curry in a Hurry *} |
17 subsection {* Curry in a Hurry *} |
18 |
18 |
19 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)" |
19 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)" |
20 nitpick [card = 1\<midarrow>12, expect = none] |
20 nitpick [card = 1\<midarrow>12, expect = unknown (*none*)] |
21 by auto |
21 by auto |
22 |
22 |
23 lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)" |
23 lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)" |
24 nitpick [card = 1\<midarrow>12, expect = none] |
24 nitpick [card = 1\<midarrow>12, expect = unknown (*none*)] |
25 by auto |
25 by auto |
26 |
26 |
27 lemma "split (curry f) = f" |
27 lemma "split (curry f) = f" |
28 nitpick [card = 1\<midarrow>12, expect = none] |
28 nitpick [card = 1\<midarrow>12, expect = none] |
29 by auto |
29 by auto |
59 lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y" |
59 lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y" |
60 nitpick [card = 1\<midarrow>12, expect = none] |
60 nitpick [card = 1\<midarrow>12, expect = none] |
61 by auto |
61 by auto |
62 |
62 |
63 lemma "split o curry = (\<lambda>x. x)" |
63 lemma "split o curry = (\<lambda>x. x)" |
64 nitpick [card = 1\<midarrow>12, expect = none] |
64 nitpick [card = 1\<midarrow>12, expect = unknown (*none*)] |
65 apply (rule ext)+ |
65 apply (rule ext)+ |
66 by auto |
66 by auto |
67 |
67 |
68 lemma "curry o split = (\<lambda>x. x)" |
68 lemma "curry o split = (\<lambda>x. x)" |
69 nitpick [card = 1\<midarrow>12, expect = none] |
69 nitpick [card = 1\<midarrow>12, expect = unknown (*none*)] |
70 apply (rule ext)+ |
70 apply (rule ext)+ |
71 by auto |
71 by auto |
72 |
72 |
73 lemma "split (\<lambda>x y. f (x, y)) = f" |
73 lemma "split (\<lambda>x y. f (x, y)) = f" |
74 nitpick [card = 1\<midarrow>12, expect = none] |
74 nitpick [card = 1\<midarrow>12, expect = none] |