114 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list |
114 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list |
115 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info |
115 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info |
116 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
116 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
117 |
117 |
118 (* tactics for function package *) |
118 (* tactics for function package *) |
|
119 val size_simpset: simpset |
119 val pat_completeness_simp: thm list -> Proof.context -> tactic |
120 val pat_completeness_simp: thm list -> Proof.context -> tactic |
120 val prove_termination: thm list -> Proof.context -> Function.info * local_theory |
121 val prove_termination_ind: Proof.context -> int -> tactic |
|
122 val prove_termination_fun: thm list -> Proof.context -> Function.info * local_theory |
121 |
123 |
122 (* transformations of premises in inductions *) |
124 (* transformations of premises in inductions *) |
123 val transform_prem1: Proof.context -> string list -> thm -> thm |
125 val transform_prem1: Proof.context -> string list -> thm -> thm |
124 val transform_prem2: Proof.context -> string list -> thm -> thm |
126 val transform_prem2: Proof.context -> string list -> thm -> thm |
125 |
127 |
471 in |
473 in |
472 Pat_Completeness.pat_completeness_tac lthy 1 |
474 Pat_Completeness.pat_completeness_tac lthy 1 |
473 THEN ALLGOALS (asm_full_simp_tac simp_set) |
475 THEN ALLGOALS (asm_full_simp_tac simp_set) |
474 end |
476 end |
475 |
477 |
476 |
478 (* simpset for size goals *) |
477 fun prove_termination_tac size_simps ctxt = |
479 val size_simpset = HOL_ss |
478 let |
480 addsimprocs Nat_Numeral_Simprocs.cancel_numerals |
479 val natT = @{typ nat} |
481 addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
480 fun prod_size_const fT sT = |
482 zero_less_Suc prod.size(1) mult_Suc_right} |
481 let |
483 |
482 val fT_fun = fT --> natT |
484 val natT = @{typ nat} |
483 val sT_fun = sT --> natT |
485 |
484 val prodT = Type (@{type_name prod}, [fT, sT]) |
486 fun prod_size_const T1 T2 = |
485 in |
487 let |
486 Const (@{const_name prod_size}, [fT_fun, sT_fun, prodT] ---> natT) |
488 val T1_fun = T1 --> natT |
487 end |
489 val T2_fun = T2 --> natT |
488 |
490 val prodT = HOLogic.mk_prodT (T1, T2) |
|
491 in |
|
492 Const (@{const_name prod_size}, [T1_fun, T2_fun, prodT] ---> natT) |
|
493 end |
|
494 |
|
495 fun snd_const T1 T2 = |
|
496 Const ("Product_Type.snd", HOLogic.mk_prodT (T1, T2) --> T2) |
|
497 |
|
498 |
|
499 fun mk_measure_trm f ctxt T = |
|
500 HOLogic.dest_setT T |
|
501 |> fst o HOLogic.dest_prodT |
|
502 |> f |
|
503 |> curry (op $) (Const (@{const_name "measure"}, dummyT)) |
|
504 |> Syntax.check_term ctxt |
|
505 |
|
506 (* wf-goal arising in induction_schema *) |
|
507 fun prove_termination_ind ctxt = |
|
508 let |
489 fun mk_size_measure T = |
509 fun mk_size_measure T = |
490 case T of |
510 case T of |
491 (Type (@{type_name Sum_Type.sum}, [fT, sT])) => |
511 (Type (@{type_name Sum_Type.sum}, [T1, T2])) => |
492 SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT) |
512 SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) |
493 | (Type (@{type_name Product_Type.prod}, [fT, sT])) => |
513 | (Type (@{type_name Product_Type.prod}, [T1, T2])) => |
494 prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT) |
514 HOLogic.mk_comp (mk_size_measure T2, snd_const T1 T2) |
495 | _ => HOLogic.size_const T |
515 | _ => HOLogic.size_const T |
496 |
516 |
497 fun mk_measure_trm T = |
517 val measure_trm = mk_measure_trm (mk_size_measure) ctxt |
498 HOLogic.dest_setT T |
518 in |
499 |> fst o HOLogic.dest_prodT |
519 Function_Relation.relation_tac ctxt measure_trm |
500 |> mk_size_measure |
520 end |
501 |> curry (op $) (Const (@{const_name "measure"}, dummyT)) |
521 |
502 |> Syntax.check_term ctxt |
522 (* wf-goal arising in function definitions *) |
503 |
523 fun prove_termination_fun size_simps ctxt = |
504 val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
524 let |
505 zero_less_Suc prod.size(1) mult_Suc_right} @ size_simps |
525 fun mk_size_measure T = |
506 val ss' = ss addsimprocs Nat_Numeral_Simprocs.cancel_numerals |
526 case T of |
507 in |
527 (Type (@{type_name Sum_Type.sum}, [T1, T2])) => |
508 Function_Relation.relation_tac ctxt mk_measure_trm |
528 SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) |
509 THEN_ALL_NEW simp_tac ss' |
529 | (Type (@{type_name Product_Type.prod}, [T1, T2])) => |
510 end |
530 prod_size_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2) |
511 |
531 | _ => HOLogic.size_const T |
512 fun prove_termination size_simps ctxt = |
532 |
513 Function.prove_termination NONE |
533 val measure_trm = mk_measure_trm (mk_size_measure) ctxt |
514 (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt |
534 |
|
535 val tac = |
|
536 Function_Relation.relation_tac ctxt measure_trm |
|
537 THEN_ALL_NEW simp_tac (size_simpset addsimps size_simps) |
|
538 in |
|
539 Function.prove_termination NONE (HEADGOAL tac) ctxt |
|
540 end |
515 |
541 |
516 (** transformations of premises (in inductive proofs) **) |
542 (** transformations of premises (in inductive proofs) **) |
517 |
543 |
518 (* |
544 (* |
519 given the theorem F[t]; proves the theorem F[f t] |
545 given the theorem F[t]; proves the theorem F[f t] |