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