src/HOL/Tools/Function/relation.ML

made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded

(*  Title:      HOL/Tools/Function/relation.ML
    Author:     Alexander Krauss, TU Muenchen

Method "relation" to start a termination proof using a user-specified relation.
*)

signature FUNCTION_RELATION =
sig
  val relation_tac: Proof.context -> (typ -> term) -> int -> tactic
  val setup: theory -> theory
end

structure Function_Relation : FUNCTION_RELATION =
struct

(* tactic version *)

fun inst_state_tac inst st =
  case Term.add_vars (prop_of st) [] of
    [v as (_, T)] =>
      let val cert = Thm.cterm_of (Thm.theory_of_thm st);
      in PRIMITIVE (Thm.instantiate ([], [(cert (Var v), cert (inst T))])) st end
  | _ => Seq.empty;

fun relation_tac ctxt rel i =
  TRY (Function_Common.apply_termination_rule ctxt i)
  THEN inst_state_tac rel;


(* method version (with type inference) *)

fun inst_state_infer_tac ctxt rel st =
  case Term.add_vars (prop_of st) [] of
    [v as (_, T)] =>
      let
        val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
        val rel' = singleton (Variable.polymorphic ctxt) rel
          |> map_types Type_Infer.paramify_vars
          |> Type.constraint T
          |> Syntax.check_term ctxt
          |> cert;
      in
        PRIMITIVE (Thm.instantiate ([], [(cert (Var v), rel')])) st
      end
  | _ => Seq.empty;

fun relation_meth rel ctxt = SIMPLE_METHOD' (fn i =>
  TRY (Function_Common.apply_termination_rule ctxt i)
  THEN inst_state_infer_tac ctxt rel);

val setup =
  Method.setup @{binding relation} (Args.term >> relation_meth)
    "proves termination using a user-specified wellfounded relation";

end