# HG changeset patch
# User noschinl
# Date 1378457800 -7200
# Node ID d92578436d470d186151fb80376334af24c3d2e3
# Parent  9d9945941eabfa1fb5614670b0c3e78026f7515e
added examples for Simps_Case_Conv

diff -r 9d9945941eab -r d92578436d47 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Sep 06 10:56:40 2013 +0200
+++ b/src/HOL/ROOT	Fri Sep 06 10:56:40 2013 +0200
@@ -559,6 +559,7 @@
     Parallel_Example
     IArray_Examples
     SVC_Oracle
+    Simps_Case_Conv_Examples
   theories [skip_proofs = false]
     Meson_Test
   theories [condition = SVC_HOME]
diff -r 9d9945941eab -r d92578436d47 src/HOL/ex/Simps_Case_Conv_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Simps_Case_Conv_Examples.thy	Fri Sep 06 10:56:40 2013 +0200
@@ -0,0 +1,71 @@
+theory Simps_Case_Conv_Examples imports
+  "~~/src/HOL/Library/Simps_Case_Conv"
+begin
+
+section {* Tests for the Simps<->Case conversion tools *}
+
+fun foo where
+  "foo (x # xs) Nil = 0" |
+  "foo (x # xs) (y # ys) = foo [] []" |
+  "foo Nil (y # ys) = 1" |
+  "foo Nil Nil = 3"
+
+fun bar where
+  "bar x 0 y = 0 + x" |
+  "bar x (Suc n) y = n + x"
+
+definition
+  split_rule_test :: "((nat => 'a) + ('b * (('b => 'a) option))) => ('a => nat) => nat"
+where
+ "split_rule_test x f = f (case x of Inl af \<Rightarrow> af 1
+    | Inr (b, None) => inv f 0
+    | Inr (b, Some g) => g b)"
+
+definition test where "test x y = (case x of None => (case y of [] => 1 | _ # _ => 2) | Some x => x)"
+
+definition nosplit where "nosplit x = x @ (case x of [] \<Rightarrow> [1] | xs \<Rightarrow> xs)"
+
+
+text {* Function with complete, non-overlapping patterns *}
+case_of_simps foo_cases1: foo.simps
+
+text {* Redundant equations are ignored *}
+case_of_simps foo_cases2: foo.simps foo.simps
+print_theorems
+
+text {* Variable patterns *}
+case_of_simps bar_cases: bar.simps
+print_theorems
+
+text {* Case expression not at top level *}
+simps_of_case split_rule_test_simps: split_rule_test_def
+print_theorems
+
+text {* Argument occurs both as case parameter and seperately*}
+simps_of_case nosplit_simps1: nosplit_def
+print_theorems
+
+text {* Nested case expressions *}
+simps_of_case test_simps1: test_def
+print_theorems
+
+text {* Partial split of case *}
+simps_of_case nosplit_simps2: nosplit_def (splits: list.split)
+print_theorems
+simps_of_case test_simps2: test_def (splits: option.split)
+print_theorems
+
+text {* Reversal *}
+case_of_simps test_def1: test_simps1
+print_theorems
+
+text {* Case expressions on RHS *}
+case_of_simps test_def2: test_simps2
+print_theorems
+
+text {* Partial split of simps *}
+case_of_simps foo_cons_def: foo.simps(1,2)
+print_theorems
+
+
+end