equal
deleted
inserted
replaced
87 type cns_info = (term * typ * typ list * bool list) list |
87 type cns_info = (term * typ * typ list * bool list) list |
88 |
88 |
89 val all_dtyp_constrs_types: Datatype_Aux.descr -> cns_info list |
89 val all_dtyp_constrs_types: Datatype_Aux.descr -> cns_info list |
90 |
90 |
91 (* tactics for function package *) |
91 (* tactics for function package *) |
92 val size_simpset: simpset |
92 val size_ss: simpset |
93 val pat_completeness_simp: thm list -> Proof.context -> tactic |
93 val pat_completeness_simp: thm list -> Proof.context -> tactic |
94 val prove_termination_ind: Proof.context -> int -> tactic |
94 val prove_termination_ind: Proof.context -> int -> tactic |
95 val prove_termination_fun: thm list -> Proof.context -> Function.info * local_theory |
95 val prove_termination_fun: thm list -> Proof.context -> Function.info * local_theory |
96 |
96 |
97 (* transformations of premises in inductions *) |
97 (* transformations of premises in inductions *) |
344 map (map aux) (all_dtyp_constrs_info descr) |
344 map (map aux) (all_dtyp_constrs_info descr) |
345 end |
345 end |
346 |
346 |
347 (** function package tactics **) |
347 (** function package tactics **) |
348 |
348 |
349 fun pat_completeness_simp simps lthy = |
349 fun pat_completeness_simp simps ctxt = |
350 let |
350 let |
351 val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps) |
351 val simpset = |
352 in |
352 put_simpset HOL_basic_ss ctxt addsimps (@{thms sum.inject sum.distinct} @ simps) |
353 Pat_Completeness.pat_completeness_tac lthy 1 |
353 in |
354 THEN ALLGOALS (asm_full_simp_tac simp_set) |
354 Pat_Completeness.pat_completeness_tac ctxt 1 |
|
355 THEN ALLGOALS (asm_full_simp_tac simpset) |
355 end |
356 end |
356 |
357 |
357 (* simpset for size goals *) |
358 (* simpset for size goals *) |
358 val size_simpset = HOL_ss |
359 val size_ss = |
|
360 simpset_of (put_simpset HOL_ss @{context} |
359 addsimprocs [@{simproc natless_cancel_numerals}] |
361 addsimprocs [@{simproc natless_cancel_numerals}] |
360 addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
362 addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
361 zero_less_Suc prod.size(1) mult_Suc_right} |
363 zero_less_Suc prod.size(1) mult_Suc_right}) |
362 |
364 |
363 val natT = @{typ nat} |
365 val natT = @{typ nat} |
364 |
366 |
365 fun prod_size_const T1 T2 = |
367 fun prod_size_const T1 T2 = |
366 let |
368 let |
411 |
413 |
412 val measure_trm = mk_measure_trm (mk_size_measure) ctxt |
414 val measure_trm = mk_measure_trm (mk_size_measure) ctxt |
413 |
415 |
414 val tac = |
416 val tac = |
415 Function_Relation.relation_tac ctxt measure_trm |
417 Function_Relation.relation_tac ctxt measure_trm |
416 THEN_ALL_NEW simp_tac (size_simpset addsimps size_simps) |
418 THEN_ALL_NEW simp_tac (put_simpset size_ss ctxt addsimps size_simps) |
417 in |
419 in |
418 Function.prove_termination NONE (HEADGOAL tac) ctxt |
420 Function.prove_termination NONE (HEADGOAL tac) ctxt |
419 end |
421 end |
420 |
422 |
421 (** transformations of premises (in inductive proofs) **) |
423 (** transformations of premises (in inductive proofs) **) |
444 | map_term' _ _ = NONE; |
446 | map_term' _ _ = NONE; |
445 |
447 |
446 fun map_thm_tac ctxt tac thm = |
448 fun map_thm_tac ctxt tac thm = |
447 let |
449 let |
448 val monos = Inductive.get_monos ctxt |
450 val monos = Inductive.get_monos ctxt |
449 val simps = HOL_basic_ss addsimps @{thms split_def} |
451 val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def} |
450 in |
452 in |
451 EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, |
453 EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, |
452 REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), |
454 REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac monos)), |
453 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] |
455 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] |
454 end |
456 end |
455 |
457 |
456 fun map_thm ctxt f tac thm = |
458 fun map_thm ctxt f tac thm = |
457 let |
459 let |