src/HOL/ex/Simps_Case_Conv_Examples.thy
 author haftmann Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) changeset 58646 cd63a4b12a33 parent 53430 d92578436d47 child 60701 61352c31b273 permissions -rw-r--r--
specialized specification: avoid trivial instances
 noschinl@53430 1 theory Simps_Case_Conv_Examples imports noschinl@53430 2 "~~/src/HOL/Library/Simps_Case_Conv" noschinl@53430 3 begin noschinl@53430 4 noschinl@53430 5 section {* Tests for the Simps<->Case conversion tools *} noschinl@53430 6 noschinl@53430 7 fun foo where noschinl@53430 8 "foo (x # xs) Nil = 0" | noschinl@53430 9 "foo (x # xs) (y # ys) = foo [] []" | noschinl@53430 10 "foo Nil (y # ys) = 1" | noschinl@53430 11 "foo Nil Nil = 3" noschinl@53430 12 noschinl@53430 13 fun bar where noschinl@53430 14 "bar x 0 y = 0 + x" | noschinl@53430 15 "bar x (Suc n) y = n + x" noschinl@53430 16 noschinl@53430 17 definition noschinl@53430 18 split_rule_test :: "((nat => 'a) + ('b * (('b => 'a) option))) => ('a => nat) => nat" noschinl@53430 19 where noschinl@53430 20 "split_rule_test x f = f (case x of Inl af \ af 1 noschinl@53430 21 | Inr (b, None) => inv f 0 noschinl@53430 22 | Inr (b, Some g) => g b)" noschinl@53430 23 noschinl@53430 24 definition test where "test x y = (case x of None => (case y of [] => 1 | _ # _ => 2) | Some x => x)" noschinl@53430 25 noschinl@53430 26 definition nosplit where "nosplit x = x @ (case x of [] \ [1] | xs \ xs)" noschinl@53430 27 noschinl@53430 28 noschinl@53430 29 text {* Function with complete, non-overlapping patterns *} noschinl@53430 30 case_of_simps foo_cases1: foo.simps noschinl@53430 31 noschinl@53430 32 text {* Redundant equations are ignored *} noschinl@53430 33 case_of_simps foo_cases2: foo.simps foo.simps noschinl@53430 34 print_theorems noschinl@53430 35 noschinl@53430 36 text {* Variable patterns *} noschinl@53430 37 case_of_simps bar_cases: bar.simps noschinl@53430 38 print_theorems noschinl@53430 39 noschinl@53430 40 text {* Case expression not at top level *} noschinl@53430 41 simps_of_case split_rule_test_simps: split_rule_test_def noschinl@53430 42 print_theorems noschinl@53430 43 noschinl@53430 44 text {* Argument occurs both as case parameter and seperately*} noschinl@53430 45 simps_of_case nosplit_simps1: nosplit_def noschinl@53430 46 print_theorems noschinl@53430 47 noschinl@53430 48 text {* Nested case expressions *} noschinl@53430 49 simps_of_case test_simps1: test_def noschinl@53430 50 print_theorems noschinl@53430 51 noschinl@53430 52 text {* Partial split of case *} noschinl@53430 53 simps_of_case nosplit_simps2: nosplit_def (splits: list.split) noschinl@53430 54 print_theorems noschinl@53430 55 simps_of_case test_simps2: test_def (splits: option.split) noschinl@53430 56 print_theorems noschinl@53430 57 noschinl@53430 58 text {* Reversal *} noschinl@53430 59 case_of_simps test_def1: test_simps1 noschinl@53430 60 print_theorems noschinl@53430 61 noschinl@53430 62 text {* Case expressions on RHS *} noschinl@53430 63 case_of_simps test_def2: test_simps2 noschinl@53430 64 print_theorems noschinl@53430 65 noschinl@53430 66 text {* Partial split of simps *} noschinl@53430 67 case_of_simps foo_cons_def: foo.simps(1,2) noschinl@53430 68 print_theorems noschinl@53430 69 noschinl@53430 70 noschinl@53430 71 end