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