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 |
258 |
259 (** FIX: my_relation is necessary because of problem in Function Package *) |
259 fun prove_termination_tac size_simps ctxt = |
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 |
|
279 fun prove_termination_tac size_simps ctxt i st = |
|
280 let |
260 let |
281 fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
261 fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
282 SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) |
262 SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) |
283 | mk_size_measure T = size_const T |
263 | mk_size_measure T = size_const T |
284 |
264 |
285 val ((_ $ (_ $ rel)) :: _) = prems_of st |
265 fun mk_measure_trm T = |
286 val measure_trm = |
266 HOLogic.dest_setT T |
287 fastype_of rel |
267 |> fst o HOLogic.dest_prodT |
288 |> HOLogic.dest_setT |
|
289 |> mk_size_measure |
268 |> mk_size_measure |
290 |> curry (op $) (Const (@{const_name measure}, dummyT)) |
269 |> curry (op $) (Const (@{const_name measure}, dummyT)) |
291 |> Syntax.check_term ctxt |
270 |> Syntax.check_term ctxt |
|
271 |
292 val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
272 val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
293 zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals |
273 zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals |
294 |
274 in |
295 in |
275 Function_Relation.relation_tac ctxt mk_measure_trm |
296 (*see above Function_Relation.relation_tac ctxt measure_trm*) |
276 THEN_ALL_NEW simp_tac ss |
297 (my_relation_tac ctxt measure_trm |
|
298 THEN_ALL_NEW simp_tac ss) i st |
|
299 end |
277 end |
300 |
278 |
301 fun prove_termination size_simps ctxt = |
279 fun prove_termination size_simps ctxt = |
302 Function.prove_termination NONE |
280 Function.prove_termination NONE |
303 (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt |
281 (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt |