isabelle: src/HOL/Tools/Function/relation.ML@6a53d57fa902 (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
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	4	A package for general recursive function definitions.
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	5	Method "relation" to commence a termination proof using a user-specified relation.
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	6	*)
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	7
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	8	signature FUNCTION_RELATION =
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	9	sig
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	10	val relation_tac: Proof.context -> term -> int -> tactic
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	11	val setup: theory -> theory
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	12	end
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	13
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	14	structure Function_Relation : FUNCTION_RELATION =
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	15	struct
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	16
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	17	fun gen_inst_state_tac prep ctxt rel st =
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	18	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	19	[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	20	let
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	21	val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
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	22	val rel' = prep T (singleton (Variable.polymorphic ctxt) rel)
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	23	\|> cert
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	24	val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st (FIXME??)
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	25	in
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	26	PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
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	27	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	28	\| _ => Seq.empty;
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	29
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	30	fun gen_relation_tac prep ctxt rel i =
34232 36a2a3029fd3 new year's resolution: reindented code in function package krauss parents: 33100 diff changeset	31	TRY (Function_Common.apply_termination_rule ctxt i)
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	32	THEN gen_inst_state_tac prep ctxt rel
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
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	val relation_tac = gen_relation_tac (K I)
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
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	36	fun relation_meth rel ctxt = SIMPLE_METHOD'
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	37	(gen_relation_tac (fn T => map_types Type_Infer.paramify_vars
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	38	#> Type.constraint T #> Syntax.check_term ctxt)
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	39	ctxt rel)
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	40
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	41	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	42	Method.setup @{binding relation} (Args.term >> relation_meth)
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	43	"proves termination using a user-specified wellfounded relation"
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	44
acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: diff changeset	45	end

author	bulwahn
	Mon, 25 Oct 2010 21:17:14 +0200
changeset 40139	6a53d57fa902
parent 40057	b237f757b215
child 40445	65bd37d7d501
permissions	-rw-r--r--