equal
deleted
inserted
replaced
253 in |
253 in |
254 Pat_Completeness.pat_completeness_tac lthy 1 |
254 Pat_Completeness.pat_completeness_tac lthy 1 |
255 THEN ALLGOALS (asm_full_simp_tac simp_set) |
255 THEN ALLGOALS (asm_full_simp_tac simp_set) |
256 end |
256 end |
257 |
257 |
|
258 |
|
259 (** FIX: my_relation is necessary because of problem in Function Package *) |
|
260 |
|
261 fun inst_state_tac ctxt rel st = |
|
262 let |
|
263 val cert = Thm.cterm_of (ProofContext.theory_of ctxt) |
|
264 val rel' = cert (singleton (Variable.polymorphic ctxt) rel) |
|
265 val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st |
|
266 in case Term.add_vars (prop_of st') [] of |
|
267 [v] => |
|
268 PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st' |
|
269 | _ => Seq.empty |
|
270 end |
|
271 |
|
272 fun my_relation_tac ctxt rel i = |
|
273 TRY (Function_Common.apply_termination_rule ctxt i) |
|
274 THEN inst_state_tac ctxt rel |
|
275 |
|
276 (** FIX: end *) |
|
277 |
|
278 |
258 fun prove_termination_tac size_simps ctxt i st = |
279 fun prove_termination_tac size_simps ctxt i st = |
259 let |
280 let |
260 fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
281 fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
261 SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) |
282 SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) |
262 | mk_size_measure T = size_const T |
283 | mk_size_measure T = size_const T |
268 |> mk_size_measure |
289 |> mk_size_measure |
269 |> curry (op $) (Const (@{const_name measure}, dummyT)) |
290 |> curry (op $) (Const (@{const_name measure}, dummyT)) |
270 |> Syntax.check_term ctxt |
291 |> Syntax.check_term ctxt |
271 val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
292 val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
272 zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals |
293 zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals |
273 in |
294 |
274 (Function_Relation.relation_tac ctxt measure_trm |
295 in |
|
296 (*see above Function_Relation.relation_tac ctxt measure_trm*) |
|
297 (my_relation_tac ctxt measure_trm |
275 THEN_ALL_NEW simp_tac ss) i st |
298 THEN_ALL_NEW simp_tac ss) i st |
276 end |
299 end |
277 |
300 |
278 fun prove_termination size_simps ctxt = |
301 fun prove_termination size_simps ctxt = |
279 Function.prove_termination NONE |
302 Function.prove_termination NONE |