equal
deleted
inserted
replaced
41 (term * typ * typ list * bool list) list list |
41 (term * typ * typ list * bool list) list list |
42 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> |
42 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> |
43 (term * typ * typ list * bool list) list |
43 (term * typ * typ list * bool list) list |
44 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
44 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
45 |
45 |
|
46 (* tactics for function package *) |
|
47 val pat_completeness_auto: Proof.context -> tactic |
|
48 val pat_completeness_simp: thm list -> Proof.context -> tactic |
|
49 val prove_termination: Proof.context -> Function.info * local_theory |
|
50 |
|
51 |
46 end |
52 end |
47 |
53 |
48 |
54 |
49 structure Nominal_Library: NOMINAL_LIBRARY = |
55 structure Nominal_Library: NOMINAL_LIBRARY = |
50 struct |
56 struct |
148 Datatype_Prop.indexify_names |
154 Datatype_Prop.indexify_names |
149 (map (prefix str o get_nth_name) descr) |
155 (map (prefix str o get_nth_name) descr) |
150 end |
156 end |
151 |
157 |
152 |
158 |
|
159 (** function package **) |
|
160 fun pat_completeness_auto lthy = |
|
161 Pat_Completeness.pat_completeness_tac lthy 1 |
|
162 THEN auto_tac (clasimpset_of lthy) |
|
163 |
|
164 fun pat_completeness_simp simps lthy = |
|
165 let |
|
166 val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps) |
|
167 in |
|
168 Pat_Completeness.pat_completeness_tac lthy 1 |
|
169 THEN ALLGOALS (asm_full_simp_tac simp_set) |
|
170 end |
|
171 |
|
172 fun prove_termination lthy = |
|
173 Function.prove_termination NONE |
|
174 (Lexicographic_Order.lexicographic_order_tac true lthy) lthy |
|
175 |
153 end (* structure *) |
176 end (* structure *) |
154 |
177 |
155 open Nominal_Library; |
178 open Nominal_Library; |