author  krauss 
Tue, 02 Aug 2011 10:36:50 +0200  
changeset 44013  5cfc1c36ae97 
parent 39302  src/HOL/Recdef.thy@d7728f65b353 
child 44014  88bd7d74a2c1 
permissions  rwrr 
44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

1 
(* Title: HOL/Library/Old_Recdef.thy 
10773  2 
Author: Konrad Slind and Markus Wenzel, TU Muenchen 
12023  3 
*) 
5123  4 

12023  5 
header {* TFL: recursive function definitions *} 
7701  6 

44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

7 
theory Old_Recdef 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

8 
imports Main 
16417  9 
uses 
44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

10 
("~~/src/HOL/Tools/TFL/casesplit.ML") 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

11 
("~~/src/HOL/Tools/TFL/utils.ML") 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

12 
("~~/src/HOL/Tools/TFL/usyntax.ML") 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

13 
("~~/src/HOL/Tools/TFL/dcterm.ML") 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

14 
("~~/src/HOL/Tools/TFL/thms.ML") 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

15 
("~~/src/HOL/Tools/TFL/rules.ML") 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

16 
("~~/src/HOL/Tools/TFL/thry.ML") 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

17 
("~~/src/HOL/Tools/TFL/tfl.ML") 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

18 
("~~/src/HOL/Tools/TFL/post.ML") 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

19 
("~~/src/HOL/Tools/recdef.ML") 
15131  20 
begin 
10773  21 

32462  22 
inductive 
23 
wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool" 

24 
for R :: "('a * 'a) set" 

25 
and F :: "('a => 'b) => 'a => 'b" 

26 
where 

27 
wfrecI: "ALL z. (z, x) : R > wfrec_rel R F z (g z) ==> 

28 
wfrec_rel R F x (F g x)" 

29 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32462
diff
changeset

30 
definition 
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32462
diff
changeset

31 
cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where 
32462  32 
"cut f r x == (%y. if (y,x):r then f y else undefined)" 
33 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32462
diff
changeset

34 
definition 
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32462
diff
changeset

35 
adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where 
32462  36 
"adm_wf R F == ALL f g x. 
37 
(ALL z. (z, x) : R > f z = g z) > F f x = F g x" 

38 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32462
diff
changeset

39 
definition 
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32462
diff
changeset

40 
wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where 
37767  41 
"wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" 
32462  42 

43 
subsection{*WellFounded Recursion*} 

44 

45 
text{*cut*} 

46 

47 
lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r > f(y)=g(y))" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

48 
by (simp add: fun_eq_iff cut_def) 
32462  49 

50 
lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)" 

51 
by (simp add: cut_def) 

52 

53 
text{*Inductive characterization of wfrec combinator; for details see: 

54 
John Harrison, "Inductive definitions: automation and application"*} 

55 

56 
lemma wfrec_unique: "[ adm_wf R F; wf R ] ==> EX! y. wfrec_rel R F x y" 

57 
apply (simp add: adm_wf_def) 

58 
apply (erule_tac a=x in wf_induct) 

59 
apply (rule ex1I) 

60 
apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI) 

61 
apply (fast dest!: theI') 

62 
apply (erule wfrec_rel.cases, simp) 

63 
apply (erule allE, erule allE, erule allE, erule mp) 

64 
apply (fast intro: the_equality [symmetric]) 

65 
done 

66 

67 
lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)" 

68 
apply (simp add: adm_wf_def) 

69 
apply (intro strip) 

70 
apply (rule cuts_eq [THEN iffD2, THEN subst], assumption) 

71 
apply (rule refl) 

72 
done 

73 

74 
lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a" 

75 
apply (simp add: wfrec_def) 

76 
apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption) 

77 
apply (rule wfrec_rel.wfrecI) 

78 
apply (intro strip) 

