1.1 --- a/src/HOL/ex/Recdefs.thy Thu Aug 11 09:15:45 2011 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,144 +0,0 @@
1.4 -(* Title: HOL/ex/Recdefs.thy
1.5 - Author: Konrad Slind and Lawrence C Paulson
1.6 - Copyright 1996 University of Cambridge
1.7 -
1.8 -Examples of recdef definitions. Most, but not all, are handled automatically.
1.9 -*)
1.10 -
1.11 -header {* Examples of recdef definitions *}
1.12 -
1.13 -theory Recdefs imports "~~/src/HOL/Library/Old_Recdef" begin
1.14 -
1.15 -consts fact :: "nat => nat"
1.16 -recdef fact less_than
1.17 - "fact x = (if x = 0 then 1 else x * fact (x - 1))"
1.18 -
1.19 -consts Fact :: "nat => nat"
1.20 -recdef Fact less_than
1.21 - "Fact 0 = 1"
1.22 - "Fact (Suc x) = Fact x * Suc x"
1.23 -
1.24 -consts fib :: "int => int"
1.25 -recdef fib "measure nat"
1.26 - eqn: "fib n = (if n < 1 then 0
1.27 - else if n=1 then 1
1.28 - else fib(n - 2) + fib(n - 1))";
1.29 -
1.30 -lemma "fib 7 = 13"
1.31 -by simp
1.32 -
1.33 -
1.34 -consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
1.35 -recdef map2 "measure(\<lambda>(f, l1, l2). size l1)"
1.36 - "map2 (f, [], []) = []"
1.37 - "map2 (f, h # t, []) = []"
1.38 - "map2 (f, h1 # t1, h2 # t2) = f h1 h2 # map2 (f, t1, t2)"
1.39 -
1.40 -consts finiteRchain :: "('a => 'a => bool) * 'a list => bool"
1.41 -recdef finiteRchain "measure (\<lambda>(R, l). size l)"
1.42 - "finiteRchain(R, []) = True"
1.43 - "finiteRchain(R, [x]) = True"
1.44 - "finiteRchain(R, x # y # rst) = (R x y \<and> finiteRchain (R, y # rst))"
1.45 -
1.46 -text {* Not handled automatically: too complicated. *}
1.47 -consts variant :: "nat * nat list => nat"
1.48 -recdef (permissive) variant "measure (\<lambda>(n,ns). size (filter (\<lambda>y. n \<le> y) ns))"
1.49 - "variant (x, L) = (if x \<in> set L then variant (Suc x, L) else x)"
1.50 -
1.51 -consts gcd :: "nat * nat => nat"
1.52 -recdef gcd "measure (\<lambda>(x, y). x + y)"
1.53 - "gcd (0, y) = y"
1.54 - "gcd (Suc x, 0) = Suc x"
1.55 - "gcd (Suc x, Suc y) =
1.56 - (if y \<le> x then gcd (x - y, Suc y) else gcd (Suc x, y - x))"
1.57 -
1.58 -
1.59 -text {*
1.60 - \medskip The silly @{term g} function: example of nested recursion.
1.61 - Not handled automatically. In fact, @{term g} is the zero constant
1.62 - function.
1.63 - *}
1.64 -
1.65 -consts g :: "nat => nat"
1.66 -recdef (permissive) g less_than
1.67 - "g 0 = 0"
1.68 - "g (Suc x) = g (g x)"
1.69 -
1.70 -lemma g_terminates: "g x < Suc x"
1.71 - apply (induct x rule: g.induct)
1.72 - apply (auto simp add: g.simps)
1.73 - done
1.74 -
1.75 -lemma g_zero: "g x = 0"
1.76 - apply (induct x rule: g.induct)
1.77 - apply (simp_all add: g.simps g_terminates)
1.78 - done
1.79 -
1.80 -
1.81 -consts Div :: "nat * nat => nat * nat"
1.82 -recdef Div "measure fst"
1.83 - "Div (0, x) = (0, 0)"
1.84 - "Div (Suc x, y) =
1.85 - (let (q, r) = Div (x, y)
1.86 - in if y \<le> Suc r then (Suc q, 0) else (q, Suc r))"
1.87 -
1.88 -text {*
1.89 - \medskip Not handled automatically. Should be the predecessor
1.90 - function, but there is an unnecessary "looping" recursive call in
1.91 - @{text "k 1"}.
1.92 -*}
1.93 -
1.94 -consts k :: "nat => nat"
1.95 -
1.96 -recdef (permissive) k less_than
1.97 - "k 0 = 0"
1.98 - "k (Suc n) =
1.99 - (let x = k 1
1.100 - in if False then k (Suc 1) else n)"
1.101 -
1.102 -consts part :: "('a => bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
1.103 -recdef part "measure (\<lambda>(P, l, l1, l2). size l)"
1.104 - "part (P, [], l1, l2) = (l1, l2)"
1.105 - "part (P, h # rst, l1, l2) =
1.106 - (if P h then part (P, rst, h # l1, l2)
1.107 - else part (P, rst, l1, h # l2))"
1.108 -
1.109 -consts fqsort :: "('a => 'a => bool) * 'a list => 'a list"
1.110 -recdef (permissive) fqsort "measure (size o snd)"
1.111 - "fqsort (ord, []) = []"
1.112 - "fqsort (ord, x # rst) =
1.113 - (let (less, more) = part ((\<lambda>y. ord y x), rst, ([], []))
1.114 - in fqsort (ord, less) @ [x] @ fqsort (ord, more))"
1.115 -
1.116 -text {*
1.117 - \medskip Silly example which demonstrates the occasional need for
1.118 - additional congruence rules (here: @{thm [source] map_cong}). If
1.119 - the congruence rule is removed, an unprovable termination condition
1.120 - is generated! Termination not proved automatically. TFL requires
1.121 - @{term [source] "\<lambda>x. mapf x"} instead of @{term [source] mapf}.
1.122 -*}
1.123 -
1.124 -consts mapf :: "nat => nat list"
1.125 -recdef mapf "measure (\<lambda>m. m)"
1.126 - "mapf 0 = []"
1.127 - "mapf (Suc n) = concat (map (\<lambda>x. mapf x) (replicate n n))"
1.128 - (hints cong: map_cong)
1.129 -
1.130 -(* This used to be an example where recdef_tc etc is needed,
1.131 - but now termination is proved outright
1.132 -recdef_tc mapf_tc: mapf
1.133 - apply (rule allI)
1.134 - apply (case_tac "n = 0")
1.135 - apply simp_all
1.136 - done
1.137 -
1.138 -text {* Removing the termination condition from the generated thms: *}
1.139 -
1.140 -lemma "mapf (Suc n) = concat (map mapf (replicate n n))"
1.141 - apply (simp add: mapf.simps mapf_tc)
1.142 - done
1.143 -
1.144 -lemmas mapf_induct = mapf.induct [OF mapf_tc]
1.145 -*)
1.146 -
1.147 -end