|
1 (* Title: HOL/Library/Old_Recdef.thy |
|
2 Author: Konrad Slind and Markus Wenzel, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* TFL: recursive function definitions *} |
|
6 |
|
7 theory Old_Recdef |
|
8 imports Main |
|
9 uses |
|
10 ("~~/src/HOL/Tools/TFL/casesplit.ML") |
|
11 ("~~/src/HOL/Tools/TFL/utils.ML") |
|
12 ("~~/src/HOL/Tools/TFL/usyntax.ML") |
|
13 ("~~/src/HOL/Tools/TFL/dcterm.ML") |
|
14 ("~~/src/HOL/Tools/TFL/thms.ML") |
|
15 ("~~/src/HOL/Tools/TFL/rules.ML") |
|
16 ("~~/src/HOL/Tools/TFL/thry.ML") |
|
17 ("~~/src/HOL/Tools/TFL/tfl.ML") |
|
18 ("~~/src/HOL/Tools/TFL/post.ML") |
|
19 ("~~/src/HOL/Tools/recdef.ML") |
|
20 begin |
|
21 |
|
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 |
|
30 definition |
|
31 cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where |
|
32 "cut f r x == (%y. if (y,x):r then f y else undefined)" |
|
33 |
|
34 definition |
|
35 adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where |
|
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 |
|
39 definition |
|
40 wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where |
|
41 "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" |
|
42 |
|
43 subsection{*Well-Founded 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))" |
|
48 by (simp add: fun_eq_iff cut_def) |
|
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 |
|
83 text{** This form avoids giant explosions in proofs. NOTE USE OF ==*} |
|
84 lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a" |
|
85 apply auto |
|
86 apply (blast intro: wfrec) |
|
87 done |
|
88 |
|
89 |
|
90 subsection {* Nitpick setup *} |
|
91 |
|
92 axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
93 |
|
94 definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where |
|
95 [nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x" |
|
96 |
|
97 definition wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where |
|
98 "wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x |
|
99 else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" |
|
100 |
|
101 setup {* |
|
102 Nitpick_HOL.register_ersatz_global |
|
103 [(@{const_name wf_wfrec}, @{const_name wf_wfrec'}), |
|
104 (@{const_name wfrec}, @{const_name wfrec'})] |
|
105 *} |
|
106 |
|
107 hide_const (open) wf_wfrec wf_wfrec' wfrec' |
|
108 hide_fact (open) wf_wfrec'_def wfrec'_def |
|
109 |
|
110 |
|
111 subsection {* Lemmas for TFL *} |
|
112 |
|
113 lemma tfl_wf_induct: "ALL R. wf R --> |
|
114 (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))" |
|
115 apply clarify |
|
116 apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast) |
|
117 done |
|
118 |
|
119 lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)" |
|
120 apply clarify |
|
121 apply (rule cut_apply, assumption) |
|
122 done |
|
123 |
|
124 lemma tfl_wfrec: |
|
125 "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)" |
|
126 apply clarify |
|
127 apply (erule wfrec) |
|
128 done |
|
129 |
|
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 |
|
138 |
|
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 |
|
145 lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)" |
|
146 by simp |
|
147 |
|
148 lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R" |
|
149 by blast |
|
150 |
|
151 lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q" |
|
152 by blast |
|
153 |
|
154 use "~~/src/HOL/Tools/TFL/casesplit.ML" |
|
155 use "~~/src/HOL/Tools/TFL/utils.ML" |
|
156 use "~~/src/HOL/Tools/TFL/usyntax.ML" |
|
157 use "~~/src/HOL/Tools/TFL/dcterm.ML" |
|
158 use "~~/src/HOL/Tools/TFL/thms.ML" |
|
159 use "~~/src/HOL/Tools/TFL/rules.ML" |
|
160 use "~~/src/HOL/Tools/TFL/thry.ML" |
|
161 use "~~/src/HOL/Tools/TFL/tfl.ML" |
|
162 use "~~/src/HOL/Tools/TFL/post.ML" |
|
163 use "~~/src/HOL/Tools/recdef.ML" |
|
164 setup Recdef.setup |
|
165 |
|
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 |
|
192 lemmas [recdef_simp] = |
|
193 inv_image_def |
|
194 measure_def |
|
195 lex_prod_def |
|
196 same_fst_def |
|
197 less_Suc_eq [THEN iffD2] |
|
198 |
|
199 lemmas [recdef_cong] = |
|
200 if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong |
|
201 map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong |
|
202 |
|
203 lemmas [recdef_wf] = |
|
204 wf_trancl |
|
205 wf_less_than |
|
206 wf_lex_prod |
|
207 wf_inv_image |
|
208 wf_measure |
|
209 wf_measures |
|
210 wf_pred_nat |
|
211 wf_same_fst |
|
212 wf_empty |
|
213 |
|
214 end |