# HG changeset patch
# User noschinl
# Date 1436449500 -7200
# Node ID 61352c31b273672ab1ee3d50cf0368d06828747a
# Parent  a9e45c9588c3679fad39383356c6a7d3a872c41b
tests for Simps_Case_Conv

diff -r a9e45c9588c3 -r 61352c31b273 src/HOL/ex/Simps_Case_Conv_Examples.thy
--- 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 [] = [] @ [1]"
+  "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 [] = [] @ [1]"
+  "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