1.1 --- a/src/HOL/Tools/Function/relation.ML	Mon Nov 08 17:44:47 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/relation.ML	Mon Nov 08 23:02:20 2010 +0100
     1.3 @@ -7,39 +7,50 @@
     1.4  
     1.5  signature FUNCTION_RELATION =
     1.6  sig
     1.7 -  val relation_tac: Proof.context -> term -> int -> tactic
     1.8 +  val relation_tac: Proof.context -> (typ -> term) -> int -> tactic
     1.9    val setup: theory -> theory
    1.10  end
    1.11  
    1.12  structure Function_Relation : FUNCTION_RELATION =
    1.13  struct
    1.14  
    1.15 -fun gen_inst_state_tac prep ctxt rel st =
    1.16 +(* tactic version *)
    1.17 +
    1.18 +fun inst_state_tac inst st =
    1.19 +  case Term.add_vars (prop_of st) [] of
    1.20 +    [v as (_, T)] =>
    1.21 +      let val cert = Thm.cterm_of (Thm.theory_of_thm st);
    1.22 +      in PRIMITIVE (Thm.instantiate ([], [(cert (Var v), cert (inst T))])) st end
    1.23 +  | _ => Seq.empty;
    1.24 +
    1.25 +fun relation_tac ctxt rel i =
    1.26 +  TRY (Function_Common.apply_termination_rule ctxt i)
    1.27 +  THEN inst_state_tac rel;
    1.28 +
    1.29 +
    1.30 +(* method version (with type inference) *)
    1.31 +
    1.32 +fun inst_state_infer_tac ctxt rel st =
    1.33    case Term.add_vars (prop_of st) [] of
    1.34      [v as (_, T)] =>
    1.35        let
    1.36 -        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
    1.37 -        val rel' = prep T (singleton (Variable.polymorphic ctxt) rel) 
    1.38 -          |> cert
    1.39 -        val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st (*FIXME??*)
    1.40 -      in        
    1.41 -        PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
    1.42 +        val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
    1.43 +        val rel' = singleton (Variable.polymorphic ctxt) rel
    1.44 +          |> map_types Type_Infer.paramify_vars
    1.45 +          |> Type.constraint T
    1.46 +          |> Syntax.check_term ctxt
    1.47 +          |> cert;
    1.48 +      in
    1.49 +        PRIMITIVE (Thm.instantiate ([], [(cert (Var v), rel')])) st
    1.50        end
    1.51    | _ => Seq.empty;
    1.52  
    1.53 -fun gen_relation_tac prep ctxt rel i =
    1.54 +fun relation_meth rel ctxt = SIMPLE_METHOD' (fn i =>
    1.55    TRY (Function_Common.apply_termination_rule ctxt i)
    1.56 -  THEN gen_inst_state_tac prep ctxt rel
    1.57 -
    1.58 -val relation_tac = gen_relation_tac (K I)
    1.59 -
    1.60 -fun relation_meth rel ctxt = SIMPLE_METHOD' 
    1.61 -  (gen_relation_tac (fn T => map_types Type_Infer.paramify_vars
    1.62 -      #> Type.constraint T #> Syntax.check_term ctxt)
    1.63 -    ctxt rel)
    1.64 +  THEN inst_state_infer_tac ctxt rel);
    1.65  
    1.66  val setup =
    1.67    Method.setup @{binding relation} (Args.term >> relation_meth)
    1.68 -    "proves termination using a user-specified wellfounded relation"
    1.69 +    "proves termination using a user-specified wellfounded relation";
    1.70  
    1.71  end