isabelle: src/HOL/Tools/Function/relation.ML@ac5cb4c86448 (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
41114 f9ae7c2abf7e tuned headers krauss parents: 40445 diff changeset	4	Method "relation" 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
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	10	val setup: theory -> theory
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
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	18	fun inst_state_tac inst st =
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	19	case Term.add_vars (prop_of st) [] of
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	20	[v as (_, T)] =>
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	21	let val cert = Thm.cterm_of (Thm.theory_of_thm st);
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	22	in PRIMITIVE (Thm.instantiate ([], [(cert (Var v), cert (inst T))])) st end
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	23	\| _ => Seq.empty;
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	24
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	25	fun relation_tac ctxt rel i =
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	26	TRY (Function_Common.apply_termination_rule ctxt i)
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	27	THEN inst_state_tac rel;
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	28
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	29
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	30	(* method version (with type inference) *)
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	31
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	32	fun inst_state_infer_tac ctxt 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	33	case Term.add_vars (prop_of st) [] of
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	[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	35	let
42361 23f352990944 modernized structure Proof_Context; wenzelm parents: 41114 diff changeset	36	val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	37	val rel' = singleton (Variable.polymorphic ctxt) rel
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	38	\|> map_types Type_Infer.paramify_vars
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	39	\|> Type.constraint T
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	40	\|> Syntax.check_term ctxt
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	41	\|> cert;
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	42	in
65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	43	PRIMITIVE (Thm.instantiate ([], [(cert (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	44	end
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	45	\| _ => Seq.empty;
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	46
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	47	fun relation_meth rel ctxt = SIMPLE_METHOD' (fn i =>
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 33100 diff changeset	48	TRY (Function_Common.apply_termination_rule ctxt i)
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	49	THEN inst_state_infer_tac ctxt rel);
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	50
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	51	val setup =
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	52	Method.setup @{binding relation} (Args.term >> relation_meth)
40445 65bd37d7d501 removed type-inference-like behaviour from relation_tac completely; tuned krauss parents: 40057 diff changeset	53	"proves termination using a user-specified wellfounded relation";
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	54
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	55	end

author	huffman
	Wed, 10 Aug 2011 14:10:52 -0700
changeset 44137	ac5cb4c86448
parent 42361	23f352990944
child 47701	157e6108a342
permissions	-rw-r--r--