author  haftmann 
Wed, 11 Mar 2009 15:56:49 +0100  
changeset 30446  e3641cac56fa 
parent 30428  14f469e70eab 
child 30480  f3421e8379ab 
permissions  rwrr 
20324  1 
(* Title: HOL/FunDef.thy 
2 
Author: Alexander Krauss, TU Muenchen 

22816  3 
*) 
20324  4 

29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

5 
header {* Function Definitions and Termination Proofs *} 
20324  6 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

7 
theory FunDef 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
25567
diff
changeset

8 
imports Wellfounded 
22816  9 
uses 
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

10 
"Tools/prop_logic.ML" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

11 
"Tools/sat_solver.ML" 
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
22919
diff
changeset

12 
("Tools/function_package/fundef_lib.ML") 
22816  13 
("Tools/function_package/fundef_common.ML") 
14 
("Tools/function_package/inductive_wrap.ML") 

15 
("Tools/function_package/context_tree.ML") 

16 
("Tools/function_package/fundef_core.ML") 

25556  17 
("Tools/function_package/sum_tree.ML") 
22816  18 
("Tools/function_package/mutual.ML") 
19 
("Tools/function_package/pattern_split.ML") 

20 
("Tools/function_package/fundef_package.ML") 

21 
("Tools/function_package/auto_term.ML") 

26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

22 
("Tools/function_package/measure_functions.ML") 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
25567
diff
changeset

23 
("Tools/function_package/lexicographic_order.ML") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
25567
diff
changeset

24 
("Tools/function_package/fundef_datatype.ML") 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26875
diff
changeset

25 
("Tools/function_package/induction_scheme.ML") 
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

26 
("Tools/function_package/termination.ML") 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

27 
("Tools/function_package/decompose.ML") 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

28 
("Tools/function_package/descent.ML") 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

29 
("Tools/function_package/scnp_solve.ML") 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

30 
("Tools/function_package/scnp_reconstruct.ML") 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

31 
begin 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

32 

29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

33 
subsection {* Definitions with default value. *} 
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset

34 

f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset

35 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21364
diff
changeset

36 
THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where 
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset

37 
"THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)" 
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset

38 

f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset

