author  krauss 
Sat, 27 Dec 2008 17:35:00 +0100  
changeset 29181  cc177742e607 
child 32399  4dc441c71cce 
permissions  rwrr 
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 
ID: $Id$ 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

3 
Author: Lukas Bulwahn, TU Muenchen 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

4 
Author: Alexander Krauss, TU Muenchen 
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 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

7 
header {* Examples and regression tests for automated termination proofs *} 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

8 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

9 
theory Termination 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

10 
imports Main Multiset 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

11 
begin 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

12 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

13 
text {* 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

14 
The @{text fun} command uses the method @{text lexicographic_order} by default. 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

15 
*} 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

16 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

17 
subsection {* Trivial examples *} 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

18 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

19 
fun identity :: "nat \<Rightarrow> nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

20 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

21 
"identity n = n" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

22 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

23 
fun yaSuc :: "nat \<Rightarrow> nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

24 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

25 
"yaSuc 0 = 0" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

26 
 "yaSuc (Suc n) = Suc (yaSuc n)" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

27 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

28 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

29 
subsection {* Examples on natural numbers *} 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

30 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

31 
fun bin :: "(nat * nat) \<Rightarrow> nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

32 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

33 
"bin (0, 0) = 1" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

34 
 "bin (Suc n, 0) = 0" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

35 
 "bin (0, Suc m) = 0" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

36 
 "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

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 t :: "(nat * 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 
"t (0,n) = 0" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

42 
 "t (n,0) = 0" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

43 
 "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

44 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

45 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

46 
fun k :: "(nat * nat) * (nat * nat) \<Rightarrow> nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

47 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

48 
"k ((0,0),(0,0)) = 0" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

49 
 "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

50 
 "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

51 
 "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

52 
 "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

53 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

54 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

55 
fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

56 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

57 
"gcd2 x 0 = x" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

58 
 "gcd2 0 y = y" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

59 
 "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

60 
else gcd2 (x  y) (Suc y))" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

61 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

62 
fun ack :: "(nat * nat) \<Rightarrow> nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

63 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

64 
"ack (0, m) = Suc m" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

65 
 "ack (Suc n, 0) = ack(n, 1)" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

66 
 "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

67 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

68 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

69 
fun greedy :: "nat * nat * nat * nat * nat => nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

70 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

71 
"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

72 
(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

73 
(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

74 
(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

75 
(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

76 
(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

77 
(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

78 
(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

79 
(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

80 
(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

81 
greedy (Suc a, Suc b, Suc c, d, e))))))))))" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

82 
 "greedy (a, b, c, d, e) = 0" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

83 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

84 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

85 
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

86 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

87 
"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

88 
 "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

89 
 "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

90 
 "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

91 
 "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

92 
 "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

93 
 "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

94 
 "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

95 
 "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

96 
 "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

97 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

98 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

99 
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

100 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

101 
datatype tree = Node  Branch tree tree 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

102 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

103 
fun g_tree :: "tree * tree \<Rightarrow> tree" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

104 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

105 
"g_tree (Node, Node) = Node" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

106 
 "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

107 
 "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

108 
 "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

109 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

110 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

111 
fun acklist :: "'a list * 'a list \<Rightarrow> 'a list" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

112 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

113 
"acklist ([], m) = ((hd m)#m)" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

114 
 "acklist (n#ns, []) = acklist (ns, [n])" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

115 
 "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

116 

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 
subsection {* Examples with mutual recursion *} 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

119 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

120 
fun evn od :: "nat \<Rightarrow> bool" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

121 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

122 
"evn 0 = True" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

123 
 "od 0 = False" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

124 
 "evn (Suc n) = od (Suc n)" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

125 
 "od (Suc n) = evn n" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

126 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

127 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

128 
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

129 
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

130 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

131 
"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

132 
 "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

133 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

134 
fun 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

135 
pedal :: "nat => nat => nat => nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

136 
and 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

137 
coast :: "nat => nat => nat => nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

138 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

139 
"pedal 0 m c = c" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

140 
 "pedal n 0 c = c" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

141 
 "pedal n m c = 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

142 
(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

143 
else pedal (n  1) m (c + m))" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

144 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

145 
 "coast n m c = 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

146 
(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

147 
else pedal n m (c + n))" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

148 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

149 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

150 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

151 
subsection {* Refined analysis: The @{text sizechange} method *} 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

152 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

153 
text {* Unsolvable for @{text lexicographic_order} *} 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

154 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

155 
function fun1 :: "nat * nat \<Rightarrow> nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

156 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

157 
"fun1 (0,0) = 1" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

158 
 "fun1 (0, Suc b) = 0" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

159 
 "fun1 (Suc a, 0) = 0" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

160 
 "fun1 (Suc a, Suc b) = fun1 (b, a)" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

161 
by pat_completeness auto 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

162 
termination by sizechange 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

163 

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 
text {* 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

166 
@{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

167 
*} 
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 
function 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

170 
prod :: "nat => nat => nat => nat" and 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

171 
eprod :: "nat => nat => nat => nat" and 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

172 
oprod :: "nat => nat => nat => nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

173 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

174 
"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

175 
 "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

176 
 "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

177 
by pat_completeness auto 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

178 
termination by sizechange 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

179 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

180 
text {* 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

181 
Permutations of arguments: 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

182 
*} 
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 
function perm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

185 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

186 
"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

187 
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

188 
else m)" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

189 
by auto 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

190 
termination by sizechange 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

191 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

192 
text {* 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

193 
Artificial examples and regression tests: 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

194 
*} 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

195 

cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

196 
function 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

197 
fun2 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

198 
where 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

199 
"fun2 x y z = 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

200 
(if x > 1000 \<and> z > 0 then 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

201 
fun2 (min x y) y (z  1) 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

202 
else if y > 0 \<and> x > 100 then 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

203 
fun2 x (y  1) (2 * z) 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

204 
else if z > 0 then 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

205 
fun2 (min y (z  1)) x x 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

206 
else 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

207 
0 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

208 
)" 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

209 
by pat_completeness auto 
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
diff
changeset

210 
termination by sizechange  {* requires Multiset *} 
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 
end 