isabelle: src/HOL/Tools/Function/measure_functions.ML@fff6f11b1f09 (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
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 )
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	(
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	21	val name = "measure_function"
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	22	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	23	);
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	24
32603 e08fdd615333 tuned const_name antiquotations haftmann parents: 31902 diff changeset	25	fun mk_is_measures t = 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	26
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	27	fun find_measures ctxt T =
31902 862ae16a799d renamed NamedThmsFun to Named_Thms; wenzelm parents: 31775 diff changeset	28	DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	29	(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	30	\|> 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	31	\|> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	32	\|> Seq.list_of
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
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	35	( Generating Measure Functions )
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	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	38	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	39
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	40	fun mk_funorder_funs (Type ("+", [fT, sT])) =
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 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	42	@ 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	43	\| mk_funorder_funs T = [ constant_1 T ]
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	44
31902 862ae16a799d renamed NamedThmsFun to Named_Thms; wenzelm parents: 31775 diff changeset	45	fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) =
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	46	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	47	(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	48	\| 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	49
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	50	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	51	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	52	\| 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	53
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	54	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	55
31902 862ae16a799d renamed NamedThmsFun to Named_Thms; wenzelm parents: 31775 diff changeset	56	val setup = Measure_Heuristic_Rules.setup
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	57
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	58	end
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	59

author	haftmann
	Tue, 24 Nov 2009 17:28:25 +0100
changeset 33955	fff6f11b1f09
parent 32603	e08fdd615333
child 34232	36a2a3029fd3
permissions	-rw-r--r--