src/HOL/ex/Recdefs.thy

use structure Same;
do not open Envir;

(*  Title:      HOL/ex/Recdefs.thy
    ID:         $Id$
    Author:     Konrad Slind and Lawrence C Paulson
    Copyright   1996  University of Cambridge

Examples of recdef definitions.  Most, but not all, are handled automatically.
*)

header {* Examples of recdef definitions *}

theory Recdefs imports Main begin

consts fact :: "nat => nat"
recdef fact  less_than
  "fact x = (if x = 0 then 1 else x * fact (x - 1))"

consts Fact :: "nat => nat"
recdef Fact  less_than
  "Fact 0 = 1"
  "Fact (Suc x) = Fact x * Suc x"

consts fib :: "int => int"
recdef fib  "measure nat"
  eqn:  "fib n = (if n < 1 then 0
                  else if n=1 then 1
                  else fib(n - 2) + fib(n - 1))";

lemma "fib 7 = 13"
by simp


consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
recdef map2  "measure(\<lambda>(f, l1, l2). size l1)"
  "map2 (f, [], [])  = []"
  "map2 (f, h # t, []) = []"
  "map2 (f, h1 # t1, h2 # t2) = f h1 h2 # map2 (f, t1, t2)"

consts finiteRchain :: "('a => 'a => bool) * 'a list => bool"
recdef finiteRchain  "measure (\<lambda>(R, l). size l)"
  "finiteRchain(R,  []) = True"
  "finiteRchain(R, [x]) = True"
  "finiteRchain(R, x # y # rst) = (R x y \<and> finiteRchain (R, y # rst))"

text {* Not handled automatically: too complicated. *}
consts variant :: "nat * nat list => nat"
recdef (permissive) variant "measure (\<lambda>(n,ns). size (filter (\<lambda>y. n \<le> y) ns))"
  "variant (x, L) = (if x mem L then variant (Suc x, L) else x)"

consts gcd :: "nat * nat => nat"
recdef gcd  "measure (\<lambda>(x, y). x + y)"
  "gcd (0, y) = y"
  "gcd (Suc x, 0) = Suc x"
  "gcd (Suc x, Suc y) =
    (if y \<le> x then gcd (x - y, Suc y) else gcd (Suc x, y - x))"


text {*
  \medskip The silly @{term g} function: example of nested recursion.
  Not handled automatically.  In fact, @{term g} is the zero constant
  function.
 *}

consts g :: "nat => nat"
recdef (permissive) g  less_than
  "g 0 = 0"
  "g (Suc x) = g (g x)"

lemma g_terminates: "g x < Suc x"
  apply (induct x rule: g.induct)
   apply (auto simp add: g.simps)
  done

lemma g_zero: "g x = 0"
  apply (induct x rule: g.induct)
   apply (simp_all add: g.simps g_terminates)
  done


consts Div :: "nat * nat => nat * nat"
recdef Div  "measure fst"
  "Div (0, x) = (0, 0)"
  "Div (Suc x, y) =
    (let (q, r) = Div (x, y)
    in if y \<le> Suc r then (Suc q, 0) else (q, Suc r))"

text {*
  \medskip Not handled automatically.  Should be the predecessor
  function, but there is an unnecessary "looping" recursive call in
  @{text "k 1"}.
*}

consts k :: "nat => nat"

recdef (permissive) k  less_than
  "k 0 = 0"
  "k (Suc n) =
   (let x = k 1
    in if False then k (Suc 1) else n)"

consts part :: "('a => bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
recdef part  "measure (\<lambda>(P, l, l1, l2). size l)"
  "part (P, [], l1, l2) = (l1, l2)"
  "part (P, h # rst, l1, l2) =
    (if P h then part (P, rst, h # l1, l2)
    else part (P, rst, l1, h # l2))"

consts fqsort :: "('a => 'a => bool) * 'a list => 'a list"
recdef (permissive) fqsort  "measure (size o snd)"
  "fqsort (ord, []) = []"
  "fqsort (ord, x # rst) =
  (let (less, more) = part ((\<lambda>y. ord y x), rst, ([], []))
  in fqsort (ord, less) @ [x] @ fqsort (ord, more))"

text {*
  \medskip Silly example which demonstrates the occasional need for
  additional congruence rules (here: @{thm [source] map_cong}).  If
  the congruence rule is removed, an unprovable termination condition
  is generated!  Termination not proved automatically.  TFL requires
  @{term [source] "\<lambda>x. mapf x"} instead of @{term [source] mapf}.
*}

consts mapf :: "nat => nat list"
recdef (permissive) mapf  "measure (\<lambda>m. m)"
  "mapf 0 = []"
  "mapf (Suc n) = concat (map (\<lambda>x. mapf x) (replicate n n))"
  (hints cong: map_cong)

recdef_tc mapf_tc: mapf
  apply (rule allI)
  apply (case_tac "n = 0")
   apply simp_all
  done

text {* Removing the termination condition from the generated thms: *}

lemma "mapf (Suc n) = concat (map mapf (replicate n n))"
  apply (simp add: mapf.simps mapf_tc)
  done

lemmas mapf_induct = mapf.induct [OF mapf_tc]

end