98 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) |
98 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) |
99 |
99 |
100 fun sum_case_const ty1 ty2 ty3 = |
100 fun sum_case_const ty1 ty2 ty3 = |
101 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
101 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
102 fun mk_sum_case trm1 trm2 = |
102 fun mk_sum_case trm1 trm2 = |
103 let |
103 let |
104 val ([ty1], ty3) = strip_type (fastype_of trm1) |
104 val ([ty1], ty3) = strip_type (fastype_of trm1) |
105 val ty2 = domain_type (fastype_of trm2) |
105 val ty2 = domain_type (fastype_of trm2) |
106 in |
106 in |
107 sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 |
107 sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 |
108 end |
108 end |
109 |
109 |
110 |
110 |
111 |
111 |
112 fun mk_minus p = @{term "uminus::perm => perm"} $ p |
112 fun mk_minus p = @{term "uminus::perm => perm"} $ p |
113 |
113 |
207 map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr |
207 map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr |
208 |
208 |
209 (* returns the constants of the constructors plus the |
209 (* returns the constants of the constructors plus the |
210 corresponding type and types of arguments *) |
210 corresponding type and types of arguments *) |
211 fun all_dtyp_constrs_types descr sorts = |
211 fun all_dtyp_constrs_types descr sorts = |
212 let |
212 let |
213 fun aux ((ty_name, vs), (cname, args)) = |
213 fun aux ((ty_name, vs), (cname, args)) = |
214 let |
214 let |
215 val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs |
215 val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs |
216 val ty = Type (ty_name, vs_tys) |
216 val ty = Type (ty_name, vs_tys) |
217 val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args |
217 val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args |
218 val is_rec = map Datatype_Aux.is_rec_type args |
218 val is_rec = map Datatype_Aux.is_rec_type args |
219 in |
219 in |
220 (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) |
220 (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) |
221 end |
221 end |
222 in |
222 in |
223 map (map aux) (all_dtyp_constrs_info descr) |
223 map (map aux) (all_dtyp_constrs_info descr) |
224 end |
224 end |
225 |
225 |
226 fun nth_dtyp_constrs_types descr sorts n = |
226 fun nth_dtyp_constrs_types descr sorts n = |
227 nth (all_dtyp_constrs_types descr sorts) n |
227 nth (all_dtyp_constrs_types descr sorts) n |
228 |
228 |
229 |
229 |
230 (* generates for every datatype a name str ^ dt_name |
230 (* generates for every datatype a name str ^ dt_name |
231 plus and index for multiple occurences of a string *) |
231 plus and index for multiple occurences of a string *) |
232 fun prefix_dt_names descr sorts str = |
232 fun prefix_dt_names descr sorts str = |
233 let |
233 let |
234 fun get_nth_name (i, _) = |
234 fun get_nth_name (i, _) = |
235 Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) |
235 Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) |
236 in |
236 in |
237 Datatype_Prop.indexify_names |
237 Datatype_Prop.indexify_names |
238 (map (prefix str o get_nth_name) descr) |
238 (map (prefix str o get_nth_name) descr) |
239 end |
239 end |
240 |
240 |
241 |
241 |
242 |
242 |
243 (** function package tactics **) |
243 (** function package tactics **) |
244 |
244 |
245 fun pat_completeness_simp simps lthy = |
245 fun pat_completeness_simp simps lthy = |
246 let |
246 let |
247 val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps) |
247 val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps) |
248 in |
248 in |
249 Pat_Completeness.pat_completeness_tac lthy 1 |
249 Pat_Completeness.pat_completeness_tac lthy 1 |
250 THEN ALLGOALS (asm_full_simp_tac simp_set) |
250 THEN ALLGOALS (asm_full_simp_tac simp_set) |
251 end |
251 end |
252 |
252 |
253 fun prove_termination_tac size_simps ctxt i st = |
253 fun prove_termination_tac size_simps ctxt i st = |
254 let |
254 let |
255 fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
255 fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
256 SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) |
256 SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) |
257 | mk_size_measure T = size_const T |
257 | mk_size_measure T = size_const T |
258 |
258 |
259 val ((_ $ (_ $ rel)) :: tl) = prems_of st |
259 val ((_ $ (_ $ rel)) :: tl) = prems_of st |
260 val measure_trm = |
260 val measure_trm = |
261 fastype_of rel |
261 fastype_of rel |
262 |> HOLogic.dest_setT |
262 |> HOLogic.dest_setT |
263 |> mk_size_measure |
263 |> mk_size_measure |
264 |> curry (op $) (Const (@{const_name measure}, dummyT)) |
264 |> curry (op $) (Const (@{const_name measure}, dummyT)) |
265 |> Syntax.check_term ctxt |
265 |> Syntax.check_term ctxt |
266 val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
266 val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
267 zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals |
267 zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals |
268 in |
268 in |
269 (Function_Relation.relation_tac ctxt measure_trm |
269 (Function_Relation.relation_tac ctxt measure_trm |
270 THEN_ALL_NEW simp_tac ss) i st |
270 THEN_ALL_NEW simp_tac ss) i st |
271 end |
271 end |
272 |
272 |
273 fun prove_termination size_simps ctxt = |
273 fun prove_termination size_simps ctxt = |
274 Function.prove_termination NONE |
274 Function.prove_termination NONE |
275 (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt |
275 (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt |
276 |
276 |
298 NONE => NONE |
298 NONE => NONE |
299 | SOME t'' => SOME (Abs (s, T, t''))) |
299 | SOME t'' => SOME (Abs (s, T, t''))) |
300 | map_term' _ _ = NONE; |
300 | map_term' _ _ = NONE; |
301 |
301 |
302 fun map_thm_tac ctxt tac thm = |
302 fun map_thm_tac ctxt tac thm = |
303 let |
303 let |
304 val monos = Inductive.get_monos ctxt |
304 val monos = Inductive.get_monos ctxt |
305 val simps = HOL_basic_ss addsimps @{thms split_def} |
305 val simps = HOL_basic_ss addsimps @{thms split_def} |
306 in |
306 in |
307 EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, |
307 EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, |
308 REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), |
308 REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), |
309 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] |
309 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] |
310 end |
310 end |
311 |
311 |
312 fun map_thm ctxt f tac thm = |
312 fun map_thm ctxt f tac thm = |
313 let |
313 let |
314 val opt_goal_trm = map_term f (prop_of thm) |
314 val opt_goal_trm = map_term f (prop_of thm) |
315 in |
315 in |
316 case opt_goal_trm of |
316 case opt_goal_trm of |
317 NONE => thm |
317 NONE => thm |
318 | SOME goal => |
318 | SOME goal => |
319 Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) |
319 Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) |
320 end |
320 end |
321 |
321 |
322 (* |
322 (* |
323 inductive premises can be of the form |
323 inductive premises can be of the form |
324 R ... /\ P ...; split_conj_i picks out |
324 R ... /\ P ...; split_conj_i picks out |
325 the part R or P part |
325 the part R or P part |