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 \<Rightarrow> 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 [] \<Rightarrow> [1] | xs \<Rightarrow> 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
    ( [], []) \<Rightarrow> 3
noschinl@60701
    35
    | ([], y # ys) \<Rightarrow> 1
noschinl@60701
    36
    | (x # xs, []) \<Rightarrow> 0
noschinl@60701
    37
    | (x # xs, y # ys) \<Rightarrow> 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
    ( [], []) \<Rightarrow> 3
noschinl@60701
    46
    | ([], y # ys) \<Rightarrow> 1
noschinl@60701
    47
    | (x # xs, []) \<Rightarrow> 0
noschinl@60701
    48
    | (x # xs, y # ys) \<Rightarrow> 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) \<Rightarrow> 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 [] \<Rightarrow> 1 | x # xs \<Rightarrow> 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, []) \<Rightarrow> 1
noschinl@60701
   101
  | (None, _#_) \<Rightarrow> 2
noschinl@60701
   102
  | (Some x, _) \<Rightarrow> 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, []) \<Rightarrow> 1 | (None, x # xa) \<Rightarrow> 2 | (Some x, y) \<Rightarrow> 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
      (_,_,[]) \<Rightarrow> 0
noschinl@60701
   116
    | (_,_,_ # _) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
noschinl@60701
   117
  by (fact foo_cons_def)
noschinl@53430
   118
noschinl@53430
   119
end