5 *) |
5 *) |
6 |
6 |
7 signature MEASURE_FUNCTIONS = |
7 signature MEASURE_FUNCTIONS = |
8 sig |
8 sig |
9 val get_measure_functions : Proof.context -> typ -> term list |
9 val get_measure_functions : Proof.context -> typ -> term list |
10 val setup : theory -> theory |
|
11 end |
10 end |
12 |
11 |
13 structure MeasureFunctions : MEASURE_FUNCTIONS = |
12 structure Measure_Functions : MEASURE_FUNCTIONS = |
14 struct |
13 struct |
15 |
14 |
16 (** User-declared size functions **) |
15 (** User-declared size functions **) |
17 structure Measure_Heuristic_Rules = Named_Thms |
|
18 ( |
|
19 val name = @{binding measure_function} |
|
20 val description = |
|
21 "rules that guide the heuristic generation of measure functions" |
|
22 ); |
|
23 |
16 |
24 fun mk_is_measure t = |
17 fun mk_is_measure t = |
25 Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t |
18 Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t |
26 |
19 |
27 fun find_measures ctxt T = |
20 fun find_measures ctxt T = |
28 DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) |
21 DEPTH_SOLVE (resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1) |
29 (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT))) |
22 (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT))) |
30 |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init) |
23 |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init) |
31 |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) |
24 |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) |
32 |> Seq.list_of |
25 |> Seq.list_of |
33 |
26 |