1(*  Title:      HOL/Tools/Function/relation.ML
2    Author:     Alexander Krauss, TU Muenchen
3
4Tactics to start a termination proof using a user-specified relation.
5*)
6
7signature FUNCTION_RELATION =
8sig
9  val relation_tac: Proof.context -> (typ -> term) -> int -> tactic
10  val relation_infer_tac: Proof.context -> term -> int -> tactic
11end
12
13structure Function_Relation: FUNCTION_RELATION =
14struct
15
16(* tactic version *)
17
18fun inst_state_tac ctxt inst =
19  SUBGOAL (fn (goal, _) =>
20    (case Term.add_vars goal [] of
21      [v as (_, T)] => PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (inst T))]))
22    | _ => no_tac));
23
24fun relation_tac ctxt rel i =
25  TRY (Function_Common.termination_rule_tac ctxt i)
26  THEN inst_state_tac ctxt rel i;
27
28
29(* version with type inference *)
30
31fun inst_state_infer_tac ctxt rel =
32  SUBGOAL (fn (goal, _) =>
33    (case Term.add_vars goal [] of
34      [v as (_, T)] =>
35        let
36          val rel' =
37            singleton (Variable.polymorphic ctxt) rel
38            |> map_types Type_Infer.paramify_vars
39            |> Type.constraint T
40            |> Syntax.check_term ctxt;
41        in PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt rel')])) end
42    | _ => no_tac));
43
44fun relation_infer_tac ctxt rel i =
45  TRY (Function_Common.termination_rule_tac ctxt i)
46  THEN inst_state_infer_tac ctxt rel i;
47
48end
49