isabelle: src/HOL/Tools/function_package/auto_term.ML@c5531bf7c6b2 (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
22733 0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	18	fun inst_thm ctxt rel st =
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)
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	21	val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
22733 0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	22	val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	23	val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	24	in
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	25	Drule.cterm_instantiate [(Rvar, rel')] st'
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	26	end
21588 cd0dc678a205 simplified method setup; wenzelm parents: 21319 diff changeset	27
22733 0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	28	fun relation_tac ctxt rel i =
25545 21cd20c1ce98 methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function. krauss parents: 22733 diff changeset	29	TRY (FundefCommon.apply_termination_rule ctxt i)
22733 0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	30	THEN PRIMITIVE (inst_thm ctxt rel)
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	31
20295 8b3e97502fd9 use proper RecdefPackage.get_hints; wenzelm parents: 19770 diff changeset	32	val setup = Method.add_methods
21879 a3efbae45735 switched argument order in .syntax lifters haftmann* parents: 21815 diff changeset	33	[("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	34	"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	35
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	36	end

author	wenzelm
	Wed, 31 Dec 2008 19:56:38 +0100
changeset 29280	c5531bf7c6b2
parent 25545	21cd20c1ce98
child 30510	4120fc59dd85
permissions	-rw-r--r--