isabelle: src/HOL/Tools/function_package/auto_term.ML@0fba71f35a9c (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
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	9	signature FUNDEF_RELATION =
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	10	sig
21588 cd0dc678a205 simplified method setup; wenzelm parents: 21319 diff changeset	11	val relation_tac: Proof.context -> term -> int -> tactic
20873 4066ee15b278 tuned method syntax: polymorhic term argument; wenzelm parents: 20295 diff changeset	12	val setup: theory -> theory
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	13	end
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	14
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	15	structure FundefRelation : FUNDEF_RELATION =
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	16	struct
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	17
21588 cd0dc678a205 simplified method setup; wenzelm parents: 21319 diff changeset	18	fun relation_tac ctxt rel =
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	19	let
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	20	val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
21588 cd0dc678a205 simplified method setup; wenzelm parents: 21319 diff changeset	21
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	22	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	23	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	24	\|> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
21588 cd0dc678a205 simplified method setup; wenzelm parents: 21319 diff changeset	25
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	26	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	27	val Rvar = cert (Var (the_single (Term.add_vars prem [])))
21588 cd0dc678a205 simplified method setup; wenzelm parents: 21319 diff changeset	28	in rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) end
cd0dc678a205 simplified method setup; wenzelm parents: 21319 diff changeset	29
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	30
20295 8b3e97502fd9 use proper RecdefPackage.get_hints; wenzelm parents: 19770 diff changeset	31	val setup = Method.add_methods
21815 0fba71f35a9c simplified krauss parents: 21588 diff changeset	32	[("relation", (Method.SIMPLE_METHOD' o uncurry relation_tac) oo (Method.syntax Args.term),
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	33	"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	34
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	35	end

author	krauss
	Wed, 13 Dec 2006 14:52:50 +0100
changeset 21815	0fba71f35a9c
parent 21588	cd0dc678a205
child 21879	a3efbae45735
permissions	-rw-r--r--