modernized method setup;
authorwenzelm
Mon May 25 12:48:18 2009 +0200 (2009-05-25)
changeset 31241b3c7044d47b6
parent 31240 2c20bcd70fbe
child 31242 ed40b987a474
modernized method setup;
tuned signature;
src/HOL/Import/import_package.ML
src/HOL/Import/shuffler.ML
src/Tools/coherent.ML
     1.1 --- a/src/HOL/Import/import_package.ML	Mon May 25 12:46:14 2009 +0200
     1.2 +++ b/src/HOL/Import/import_package.ML	Mon May 25 12:48:18 2009 +0200
     1.3 @@ -1,13 +1,12 @@
     1.4  (*  Title:      HOL/Import/import_package.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Sebastian Skalberg (TU Muenchen)
     1.7  *)
     1.8  
     1.9  signature IMPORT_PACKAGE =
    1.10  sig
    1.11 -    val import_meth: Method.src -> Proof.context -> Proof.method
    1.12 +    val debug      : bool ref
    1.13 +    val import_tac : Proof.context -> string * string -> tactic
    1.14      val setup      : theory -> theory
    1.15 -    val debug      : bool ref
    1.16  end
    1.17  
    1.18  structure ImportData = TheoryDataFun
    1.19 @@ -25,20 +24,16 @@
    1.20  val debug = ref false
    1.21  fun message s = if !debug then writeln s else ()
    1.22  
    1.23 -val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
    1.24 -val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
    1.25 -
    1.26 -fun import_tac (thyname,thmname) =
    1.27 +fun import_tac ctxt (thyname, thmname) =
    1.28      if ! quick_and_dirty
    1.29      then SkipProof.cheat_tac
    1.30      else
    1.31 -     fn thy =>
    1.32       fn th =>
    1.33          let
    1.34 -            val sg = Thm.theory_of_thm th
    1.35 +            val thy = ProofContext.theory_of ctxt
    1.36              val prem = hd (prems_of th)
    1.37 -            val _ = message ("Import_tac: thyname="^thyname^", thmname="^thmname)
    1.38 -            val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem)))
    1.39 +            val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname)
    1.40 +            val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem)
    1.41              val int_thms = case ImportData.get thy of
    1.42                                 NONE => fst (Replay.setup_int_thms thyname thy)
    1.43                               | SOME a => a
    1.44 @@ -49,9 +44,9 @@
    1.45              val thm = equal_elim rew thm
    1.46              val prew = ProofKernel.rewrite_hol4_term prem thy
    1.47              val prem' = #2 (Logic.dest_equals (prop_of prew))
    1.48 -            val _ = message ("Import proved " ^ (string_of_thm thm))
    1.49 +            val _ = message ("Import proved " ^ Display.string_of_thm thm)
    1.50              val thm = ProofKernel.disambiguate_frees thm
    1.51 -            val _ = message ("Disambiguate: " ^ (string_of_thm thm))
    1.52 +            val _ = message ("Disambiguate: " ^ Display.string_of_thm thm)
    1.53          in
    1.54              case Shuffler.set_prop thy prem' [("",thm)] of
    1.55                  SOME (_,thm) =>
    1.56 @@ -67,15 +62,10 @@
    1.57                | NONE => (message "import: set_prop didn't succeed"; no_tac th)
    1.58          end
    1.59  
    1.60 -val import_meth = Method.simple_args (Args.name -- Args.name)
    1.61 -                  (fn arg =>
    1.62 -                   fn ctxt =>
    1.63 -                      let
    1.64 -                          val thy = ProofContext.theory_of ctxt
    1.65 -                      in
    1.66 -                          SIMPLE_METHOD (import_tac arg thy)
    1.67 -                      end)
    1.68 +val setup = Method.setup @{binding import}
    1.69 +  (Scan.lift (Args.name -- Args.name) >>
    1.70 +    (fn arg => fn ctxt => SIMPLE_METHOD (import_tac ctxt arg)))
    1.71 +  "import HOL4 theorem"
    1.72  
    1.73 -val setup = Method.add_method("import",import_meth,"Import HOL4 theorem")
    1.74  end
    1.75  
     2.1 --- a/src/HOL/Import/shuffler.ML	Mon May 25 12:46:14 2009 +0200
     2.2 +++ b/src/HOL/Import/shuffler.ML	Mon May 25 12:48:18 2009 +0200
     2.3 @@ -15,10 +15,9 @@
     2.4  
     2.5      val find_potential: theory -> term -> (string * thm) list
     2.6  
     2.7 -    val gen_shuffle_tac: theory -> bool -> (string * thm) list -> int -> tactic
     2.8 -
     2.9 -    val shuffle_tac: (string * thm) list -> int -> tactic
    2.10 -    val search_tac : (string * thm) list -> int -> tactic
    2.11 +    val gen_shuffle_tac: Proof.context -> bool -> (string * thm) list -> int -> tactic
    2.12 +    val shuffle_tac: Proof.context -> thm list -> int -> tactic
    2.13 +    val search_tac : Proof.context -> int -> tactic
    2.14  
    2.15      val print_shuffles: theory -> unit
    2.16  
    2.17 @@ -631,8 +630,9 @@
    2.18          List.filter (match_consts ignored t) all_thms
    2.19      end
    2.20  
    2.21 -fun gen_shuffle_tac thy search thms i st =
    2.22 +fun gen_shuffle_tac ctxt search thms i st =
    2.23      let
    2.24 +        val thy = ProofContext.theory_of ctxt
    2.25          val _ = message ("Shuffling " ^ (string_of_thm st))
    2.26          val t = List.nth(prems_of st,i-1)
    2.27          val set = set_prop thy t
    2.28 @@ -646,26 +646,8 @@
    2.29                                    else no_tac)) st
    2.30      end
    2.31  
    2.32 -fun shuffle_tac thms i st =
    2.33 -    gen_shuffle_tac (the_context()) false thms i st
    2.34 -
    2.35 -fun search_tac thms i st =
    2.36 -    gen_shuffle_tac (the_context()) true thms i st
    2.37 -
    2.38 -fun shuffle_meth (thms:thm list) ctxt =
    2.39 -    let
    2.40 -        val thy = ProofContext.theory_of ctxt
    2.41 -    in
    2.42 -        SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms))
    2.43 -    end
    2.44 -
    2.45 -fun search_meth ctxt =
    2.46 -    let
    2.47 -        val thy = ProofContext.theory_of ctxt
    2.48 -        val prems = Assumption.all_prems_of ctxt
    2.49 -    in
    2.50 -        SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
    2.51 -    end
    2.52 +fun shuffle_tac ctxt thms = gen_shuffle_tac ctxt false (map (pair "") thms);
    2.53 +fun search_tac ctxt = gen_shuffle_tac thy true (map (pair "premise") (Assumption.all_prems_of ctxt);
    2.54  
    2.55  fun add_shuffle_rule thm thy =
    2.56      let
    2.57 @@ -680,10 +662,11 @@
    2.58  val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
    2.59  
    2.60  val setup =
    2.61 -  Method.add_method ("shuffle_tac",
    2.62 -    Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
    2.63 -  Method.add_method ("search_tac",
    2.64 -    Method.ctxt_args search_meth,"search for suitable theorems") #>
    2.65 +  Method.setup @{binding shuffle_tac}
    2.66 +    (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (shuffle_tac ctxt thms)))
    2.67 +    "solve goal by shuffling terms around" #>
    2.68 +  Method.setup @{binding search_tac}
    2.69 +    (Scan.succeed (SIMPLE_METHOD' o search_tac)) "search for suitable theorems" #>
    2.70    add_shuffle_rule weaken #>
    2.71    add_shuffle_rule equiv_comm #>
    2.72    add_shuffle_rule imp_comm #>
     3.1 --- a/src/Tools/coherent.ML	Mon May 25 12:46:14 2009 +0200
     3.2 +++ b/src/Tools/coherent.ML	Mon May 25 12:48:18 2009 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  (*  Title:      Tools/coherent.ML
     3.5      Author:     Stefan Berghofer, TU Muenchen
     3.6 -    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
     3.7 +    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen
     3.8  
     3.9  Prover for coherent logic, see e.g.
    3.10  
    3.11 @@ -22,14 +22,15 @@
    3.12  sig
    3.13    val verbose: bool ref
    3.14    val show_facts: bool ref
    3.15 -  val coherent_tac: thm list -> Proof.context -> int -> tactic
    3.16 -  val coherent_meth: thm list -> Proof.context -> Proof.method
    3.17 +  val coherent_tac: Proof.context -> thm list -> int -> tactic
    3.18    val setup: theory -> theory
    3.19  end;
    3.20  
    3.21  functor CoherentFun(Data: COHERENT_DATA) : COHERENT =
    3.22  struct
    3.23  
    3.24 +(** misc tools **)
    3.25 +
    3.26  val verbose = ref false;
    3.27  
    3.28  fun message f = if !verbose then tracing (f ()) else ();
    3.29 @@ -170,6 +171,7 @@
    3.30            | SOME prfs => SOME ((params, prf) :: prfs))
    3.31        end;
    3.32  
    3.33 +
    3.34  (** proof replaying **)
    3.35  
    3.36  fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
    3.37 @@ -210,7 +212,7 @@
    3.38  
    3.39  (** external interface **)
    3.40  
    3.41 -fun coherent_tac rules ctxt = SUBPROOF (fn {prems, concl, params, context, ...} =>
    3.42 +fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
    3.43    rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
    3.44    SUBPROOF (fn {prems = prems', concl, context, ...} =>
    3.45      let val xs = map term_of params @
    3.46 @@ -224,10 +226,9 @@
    3.47             rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1
    3.48      end) context 1) ctxt;
    3.49  
    3.50 -fun coherent_meth rules ctxt =
    3.51 -  METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
    3.52 -
    3.53 -val setup = Method.add_method
    3.54 -  ("coherent", Method.thms_ctxt_args coherent_meth, "prove coherent formula");
    3.55 +val setup = Method.setup @{binding coherent}
    3.56 +  (Attrib.thms >> (fn rules => fn ctxt =>
    3.57 +      METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
    3.58 +    "prove coherent formula";
    3.59  
    3.60  end;