4 Measure functions, generated heuristically. |
4 Measure functions, generated heuristically. |
5 *) |
5 *) |
6 |
6 |
7 signature MEASURE_FUNCTIONS = |
7 signature MEASURE_FUNCTIONS = |
8 sig |
8 sig |
9 |
|
10 val get_measure_functions : Proof.context -> typ -> term list |
9 val get_measure_functions : Proof.context -> typ -> term list |
11 val setup : theory -> theory |
10 val setup : theory -> theory |
12 |
|
13 end |
11 end |
14 |
12 |
15 structure MeasureFunctions : MEASURE_FUNCTIONS = |
13 structure MeasureFunctions : MEASURE_FUNCTIONS = |
16 struct |
14 struct |
17 |
15 |
38 |
36 |
39 fun constant_0 T = Abs ("x", T, HOLogic.zero) |
37 fun constant_0 T = Abs ("x", T, HOLogic.zero) |
40 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero) |
38 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero) |
41 |
39 |
42 fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
40 fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
43 map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT) |
41 map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT) |
44 @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT) |
42 @ map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT) |
45 | mk_funorder_funs T = [ constant_1 T ] |
43 | mk_funorder_funs T = [ constant_1 T ] |
46 |
44 |
47 fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
45 fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
48 map_product (SumTree.mk_sumcase fT sT HOLogic.natT) |
46 map_product (Sum_Tree.mk_sumcase fT sT HOLogic.natT) |
49 (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT) |
47 (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT) |
50 | mk_ext_base_funs ctxt T = find_measures ctxt T |
48 | mk_ext_base_funs ctxt T = find_measures ctxt T |
51 |
49 |
52 fun mk_all_measure_funs ctxt (T as Type (@{type_name Sum_Type.sum}, _)) = |
50 fun mk_all_measure_funs ctxt (T as Type (@{type_name Sum_Type.sum}, _)) = |
53 mk_ext_base_funs ctxt T @ mk_funorder_funs T |
51 mk_ext_base_funs ctxt T @ mk_funorder_funs T |