| author | nipkow |
| Sat, 27 Jun 2009 09:43:41 +0200 | |
| changeset 31816 | ffaf6dd53045 |
| parent 31775 | 2b04504fcb69 |
| child 31902 | 862ae16a799d |
| permissions | -rw-r--r-- |
| 31775 | 1 |
(* Title: HOL/Tools/Function/measure_functions.ML |
|
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
3 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
4 |
Measure functions, generated heuristically |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
5 |
*) |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
6 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
7 |
signature MEASURE_FUNCTIONS = |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
8 |
sig |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
9 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
10 |
val get_measure_functions : Proof.context -> typ -> term list |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
11 |
val setup : theory -> theory |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
12 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
13 |
end |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
14 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
15 |
structure MeasureFunctions : MEASURE_FUNCTIONS = |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
16 |
struct |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
17 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
18 |
(** User-declared size functions **) |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
19 |
structure MeasureHeuristicRules = NamedThmsFun( |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
20 |
val name = "measure_function" |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
21 |
val description = "Rules that guide the heuristic generation of measure functions" |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
22 |
); |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
23 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
24 |
fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
25 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
26 |
fun find_measures ctxt T = |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
27 |
DEPTH_SOLVE (resolve_tac (MeasureHeuristicRules.get ctxt) 1) |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
28 |
(HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT)))
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
29 |
|> cterm_of (ProofContext.theory_of ctxt) |> Goal.init) |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
30 |
|> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
31 |
|> Seq.list_of |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
32 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
33 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
34 |
(** Generating Measure Functions **) |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
35 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
36 |
fun constant_0 T = Abs ("x", T, HOLogic.zero)
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
37 |
fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
38 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
39 |
fun mk_funorder_funs (Type ("+", [fT, sT])) =
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
40 |
map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT) |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
41 |
@ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT) |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
42 |
| mk_funorder_funs T = [ constant_1 T ] |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
43 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
44 |
fun mk_ext_base_funs ctxt (Type("+", [fT, sT])) =
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
45 |
map_product (SumTree.mk_sumcase fT sT HOLogic.natT) |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
46 |
(mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT) |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
47 |
| mk_ext_base_funs ctxt T = find_measures ctxt T |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
48 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
49 |
fun mk_all_measure_funs ctxt (T as Type ("+", _)) =
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
50 |
mk_ext_base_funs ctxt T @ mk_funorder_funs T |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
51 |
| mk_all_measure_funs ctxt T = find_measures ctxt T |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
52 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
53 |
val get_measure_functions = mk_all_measure_funs |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
54 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
55 |
val setup = MeasureHeuristicRules.setup |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
56 |
|
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
57 |
end |
|
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
diff
changeset
|
58 |