src/HOL/ex/Recdefs.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 16417 9bc16273c2d4
child 37456 0a1cc2675958
permissions -rw-r--r--
added lemmas
wenzelm@6481
     1
(*  Title:      HOL/ex/Recdefs.thy
wenzelm@5124
     2
    ID:         $Id$
wenzelm@5124
     3
    Author:     Konrad Slind and Lawrence C Paulson
wenzelm@5124
     4
    Copyright   1996  University of Cambridge
wenzelm@5124
     5
wenzelm@5124
     6
Examples of recdef definitions.  Most, but not all, are handled automatically.
wenzelm@5124
     7
*)
wenzelm@5124
     8
wenzelm@11024
     9
header {* Examples of recdef definitions *}
wenzelm@11024
    10
haftmann@16417
    11
theory Recdefs imports Main begin
wenzelm@5124
    12
wenzelm@5124
    13
consts fact :: "nat => nat"
wenzelm@11024
    14
recdef fact  less_than
wenzelm@11024
    15
  "fact x = (if x = 0 then 1 else x * fact (x - 1))"
wenzelm@5124
    16
wenzelm@5124
    17
consts Fact :: "nat => nat"
wenzelm@11024
    18
recdef Fact  less_than
wenzelm@11024
    19
  "Fact 0 = 1"
wenzelm@11024
    20
  "Fact (Suc x) = Fact x * Suc x"
wenzelm@5124
    21
paulson@14953
    22
consts fib :: "int => int"
paulson@14953
    23
recdef fib  "measure nat"
paulson@14953
    24
  eqn:  "fib n = (if n < 1 then 0
paulson@14953
    25
                  else if n=1 then 1
paulson@14953
    26
                  else fib(n - 2) + fib(n - 1))";
paulson@14953
    27
paulson@14953
    28
lemma "fib 7 = 13"
paulson@14953
    29
by simp
paulson@14953
    30
paulson@14953
    31
wenzelm@5124
    32
consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
wenzelm@11024
    33
recdef map2  "measure(\<lambda>(f, l1, l2). size l1)"
wenzelm@11024
    34
  "map2 (f, [], [])  = []"
wenzelm@11024
    35
  "map2 (f, h # t, []) = []"
wenzelm@11024
    36
  "map2 (f, h1 # t1, h2 # t2) = f h1 h2 # map2 (f, t1, t2)"
wenzelm@5124
    37
wenzelm@11024
    38
consts finiteRchain :: "('a => 'a => bool) * 'a list => bool"
wenzelm@11024
    39
recdef finiteRchain  "measure (\<lambda>(R, l). size l)"
wenzelm@11024
    40
  "finiteRchain(R,  []) = True"
wenzelm@11024
    41
  "finiteRchain(R, [x]) = True"
wenzelm@11024
    42
  "finiteRchain(R, x # y # rst) = (R x y \<and> finiteRchain (R, y # rst))"
wenzelm@5124
    43
wenzelm@11024
    44
text {* Not handled automatically: too complicated. *}
wenzelm@5124
    45
consts variant :: "nat * nat list => nat"
paulson@14244
    46
recdef (permissive) variant "measure (\<lambda>(n,ns). size (filter (\<lambda>y. n \<le> y) ns))"
wenzelm@11024
    47
  "variant (x, L) = (if x mem L then variant (Suc x, L) else x)"
wenzelm@5124
    48
wenzelm@5124
    49
consts gcd :: "nat * nat => nat"
wenzelm@11024
    50
recdef gcd  "measure (\<lambda>(x, y). x + y)"
wenzelm@11024
    51
  "gcd (0, y) = y"
wenzelm@11024
    52
  "gcd (Suc x, 0) = Suc x"
wenzelm@11024
    53
  "gcd (Suc x, Suc y) =
wenzelm@11024
    54
    (if y \<le> x then gcd (x - y, Suc y) else gcd (Suc x, y - x))"
wenzelm@11024
    55
wenzelm@11024
    56
wenzelm@11024
    57
text {*
wenzelm@11024
    58
  \medskip The silly @{term g} function: example of nested recursion.
wenzelm@11024
    59
  Not handled automatically.  In fact, @{term g} is the zero constant
wenzelm@11024
    60
  function.
wenzelm@11024
    61
 *}
wenzelm@5124
    62
wenzelm@11024
    63
consts g :: "nat => nat"
wenzelm@11626
    64
recdef (permissive) g  less_than
wenzelm@11024
    65
  "g 0 = 0"
wenzelm@11024
    66
  "g (Suc x) = g (g x)"
wenzelm@11024
    67
wenzelm@11024
    68
lemma g_terminates: "g x < Suc x"
wenzelm@11024
    69
  apply (induct x rule: g.induct)
