author  krauss 
Thu, 19 Jun 2008 11:46:14 +0200  
changeset 27271  ba2a00d35df1 
parent 26875  e18574413bc4 
child 29125  d41182a8135c 
permissions  rwrr 
20324  1 
(* Title: HOL/FunDef.thy 
2 
ID: $Id$ 

3 
Author: Alexander Krauss, TU Muenchen 

22816  4 
*) 
20324  5 

22816  6 
header {* General recursive function definitions *} 
20324  7 

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

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

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

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

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

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

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

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

20 
("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

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

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

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

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

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

26 

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

28 

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

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

30 
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

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

32 

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

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

35 

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

38 
by (simp add: the1_equality THE_default_def) 

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

39 

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

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

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

43 

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

44 

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

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

48 
shows "G x (f x)" 

49 
apply (simp only: f_def) 

50 
apply (rule THE_defaultI') 

51 
apply (rule ex1) 

52 
done 

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

53 

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

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

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

58 
shows "h x = f x" 

59 
apply (simp only: f_def) 

60 
apply (rule THE_default1_equality [symmetric]) 

61 
apply (rule ex1) 

62 
apply (rule elm) 

63 
done 

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

64 

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

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

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

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

69 
apply (auto simp:ex1 f_def THE_default1_equality) 
22816  70 
apply (rule THE_defaultI') 
71 
apply (rule ex1) 

72 
done 

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

73 

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

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

77 
assumes "\<not> D x" 

78 
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

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

80 
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

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

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

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

84 
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

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

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

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

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

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

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

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

92 

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

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

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

95 

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

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

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

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

99 

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

100 
inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool" 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

101 
where is_measure_trivial: "is_measure f" 
23739
c5ead5df7f35
Inserted definition of in_rel again (since member2 was removed).
berghofe
parents:
23494
diff
changeset

102 

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

103 
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

104 
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

105 
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

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

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

110 
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

111 
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

112 
use "Tools/function_package/fundef_package.ML" 
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

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

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

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

116 
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

117 

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

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

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

120 
#> InductionScheme.setup 
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

121 
#> MeasureFunctions.setup 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
25567
diff
changeset

122 
#> LexicographicOrder.setup 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
25567
diff
changeset

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

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

125 

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

22816  128 
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

129 

22816  130 
lemmas [fundef_cong] = 
22838  131 
if_cong image_cong INT_cong UN_cong 
132 
bex_cong ball_cong imp_cong 

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

133 

22816  134 
lemma split_cong [fundef_cong]: 
22838  135 
"(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q 
22816  136 
\<Longrightarrow> split f p = split g q" 
137 
by (auto simp: split_def) 

19934  138 

22816  139 
lemma comp_cong [fundef_cong]: 
22838  140 
"f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'" 
22816  141 
unfolding o_apply . 
19934  142 

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

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

144 

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

145 
text {* Rules for generating measure functions *} 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

146 

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

147 
lemma [measure_function]: "is_measure size" 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

148 
by (rule is_measure_trivial) 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

149 

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

150 
lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))" 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

151 
by (rule is_measure_trivial) 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

152 
lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))" 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

153 
by (rule is_measure_trivial) 
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

154 

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

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

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

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

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

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

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

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

162 

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

163 
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

164 

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

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

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

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

168 

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

169 

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

170 
end 