src/Tools/coherent.ML
changeset 31241 b3c7044d47b6
parent 30552 58db56278478
child 31855 7c2a5e79a654
     1.1 --- a/src/Tools/coherent.ML	Mon May 25 12:46:14 2009 +0200
     1.2 +++ b/src/Tools/coherent.ML	Mon May 25 12:48:18 2009 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      Tools/coherent.ML
     1.5      Author:     Stefan Berghofer, TU Muenchen
     1.6 -    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
     1.7 +    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen
     1.8  
     1.9  Prover for coherent logic, see e.g.
    1.10  
    1.11 @@ -22,14 +22,15 @@
    1.12  sig
    1.13    val verbose: bool ref
    1.14    val show_facts: bool ref
    1.15 -  val coherent_tac: thm list -> Proof.context -> int -> tactic
    1.16 -  val coherent_meth: thm list -> Proof.context -> Proof.method
    1.17 +  val coherent_tac: Proof.context -> thm list -> int -> tactic
    1.18    val setup: theory -> theory
    1.19  end;
    1.20  
    1.21  functor CoherentFun(Data: COHERENT_DATA) : COHERENT =
    1.22  struct
    1.23  
    1.24 +(** misc tools **)
    1.25 +
    1.26  val verbose = ref false;
    1.27  
    1.28  fun message f = if !verbose then tracing (f ()) else ();
    1.29 @@ -170,6 +171,7 @@
    1.30            | SOME prfs => SOME ((params, prf) :: prfs))
    1.31        end;
    1.32  
    1.33 +
    1.34  (** proof replaying **)
    1.35  
    1.36  fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
    1.37 @@ -210,7 +212,7 @@
    1.38  
    1.39  (** external interface **)
    1.40  
    1.41 -fun coherent_tac rules ctxt = SUBPROOF (fn {prems, concl, params, context, ...} =>
    1.42 +fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
    1.43    rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
    1.44    SUBPROOF (fn {prems = prems', concl, context, ...} =>
    1.45      let val xs = map term_of params @
    1.46 @@ -224,10 +226,9 @@
    1.47             rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1
    1.48      end) context 1) ctxt;
    1.49  
    1.50 -fun coherent_meth rules ctxt =
    1.51 -  METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
    1.52 -
    1.53 -val setup = Method.add_method
    1.54 -  ("coherent", Method.thms_ctxt_args coherent_meth, "prove coherent formula");
    1.55 +val setup = Method.setup @{binding coherent}
    1.56 +  (Attrib.thms >> (fn rules => fn ctxt =>
    1.57 +      METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
    1.58 +    "prove coherent formula";
    1.59  
    1.60  end;