wenzelm@11024
    70
   apply (auto simp add: g.simps)
wenzelm@11024
    71
  done
wenzelm@11024
    72
wenzelm@11024
    73
lemma g_zero: "g x = 0"
wenzelm@11024
    74
  apply (induct x rule: g.induct)
wenzelm@11024
    75
   apply (simp_all add: g.simps g_terminates)
wenzelm@11024
    76
  done
wenzelm@11024
    77
wenzelm@5124
    78
wenzelm@5124
    79
consts Div :: "nat * nat => nat * nat"
wenzelm@11024
    80
recdef Div  "measure fst"
wenzelm@11024
    81
  "Div (0, x) = (0, 0)"
wenzelm@11024
    82
  "Div (Suc x, y) =
wenzelm@11024
    83
    (let (q, r) = Div (x, y)
wenzelm@11024
    84
    in if y \<le> Suc r then (Suc q, 0) else (q, Suc r))"
wenzelm@11024
    85
wenzelm@11024
    86
text {*
wenzelm@11024
    87
  \medskip Not handled automatically.  Should be the predecessor
wenzelm@11024
    88
  function, but there is an unnecessary "looping" recursive call in
wenzelm@12023
    89
  @{text "k 1"}.
wenzelm@11024
    90
*}
wenzelm@5124
    91
wenzelm@11024
    92
consts k :: "nat => nat"
wenzelm@11701
    93
wenzelm@11626
    94
recdef (permissive) k  less_than
wenzelm@11024
    95
  "k 0 = 0"
wenzelm@11024
    96
  "k (Suc n) =
wenzelm@11024
    97
   (let x = k 1
wenzelm@11701
    98
    in if False then k (Suc 1) else n)"
wenzelm@11024
    99
wenzelm@11024
   100
consts part :: "('a => bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
wenzelm@11024
   101
recdef part  "measure (\<lambda>(P, l, l1, l2). size l)"
wenzelm@11024
   102
  "part (P, [], l1, l2) = (l1, l2)"
wenzelm@11024
   103
  "part (P, h # rst, l1, l2) =
wenzelm@11024
   104
    (if P h then part (P, rst, h # l1, l2)
wenzelm@11024
   105
    else part (P, rst, l1, h # l2))"
wenzelm@5124
   106
wenzelm@11024
   107
consts fqsort :: "('a => 'a => bool) * 'a list => 'a list"
wenzelm@11626
   108
recdef (permissive) fqsort  "measure (size o snd)"
wenzelm@11024
   109
  "fqsort (ord, []) = []"
wenzelm@11024
   110
  "fqsort (ord, x # rst) =
wenzelm@11024
   111
  (let (less, more) = part ((\<lambda>y. ord y x), rst, ([], []))
wenzelm@11024
   112
  in fqsort (ord, less) @ [x] @ fqsort (ord, more))"
wenzelm@11024
   113
wenzelm@11024
   114
text {*
wenzelm@11024
   115
  \medskip Silly example which demonstrates the occasional need for
wenzelm@11024
   116
  additional congruence rules (here: @{thm [source] map_cong}).  If
wenzelm@11024
   117
  the congruence rule is removed, an unprovable termination condition
wenzelm@11024
   118
  is generated!  Termination not proved automatically.  TFL requires
wenzelm@11024
   119
  @{term [source] "\<lambda>x. mapf x"} instead of @{term [source] mapf}.
wenzelm@11024
   120
*}
wenzelm@5124
   121
wenzelm@11024
   122
consts mapf :: "nat => nat list"
wenzelm@11626
   123
recdef (permissive) mapf  "measure (\<lambda>m. m)"
wenzelm@11024
   124
  "mapf 0 = []"
wenzelm@11024
   125
  "mapf (Suc n) = concat (map (\<lambda>x. mapf x) (replicate n n))"
wenzelm@11024
   126
  (hints cong: map_cong)
wenzelm@5124
   127
wenzelm@11024
   128
recdef_tc mapf_tc: mapf
wenzelm@11024
   129
  apply (rule allI)
wenzelm@11024
   130
  apply (case_tac "n = 0")
wenzelm@11024
   131
   apply simp_all
wenzelm@11024
   132
  done
wenzelm@11024
   133
wenzelm@11024
   134
text {* Removing the termination condition from the generated thms: *}
wenzelm@11024
   135
wenzelm@11024
   136
lemma "mapf (Suc n) = concat (map mapf (replicate n n))"
wenzelm@11024
   137
  apply (simp add: mapf.simps mapf_tc)
wenzelm@11024
   138
  done
wenzelm@11024
   139
wenzelm@11024
   140
lemmas mapf_induct = mapf.induct [OF mapf_tc]
wenzelm@5124
   141
wenzelm@5124
   142
end