isabelle: src/HOL/Tools/Function/relation.ML@e5dc7e7744f0 (annotated)

33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	1	(* Title: HOL/Tools/Function/relation.ML
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	2	Author: Alexander Krauss, TU Muenchen
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	3
47701 157e6108a342 more standard method setup; wenzelm parents: 42361 diff changeset	4	Tactics to start a termination proof using a user-specified relation.
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	5	*)
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	6
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	7	signature FUNCTION_RELATION =
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	8	sig
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	9	val relation_tac: Proof.context -> (typ -> term) -> int -> tactic
47701 157e6108a342 more standard method setup; wenzelm parents: 42361 diff changeset	10	val relation_infer_tac: Proof.context -> term -> int -> tactic
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	11	end
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	12
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	13	structure Function_Relation : FUNCTION_RELATION =
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	14	struct
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	15
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	16	(* tactic version *)
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	17
59627 bb1e4a35d506 clarified context; wenzelm parents: 59621 diff changeset	18	fun inst_state_tac ctxt inst st =
59618 e6939796717e clarified context; wenzelm parents: 59582 diff changeset	19	(case Term.add_vars (Thm.prop_of st) [] of (* FIXME tactic should not inspect main conclusion *)
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	20	[v as (_, T)] =>
59627 bb1e4a35d506 clarified context; wenzelm parents: 59621 diff changeset	21	PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))])) st
59582 0fbed69ff081 tuned signature -- prefer qualified names; wenzelm parents: 59580 diff changeset	22	\| _ => Seq.empty);
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	23
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	24	fun relation_tac ctxt rel i =
59159 9312710451f5 just one data slot per program unit; wenzelm parents: 47701 diff changeset	25	TRY (Function_Common.termination_rule_tac ctxt i)
59627 bb1e4a35d506 clarified context; wenzelm parents: 59621 diff changeset	26	THEN inst_state_tac ctxt rel;
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	27
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	28
47701 157e6108a342 more standard method setup; wenzelm parents: 42361 diff changeset	29	(* version with type inference *)
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	30
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	31	fun inst_state_infer_tac ctxt rel st =
59618 e6939796717e clarified context; wenzelm parents: 59582 diff changeset	32	(case Term.add_vars (Thm.prop_of st) [] of (* FIXME tactic should not inspect main conclusion *)
40057 b237f757b215 relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version krauss parents: 36636 diff changeset	33	[v as (_, T)] =>
b237f757b215 relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version krauss parents: 36636 diff changeset	34	let
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	35	val rel' = singleton (Variable.polymorphic ctxt) rel
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	36	\|> map_types Type_Infer.paramify_vars
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	37	\|> Type.constraint T
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	38	\|> Syntax.check_term ctxt
59621 291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context; wenzelm parents: 59618 diff changeset	39	\|> Thm.cterm_of ctxt;
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	40	in
59621 291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context; wenzelm parents: 59618 diff changeset	41	PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), rel')])) st
40057 b237f757b215 relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version krauss parents: 36636 diff changeset	42	end
59582 0fbed69ff081 tuned signature -- prefer qualified names; wenzelm parents: 59580 diff changeset	43	\| _ => Seq.empty);
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	44
47701 157e6108a342 more standard method setup; wenzelm parents: 42361 diff changeset	45	fun relation_infer_tac ctxt rel i =
59159 9312710451f5 just one data slot per program unit; wenzelm parents: 47701 diff changeset	46	TRY (Function_Common.termination_rule_tac ctxt i)
47701 157e6108a342 more standard method setup; wenzelm parents: 42361 diff changeset	47	THEN inst_state_infer_tac ctxt rel;
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	48
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	49	end

author	blanchet
	Mon, 16 Mar 2015 23:00:38 +0100
changeset 59725	e5dc7e7744f0
parent 59627	bb1e4a35d506
child 59968	d69dc7a133e7
permissions	-rw-r--r--