factor out "Meson_Tactic" from "Meson_Clausify"
authorblanchet
Tue Oct 05 10:28:11 2010 +0200 (2010-10-05)
changeset 39948317010af8972
parent 39947 f95834c8bb4d
child 39949 186a3b447e0b
factor out "Meson_Tactic" from "Meson_Clausify"
src/HOL/IsaMakefile
src/HOL/Meson.thy
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Meson/meson_tactic.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Oct 04 22:51:53 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Oct 05 10:28:11 2010 +0200
     1.3 @@ -205,6 +205,7 @@
     1.4    Tools/lin_arith.ML \
     1.5    Tools/Meson/meson.ML \
     1.6    Tools/Meson/meson_clausify.ML \
     1.7 +  Tools/Meson/meson_tactic.ML \
     1.8    Tools/Metis/metis_reconstruct.ML \
     1.9    Tools/Metis/metis_translate.ML \
    1.10    Tools/Metis/metis_tactics.ML \
     2.1 --- a/src/HOL/Meson.thy	Mon Oct 04 22:51:53 2010 +0200
     2.2 +++ b/src/HOL/Meson.thy	Tue Oct 05 10:28:11 2010 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  imports Datatype
     2.5  uses ("Tools/Meson/meson.ML")
     2.6       ("Tools/Meson/meson_clausify.ML")
     2.7 +     ("Tools/Meson/meson_tactic.ML")
     2.8  begin
     2.9  
    2.10  section {* Negation Normal Form *}
    2.11 @@ -197,11 +198,12 @@
    2.12  
    2.13  use "Tools/Meson/meson.ML"
    2.14  use "Tools/Meson/meson_clausify.ML"
    2.15 +use "Tools/Meson/meson_tactic.ML"
    2.16  
    2.17  setup {*
    2.18    Meson_Choices.setup
    2.19    #> Meson.setup
    2.20 -  #> Meson_Clausify.setup
    2.21 +  #> Meson_Tactic.setup
    2.22  *}
    2.23  
    2.24  end
     3.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon Oct 04 22:51:53 2010 +0200
     3.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:28:11 2010 +0200
     3.3 @@ -3,7 +3,6 @@
     3.4      Author:     Jasmin Blanchette, TU Muenchen
     3.5  
     3.6  Transformation of HOL theorems into CNF forms.
     3.7 -The "meson" proof method for HOL.
     3.8  *)
     3.9  
    3.10  signature MESON_CLAUSIFY =
    3.11 @@ -16,8 +15,6 @@
    3.12    val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
    3.13    val cnf_axiom :
    3.14      Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
    3.15 -  val meson_general_tac : Proof.context -> thm list -> int -> tactic
    3.16 -  val setup: theory -> theory
    3.17  end;
    3.18  
    3.19  structure Meson_Clausify : MESON_CLAUSIFY =
    3.20 @@ -365,14 +362,4 @@
    3.21    end
    3.22    handle THM _ => (NONE, [])
    3.23  
    3.24 -fun meson_general_tac ctxt ths =
    3.25 -  let val ctxt = Classical.put_claset HOL_cs ctxt in
    3.26 -    Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths)
    3.27 -  end
    3.28 -
    3.29 -val setup =
    3.30 -  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
    3.31 -     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
    3.32 -     "MESON resolution proof procedure"
    3.33 -
    3.34  end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Meson/meson_tactic.ML	Tue Oct 05 10:28:11 2010 +0200
     4.3 @@ -0,0 +1,29 @@
     4.4 +(*  Title:      HOL/Tools/Meson/meson_tactic.ML
     4.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     4.6 +    Author:     Jasmin Blanchette, TU Muenchen
     4.7 +
     4.8 +The "meson" proof method for HOL.
     4.9 +*)
    4.10 +
    4.11 +signature MESON_TACTIC =
    4.12 +sig
    4.13 +  val meson_general_tac : Proof.context -> thm list -> int -> tactic
    4.14 +  val setup: theory -> theory
    4.15 +end;
    4.16 +
    4.17 +structure Meson_Tactic : MESON_TACTIC =
    4.18 +struct
    4.19 +
    4.20 +open Meson_Clausify
    4.21 +
    4.22 +fun meson_general_tac ctxt ths =
    4.23 +  let val ctxt = Classical.put_claset HOL_cs ctxt in
    4.24 +    Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths)
    4.25 +  end
    4.26 +
    4.27 +val setup =
    4.28 +  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
    4.29 +     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
    4.30 +     "MESON resolution proof procedure"
    4.31 +
    4.32 +end;