src/HOL/ex/Recdef.thy
 author paulson Wed Nov 05 13:23:46 1997 +0100 (1997-11-05) changeset 4153 e534c4c32d54 parent 4100 9f6907c40442 child 4606 73227403d497 permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
```     1 (*  Title:      HOL/ex/Recdef.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 Recdef = WF_Rel + List +
```
```    10
```
```    11 consts fact :: "nat => nat"
```
```    12 recdef fact "less_than"
```
```    13     "fact x = (if (x = 0) then 1 else x * fact (x - 1))"
```
```    14
```
```    15 consts Fact :: "nat => nat"
```
```    16 recdef Fact "less_than"
```
```    17     "Fact 0 = 1"
```
```    18     "Fact (Suc x) = (Fact x * Suc x)"
```
```    19
```
```    20 consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
```
```    21 recdef map2 "measure(%(f,l1,l2).size l1)"
```
```    22     "map2(f, [], [])  = []"
```
```    23     "map2(f, h#t, []) = []"
```
```    24     "map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2)"
```
```    25
```
```    26 consts finiteRchain :: "(['a,'a] => bool) * 'a list => bool"
```
```    27 recdef finiteRchain "measure (%(R,l).size l)"
```
```    28     "finiteRchain(R,  []) = True"
```
```    29     "finiteRchain(R, [x]) = True"
```
```    30     "finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst))"
```
```    31
```
```    32 consts qsort   ::"('a => 'a => bool) * 'a list => 'a list"
```
```    33 recdef qsort "measure (size o snd)"
```
```    34     simpset "simpset() addsimps [le_eq_less_Suc RS sym, filter_size]"
```
```    35     "qsort(ord, [])    = []"
```
```    36     "qsort(ord, x#rst) = qsort(ord, filter(Not o ord x) rst)
```
```    37                          @ [x] @
```
```    38                          qsort(ord, filter(ord x) rst)"
```
```    39
```
```    40 (*Not handled automatically: too complicated.*)
```
```    41 consts variant :: "nat * nat list => nat"
```
```    42 recdef variant "measure(%(n::nat, ns). size(filter(%y. n <= y) ns))"
```
```    43     "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)"
```
```    44
```
```    45 consts gcd :: "nat * nat => nat"
```
```    46 recdef gcd "measure (%(x,y).x+y)"
```
```    47     simpset "simpset() addsimps [le_eq_less_Suc RS sym, le_add1, diff_le_self]"
```
```    48     "gcd (0,y)          = y"
```
```    49     "gcd (Suc x, 0)     = Suc x"
```
```    50     "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)
```
```    51                                        else gcd(Suc x, y - x))"
```
```    52
```
```    53 (*Not handled automatically.  In fact, g is the zero constant function.*)
```
```    54 consts g   :: "nat => nat"
```
```    55 recdef g "less_than"
```
```    56     "g 0 = 0"
```
```    57     "g(Suc x) = g(g x)"
```
```    58
```
```    59 consts Div :: "nat * nat => nat * nat"
```
```    60 recdef Div "measure fst"
```
```    61     "Div(0,x)      = (0,0)"
```
```    62     "Div(Suc x, y) =
```
```    63          (let (q,r) = Div(x,y)
```
```    64           in
```
```    65           if (y <= Suc r) then (Suc q,0) else (q, Suc r))"
```
```    66
```
```    67 (*Not handled automatically.  Should be the predecessor function, but there
```
```    68   is an unnecessary "looping" recursive call in k(1) *)
```
```    69 consts k   :: "nat => nat"
```
```    70 recdef k "less_than"
```
```    71     "k 0 = 0"
```
```    72     "k (Suc n) = (let x = k 1
```
```    73                   in if (0=1) then k (Suc 1) else n)"
```
```    74
```
```    75 consts part :: "('a=>bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
```
```    76 recdef part "measure (%(P,l,l1,l2).size l)"
```
```    77     "part(P, [], l1,l2) = (l1,l2)"
```
```    78     "part(P, h#rst, l1,l2) =
```
```    79         (if P h then part(P,rst, h#l1,  l2)
```
```    80                 else part(P,rst,  l1,  h#l2))"
```
```    81
```
```    82 consts fqsort :: "(['a,'a] => bool) * 'a list => 'a list"
```
```    83 recdef fqsort "measure (size o snd)"
```
```    84     "fqsort(ord,[]) = []"
```
```    85     "fqsort(ord, x#rst) =
```
```    86      (let (less,more) = part((%y. ord y x), rst, ([],[]))
```
```    87       in
```
```    88       fqsort(ord,less)@[x]@fqsort(ord,more))"
```
```    89
```
```    90 (* silly example which demonstrates the occasional need for additional
```
```    91    congruence rules (here: map_cong from List). If the congruence rule is
```
```    92    removed, an unprovable termination condition is generated!
```
```    93    Termination not proved automatically; see the ML file.
```
```    94    TFL requires (%x.mapf x) instead of mapf.
```
```    95 *)
```
```    96 consts mapf :: nat => nat list
```
```    97 recdef mapf "measure(%m. m)"
```
```    98 congs "[map_cong]"
```
```    99 "mapf 0 = []"
```
```   100 "mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"
```
```   101
```
```   102 end
```