src/HOL/ex/Recdefs.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8522 581dfabf22dd
child 11024 23bf8d787b04
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6481
dbf2d9b3d6c8 recdef requires theory Recdef;
wenzelm
parents: 6455
diff changeset
     1
(*  Title:      HOL/ex/Recdefs.thy
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     3
    Author:     Konrad Slind and Lawrence C Paulson
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     5
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     6
Examples of recdef definitions.  Most, but not all, are handled automatically.
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     7
*)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
     8
6455
34c6c2944908 Main is the correct parent
paulson
parents: 5502
diff changeset
     9
Recdefs = Main +
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    10
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    11
consts fact :: "nat => nat"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    12
recdef fact "less_than"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    13
    "fact x = (if (x = 0) then 1 else x * fact (x - 1))"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    14
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    15
consts Fact :: "nat => nat"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    16
recdef Fact "less_than"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    17
    "Fact 0 = 1"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    18
    "Fact (Suc x) = (Fact x * Suc x)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    19
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    20
consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    21
recdef map2 "measure(%(f,l1,l2).size l1)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    22
    "map2(f, [], [])  = []"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    23
    "map2(f, h#t, []) = []"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    24
    "map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    25
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    26
consts finiteRchain :: "(['a,'a] => bool) * 'a list => bool"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    27
recdef finiteRchain "measure (%(R,l).size l)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    28
    "finiteRchain(R,  []) = True"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    29
    "finiteRchain(R, [x]) = True"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    30
    "finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst))"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    31
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    32
(*Not handled automatically: too complicated.*)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    33
consts variant :: "nat * nat list => nat"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    34
recdef variant "measure(%(n::nat, ns). size(filter(%y. n <= y) ns))"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    35
    "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    36
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    37
consts gcd :: "nat * nat => nat"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    38
recdef gcd "measure (%(x,y).x+y)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    39
    "gcd (0,y)          = y"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    40
    "gcd (Suc x, 0)     = Suc x"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    41
    "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)  
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    42
                                       else gcd(Suc x, y - x))"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    43
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    44
(*Not handled automatically.  In fact, g is the zero constant function.*)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    45
consts g   :: "nat => nat"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    46
recdef g "less_than"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    47
    "g 0 = 0"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    48
    "g(Suc x) = g(g x)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    49
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    50
consts Div :: "nat * nat => nat * nat"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    51
recdef Div "measure fst"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    52
    "Div(0,x)      = (0,0)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    53
    "Div(Suc x, y) =      
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    54
         (let (q,r) = Div(x,y)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    55
          in                      
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    56
          if (y <= Suc r) then (Suc q,0) else (q, Suc r))"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    57
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    58
(*Not handled automatically.  Should be the predecessor function, but there
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    59
  is an unnecessary "looping" recursive call in k(1) *)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    60
consts k   :: "nat => nat"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    61
recdef k "less_than"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    62
    "k 0 = 0"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    63
    "k (Suc n) = (let x = k 1  
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    64
                  in if (0=1) then k (Suc 1) else n)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    65
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    66
consts part :: "('a=>bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    67
recdef part "measure (%(P,l,l1,l2).size l)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    68
    "part(P, [], l1,l2) = (l1,l2)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    69
    "part(P, h#rst, l1,l2) =  
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    70
        (if P h then part(P,rst, h#l1,  l2)  
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    71
                else part(P,rst,  l1,  h#l2))"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    72
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    73
consts fqsort :: "(['a,'a] => bool) * 'a list => 'a list"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    74
recdef fqsort "measure (size o snd)"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    75
    "fqsort(ord,[]) = []"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    76
    "fqsort(ord, x#rst) =    
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    77
     (let (less,more) = part((%y. ord y x), rst, ([],[]))
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    78
      in  
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    79
      fqsort(ord,less)@[x]@fqsort(ord,more))"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    80
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    81
(* silly example which demonstrates the occasional need for additional
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    82
   congruence rules (here: map_cong from List). If the congruence rule is
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    83
   removed, an unprovable termination condition is generated!
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    84
   Termination not proved automatically; see the ML file.
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    85
   TFL requires (%x.mapf x) instead of mapf.
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    86
*)
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    87
consts mapf :: nat => nat list
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    88
recdef mapf "measure(%m. m)"
6481
dbf2d9b3d6c8 recdef requires theory Recdef;
wenzelm
parents: 6455
diff changeset
    89
congs map_cong
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    90
"mapf 0 = []"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    91
"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    92
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents:
diff changeset
    93
end