src/HOL/ex/Termination.thy
author wenzelm
Wed, 29 Dec 2010 17:34:41 +0100
changeset 41413 64cd30d6b0b8
parent 33468 91ea7115da1b
child 47836 471cc845430b
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29181
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
     1
(* Title:       HOL/ex/Termination.thy
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
     2
   Author:      Lukas Bulwahn, TU Muenchen
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
     3
   Author:      Alexander Krauss, TU Muenchen
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
     4
*)
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
     5
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
     6
header {* Examples and regression tests for automated termination proofs *}
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
     7
 
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
     8
theory Termination
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 33468
diff changeset
     9
imports Main "~~/src/HOL/Library/Multiset"
29181
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    10
begin
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    11
32399
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    12
subsection {* Manually giving termination relations using @{text relation} and
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    13
@{term measure} *}
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    14
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    15
function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    16
where
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    17
  "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    18
by pat_completeness auto
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    19
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    20
termination by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    21
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    22
function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    23
where
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    24
  "foo i N = (if i > N 
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    25
              then (if N = 0 then 0 else foo 0 (N - 1))
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    26
              else i + foo (Suc i) N)"
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    27
by pat_completeness auto
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    28
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    29
termination by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    30
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    31
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    32
subsection {* @{text lexicographic_order}: Trivial examples *}
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    33
29181
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    34
text {*
32399
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    35
  The @{text fun} command uses the method @{text lexicographic_order} by default,
4dc441c71cce some examples for giving measures manually
krauss
parents: 29181
diff changeset
    36
  so it is not explicitly invoked.
29181
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    37
*}
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    38
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    39
fun identity :: "nat \<Rightarrow> nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    40
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    41
  "identity n = n"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    42
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    43
fun yaSuc :: "nat \<Rightarrow> nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    44
where 
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    45
  "yaSuc 0 = 0"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    46
| "yaSuc (Suc n) = Suc (yaSuc n)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    47
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    48
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    49
subsection {* Examples on natural numbers *}
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    50
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    51
fun bin :: "(nat * nat) \<Rightarrow> nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    52
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    53
  "bin (0, 0) = 1"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    54
| "bin (Suc n, 0) = 0"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    55
| "bin (0, Suc m) = 0"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    56
| "bin (Suc n, Suc m) = bin (n, m) + bin (Suc n, m)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    57
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    58
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    59
fun t :: "(nat * nat) \<Rightarrow> nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    60
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    61
  "t (0,n) = 0"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    62
| "t (n,0) = 0"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    63
| "t (Suc n, Suc m) = (if (n mod 2 = 0) then (t (Suc n, m)) else (t (n, Suc m)))" 
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    64
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    65
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    66
fun k :: "(nat * nat) * (nat * nat) \<Rightarrow> nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    67
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    68
  "k ((0,0),(0,0)) = 0"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    69
| "k ((Suc z, y), (u,v)) = k((z, y), (u, v))" (* z is descending *)
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    70
| "k ((0, Suc y), (u,v)) = k((1, y), (u, v))" (* y is descending *)
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    71
| "k ((0,0), (Suc u, v)) = k((1, 1), (u, v))" (* u is descending *)
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    72
| "k ((0,0), (0, Suc v)) = k((1,1), (1,v))"   (* v is descending *)
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    73
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    74
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    75
fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    76
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    77
  "gcd2 x 0 = x"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    78
| "gcd2 0 y = y"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    79
| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    80
                                    else gcd2 (x - y) (Suc y))"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    81
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    82
fun ack :: "(nat * nat) \<Rightarrow> nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    83
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    84
  "ack (0, m) = Suc m"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    85
| "ack (Suc n, 0) = ack(n, 1)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    86
| "ack (Suc n, Suc m) = ack (n, ack (Suc n, m))"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    87
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    88
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    89
fun greedy :: "nat * nat * nat * nat * nat => nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    90
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    91
  "greedy (Suc a, Suc b, Suc c, Suc d, Suc e) =
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    92
  (if (a < 10) then greedy (Suc a, Suc b, c, d + 2, Suc e) else
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    93
  (if (a < 20) then greedy (Suc a, b, Suc c, d, Suc e) else
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    94
  (if (a < 30) then greedy (Suc a, b, Suc c, d, Suc e) else
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    95
  (if (a < 40) then greedy (Suc a, b, Suc c, d, Suc e) else
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    96
  (if (a < 50) then greedy (Suc a, b, Suc c, d, Suc e) else
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    97
  (if (a < 60) then greedy (a, Suc b, Suc c, d, Suc e) else
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    98
  (if (a < 70) then greedy (a, Suc b, Suc c, d, Suc e) else
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
    99
  (if (a < 80) then greedy (a, Suc b, Suc c, d, Suc e) else
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   100
  (if (a < 90) then greedy (Suc a, Suc b, Suc c, d, e) else
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   101
  greedy (Suc a, Suc b, Suc c, d, e))))))))))"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   102
| "greedy (a, b, c, d, e) = 0"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   103
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   104
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   105
fun blowup :: "nat => nat => nat => nat => nat => nat => nat => nat => nat => nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   106
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   107
  "blowup 0 0 0 0 0 0 0 0 0 = 0"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   108
