10 |
10 |
11 val dest_listT: typ -> typ |
11 val dest_listT: typ -> typ |
12 |
12 |
13 val size_const: typ -> term |
13 val size_const: typ -> term |
14 |
14 |
|
15 val sum_case_const: typ -> typ -> typ -> term |
|
16 val mk_sum_case: term -> term -> term |
|
17 |
15 val mk_minus: term -> term |
18 val mk_minus: term -> term |
16 val mk_plus: term -> term -> term |
19 val mk_plus: term -> term -> term |
17 |
20 |
18 val perm_ty: typ -> typ |
21 val perm_ty: typ -> typ |
19 val mk_perm_ty: typ -> term -> term -> term |
22 val mk_perm_ty: typ -> term -> term -> term |
49 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info |
52 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 |
53 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
51 |
54 |
52 (* tactics for function package *) |
55 (* tactics for function package *) |
53 val pat_completeness_simp: thm list -> Proof.context -> tactic |
56 val pat_completeness_simp: thm list -> Proof.context -> tactic |
54 val prove_termination: Proof.context -> Function.info * local_theory |
57 val prove_termination: thm list -> Proof.context -> Function.info * local_theory |
55 |
58 |
56 (* transformations of premises in inductions *) |
59 (* transformations of premises in inductions *) |
57 val transform_prem1: Proof.context -> string list -> thm -> thm |
60 val transform_prem1: Proof.context -> string list -> thm -> thm |
58 val transform_prem2: Proof.context -> string list -> thm -> thm |
61 val transform_prem2: Proof.context -> string list -> thm -> thm |
59 |
62 |
73 |
76 |
74 fun dest_listT (Type (@{type_name list}, [T])) = T |
77 fun dest_listT (Type (@{type_name list}, [T])) = T |
75 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
78 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
76 |
79 |
77 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) |
80 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) |
|
81 |
|
82 fun sum_case_const ty1 ty2 ty3 = |
|
83 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
|
84 fun mk_sum_case trm1 trm2 = |
|
85 let |
|
86 val ([ty1], ty3) = strip_type (fastype_of trm1) |
|
87 val ty2 = domain_type (fastype_of trm2) |
|
88 in |
|
89 sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 |
|
90 end |
|
91 |
|
92 |
78 |
93 |
79 fun mk_minus p = @{term "uminus::perm => perm"} $ p |
94 fun mk_minus p = @{term "uminus::perm => perm"} $ p |
80 |
95 |
81 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q |
96 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q |
82 |
97 |
185 in |
200 in |
186 Pat_Completeness.pat_completeness_tac lthy 1 |
201 Pat_Completeness.pat_completeness_tac lthy 1 |
187 THEN ALLGOALS (asm_full_simp_tac simp_set) |
202 THEN ALLGOALS (asm_full_simp_tac simp_set) |
188 end |
203 end |
189 |
204 |
190 fun prove_termination lthy = |
205 fun prove_termination_tac size_simps ctxt i st = |
191 Function.prove_termination NONE |
206 let |
192 (Lexicographic_Order.lexicographic_order_tac true lthy) lthy |
207 fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
193 |
208 SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) |
|
209 | mk_size_measure T = size_const T |
|
210 |
|
211 val ((_ $ (_ $ rel)) :: tl) = prems_of st |
|
212 val measure_trm = |
|
213 fastype_of rel |
|
214 |> HOLogic.dest_setT |
|
215 |> mk_size_measure |
|
216 |> curry (op $) (Const (@{const_name measure}, dummyT)) |
|
217 |> Syntax.check_term ctxt |
|
218 val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
|
219 zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals |
|
220 in |
|
221 (Function_Relation.relation_tac ctxt measure_trm |
|
222 THEN_ALL_NEW simp_tac ss) i st |
|
223 end |
|
224 |
|
225 fun prove_termination size_simps ctxt = |
|
226 Function.prove_termination NONE |
|
227 (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt |
194 |
228 |
195 (** transformations of premises (in inductive proofs) **) |
229 (** transformations of premises (in inductive proofs) **) |
196 |
230 |
197 (* |
231 (* |
198 given the theorem F[t]; proves the theorem F[f t] |
232 given the theorem F[t]; proves the theorem F[f t] |