6 |
6 |
7 signature MEASURE_FUNCTIONS = |
7 signature MEASURE_FUNCTIONS = |
8 sig |
8 sig |
9 |
9 |
10 val get_measure_functions : Proof.context -> typ -> term list |
10 val get_measure_functions : Proof.context -> typ -> term list |
11 val setup : theory -> theory |
11 val setup : theory -> theory |
12 |
12 |
13 end |
13 end |
14 |
14 |
15 structure MeasureFunctions : MEASURE_FUNCTIONS = |
15 structure MeasureFunctions : MEASURE_FUNCTIONS = |
16 struct |
16 struct |
17 |
17 |
18 (** User-declared size functions **) |
18 (** User-declared size functions **) |
19 structure Measure_Heuristic_Rules = Named_Thms |
19 structure Measure_Heuristic_Rules = Named_Thms |
20 ( |
20 ( |
21 val name = "measure_function" |
21 val name = "measure_function" |
22 val description = "Rules that guide the heuristic generation of measure functions" |
22 val description = |
|
23 "Rules that guide the heuristic generation of measure functions" |
23 ); |
24 ); |
24 |
25 |
25 fun mk_is_measures t = Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t |
26 fun mk_is_measure t = |
|
27 Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t |
26 |
28 |
27 fun find_measures ctxt T = |
29 fun find_measures ctxt T = |
28 DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) |
30 DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) |
29 (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT))) |
31 (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT))) |
30 |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init) |
32 |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init) |
31 |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) |
33 |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) |
32 |> Seq.list_of |
34 |> Seq.list_of |
33 |
35 |
34 |
36 |
35 (** Generating Measure Functions **) |
37 (** Generating Measure Functions **) |
36 |
38 |
37 fun constant_0 T = Abs ("x", T, HOLogic.zero) |
39 fun constant_0 T = Abs ("x", T, HOLogic.zero) |
38 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero) |
40 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero) |
39 |
41 |
40 fun mk_funorder_funs (Type ("+", [fT, sT])) = |
42 fun mk_funorder_funs (Type ("+", [fT, sT])) = |
41 map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT) |
43 map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT) |
42 @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT) |
44 @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT) |
43 | mk_funorder_funs T = [ constant_1 T ] |
45 | mk_funorder_funs T = [ constant_1 T ] |
44 |
46 |
45 fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) = |
47 fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) = |
46 map_product (SumTree.mk_sumcase fT sT HOLogic.natT) |
48 map_product (SumTree.mk_sumcase fT sT HOLogic.natT) |
47 (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT) |
49 (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT) |
48 | mk_ext_base_funs ctxt T = find_measures ctxt T |
50 | mk_ext_base_funs ctxt T = find_measures ctxt T |
49 |
51 |
50 fun mk_all_measure_funs ctxt (T as Type ("+", _)) = |
52 fun mk_all_measure_funs ctxt (T as Type ("+", _)) = |
51 mk_ext_base_funs ctxt T @ mk_funorder_funs T |
53 mk_ext_base_funs ctxt T @ mk_funorder_funs T |
52 | mk_all_measure_funs ctxt T = find_measures ctxt T |
54 | mk_all_measure_funs ctxt T = find_measures ctxt T |