26 definition nosplit where "nosplit x = x @ (case x of [] \<Rightarrow> [1] | xs \<Rightarrow> xs)" |
26 definition nosplit where "nosplit x = x @ (case x of [] \<Rightarrow> [1] | xs \<Rightarrow> xs)" |
27 |
27 |
28 |
28 |
29 text {* Function with complete, non-overlapping patterns *} |
29 text {* Function with complete, non-overlapping patterns *} |
30 case_of_simps foo_cases1: foo.simps |
30 case_of_simps foo_cases1: foo.simps |
|
31 lemma |
|
32 fixes xs :: "'a list" and ys :: "'b list" |
|
33 shows "foo xs ys = (case (xs, ys) of |
|
34 ( [], []) \<Rightarrow> 3 |
|
35 | ([], y # ys) \<Rightarrow> 1 |
|
36 | (x # xs, []) \<Rightarrow> 0 |
|
37 | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))" |
|
38 by (fact foo_cases1) |
31 |
39 |
32 text {* Redundant equations are ignored *} |
40 text {* Redundant equations are ignored *} |
33 case_of_simps foo_cases2: foo.simps foo.simps |
41 case_of_simps foo_cases2: foo.simps foo.simps |
34 print_theorems |
42 lemma |
|
43 fixes xs :: "'a list" and ys :: "'b list" |
|
44 shows "foo xs ys = (case (xs, ys) of |
|
45 ( [], []) \<Rightarrow> 3 |
|
46 | ([], y # ys) \<Rightarrow> 1 |
|
47 | (x # xs, []) \<Rightarrow> 0 |
|
48 | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))" |
|
49 by (fact foo_cases2) |
35 |
50 |
36 text {* Variable patterns *} |
51 text {* Variable patterns *} |
37 case_of_simps bar_cases: bar.simps |
52 case_of_simps bar_cases: bar.simps |
38 print_theorems |
53 print_theorems |
39 |
54 |
40 text {* Case expression not at top level *} |
55 text {* Case expression not at top level *} |
41 simps_of_case split_rule_test_simps: split_rule_test_def |
56 simps_of_case split_rule_test_simps: split_rule_test_def |
42 print_theorems |
57 lemma |
|
58 "split_rule_test (Inl x) f = f (x 1)" |
|
59 "split_rule_test (Inr (x, None)) f = f (inv f 0)" |
|
60 "split_rule_test (Inr (x, Some y)) f = f (y x)" |
|
61 by (fact split_rule_test_simps)+ |
43 |
62 |
44 text {* Argument occurs both as case parameter and seperately*} |
63 text {* Argument occurs both as case parameter and seperately*} |
45 simps_of_case nosplit_simps1: nosplit_def |
64 simps_of_case nosplit_simps1: nosplit_def |
46 print_theorems |
65 lemma |
|
66 "nosplit [] = [] @ [1]" |
|
67 "nosplit (x # xs) = (x # xs) @ x # xs" |
|
68 by (fact nosplit_simps1)+ |
47 |
69 |
48 text {* Nested case expressions *} |
70 text {* Nested case expressions *} |
49 simps_of_case test_simps1: test_def |
71 simps_of_case test_simps1: test_def |
50 print_theorems |
72 lemma |
|
73 "test None [] = 1" |
|
74 "test None (x # xs) = 2" |
|
75 "test (Some x) y = x" |
|
76 by (fact test_simps1)+ |
51 |
77 |
52 text {* Partial split of case *} |
78 text {* Partial split of case *} |
53 simps_of_case nosplit_simps2: nosplit_def (splits: list.split) |
79 simps_of_case nosplit_simps2: nosplit_def (splits: list.split) |
54 print_theorems |
80 lemma |
|
81 "nosplit [] = [] @ [1]" |
|
82 "nosplit (x # xs) = (x # xs) @ x # xs" |
|
83 by (fact nosplit_simps1)+ |
|
84 |
55 simps_of_case test_simps2: test_def (splits: option.split) |
85 simps_of_case test_simps2: test_def (splits: option.split) |
56 print_theorems |
86 lemma |
|
87 "test None y = (case y of [] \<Rightarrow> 1 | x # xs \<Rightarrow> 2)" |
|
88 "test (Some x) y = x" |
|
89 by (fact test_simps2)+ |
57 |
90 |
58 text {* Reversal *} |
91 text {* Reversal *} |
59 case_of_simps test_def1: test_simps1 |
92 case_of_simps test_def1: test_simps1 |
60 print_theorems |
93 lemma |
|
94 "test x y = (case (x,y) of |
|
95 (None, []) \<Rightarrow> 1 |
|
96 | (None, _#_) \<Rightarrow> 2 |
|
97 | (Some x, _) \<Rightarrow> x)" |
|
98 by (fact test_def1) |
61 |
99 |
62 text {* Case expressions on RHS *} |
100 text {* Case expressions on RHS *} |
63 case_of_simps test_def2: test_simps2 |
101 case_of_simps test_def2: test_simps2 |
64 print_theorems |
102 lemma "test xs y = (case (xs, y) of (None, []) \<Rightarrow> 1 | (None, x # xa) \<Rightarrow> 2 | (Some x, y) \<Rightarrow> x)" |
|
103 by (fact test_def2) |
65 |
104 |
66 text {* Partial split of simps *} |
105 text {* Partial split of simps *} |
67 case_of_simps foo_cons_def: foo.simps(1,2) |
106 case_of_simps foo_cons_def: foo.simps(1,2) |
68 print_theorems |
107 lemma |
69 |
108 fixes xs :: "'a list" and ys :: "'b list" |
|
109 shows "foo (x # xs) ys = (case (x,xs,ys) of |
|
110 (_,_,[]) \<Rightarrow> 0 |
|
111 | (_,_,_ # _) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))" |
|
112 by (fact foo_cons_def) |
70 |
113 |
71 end |
114 end |