65 lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization |
65 lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization |
66 |
66 |
67 lemma "[] @ [] = []" by normalization |
67 lemma "[] @ [] = []" by normalization |
68 lemma "[] @ xs = xs" by normalization |
68 lemma "[] @ xs = xs" by normalization |
69 lemma "[a, b, c] @ xs = a # b # c # xs" by normalization |
69 lemma "[a, b, c] @ xs = a # b # c # xs" by normalization |
70 lemma "[%a::'x. a, %b. b, c] @ xs = (%x. x) # (%x. x) # c # xs" by normalization |
|
71 lemma "[%a::'x. a, %b. b, c] @ [u, v] = [%x. x, %x. x, c, u, v]" by normalization |
|
72 lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization |
70 lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization |
73 normal_form "map (%f. f True) [id, g, Not] = [True, g True, False]" |
71 normal_form "map (%f. f True) [id, g, Not] = [True, g True, False]" |
74 normal_form "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" |
72 normal_form "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" |
75 lemma "rev [a, b, c] = [c, b, a]" by normalization |
73 lemma "rev [a, b, c] = [c, b, a]" by normalization |
76 normal_form "rev (a#b#cs) = rev cs @ [b, a]" |
74 normal_form "rev (a#b#cs) = rev cs @ [b, a]" |