isabelle: src/HOL/Tools/Function/relation.ML@3e84f4e9651a (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
59968 d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	13	structure Function_Relation: FUNCTION_RELATION =
33100 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
59968 d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	18	fun inst_state_tac ctxt inst =
d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	19	SUBGOAL (fn (goal, _) =>
d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	20	(case Term.add_vars goal [] of
60642 48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored); wenzelm parents: 59968 diff changeset	21	[v as (_, T)] => PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (inst T))]))
59968 d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	22	\| _ => no_tac));
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)
59968 d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	26	THEN inst_state_tac ctxt rel i;
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
59968 d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	31	fun inst_state_infer_tac ctxt rel =
d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	32	SUBGOAL (fn (goal, _) =>
d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	33	(case Term.add_vars goal [] of
d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	34	[v as (_, T)] =>
d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	35	let
d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	36	val rel' =
d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	37	singleton (Variable.polymorphic ctxt) rel
d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	38	\|> map_types Type_Infer.paramify_vars
d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	39	\|> Type.constraint T
d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	40	\|> Syntax.check_term ctxt;
60642 48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored); wenzelm parents: 59968 diff changeset	41	in PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt rel')])) end
59968 d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	42	\| _ => no_tac));
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	43
47701 157e6108a342 more standard method setup; wenzelm parents: 42361 diff changeset	44	fun relation_infer_tac ctxt rel i =
59159 9312710451f5 just one data slot per program unit; wenzelm parents: 47701 diff changeset	45	TRY (Function_Common.termination_rule_tac ctxt i)
59968 d69dc7a133e7 more standard access to specific subgoal; wenzelm parents: 59627 diff changeset	46	THEN inst_state_infer_tac ctxt rel i;
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	47
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	48	end

author	wenzelm
	Sat, 03 Oct 2020 21:54:53 +0200
changeset 72371	3e84f4e9651a
parent 60642	48dd1cefb4ae
child 74282	c2ee8d993d6a
permissions	-rw-r--r--