isabelle: src/HOL/Tools/Function/auto_term.ML@f2a8dbceb615 (annotated)

31775 2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 30515 diff changeset	1	(* Title: HOL/Tools/Function/auto_term.ML
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	2	Author: Alexander Krauss, TU Muenchen
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	3
20873 4066ee15b278 tuned method syntax: polymorhic term argument; wenzelm parents: 20295 diff changeset	4	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	5	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	6	*)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	7
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	8	signature FUNDEF_RELATION =
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	9	sig
21588 cd0dc678a205 simplified method setup; wenzelm parents: 21319 diff changeset	10	val relation_tac: Proof.context -> term -> int -> tactic
20873 4066ee15b278 tuned method syntax: polymorhic term argument; wenzelm parents: 20295 diff changeset	11	val setup: theory -> theory
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	12	end
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	13
21319 cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	14	structure FundefRelation : FUNDEF_RELATION =
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	15	struct
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	16
22733 0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	17	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	18	let
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try krauss parents: 21104 diff changeset	19	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	20	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	21	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	22	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	23	in
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	24	Drule.cterm_instantiate [(Rvar, rel')] st'
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	25	end
21588 cd0dc678a205 simplified method setup; wenzelm parents: 21319 diff changeset	26
22733 0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" krauss parents: 22496 diff changeset	27	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	28	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	29	THEN PRIMITIVE (inst_thm ctxt rel)
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: diff changeset	30
30515 bca05b17b618 simplified method setup; wenzelm parents: 30510 diff changeset	31	val setup =
bca05b17b618 simplified method setup; wenzelm parents: 30510 diff changeset	32	Method.setup @{binding relation}
bca05b17b618 simplified method setup; wenzelm parents: 30510 diff changeset	33	(Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
bca05b17b618 simplified method setup; wenzelm parents: 30510 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, 15 Jul 2009 23:50:40 +0200
changeset 32012	f2a8dbceb615
parent 31775	2b04504fcb69
child 33099	b8cdd3d73022
permissions	-rw-r--r--