isabelle: src/HOL/Tools/function_package/auto_term.ML@cf814e36f788 (annotated)

19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	1	(* Title: HOL/Tools/function_package/auto_term.ML
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	2	ID: $Id$
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	3	Author: Alexander Krauss, TU Muenchen
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	4
20873 4066ee15b278 tuned method syntax: polymorhic term argument; wenzelm parents: 20295 diff changeset	5	A package for general recursive function definitions.
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	6	Method "relation" to commence a termination proof using a user-specified relation.
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	7	*)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	8
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	9
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	10	signature FUNDEF_RELATION =
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	11	sig
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	12	val relation_meth : Proof.context -> term -> Method.method
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	13
20873 4066ee15b278 tuned method syntax: polymorhic term argument; wenzelm parents: 20295 diff changeset	14	val setup: theory -> theory
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	15	end
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	16
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	17	structure FundefRelation : FUNDEF_RELATION =
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	18	struct
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	19
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	20	fun relation_meth ctxt rel =
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	21	let
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	22	val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	23
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	24	val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	25	val rule = FundefCommon.get_termination_rule ctxt \|> the
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	26	\|> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	27
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	28	val prem = #1 (Logic.dest_implies (Thm.prop_of rule))
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	29	val Rvar = cert (Var (the_single (Term.add_vars prem [])))
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	30	in
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	31	Method.SIMPLE_METHOD (rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) 1)
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	32	end
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	33
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	34
20295 8b3e97502fd9 use proper RecdefPackage.get_hints; wenzelm parents: 19770 diff changeset	35	val setup = Method.add_methods
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	36	[("relation", uncurry relation_meth oo Method.syntax Args.term,
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	37	"proves termination using a user-specified wellfounded relation")]
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	38
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	39	end

author	krauss
	Mon, 13 Nov 2006 13:51:22 +0100
changeset 21319	cf814e36f788
parent 21104	b6ab939147eb
child 21588	cd0dc678a205
permissions	-rw-r--r--