isabelle: src/HOL/Tools/Function/measure_functions.ML@ee49b4f7edc8 (annotated)

31775 2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 26875 diff changeset	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
31902 862ae16a799d renamed NamedThmsFun to Named_Thms; wenzelm parents: 31775 diff changeset	4	Measure functions, generated heuristically.
26875 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
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	11	val setup : theory -> theory
26875 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
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	15	structure MeasureFunctions : MEASURE_FUNCTIONS =
36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	16	struct
26875 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 )
31902 862ae16a799d renamed NamedThmsFun to Named_Thms; wenzelm parents: 31775 diff changeset	19	structure Measure_Heuristic_Rules = Named_Thms
862ae16a799d renamed NamedThmsFun to Named_Thms; wenzelm parents: 31775 diff changeset	20	(
45294 3c5d3d286055 tuned Named_Thms: proper binding; wenzelm parents: 42361 diff changeset	21	val name = @{binding measure_function}
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	22	val description =
38764 e6a18808873c more uniform descriptions, which end up in the collective output of 'print_attributes' for example; wenzelm parents: 37678 diff changeset	23	"rules that guide the heuristic generation of measure functions"
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	24	);
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	25
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	26	fun mk_is_measure t =
36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	27	Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	28
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	29	fun find_measures ctxt T =
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	30	DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)
36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	31	(HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
42361 23f352990944 modernized structure Proof_Context; wenzelm parents: 38764 diff changeset	32	\|> cterm_of (Proof_Context.theory_of ctxt) \|> Goal.init)
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	33	\|> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	34	\|> Seq.list_of
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
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	37	( Generating Measure Functions )
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 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	40	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	41
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37387 diff changeset	42	fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	43	map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	44	@ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	45	\| mk_funorder_funs T = [ constant_1 T ]
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	46
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37387 diff changeset	47	fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	48	map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	49	(mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	50	\| 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	51
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37387 diff changeset	52	fun mk_all_measure_funs ctxt (T as Type (@{type_name Sum_Type.sum}, _)) =
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	53	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	54	\| 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	55
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	56	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	57
31902 862ae16a799d renamed NamedThmsFun to Named_Thms; wenzelm parents: 31775 diff changeset	58	val setup = Measure_Heuristic_Rules.setup
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	59
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	60	end

author	haftmann
	Sun, 23 Feb 2014 10:33:43 +0100
changeset 55684	ee49b4f7edc8
parent 45294	3c5d3d286055
child 55968	94242fa87638
permissions	-rw-r--r--