79 
apply (erule adm_lemma [THEN wfrec_unique, THEN theI']) 

80 
done 

81 

82 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

83 
text{** This form avoids giant explosions in proofs. NOTE USE OF ==*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

84 
lemma def_wfrec: "[ f==wfrec r H; wf(r) ] ==> f(a) = H (cut f r a) a" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

85 
apply auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

86 
apply (blast intro: wfrec) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

87 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

88 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

89 

44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

90 
subsection {* Nitpick setup *} 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

91 

5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

92 
axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

93 

5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

94 
definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

95 
[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

96 

5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

97 
definition wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

98 
"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

99 
else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

100 

5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

101 
setup {* 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

102 
Nitpick_HOL.register_ersatz_global 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

103 
[(@{const_name wf_wfrec}, @{const_name wf_wfrec'}), 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

104 
(@{const_name wfrec}, @{const_name wfrec'})] 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

105 
*} 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

106 

5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

107 
hide_const (open) wf_wfrec wf_wfrec' wfrec' 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

108 
hide_fact (open) wf_wfrec'_def wfrec'_def 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

109 

5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

110 

5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

111 
subsection {* Lemmas for TFL *} 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

112 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

113 
lemma tfl_wf_induct: "ALL R. wf R > 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

114 
(ALL P. (ALL x. (ALL y. (y,x):R > P y) > P x) > (ALL x. P x))" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

115 
apply clarify 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

116 
apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

117 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

118 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

119 
lemma tfl_cut_apply: "ALL f R. (x,a):R > (cut f R a)(x) = f(x)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

120 
apply clarify 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

121 
apply (rule cut_apply, assumption) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

122 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

123 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

124 
lemma tfl_wfrec: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

125 
"ALL M R f. (f=wfrec R M) > wf R > (ALL x. f x = M (cut f R x) x)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

126 
apply clarify 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

127 
apply (erule wfrec) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

128 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
23742
diff
changeset

129 

10773  130 
lemma tfl_eq_True: "(x = True) > x" 
131 
by blast 

132 

133 
lemma tfl_rev_eq_mp: "(x = y) > y > x"; 

134 
by blast 

135 

136 
lemma tfl_simp_thm: "(x > y) > (x = x') > (x' > y)" 

137 
by blast 

6438  138 

10773  139 
lemma tfl_P_imp_P_iff_True: "P ==> P = True" 
140 
by blast 

141 

142 
lemma tfl_imp_trans: "(A > B) ==> (B > C) ==> (A > C)" 

143 
by blast 

144 

12023  145 
lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)" 
10773  146 
by simp 
147 

12023  148 
lemma tfl_disjE: "P \<or> Q ==> P > R ==> Q > R ==> R" 
10773  149 
by blast 
150 

12023  151 
lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x > Q ==> Q" 
10773  152 
by blast 
153 

44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

154 
use "~~/src/HOL/Tools/TFL/casesplit.ML" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

155 
use "~~/src/HOL/Tools/TFL/utils.ML" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

156 
use "~~/src/HOL/Tools/TFL/usyntax.ML" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

157 
use "~~/src/HOL/Tools/TFL/dcterm.ML" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

158 
use "~~/src/HOL/Tools/TFL/thms.ML" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

159 
use "~~/src/HOL/Tools/TFL/rules.ML" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

160 
use "~~/src/HOL/Tools/TFL/thry.ML" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

161 
use "~~/src/HOL/Tools/TFL/tfl.ML" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

162 
use "~~/src/HOL/Tools/TFL/post.ML" 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

163 
use "~~/src/HOL/Tools/recdef.ML" 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
29654
diff
changeset

164 
setup Recdef.setup 
6438  165 

32244  166 
text {*Wellfoundedness of @{text same_fst}*} 
167 

168 
definition 

169 
same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set" 

170 
where 

171 
"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}" 

172 
{*For @{text rec_def} declarations where the first n parameters 

173 
stay unchanged in the recursive call. *} 

174 

175 
lemma same_fstI [intro!]: 

176 
"[ P x; (y',y) : R x ] ==> ((x,y'),(x,y)) : same_fst P R" 

177 
by (simp add: same_fst_def) 

178 

179 
lemma wf_same_fst: 

180 
assumes prem: "(!!x. P x ==> wf(R x))" 

181 
shows "wf(same_fst P R)" 

182 
apply (simp cong del: imp_cong add: wf_def same_fst_def) 

183 
apply (intro strip) 

184 
apply (rename_tac a b) 

185 
apply (case_tac "wf (R a)") 

186 
apply (erule_tac a = b in wf_induct, blast) 

187 
apply (blast intro: prem) 

188 
done 

189 

190 
text {*Rule setup*} 

191 

9855  192 
lemmas [recdef_simp] = 
193 
inv_image_def 

194 
measure_def 

195 
lex_prod_def 

11284  196 
same_fst_def 
9855  197 
less_Suc_eq [THEN iffD2] 
198 

23150  199 
lemmas [recdef_cong] = 
22622
25693088396b
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
krauss
parents:
22399
diff
changeset

200 
if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong 
44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

201 
map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong 
9855  202 

203 
lemmas [recdef_wf] = 

204 
wf_trancl 

205 
wf_less_than 

206 
wf_lex_prod 

207 
wf_inv_image 

208 
wf_measure 

44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
39302
diff
changeset

209 
wf_measures 
9855  210 
wf_pred_nat 
10653  211 
wf_same_fst 
9855  212 
wf_empty 
213 

6438  214 
end 