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 \<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@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