author | wenzelm |
Fri, 23 Nov 2018 16:43:11 +0100 | |
changeset 69334 | 6b49700da068 |
parent 66453 | cc19f7ca2ed6 |
child 69568 | de09a7261120 |
permissions | -rw-r--r-- |
53430 | 1 |
theory Simps_Case_Conv_Examples imports |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
61343
diff
changeset
|
2 |
"HOL-Library.Simps_Case_Conv" |
53430 | 3 |
begin |
4 |
||
61343 | 5 |
section \<open>Tests for the Simps<->Case conversion tools\<close> |
53430 | 6 |
|
7 |
fun foo where |
|
8 |
"foo (x # xs) Nil = 0" | |
|
9 |
"foo (x # xs) (y # ys) = foo [] []" | |
|
10 |
"foo Nil (y # ys) = 1" | |
|
11 |
"foo Nil Nil = 3" |
|
12 |
||
13 |
fun bar where |
|
14 |
"bar x 0 y = 0 + x" | |
|
15 |
"bar x (Suc n) y = n + x" |
|
16 |
||
17 |
definition |
|
18 |
split_rule_test :: "((nat => 'a) + ('b * (('b => 'a) option))) => ('a => nat) => nat" |
|
19 |
where |
|
20 |
"split_rule_test x f = f (case x of Inl af \<Rightarrow> af 1 |
|
21 |
| Inr (b, None) => inv f 0 |
|
22 |
| Inr (b, Some g) => g b)" |
|
23 |
||
24 |
definition test where "test x y = (case x of None => (case y of [] => 1 | _ # _ => 2) | Some x => x)" |
|
25 |
||
26 |
definition nosplit where "nosplit x = x @ (case x of [] \<Rightarrow> [1] | xs \<Rightarrow> xs)" |
|
27 |
||
28 |
||
61343 | 29 |
text \<open>Function with complete, non-overlapping patterns\<close> |
53430 | 30 |
case_of_simps foo_cases1: foo.simps |
60701 | 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) |
|
53430 | 39 |
|
61343 | 40 |
text \<open>Redundant equations are ignored\<close> |
53430 | 41 |
case_of_simps foo_cases2: foo.simps foo.simps |
60701 | 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) |
|
53430 | 50 |
|
61343 | 51 |
text \<open>Variable patterns\<close> |
53430 | 52 |
case_of_simps bar_cases: bar.simps |
53 |
print_theorems |
|
54 |
||
61343 | 55 |
text \<open>Case expression not at top level\<close> |
53430 | 56 |
simps_of_case split_rule_test_simps: split_rule_test_def |
60701 | 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)+ |
|
53430 | 62 |
|
61343 | 63 |
text \<open>Argument occurs both as case parameter and seperately\<close> |
53430 | 64 |
simps_of_case nosplit_simps1: nosplit_def |
60701 | 65 |
lemma |
66 |
"nosplit [] = [] @ [1]" |
|
67 |
"nosplit (x # xs) = (x # xs) @ x # xs" |
|
68 |
by (fact nosplit_simps1)+ |
|
53430 | 69 |
|
61343 | 70 |
text \<open>Nested case expressions\<close> |
53430 | 71 |
simps_of_case test_simps1: test_def |
60701 | 72 |
lemma |
73 |
"test None [] = 1" |
|
74 |
"test None (x # xs) = 2" |
|
75 |
"test (Some x) y = x" |
|
76 |
by (fact test_simps1)+ |
|
53430 | 77 |
|
61343 | 78 |
text \<open>Single-constructor patterns\<close> |
60702
5e03e1bd1be0
case_of_simps: do not split for types with a single constructor
noschinl
parents:
60701
diff
changeset
|
79 |
case_of_simps fst_conv_simps: fst_conv |
5e03e1bd1be0
case_of_simps: do not split for types with a single constructor
noschinl
parents:
60701
diff
changeset
|
80 |
lemma "fst x = (case x of (a,b) \<Rightarrow> a)" |
5e03e1bd1be0
case_of_simps: do not split for types with a single constructor
noschinl
parents:
60701
diff
changeset
|
81 |
by (fact fst_conv_simps) |
5e03e1bd1be0
case_of_simps: do not split for types with a single constructor
noschinl
parents:
60701
diff
changeset
|
82 |
|
61343 | 83 |
text \<open>Partial split of case\<close> |
53430 | 84 |
simps_of_case nosplit_simps2: nosplit_def (splits: list.split) |
60701 | 85 |
lemma |
86 |
"nosplit [] = [] @ [1]" |
|
87 |
"nosplit (x # xs) = (x # xs) @ x # xs" |
|
88 |
by (fact nosplit_simps1)+ |
|
89 |
||
53430 | 90 |
simps_of_case test_simps2: test_def (splits: option.split) |
60701 | 91 |
lemma |
92 |
"test None y = (case y of [] \<Rightarrow> 1 | x # xs \<Rightarrow> 2)" |
|
93 |
"test (Some x) y = x" |
|
94 |
by (fact test_simps2)+ |
|
53430 | 95 |
|
61343 | 96 |
text \<open>Reversal\<close> |
53430 | 97 |
case_of_simps test_def1: test_simps1 |
60701 | 98 |
lemma |
99 |
"test x y = (case (x,y) of |
|
100 |
(None, []) \<Rightarrow> 1 |
|
101 |
| (None, _#_) \<Rightarrow> 2 |
|
102 |
| (Some x, _) \<Rightarrow> x)" |
|
103 |
by (fact test_def1) |
|
53430 | 104 |
|
61343 | 105 |
text \<open>Case expressions on RHS\<close> |
53430 | 106 |
case_of_simps test_def2: test_simps2 |
60701 | 107 |
lemma "test xs y = (case (xs, y) of (None, []) \<Rightarrow> 1 | (None, x # xa) \<Rightarrow> 2 | (Some x, y) \<Rightarrow> x)" |
108 |
by (fact test_def2) |
|
53430 | 109 |
|
61343 | 110 |
text \<open>Partial split of simps\<close> |
53430 | 111 |
case_of_simps foo_cons_def: foo.simps(1,2) |
60701 | 112 |
lemma |
113 |
fixes xs :: "'a list" and ys :: "'b list" |
|
114 |
shows "foo (x # xs) ys = (case (x,xs,ys) of |
|
115 |
(_,_,[]) \<Rightarrow> 0 |
|
116 |
| (_,_,_ # _) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))" |
|
117 |
by (fact foo_cons_def) |
|
53430 | 118 |
|
119 |
end |