src/HOL/ex/Simps_Case_Conv_Examples.thy
 author Andreas Lochbihler Tue Jan 01 17:04:53 2019 +0100 (6 months ago) changeset 69568 de09a7261120 parent 66453 cc19f7ca2ed6 permissions -rw-r--r--
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
```     1 theory Simps_Case_Conv_Examples imports
```
```     2   "HOL-Library.Simps_Case_Conv"
```
```     3 begin
```
```     4
```
```     5 section \<open>Tests for the Simps<->Case conversion tools\<close>
```
```     6
```
```     7 fun foo where
```
```     8   "foo (x # xs) Nil = 0" |
```
```     9   "foo (x # xs) (y # ys) = foo [] []" |
```
```    10   "foo Nil (y # ys) = 1" |
```
```    11   "foo Nil Nil = 3"
```
```    12
```
```    13 fun bar where
```
```    14   "bar x 0 y = 0 + x" |
```
```    15   "bar x (Suc n) y = n + x"
```
```    16
```
```    17 definition
```
```    18   split_rule_test :: "((nat => 'a) + ('b * (('b => 'a) option))) => ('a => nat) => nat"
```
```    19 where
```
```    20  "split_rule_test x f = f (case x of Inl af \<Rightarrow> af 1
```
```    21     | Inr (b, None) => inv f 0
```
```    22     | Inr (b, Some g) => g b)"
```
```    23
```
```    24 definition test where "test x y = (case x of None => (case y of [] => 1 | _ # _ => 2) | Some x => x)"
```
```    25
```
```    26 definition nosplit where "nosplit x = x @ (case x of [] \<Rightarrow> [1] | xs \<Rightarrow> xs)"
```
```    27
```
```    28
```
```    29 text \<open>Function with complete, non-overlapping patterns\<close>
```
```    30 case_of_simps foo_cases1: foo.simps
```
```    31 lemma
```
```    32   fixes xs :: "'a list" and ys :: "'b list"
```
```    33   shows "foo xs ys =
```
```    34    (case xs of [] \<Rightarrow> (case ys of [] \<Rightarrow> 3 | _ # _ \<Rightarrow> 1)
```
```    35     | _ # _ \<Rightarrow> (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list)))"
```
```    36   by (fact foo_cases1)
```
```    37
```
```    38 text \<open>Redundant equations are ignored\<close>
```
```    39 case_of_simps foo_cases2: foo.simps foo.simps
```
```    40 lemma
```
```    41   fixes xs :: "'a list" and ys :: "'b list"
```
```    42   shows "foo xs ys =
```
```    43    (case xs of [] \<Rightarrow> (case ys of [] \<Rightarrow> 3 | _ # _ \<Rightarrow> 1)
```
```    44     | _ # _ \<Rightarrow> (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list)))"
```
```    45   by (fact foo_cases2)
```
```    46
```
```    47 text \<open>Variable patterns\<close>
```
```    48 case_of_simps bar_cases: bar.simps
```
```    49 lemma "bar x n y = (case n of 0 \<Rightarrow> 0 + x | Suc n' \<Rightarrow> n' + x)" by(fact bar_cases)
```
```    50
```
```    51 text \<open>Case expression not at top level\<close>
```
```    52 simps_of_case split_rule_test_simps: split_rule_test_def
```
```    53 lemma
```
```    54   "split_rule_test (Inl x) f = f (x 1)"
```
```    55   "split_rule_test (Inr (x, None)) f = f (inv f 0)"
```
```    56   "split_rule_test (Inr (x, Some y)) f = f (y x)"
```
```    57   by (fact split_rule_test_simps)+
```
```    58
```
```    59 text \<open>Argument occurs both as case parameter and seperately\<close>
```
```    60 simps_of_case nosplit_simps1: nosplit_def
```
```    61 lemma
```
```    62   "nosplit [] = [] @ [1]"
```
```    63   "nosplit (x # xs) = (x # xs) @ x # xs"
```
```    64   by (fact nosplit_simps1)+
```
```    65
```
```    66 text \<open>Nested case expressions\<close>
```
```    67 simps_of_case test_simps1: test_def
```
```    68 lemma
```
```    69   "test None [] = 1"
```
```    70   "test None (x # xs) = 2"
```
```    71   "test (Some x) y = x"
```
```    72   by (fact test_simps1)+
```
```    73
```
```    74 text \<open>Single-constructor patterns\<close>
```
```    75 case_of_simps fst_conv_simps: fst_conv
```
```    76 lemma "fst x = (case x of (a,b) \<Rightarrow> a)"
```
```    77   by (fact fst_conv_simps)
```
```    78
```
```    79 text \<open>Partial split of case\<close>
```
```    80 simps_of_case nosplit_simps2: nosplit_def (splits: list.split)
```
```    81 lemma
```
```    82   "nosplit [] = [] @ [1]"
```
```    83   "nosplit (x # xs) = (x # xs) @ x # xs"
```
```    84   by (fact nosplit_simps1)+
```
```    85
```
```    86 simps_of_case test_simps2: test_def (splits: option.split)
```
```    87 lemma
```
```    88   "test None y = (case y of [] \<Rightarrow> 1 | x # xs \<Rightarrow> 2)"
```
```    89   "test (Some x) y = x"
```
```    90   by (fact test_simps2)+
```
```    91
```
```    92 text \<open>Reversal\<close>
```
```    93 case_of_simps test_def1: test_simps1
```
```    94 lemma
```
```    95   "test x y =
```
```    96    (case x of None \<Rightarrow> (case y of [] \<Rightarrow> 1 | _ # _ \<Rightarrow> 2)
```
```    97     | Some x' \<Rightarrow> x')"
```
```    98   by (fact test_def1)
```
```    99
```
```   100 text \<open>Case expressions on RHS\<close>
```
```   101 case_of_simps test_def2: test_simps2
```
```   102 lemma "test x y =
```
```   103   (case x of None \<Rightarrow> (case y of [] \<Rightarrow> 1 | _ # _ \<Rightarrow> 2)
```
```   104    | Some x' \<Rightarrow> x')"
```
```   105   by (fact test_def2)
```
```   106
```
```   107 text \<open>Partial split of simps\<close>
```
```   108 case_of_simps foo_cons_def: foo.simps(1,2)
```
```   109 lemma
```
```   110   fixes xs :: "'a list" and ys :: "'b list"
```
```   111   shows "foo (x # xs) ys = (case ys of [] \<Rightarrow> 0 | _ # _ \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
```
```   112   by (fact foo_cons_def)
```
```   113
```
```   114 end
```