equal
deleted
inserted
replaced
73 "test None [] = 1" |
73 "test None [] = 1" |
74 "test None (x # xs) = 2" |
74 "test None (x # xs) = 2" |
75 "test (Some x) y = x" |
75 "test (Some x) y = x" |
76 by (fact test_simps1)+ |
76 by (fact test_simps1)+ |
77 |
77 |
|
78 text {* Single-constructor patterns*} |
|
79 case_of_simps fst_conv_simps: fst_conv |
|
80 lemma "fst x = (case x of (a,b) \<Rightarrow> a)" |
|
81 by (fact fst_conv_simps) |
|
82 |
78 text {* Partial split of case *} |
83 text {* Partial split of case *} |
79 simps_of_case nosplit_simps2: nosplit_def (splits: list.split) |
84 simps_of_case nosplit_simps2: nosplit_def (splits: list.split) |
80 lemma |
85 lemma |
81 "nosplit [] = [] @ [1]" |
86 "nosplit [] = [] @ [1]" |
82 "nosplit (x # xs) = (x # xs) @ x # xs" |
87 "nosplit (x # xs) = (x # xs) @ x # xs" |