1.1 --- a/src/HOL/ROOT	Fri Sep 06 10:56:40 2013 +0200
     1.2 +++ b/src/HOL/ROOT	Fri Sep 06 10:56:40 2013 +0200
     1.3 @@ -559,6 +559,7 @@
     1.4      Parallel_Example
     1.5      IArray_Examples
     1.6      SVC_Oracle
     1.7 +    Simps_Case_Conv_Examples
     1.8    theories [skip_proofs = false]
     1.9      Meson_Test
    1.10    theories [condition = SVC_HOME]

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Simps_Case_Conv_Examples.thy	Fri Sep 06 10:56:40 2013 +0200
     2.3 @@ -0,0 +1,71 @@
     2.4 +theory Simps_Case_Conv_Examples imports
     2.5 +  "~~/src/HOL/Library/Simps_Case_Conv"
     2.6 +begin
     2.7 +
     2.8 +section {* Tests for the Simps<->Case conversion tools *}
     2.9 +
    2.10 +fun foo where
    2.11 +  "foo (x # xs) Nil = 0" |
    2.12 +  "foo (x # xs) (y # ys) = foo [] []" |
    2.13 +  "foo Nil (y # ys) = 1" |
    2.14 +  "foo Nil Nil = 3"
    2.15 +
    2.16 +fun bar where
    2.17 +  "bar x 0 y = 0 + x" |
    2.18 +  "bar x (Suc n) y = n + x"
    2.19 +
    2.20 +definition
    2.21 +  split_rule_test :: "((nat => 'a) + ('b * (('b => 'a) option))) => ('a => nat) => nat"
    2.22 +where
    2.23 + "split_rule_test x f = f (case x of Inl af \<Rightarrow> af 1
    2.24 +    | Inr (b, None) => inv f 0
    2.25 +    | Inr (b, Some g) => g b)"
    2.26 +
    2.27 +definition test where "test x y = (case x of None => (case y of [] => 1 | _ # _ => 2) | Some x => x)"
    2.28 +
    2.29 +definition nosplit where "nosplit x = x @ (case x of [] \<Rightarrow> [1] | xs \<Rightarrow> xs)"
    2.30 +
    2.31 +
    2.32 +text {* Function with complete, non-overlapping patterns *}
    2.33 +case_of_simps foo_cases1: foo.simps
    2.34 +
    2.35 +text {* Redundant equations are ignored *}
    2.36 +case_of_simps foo_cases2: foo.simps foo.simps
    2.37 +print_theorems
    2.38 +
    2.39 +text {* Variable patterns *}
    2.40 +case_of_simps bar_cases: bar.simps
    2.41 +print_theorems
    2.42 +
    2.43 +text {* Case expression not at top level *}
    2.44 +simps_of_case split_rule_test_simps: split_rule_test_def
    2.45 +print_theorems
    2.46 +
    2.47 +text {* Argument occurs both as case parameter and seperately*}
    2.48 +simps_of_case nosplit_simps1: nosplit_def
    2.49 +print_theorems
    2.50 +
    2.51 +text {* Nested case expressions *}
    2.52 +simps_of_case test_simps1: test_def
    2.53 +print_theorems
    2.54 +
    2.55 +text {* Partial split of case *}
    2.56 +simps_of_case nosplit_simps2: nosplit_def (splits: list.split)
    2.57 +print_theorems
    2.58 +simps_of_case test_simps2: test_def (splits: option.split)
    2.59 +print_theorems
    2.60 +
    2.61 +text {* Reversal *}
    2.62 +case_of_simps test_def1: test_simps1
    2.63 +print_theorems
    2.64 +
    2.65 +text {* Case expressions on RHS *}
    2.66 +case_of_simps test_def2: test_simps2
    2.67 +print_theorems
    2.68 +
    2.69 +text {* Partial split of simps *}
    2.70 +case_of_simps foo_cons_def: foo.simps(1,2)
    2.71 +print_theorems
    2.72 +
    2.73 +
    2.74 +end