equal
deleted
inserted
replaced
50 val mk_supp: term -> term |
50 val mk_supp: term -> term |
51 |
51 |
52 val supp_rel_ty: typ -> typ |
52 val supp_rel_ty: typ -> typ |
53 val supp_rel_const: typ -> term |
53 val supp_rel_const: typ -> term |
54 val mk_supp_rel_ty: typ -> term -> term -> term |
54 val mk_supp_rel_ty: typ -> term -> term -> term |
55 val mk_supp_rel: term -> term -> term |
55 val mk_supp_rel: term -> term -> term |
56 |
56 |
57 val supports_const: typ -> term |
57 val supports_const: typ -> term |
58 val mk_supports_ty: typ -> term -> term -> term |
58 val mk_supports_ty: typ -> term -> term -> term |
59 val mk_supports: term -> term -> term |
59 val mk_supports: term -> term -> term |
60 |
60 |
357 |
357 |
358 (* simpset for size goals *) |
358 (* simpset for size goals *) |
359 val size_ss = |
359 val size_ss = |
360 simpset_of (put_simpset HOL_ss @{context} |
360 simpset_of (put_simpset HOL_ss @{context} |
361 addsimprocs [@{simproc natless_cancel_numerals}] |
361 addsimprocs [@{simproc natless_cancel_numerals}] |
362 addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral |
362 addsimps @{thms in_measure wf_measure sum.case add_Suc_right add.right_neutral |
363 zero_less_Suc prod.size(1) mult_Suc_right}) |
363 zero_less_Suc prod.size(1) mult_Suc_right}) |
364 |
364 |
365 val natT = @{typ nat} |
365 val natT = @{typ nat} |
366 |
366 |
367 fun prod_size_const T1 T2 = |
367 fun prod_size_const T1 T2 = |
372 in |
372 in |
373 Const (@{const_name prod_size}, [T1_fun, T2_fun, prodT] ---> natT) |
373 Const (@{const_name prod_size}, [T1_fun, T2_fun, prodT] ---> natT) |
374 end |
374 end |
375 |
375 |
376 fun snd_const T1 T2 = |
376 fun snd_const T1 T2 = |
377 Const ("Product_Type.snd", HOLogic.mk_prodT (T1, T2) --> T2) |
377 Const (@{const_name Product_Type.snd}, HOLogic.mk_prodT (T1, T2) --> T2) |
378 |
378 |
379 |
379 |
380 fun mk_measure_trm f ctxt T = |
380 fun mk_measure_trm f ctxt T = |
381 HOLogic.dest_setT T |
381 HOLogic.dest_setT T |
382 |> fst o HOLogic.dest_prodT |
382 |> fst o HOLogic.dest_prodT |
388 fun prove_termination_ind ctxt = |
388 fun prove_termination_ind ctxt = |
389 let |
389 let |
390 fun mk_size_measure T = |
390 fun mk_size_measure T = |
391 case T of |
391 case T of |
392 (Type (@{type_name Sum_Type.sum}, [T1, T2])) => |
392 (Type (@{type_name Sum_Type.sum}, [T1, T2])) => |
393 SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) |
393 Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) |
394 | (Type (@{type_name Product_Type.prod}, [T1, T2])) => |
394 | (Type (@{type_name Product_Type.prod}, [T1, T2])) => |
395 HOLogic.mk_comp (mk_size_measure T2, snd_const T1 T2) |
395 HOLogic.mk_comp (mk_size_measure T2, snd_const T1 T2) |
396 | _ => HOLogic.size_const T |
396 | _ => HOLogic.size_const T |
397 |
397 |
398 val measure_trm = mk_measure_trm (mk_size_measure) ctxt |
398 val measure_trm = mk_measure_trm (mk_size_measure) ctxt |
404 fun prove_termination_fun size_simps ctxt = |
404 fun prove_termination_fun size_simps ctxt = |
405 let |
405 let |
406 fun mk_size_measure T = |
406 fun mk_size_measure T = |
407 case T of |
407 case T of |
408 (Type (@{type_name Sum_Type.sum}, [T1, T2])) => |
408 (Type (@{type_name Sum_Type.sum}, [T1, T2])) => |
409 SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) |
409 Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) |
410 | (Type (@{type_name Product_Type.prod}, [T1, T2])) => |
410 | (Type (@{type_name Product_Type.prod}, [T1, T2])) => |
411 prod_size_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2) |
411 prod_size_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2) |
412 | _ => HOLogic.size_const T |
412 | _ => HOLogic.size_const T |
413 |
413 |
414 val measure_trm = mk_measure_trm (mk_size_measure) ctxt |
414 val measure_trm = mk_measure_trm (mk_size_measure) ctxt |