author  wenzelm 
Wed, 29 Dec 2010 17:34:41 +0100  
changeset 41413  64cd30d6b0b8 
parent 33468  91ea7115da1b 
child 47836  471cc845430b 
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 
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  12 
subsection {* Manually giving termination relations using @{text relation} and 
13 
@{term measure} *} 

14 

15 
function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

16 
where 

17 
"sum i N = (if i > N then 0 else i + sum (Suc i) N)" 

18 
by pat_completeness auto 

19 

20 
termination by (relation "measure (\<lambda>(i,N). N + 1  i)") auto 

21 

22 
function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

23 
where 

24 
"foo i N = (if i > N 

25 
then (if N = 0 then 0 else foo 0 (N  1)) 

26 
else i + foo (Suc i) N)" 

27 
by pat_completeness auto 

28 

29 
termination by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1  i]") auto 

30 

31 

32 
subsection {* @{text lexicographic_order}: Trivial examples *} 

33 

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

34 
text {* 
32399  35 
The @{text fun} command uses the method @{text lexicographic_order} by default, 
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  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  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  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  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  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 