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