author noschinl Thu, 09 Jul 2015 15:45:00 +0200 changeset 60701 61352c31b273 parent 60690 a9e45c9588c3 child 60702 5e03e1bd1be0
tests for Simps_Case_Conv
```--- a/src/HOL/ex/Simps_Case_Conv_Examples.thy	Wed Jul 08 20:19:12 2015 +0200
+++ b/src/HOL/ex/Simps_Case_Conv_Examples.thy	Thu Jul 09 15:45:00 2015 +0200
@@ -28,10 +28,25 @@

text {* Function with complete, non-overlapping patterns *}
case_of_simps foo_cases1: foo.simps
+lemma
+  fixes xs :: "'a list" and ys :: "'b list"
+  shows "foo xs ys = (case (xs, ys) of
+    ( [], []) \<Rightarrow> 3
+    | ([], y # ys) \<Rightarrow> 1
+    | (x # xs, []) \<Rightarrow> 0
+    | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
+  by (fact foo_cases1)

text {* Redundant equations are ignored *}
case_of_simps foo_cases2: foo.simps foo.simps
-print_theorems
+lemma
+  fixes xs :: "'a list" and ys :: "'b list"
+  shows "foo xs ys = (case (xs, ys) of
+    ( [], []) \<Rightarrow> 3
+    | ([], y # ys) \<Rightarrow> 1
+    | (x # xs, []) \<Rightarrow> 0
+    | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
+  by (fact foo_cases2)

text {* Variable patterns *}
case_of_simps bar_cases: bar.simps
@@ -39,33 +54,61 @@

text {* Case expression not at top level *}
simps_of_case split_rule_test_simps: split_rule_test_def
-print_theorems
+lemma
+  "split_rule_test (Inl x) f = f (x 1)"
+  "split_rule_test (Inr (x, None)) f = f (inv f 0)"
+  "split_rule_test (Inr (x, Some y)) f = f (y x)"
+  by (fact split_rule_test_simps)+

text {* Argument occurs both as case parameter and seperately*}
simps_of_case nosplit_simps1: nosplit_def
-print_theorems
+lemma
+  "nosplit [] = [] @ "
+  "nosplit (x # xs) = (x # xs) @ x # xs"
+  by (fact nosplit_simps1)+

text {* Nested case expressions *}
simps_of_case test_simps1: test_def
-print_theorems
+lemma
+  "test None [] = 1"
+  "test None (x # xs) = 2"
+  "test (Some x) y = x"
+  by (fact test_simps1)+

text {* Partial split of case *}
simps_of_case nosplit_simps2: nosplit_def (splits: list.split)
-print_theorems
+lemma
+  "nosplit [] = [] @ "
+  "nosplit (x # xs) = (x # xs) @ x # xs"
+  by (fact nosplit_simps1)+
+
simps_of_case test_simps2: test_def (splits: option.split)
-print_theorems
+lemma
+  "test None y = (case y of [] \<Rightarrow> 1 | x # xs \<Rightarrow> 2)"
+  "test (Some x) y = x"
+  by (fact test_simps2)+

text {* Reversal *}
case_of_simps test_def1: test_simps1
-print_theorems
+lemma
+  "test x y = (case (x,y) of
+    (None, []) \<Rightarrow> 1
+  | (None, _#_) \<Rightarrow> 2
+  | (Some x, _) \<Rightarrow> x)"
+  by (fact test_def1)

text {* Case expressions on RHS *}
case_of_simps test_def2: test_simps2
-print_theorems
+lemma "test xs y = (case (xs, y) of (None, []) \<Rightarrow> 1 | (None, x # xa) \<Rightarrow> 2 | (Some x, y) \<Rightarrow> x)"
+  by (fact test_def2)

text {* Partial split of simps *}
case_of_simps foo_cons_def: foo.simps(1,2)
-print_theorems
-
+lemma
+  fixes xs :: "'a list" and ys :: "'b list"
+  shows "foo (x # xs) ys = (case (x,xs,ys) of
+      (_,_,[]) \<Rightarrow> 0
+    | (_,_,_ # _) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
+  by (fact foo_cons_def)

end```