src/HOL/ex/Recdefs.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 16417 9bc16273c2d4
child 37456 0a1cc2675958
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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