# HG changeset patch # User wenzelm # Date 1289297835 -3600 # Node ID 27c1a1c82eba77691b94fa5bc06d1f3a87295cba # Parent 65bd37d7d5010d8e158214887539a3afa1da8a65# Parent 020c16837866a96f797c61079d90a1e6ce89b8d9 merged diff -r 020c16837866 -r 27c1a1c82eba src/HOL/Tools/Function/relation.ML --- a/src/HOL/Tools/Function/relation.ML Mon Nov 08 20:55:27 2010 +0100 +++ b/src/HOL/Tools/Function/relation.ML Tue Nov 09 11:17:15 2010 +0100 @@ -7,39 +7,50 @@ signature FUNCTION_RELATION = sig - val relation_tac: Proof.context -> term -> int -> tactic + val relation_tac: Proof.context -> (typ -> term) -> int -> tactic val setup: theory -> theory end structure Function_Relation : FUNCTION_RELATION = struct -fun gen_inst_state_tac prep ctxt rel st = +(* 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 (ProofContext.theory_of ctxt) - val rel' = prep T (singleton (Variable.polymorphic ctxt) rel) - |> cert - val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st (*FIXME??*) - in - PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st' + val cert = Thm.cterm_of (ProofContext.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 gen_relation_tac prep ctxt rel i = +fun relation_meth rel ctxt = SIMPLE_METHOD' (fn i => TRY (Function_Common.apply_termination_rule ctxt i) - THEN gen_inst_state_tac prep ctxt rel - -val relation_tac = gen_relation_tac (K I) - -fun relation_meth rel ctxt = SIMPLE_METHOD' - (gen_relation_tac (fn T => map_types Type_Infer.paramify_vars - #> Type.constraint T #> Syntax.check_term ctxt) - ctxt rel) + 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" + "proves termination using a user-specified wellfounded relation"; end