39 
lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)" 
22816  40 
by (simp add: theI' THE_default_def) 
20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset

41 

22816  42 
lemma THE_default1_equality: 
43 
"\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a" 

44 
by (simp add: the1_equality THE_default_def) 

20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset

45 

f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset

46 
lemma THE_default_none: 
22816  47 
"\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d" 
48 
by (simp add:THE_default_def) 

20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset

49 

f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset

50 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

51 
lemma fundef_ex1_existence: 
22816  52 
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" 
53 
assumes ex1: "\<exists>!y. G x y" 

54 
shows "G x (f x)" 

55 
apply (simp only: f_def) 

56 
apply (rule THE_defaultI') 

57 
apply (rule ex1) 

58 
done 

21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset

59 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

60 
lemma fundef_ex1_uniqueness: 
22816  61 
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" 
62 
assumes ex1: "\<exists>!y. G x y" 

63 
assumes elm: "G x (h x)" 

64 
shows "h x = f x" 

65 
apply (simp only: f_def) 

66 
apply (rule THE_default1_equality [symmetric]) 

67 
apply (rule ex1) 

68 
apply (rule elm) 

69 
done 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

70 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

71 
lemma fundef_ex1_iff: 
22816  72 
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" 
73 
assumes ex1: "\<exists>!y. G x y" 

74 
shows "(G x y) = (f x = y)" 

20536
f088edff8af8
Function package: Outside their domain functions now return "arbitrary".
krauss
parents:
20523
diff
changeset

75 
apply (auto simp:ex1 f_def THE_default1_equality) 
22816  76 
apply (rule THE_defaultI') 
77 
apply (rule ex1) 

78 
done 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

79 

20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset

80 
lemma fundef_default_value: 
22816  81 
assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))" 
82 
assumes graph: "\<And>x y. G x y \<Longrightarrow> D x" 

83 
assumes "\<not> D x" 

84 
shows "f x = d x" 

20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset

85 
proof  
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset

86 
have "\<not>(\<exists>y. G x y)" 
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset

87 
proof 
21512
3786eb1b69d6
Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents:
21404
diff
changeset

88 
assume "\<exists>y. G x y" 
3786eb1b69d6
Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents:
21404
diff
changeset

89 
hence "D x" using graph .. 
3786eb1b69d6
Lemma "fundef_default_value" uses predicate instead of set.
krauss
parents:
21404
diff
changeset

90 
with `\<not> D x` show False .. 
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset

91 
qed 
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20654
diff
changeset

92 
hence "\<not>(\<exists>!y. G x y)" by blast 
22816  93 

20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset

94 
thus ?thesis 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset

95 
unfolding f_def 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset

96 
by (rule THE_default_none) 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset

97 
qed 
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset

98 

23739
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset

99 
definition in_rel_def[simp]: 
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset

100 
"in_rel R x y == (x, y) \<in> R" 
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset

101 

c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset

102 
lemma wf_in_rel: 
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset

103 
"wf R \<Longrightarrow> wfP (in_rel R)" 
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset

104 
by (simp add: wfP_def) 
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset

105 

23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
22919
diff
changeset

106 
use "Tools/function_package/fundef_lib.ML" 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

107 
use "Tools/function_package/fundef_common.ML" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20324
diff
changeset

108 
use "Tools/function_package/inductive_wrap.ML" 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

109 
use "Tools/function_package/context_tree.ML" 
22166  110 
use "Tools/function_package/fundef_core.ML" 
25556  111 
use "Tools/function_package/sum_tree.ML" 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset

112 
use "Tools/function_package/mutual.ML" 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19934
diff
changeset

113 
use "Tools/function_package/pattern_split.ML" 
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21312
diff
changeset

114 
use "Tools/function_package/auto_term.ML" 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

115 
use "Tools/function_package/fundef_package.ML" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
25567
diff
changeset

116 
use "Tools/function_package/fundef_datatype.ML" 
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26875
diff
changeset

117 
use "Tools/function_package/induction_scheme.ML" 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

118 

25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
25556
diff
changeset

119 
setup {* 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
25556
diff
changeset

120 
FundefPackage.setup 
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

121 
#> FundefDatatype.setup 
25567
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
25556
diff
changeset

122 
#> InductionScheme.setup 
5720345ea689
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
krauss
parents:
25556
diff
changeset

123 
*} 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset

124 

29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

125 
subsection {* Measure Functions *} 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

126 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

127 
inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

128 
where is_measure_trivial: "is_measure f" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

129 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

130 
use "Tools/function_package/measure_functions.ML" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

131 
setup MeasureFunctions.setup 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

132 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

133 
lemma measure_size[measure_function]: "is_measure size" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

134 
by (rule is_measure_trivial) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

135 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

136 
lemma measure_fst[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

137 
by (rule is_measure_trivial) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

138 
lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

139 
by (rule is_measure_trivial) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

140 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

141 
use "Tools/function_package/lexicographic_order.ML" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

142 
setup LexicographicOrder.setup 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

143 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

144 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

145 
subsection {* Congruence Rules *} 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

146 

22838  147 
lemma let_cong [fundef_cong]: 
148 
"M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g" 

22816  149 
unfolding Let_def by blast 
22622
25693088396b
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
krauss
parents:
22325
diff
changeset

150 

22816  151 
lemmas [fundef_cong] = 
22838  152 
if_cong image_cong INT_cong UN_cong 
153 
bex_cong ball_cong imp_cong 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

154 

22816  155 
lemma split_cong [fundef_cong]: 
22838  156 
"(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q 
22816  157 
\<Longrightarrow> split f p = split g q" 
158 
by (auto simp: split_def) 

19934  159 

22816  160 
lemma comp_cong [fundef_cong]: 
22838  161 
"f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'" 
22816  162 
unfolding o_apply . 
19934  163 

29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

164 
subsection {* Simp rules for termination proofs *} 
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

165 

26749
397a1aeede7d
* New attribute "termination_simp": Simp rules for termination proofs
krauss
parents:
26748
diff
changeset

166 
lemma termination_basic_simps[termination_simp]: 
397a1aeede7d
* New attribute "termination_simp": Simp rules for termination proofs
krauss
parents:
26748
diff
changeset

167 
"x < (y::nat) \<Longrightarrow> x < y + z" 
397a1aeede7d
* New attribute "termination_simp": Simp rules for termination proofs
krauss
parents:
26748
diff
changeset

168 
"x < z \<Longrightarrow> x < y + z" 
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

169 
"x \<le> y \<Longrightarrow> x \<le> y + (z::nat)" 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

170 
"x \<le> z \<Longrightarrow> x \<le> y + (z::nat)" 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

171 
"x < y \<Longrightarrow> x \<le> (y::nat)" 
26749
397a1aeede7d
* New attribute "termination_simp": Simp rules for termination proofs
krauss
parents:
26748
diff
changeset

172 
by arith+ 
397a1aeede7d
* New attribute "termination_simp": Simp rules for termination proofs
krauss
parents:
26748
diff
changeset

173 

26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

174 
declare le_imp_less_Suc[termination_simp] 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

175 

e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

176 
lemma prod_size_simp[termination_simp]: 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

177 
"prod_size f g p = f (fst p) + g (snd p) + Suc 0" 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

178 
by (induct p) auto 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

179 

29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

180 
subsection {* Decomposition *} 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

181 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

182 
lemma less_by_empty: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

183 
"A = {} \<Longrightarrow> A \<subseteq> B" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

184 
and union_comp_emptyL: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

185 
"\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

186 
and union_comp_emptyR: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

187 
"\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

188 
and wf_no_loop: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

189 
"R O R = {} \<Longrightarrow> wf R" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

190 
by (auto simp add: wf_comp_self[of R]) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

191 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

192 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

193 
subsection {* Reduction Pairs *} 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

194 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

195 
definition 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

196 
"reduction_pair P = (wf (fst P) \<and> snd P O fst P \<subseteq> fst P)" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

197 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

198 
lemma reduction_pairI[intro]: "wf R \<Longrightarrow> S O R \<subseteq> R \<Longrightarrow> reduction_pair (R, S)" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

199 
unfolding reduction_pair_def by auto 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

200 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

201 
lemma reduction_pair_lemma: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

202 
assumes rp: "reduction_pair P" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

203 
assumes "R \<subseteq> fst P" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

204 
assumes "S \<subseteq> snd P" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

205 
assumes "wf S" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

206 
shows "wf (R \<union> S)" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

207 
proof  
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

208 
from rp `S \<subseteq> snd P` have "wf (fst P)" "S O fst P \<subseteq> fst P" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

209 
unfolding reduction_pair_def by auto 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

210 
with `wf S` have "wf (fst P \<union> S)" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

211 
by (auto intro: wf_union_compatible) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

212 
moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

213 
ultimately show ?thesis by (rule wf_subset) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

214 
qed 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

215 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

216 
definition 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

217 
"rp_inv_image = (\<lambda>(R,S) f. (inv_image R f, inv_image S f))" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

218 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

219 
lemma rp_inv_image_rp: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

220 
"reduction_pair P \<Longrightarrow> reduction_pair (rp_inv_image P f)" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

221 
unfolding reduction_pair_def rp_inv_image_def split_def 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

222 
by force 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

223 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

224 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

225 
subsection {* Concrete orders for SCNP termination proofs *} 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

226 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

227 
definition "pair_less = less_than <*lex*> less_than" 
30428  228 
definition [code del]: "pair_leq = pair_less^=" 
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

229 
definition "max_strict = max_ext pair_less" 
30428  230 
definition [code del]: "max_weak = max_ext pair_leq \<union> {({}, {})}" 
231 
definition [code del]: "min_strict = min_ext pair_less" 

30446  232 
definition [code del]: "min_weak = min_ext pair_leq \<union> {({}, {})}" 
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

233 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

234 
lemma wf_pair_less[simp]: "wf pair_less" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

235 
by (auto simp: pair_less_def) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

236 

29127  237 
text {* Introduction rules for @{text pair_less}/@{text pair_leq} *} 
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

238 
lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

239 
and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

240 
and pair_lessI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

241 
and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

242 
unfolding pair_leq_def pair_less_def by auto 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

243 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

244 
text {* Introduction rules for max *} 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

245 
lemma smax_emptyI: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

246 
"finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

247 
and smax_insertI: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

248 
"\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

249 
and wmax_emptyI: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

250 
"finite X \<Longrightarrow> ({}, X) \<in> max_weak" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

251 
and wmax_insertI: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

252 
"\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

253 
unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

254 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

255 
text {* Introduction rules for min *} 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

256 
lemma smin_emptyI: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

257 
"X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

258 
and smin_insertI: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

259 
"\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

260 
and wmin_emptyI: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

261 
"(X, {}) \<in> min_weak" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

262 
and wmin_insertI: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

263 
"\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

264 
by (auto simp: min_strict_def min_weak_def min_ext_def) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

265 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

266 
text {* Reduction Pairs *} 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

267 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

268 
lemma max_ext_compat: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

269 
assumes "S O R \<subseteq> R" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

270 
shows "(max_ext S \<union> {({},{})}) O max_ext R \<subseteq> max_ext R" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

271 
using assms 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

272 
apply auto 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

273 
apply (elim max_ext.cases) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

274 
apply rule 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

275 
apply auto[3] 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

276 
apply (drule_tac x=xa in meta_spec) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

277 
apply simp 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

278 
apply (erule bexE) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

279 
apply (drule_tac x=xb in meta_spec) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

280 
by auto 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

281 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

282 
lemma max_rpair_set: "reduction_pair (max_strict, max_weak)" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

283 
unfolding max_strict_def max_weak_def 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

284 
apply (intro reduction_pairI max_ext_wf) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

285 
apply simp 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

286 
apply (rule max_ext_compat) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

287 
by (auto simp: pair_less_def pair_leq_def) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

288 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

289 
lemma min_ext_compat: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

290 
assumes "S O R \<subseteq> R" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

291 
shows "(min_ext S \<union> {({},{})}) O min_ext R \<subseteq> min_ext R" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

292 
using assms 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

293 
apply (auto simp: min_ext_def) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

294 
apply (drule_tac x=ya in bspec, assumption) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

295 
apply (erule bexE) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

296 
apply (drule_tac x=xc in bspec) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

297 
apply assumption 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

298 
by auto 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

299 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

300 
lemma min_rpair_set: "reduction_pair (min_strict, min_weak)" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

301 
unfolding min_strict_def min_weak_def 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

302 
apply (intro reduction_pairI min_ext_wf) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

303 
apply simp 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

304 
apply (rule min_ext_compat) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

305 
by (auto simp: pair_less_def pair_leq_def) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

306 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

307 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

308 
subsection {* Tool setup *} 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

309 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

310 
use "Tools/function_package/termination.ML" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

311 
use "Tools/function_package/decompose.ML" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

312 
use "Tools/function_package/descent.ML" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

313 
use "Tools/function_package/scnp_solve.ML" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

314 
use "Tools/function_package/scnp_reconstruct.ML" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

315 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

316 
setup {* ScnpReconstruct.setup *} 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

317 
(* 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

318 
setup {* 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

319 
Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

320 
[ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

321 
*} 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

322 
*) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

323 

d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
27271
diff
changeset

324 

26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

325 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

326 
end 