46 (* tactics for function package *) |
46 (* tactics for function package *) |
47 val pat_completeness_auto: Proof.context -> tactic |
47 val pat_completeness_auto: Proof.context -> tactic |
48 val pat_completeness_simp: thm list -> Proof.context -> tactic |
48 val pat_completeness_simp: thm list -> Proof.context -> tactic |
49 val prove_termination: Proof.context -> Function.info * local_theory |
49 val prove_termination: Proof.context -> Function.info * local_theory |
50 |
50 |
51 |
51 (* transformations of premises in inductions *) |
|
52 val transform_prem1: Proof.context -> string list -> thm -> thm |
|
53 val transform_prem2: Proof.context -> string list -> thm -> thm |
52 end |
54 end |
53 |
55 |
54 |
56 |
55 structure Nominal_Library: NOMINAL_LIBRARY = |
57 structure Nominal_Library: NOMINAL_LIBRARY = |
56 struct |
58 struct |
154 Datatype_Prop.indexify_names |
156 Datatype_Prop.indexify_names |
155 (map (prefix str o get_nth_name) descr) |
157 (map (prefix str o get_nth_name) descr) |
156 end |
158 end |
157 |
159 |
158 |
160 |
159 (** function package **) |
161 |
|
162 (** function package tactics **) |
|
163 |
160 fun pat_completeness_auto lthy = |
164 fun pat_completeness_auto lthy = |
161 Pat_Completeness.pat_completeness_tac lthy 1 |
165 Pat_Completeness.pat_completeness_tac lthy 1 |
162 THEN auto_tac (clasimpset_of lthy) |
166 THEN auto_tac (clasimpset_of lthy) |
163 |
167 |
164 fun pat_completeness_simp simps lthy = |
168 fun pat_completeness_simp simps lthy = |
171 |
175 |
172 fun prove_termination lthy = |
176 fun prove_termination lthy = |
173 Function.prove_termination NONE |
177 Function.prove_termination NONE |
174 (Lexicographic_Order.lexicographic_order_tac true lthy) lthy |
178 (Lexicographic_Order.lexicographic_order_tac true lthy) lthy |
175 |
179 |
|
180 |
|
181 (** transformations of premises (in inductive proofs) **) |
|
182 |
|
183 (* |
|
184 given the theorem F[t]; proves the theorem F[f t] |
|
185 |
|
186 - F needs to be monotone |
|
187 - f returns either SOME for a term it fires on |
|
188 and NONE elsewhere |
|
189 *) |
|
190 fun map_term f t = |
|
191 (case f t of |
|
192 NONE => map_term' f t |
|
193 | x => x) |
|
194 and map_term' f (t $ u) = |
|
195 (case (map_term f t, map_term f u) of |
|
196 (NONE, NONE) => NONE |
|
197 | (SOME t'', NONE) => SOME (t'' $ u) |
|
198 | (NONE, SOME u'') => SOME (t $ u'') |
|
199 | (SOME t'', SOME u'') => SOME (t'' $ u'')) |
|
200 | map_term' f (Abs (s, T, t)) = |
|
201 (case map_term f t of |
|
202 NONE => NONE |
|
203 | SOME t'' => SOME (Abs (s, T, t''))) |
|
204 | map_term' _ _ = NONE; |
|
205 |
|
206 fun map_thm_tac ctxt tac thm = |
|
207 let |
|
208 val monos = Inductive.get_monos ctxt |
|
209 val simps = HOL_basic_ss addsimps @{thms split_def} |
|
210 in |
|
211 EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, |
|
212 REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), |
|
213 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] |
|
214 end |
|
215 |
|
216 fun map_thm ctxt f tac thm = |
|
217 let |
|
218 val opt_goal_trm = map_term f (prop_of thm) |
|
219 in |
|
220 case opt_goal_trm of |
|
221 NONE => thm |
|
222 | SOME goal => |
|
223 Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) |
|
224 end |
|
225 |
|
226 (* |
|
227 inductive premises can be of the form |
|
228 R ... /\ P ...; split_conj_i picks out |
|
229 the part R or P part |
|
230 *) |
|
231 fun split_conj1 names (Const ("op &", _) $ f1 $ f2) = |
|
232 (case head_of f1 of |
|
233 Const (name, _) => if member (op =) names name then SOME f1 else NONE |
|
234 | _ => NONE) |
|
235 | split_conj1 _ _ = NONE; |
|
236 |
|
237 fun split_conj2 names (Const ("op &", _) $ f1 $ f2) = |
|
238 (case head_of f1 of |
|
239 Const (name, _) => if member (op =) names name then SOME f2 else NONE |
|
240 | _ => NONE) |
|
241 | split_conj2 _ _ = NONE; |
|
242 |
|
243 fun transform_prem1 ctxt names thm = |
|
244 map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm |
|
245 |
|
246 fun transform_prem2 ctxt names thm = |
|
247 map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm |
|
248 |
|
249 |
|
250 |
176 end (* structure *) |
251 end (* structure *) |
177 |
252 |
178 open Nominal_Library; |
253 open Nominal_Library; |