28 |
28 |
29 text \<open>Function with complete, non-overlapping patterns\<close> |
29 text \<open>Function with complete, non-overlapping patterns\<close> |
30 case_of_simps foo_cases1: foo.simps |
30 case_of_simps foo_cases1: foo.simps |
31 lemma |
31 lemma |
32 fixes xs :: "'a list" and ys :: "'b list" |
32 fixes xs :: "'a list" and ys :: "'b list" |
33 shows "foo xs ys = (case (xs, ys) of |
33 shows "foo xs ys = |
34 ( [], []) \<Rightarrow> 3 |
34 (case xs of [] \<Rightarrow> (case ys of [] \<Rightarrow> 3 | _ # _ \<Rightarrow> 1) |
35 | ([], y # ys) \<Rightarrow> 1 |
35 | _ # _ \<Rightarrow> (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list)))" |
36 | (x # xs, []) \<Rightarrow> 0 |
|
37 | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))" |
|
38 by (fact foo_cases1) |
36 by (fact foo_cases1) |
39 |
37 |
40 text \<open>Redundant equations are ignored\<close> |
38 text \<open>Redundant equations are ignored\<close> |
41 case_of_simps foo_cases2: foo.simps foo.simps |
39 case_of_simps foo_cases2: foo.simps foo.simps |
42 lemma |
40 lemma |
43 fixes xs :: "'a list" and ys :: "'b list" |
41 fixes xs :: "'a list" and ys :: "'b list" |
44 shows "foo xs ys = (case (xs, ys) of |
42 shows "foo xs ys = |
45 ( [], []) \<Rightarrow> 3 |
43 (case xs of [] \<Rightarrow> (case ys of [] \<Rightarrow> 3 | _ # _ \<Rightarrow> 1) |
46 | ([], y # ys) \<Rightarrow> 1 |
44 | _ # _ \<Rightarrow> (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list)))" |
47 | (x # xs, []) \<Rightarrow> 0 |
|
48 | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))" |
|
49 by (fact foo_cases2) |
45 by (fact foo_cases2) |
50 |
46 |
51 text \<open>Variable patterns\<close> |
47 text \<open>Variable patterns\<close> |
52 case_of_simps bar_cases: bar.simps |
48 case_of_simps bar_cases: bar.simps |
53 print_theorems |
49 lemma "bar x n y = (case n of 0 \<Rightarrow> 0 + x | Suc n' \<Rightarrow> n' + x)" by(fact bar_cases) |
54 |
50 |
55 text \<open>Case expression not at top level\<close> |
51 text \<open>Case expression not at top level\<close> |
56 simps_of_case split_rule_test_simps: split_rule_test_def |
52 simps_of_case split_rule_test_simps: split_rule_test_def |
57 lemma |
53 lemma |
58 "split_rule_test (Inl x) f = f (x 1)" |
54 "split_rule_test (Inl x) f = f (x 1)" |
94 by (fact test_simps2)+ |
90 by (fact test_simps2)+ |
95 |
91 |
96 text \<open>Reversal\<close> |
92 text \<open>Reversal\<close> |
97 case_of_simps test_def1: test_simps1 |
93 case_of_simps test_def1: test_simps1 |
98 lemma |
94 lemma |
99 "test x y = (case (x,y) of |
95 "test x y = |
100 (None, []) \<Rightarrow> 1 |
96 (case x of None \<Rightarrow> (case y of [] \<Rightarrow> 1 | _ # _ \<Rightarrow> 2) |
101 | (None, _#_) \<Rightarrow> 2 |
97 | Some x' \<Rightarrow> x')" |
102 | (Some x, _) \<Rightarrow> x)" |
|
103 by (fact test_def1) |
98 by (fact test_def1) |
104 |
99 |
105 text \<open>Case expressions on RHS\<close> |
100 text \<open>Case expressions on RHS\<close> |
106 case_of_simps test_def2: test_simps2 |
101 case_of_simps test_def2: test_simps2 |
107 lemma "test xs y = (case (xs, y) of (None, []) \<Rightarrow> 1 | (None, x # xa) \<Rightarrow> 2 | (Some x, y) \<Rightarrow> x)" |
102 lemma "test x y = |
|
103 (case x of None \<Rightarrow> (case y of [] \<Rightarrow> 1 | _ # _ \<Rightarrow> 2) |
|
104 | Some x' \<Rightarrow> x')" |
108 by (fact test_def2) |
105 by (fact test_def2) |
109 |
106 |
110 text \<open>Partial split of simps\<close> |
107 text \<open>Partial split of simps\<close> |
111 case_of_simps foo_cons_def: foo.simps(1,2) |
108 case_of_simps foo_cons_def: foo.simps(1,2) |
112 lemma |
109 lemma |
113 fixes xs :: "'a list" and ys :: "'b list" |
110 fixes xs :: "'a list" and ys :: "'b list" |
114 shows "foo (x # xs) ys = (case (x,xs,ys) of |
111 shows "foo (x # xs) ys = (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))" |
115 (_,_,[]) \<Rightarrow> 0 |
|
116 | (_,_,_ # _) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))" |
|
117 by (fact foo_cons_def) |
112 by (fact foo_cons_def) |
118 |
113 |
119 end |
114 end |