| "blowup 0 0 0 0 0 0 0 0 (Suc i) = Suc (blowup i i i i i i i i i)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   109
| "blowup 0 0 0 0 0 0 0 (Suc h) i = Suc (blowup h h h h h h h h i)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   110
| "blowup 0 0 0 0 0 0 (Suc g) h i = Suc (blowup g g g g g g g h i)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   111
| "blowup 0 0 0 0 0 (Suc f) g h i = Suc (blowup f f f f f f g h i)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   112
| "blowup 0 0 0 0 (Suc e) f g h i = Suc (blowup e e e e e f g h i)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   113
| "blowup 0 0 0 (Suc d) e f g h i = Suc (blowup d d d d e f g h i)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   114
| "blowup 0 0 (Suc c) d e f g h i = Suc (blowup c c c d e f g h i)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   115
| "blowup 0 (Suc b) c d e f g h i = Suc (blowup b b c d e f g h i)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   116
| "blowup (Suc a) b c d e f g h i = Suc (blowup a b c d e f g h i)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   117
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   118
  
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   119
subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *}
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   120
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   121
datatype tree = Node | Branch tree tree
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   122
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   123
fun g_tree :: "tree * tree \<Rightarrow> tree"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   124
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   125
  "g_tree (Node, Node) = Node"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   126
| "g_tree (Node, Branch a b) = Branch Node (g_tree (a,b))"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   127
| "g_tree (Branch a b, Node) = Branch (g_tree (a,Node)) b"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   128
| "g_tree (Branch a b, Branch c d) = Branch (g_tree (a,c)) (g_tree (b,d))"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   129
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   130
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   131
fun acklist :: "'a list * 'a list \<Rightarrow> 'a list"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   132
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   133
  "acklist ([], m) = ((hd m)#m)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   134
|  "acklist (n#ns, []) = acklist (ns, [n])"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   135
|  "acklist ((n#ns), (m#ms)) = acklist (ns, acklist ((n#ns), ms))"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   136
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   137
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   138
subsection {* Examples with mutual recursion *}
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   139
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   140
fun evn od :: "nat \<Rightarrow> bool"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   141
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   142
  "evn 0 = True"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   143
| "od 0 = False"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   144
| "evn (Suc n) = od (Suc n)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   145
| "od (Suc n) = evn n"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   146
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   147
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   148
fun sizechange_f :: "'a list => 'a list => 'a list" and
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   149
sizechange_g :: "'a list => 'a list => 'a list => 'a list"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   150
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   151
  "sizechange_f i x = (if i=[] then x else sizechange_g (tl i) x i)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   152
| "sizechange_g a b c = sizechange_f a (b @ c)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   153
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   154
fun
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   155
  pedal :: "nat => nat => nat => nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   156
and
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   157
  coast :: "nat => nat => nat => nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   158
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   159
  "pedal 0 m c = c"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   160
| "pedal n 0 c = c"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   161
| "pedal n m c =
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   162
     (if n < m then coast (n - 1) (m - 1) (c + m)
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   163
               else pedal (n - 1) m (c + m))"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   164
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   165
| "coast n m c =
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   166
     (if n < m then coast n (m - 1) (c + n)
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   167
               else pedal n m (c + n))"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   168
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   169
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   170
33468
91ea7115da1b renamed method sizechange to size_change
krauss
parents: 32399
diff changeset
   171
subsection {* Refined analysis: The @{text size_change} method *}
29181
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   172
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   173
text {* Unsolvable for @{text lexicographic_order} *}
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   174
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   175
function fun1 :: "nat * nat \<Rightarrow> nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   176
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   177
  "fun1 (0,0) = 1"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   178
| "fun1 (0, Suc b) = 0"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   179
| "fun1 (Suc a, 0) = 0"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   180
| "fun1 (Suc a, Suc b) = fun1 (b, a)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   181
by pat_completeness auto
33468
91ea7115da1b renamed method sizechange to size_change
krauss
parents: 32399
diff changeset
   182
termination by size_change
29181
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   183
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   184
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   185
text {* 
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   186
  @{text lexicographic_order} can do the following, but it is much slower. 
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   187
*}
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   188
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   189
function
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   190
  prod :: "nat => nat => nat => nat" and
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   191
  eprod :: "nat => nat => nat => nat" and
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   192
  oprod :: "nat => nat => nat => nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   193
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   194
  "prod x y z = (if y mod 2 = 0 then eprod x y z else oprod x y z)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   195
| "oprod x y z = eprod x (y - 1) (z+x)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   196
| "eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   197
by pat_completeness auto
33468
91ea7115da1b renamed method sizechange to size_change
krauss
parents: 32399
diff changeset
   198
termination by size_change
29181
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   199
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   200
text {* 
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   201
  Permutations of arguments:
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   202
*}
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   203
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   204
function perm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   205
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   206
  "perm m n r = (if r > 0 then perm m (r - 1) n
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   207
                  else if n > 0 then perm r (n - 1) m
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   208
                  else m)"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   209
by auto
33468
91ea7115da1b renamed method sizechange to size_change
krauss
parents: 32399
diff changeset
   210
termination by size_change
29181
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   211
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   212
text {*
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   213
  Artificial examples and regression tests:
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   214
*}
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   215
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   216
function
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   217
  fun2 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   218
where
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   219
  "fun2 x y z =
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   220
      (if x > 1000 \<and> z > 0 then
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   221
           fun2 (min x y) y (z - 1)
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   222
       else if y > 0 \<and> x > 100 then
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   223
           fun2 x (y - 1) (2 * z)
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   224
       else if z > 0 then
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   225
           fun2 (min y (z - 1)) x x
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   226
       else
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   227
           0
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   228
      )"
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   229
by pat_completeness auto
33468
91ea7115da1b renamed method sizechange to size_change
krauss
parents: 32399
diff changeset
   230
termination by size_change -- {* requires Multiset *}
29181
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   231
cc177742e607 renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff changeset
   232
end