isabelle: src/HOL/Tools/Function/measure_functions.ML@e63c8f2fbd28 (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	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	10	end
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	11
57959 1bfed12a7646 updated to named_theorems; wenzelm parents: 55968 diff changeset	12	structure Measure_Functions : MEASURE_FUNCTIONS =
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	13	struct
26875 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	( User-declared size functions )
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	16
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	17	fun mk_is_measure t =
36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	18	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	19
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	20	fun find_measures ctxt T =
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 57959 diff changeset	21	DEPTH_SOLVE (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1)
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	22	(HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
59621 291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context; wenzelm parents: 59582 diff changeset	23	\|> Thm.cterm_of ctxt \|> Goal.init)
59582 0fbed69ff081 tuned signature -- prefer qualified names; wenzelm parents: 59580 diff changeset	24	\|> Seq.map (Thm.prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	25	\|> Seq.list_of
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
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	28	( Generating Measure Functions )
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	29
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	30	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	31	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	32
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37387 diff changeset	33	fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
55968 94242fa87638 tuning blanchet parents: 45294 diff changeset	34	map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
94242fa87638 tuning blanchet parents: 45294 diff changeset	35	@ map (fn m => Sum_Tree.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	36	\| mk_funorder_funs T = [ constant_1 T ]
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	37
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37387 diff changeset	38	fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
55968 94242fa87638 tuning blanchet parents: 45294 diff changeset	39	map_product (Sum_Tree.mk_sumcase fT sT HOLogic.natT)
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 32603 diff changeset	40	(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	41	\| 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	42
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37387 diff changeset	43	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	44	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	45	\| 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	46
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	47	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	48
e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: diff changeset	49	end

author	wenzelm
	Sat, 30 Jul 2016 21:10:02 +0200
changeset 63568	e63c8f2fbd28
parent 59621	291934bac95e
child 67149	e61557884799
permissions	-rw-r--r--