equal
deleted
inserted
replaced
48 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list |
48 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list |
49 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info |
49 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info |
50 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
50 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
51 |
51 |
52 (* tactics for function package *) |
52 (* tactics for function package *) |
53 val pat_completeness_auto: Proof.context -> tactic |
|
54 val pat_completeness_simp: thm list -> Proof.context -> tactic |
53 val pat_completeness_simp: thm list -> Proof.context -> tactic |
55 val prove_termination: Proof.context -> Function.info * local_theory |
54 val prove_termination: Proof.context -> Function.info * local_theory |
56 |
55 |
57 (* transformations of premises in inductions *) |
56 (* transformations of premises in inductions *) |
58 val transform_prem1: Proof.context -> string list -> thm -> thm |
57 val transform_prem1: Proof.context -> string list -> thm -> thm |
177 end |
176 end |
178 |
177 |
179 |
178 |
180 |
179 |
181 (** function package tactics **) |
180 (** function package tactics **) |
182 |
|
183 fun pat_completeness_auto lthy = |
|
184 Pat_Completeness.pat_completeness_tac lthy 1 |
|
185 THEN auto_tac (clasimpset_of lthy) |
|
186 |
181 |
187 fun pat_completeness_simp simps lthy = |
182 fun pat_completeness_simp simps lthy = |
188 let |
183 let |
189 val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps) |
184 val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps) |
190 in |
185 in |