src/HOL/ex/Simps_Case_Conv_Examples.thy
 author wenzelm Mon Aug 31 21:28:08 2015 +0200 (2015-08-31) changeset 61070 b72a990adfe2 parent 60702 5e03e1bd1be0 child 61343 5b5656a63bd6 permissions -rw-r--r--
prefer symbols;
 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@60701 ` 31` ```lemma ``` noschinl@60701 ` 32` ``` fixes xs :: "'a list" and ys :: "'b list" ``` noschinl@60701 ` 33` ``` shows "foo xs ys = (case (xs, ys) of ``` noschinl@60701 ` 34` ``` ( [], []) \ 3 ``` noschinl@60701 ` 35` ``` | ([], y # ys) \ 1 ``` noschinl@60701 ` 36` ``` | (x # xs, []) \ 0 ``` noschinl@60701 ` 37` ``` | (x # xs, y # ys) \ foo ([] :: 'a list) ([] :: 'b list))" ``` noschinl@60701 ` 38` ``` by (fact foo_cases1) ``` noschinl@53430 ` 39` noschinl@53430 ` 40` ```text {* Redundant equations are ignored *} ``` noschinl@53430 ` 41` ```case_of_simps foo_cases2: foo.simps foo.simps ``` noschinl@60701 ` 42` ```lemma ``` noschinl@60701 ` 43` ``` fixes xs :: "'a list" and ys :: "'b list" ``` noschinl@60701 ` 44` ``` shows "foo xs ys = (case (xs, ys) of ``` noschinl@60701 ` 45` ``` ( [], []) \ 3 ``` noschinl@60701 ` 46` ``` | ([], y # ys) \ 1 ``` noschinl@60701 ` 47` ``` | (x # xs, []) \ 0 ``` noschinl@60701 ` 48` ``` | (x # xs, y # ys) \ foo ([] :: 'a list) ([] :: 'b list))" ``` noschinl@60701 ` 49` ``` by (fact foo_cases2) ``` noschinl@53430 ` 50` noschinl@53430 ` 51` ```text {* Variable patterns *} ``` noschinl@53430 ` 52` ```case_of_simps bar_cases: bar.simps ``` noschinl@53430 ` 53` ```print_theorems ``` noschinl@53430 ` 54` noschinl@53430 ` 55` ```text {* Case expression not at top level *} ``` noschinl@53430 ` 56` ```simps_of_case split_rule_test_simps: split_rule_test_def ``` noschinl@60701 ` 57` ```lemma ``` noschinl@60701 ` 58` ``` "split_rule_test (Inl x) f = f (x 1)" ``` noschinl@60701 ` 59` ``` "split_rule_test (Inr (x, None)) f = f (inv f 0)" ``` noschinl@60701 ` 60` ``` "split_rule_test (Inr (x, Some y)) f = f (y x)" ``` noschinl@60701 ` 61` ``` by (fact split_rule_test_simps)+ ``` noschinl@53430 ` 62` noschinl@53430 ` 63` ```text {* Argument occurs both as case parameter and seperately*} ``` noschinl@53430 ` 64` ```simps_of_case nosplit_simps1: nosplit_def ``` noschinl@60701 ` 65` ```lemma ``` noschinl@60701 ` 66` ``` "nosplit [] = [] @ [1]" ``` noschinl@60701 ` 67` ``` "nosplit (x # xs) = (x # xs) @ x # xs" ``` noschinl@60701 ` 68` ``` by (fact nosplit_simps1)+ ``` noschinl@53430 ` 69` noschinl@53430 ` 70` ```text {* Nested case expressions *} ``` noschinl@53430 ` 71` ```simps_of_case test_simps1: test_def ``` noschinl@60701 ` 72` ```lemma ``` noschinl@60701 ` 73` ``` "test None [] = 1" ``` noschinl@60701 ` 74` ``` "test None (x # xs) = 2" ``` noschinl@60701 ` 75` ``` "test (Some x) y = x" ``` noschinl@60701 ` 76` ``` by (fact test_simps1)+ ``` noschinl@53430 ` 77` noschinl@60702 ` 78` ```text {* Single-constructor patterns*} ``` noschinl@60702 ` 79` ```case_of_simps fst_conv_simps: fst_conv ``` noschinl@60702 ` 80` ```lemma "fst x = (case x of (a,b) \ a)" ``` noschinl@60702 ` 81` ``` by (fact fst_conv_simps) ``` noschinl@60702 ` 82` noschinl@53430 ` 83` ```text {* Partial split of case *} ``` noschinl@53430 ` 84` ```simps_of_case nosplit_simps2: nosplit_def (splits: list.split) ``` noschinl@60701 ` 85` ```lemma ``` noschinl@60701 ` 86` ``` "nosplit [] = [] @ [1]" ``` noschinl@60701 ` 87` ``` "nosplit (x # xs) = (x # xs) @ x # xs" ``` noschinl@60701 ` 88` ``` by (fact nosplit_simps1)+ ``` noschinl@60701 ` 89` noschinl@53430 ` 90` ```simps_of_case test_simps2: test_def (splits: option.split) ``` noschinl@60701 ` 91` ```lemma ``` noschinl@60701 ` 92` ``` "test None y = (case y of [] \ 1 | x # xs \ 2)" ``` noschinl@60701 ` 93` ``` "test (Some x) y = x" ``` noschinl@60701 ` 94` ``` by (fact test_simps2)+ ``` noschinl@53430 ` 95` noschinl@53430 ` 96` ```text {* Reversal *} ``` noschinl@53430 ` 97` ```case_of_simps test_def1: test_simps1 ``` noschinl@60701 ` 98` ```lemma ``` noschinl@60701 ` 99` ``` "test x y = (case (x,y) of ``` noschinl@60701 ` 100` ``` (None, []) \ 1 ``` noschinl@60701 ` 101` ``` | (None, _#_) \ 2 ``` noschinl@60701 ` 102` ``` | (Some x, _) \ x)" ``` noschinl@60701 ` 103` ``` by (fact test_def1) ``` noschinl@53430 ` 104` noschinl@53430 ` 105` ```text {* Case expressions on RHS *} ``` noschinl@53430 ` 106` ```case_of_simps test_def2: test_simps2 ``` noschinl@60701 ` 107` ```lemma "test xs y = (case (xs, y) of (None, []) \ 1 | (None, x # xa) \ 2 | (Some x, y) \ x)" ``` noschinl@60701 ` 108` ``` by (fact test_def2) ``` noschinl@53430 ` 109` noschinl@53430 ` 110` ```text {* Partial split of simps *} ``` noschinl@53430 ` 111` ```case_of_simps foo_cons_def: foo.simps(1,2) ``` noschinl@60701 ` 112` ```lemma ``` noschinl@60701 ` 113` ``` fixes xs :: "'a list" and ys :: "'b list" ``` noschinl@60701 ` 114` ``` shows "foo (x # xs) ys = (case (x,xs,ys) of ``` noschinl@60701 ` 115` ``` (_,_,[]) \ 0 ``` noschinl@60701 ` 116` ``` | (_,_,_ # _) \ foo ([] :: 'a list) ([] :: 'b list))" ``` noschinl@60701 ` 117` ``` by (fact foo_cons_def) ``` noschinl@53430 ` 118` noschinl@53430 ` 119` ```end ```