--- 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