added 'algebra' to the mix
authorblanchet
Fri Jan 31 18:43:16 2014 +0100 (2014-01-31)
changeset 552196fe9fd75f9d7
parent 55218 ed495a5088c6
child 55220 9d833fe96c51
added 'algebra' to the mix
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
     1.3 @@ -191,11 +191,11 @@
     1.4  
     1.5  val arith_methodss =
     1.6    [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
     1.7 -    Metis_Method], [Meson_Method]]
     1.8 -val datatype_methodss = [[Simp_Size_Method, Simp_Method]]
     1.9 +    Algebra_Method], [Metis_Method], [Meson_Method]]
    1.10 +val datatype_methodss = [[Simp_Method], [Simp_Size_Method]]
    1.11  val metislike_methodss =
    1.12    [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
    1.13 -    Force_Method], [Meson_Method]]
    1.14 +    Force_Method, Algebra_Method], [Meson_Method]]
    1.15  val rewrite_methodss =
    1.16    [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
    1.17  val skolem_methodss = [[Metis_Method, Blast_Method], [Meson_Method]]
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 18:43:16 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 18:43:16 2014 +0100
     2.3 @@ -101,6 +101,7 @@
     2.4      | Force_Method => Clasimp.force_tac ctxt
     2.5      | Arith_Method => Arith_Data.arith_tac ctxt
     2.6      | Blast_Method => blast_tac ctxt
     2.7 +    | Algebra_Method => Groebner.algebra_tac [] [] ctxt
     2.8      | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
     2.9  
    2.10  (* main function for preplaying Isar steps; may throw exceptions *)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
     3.3 @@ -15,7 +15,7 @@
     3.4  
     3.5    datatype proof_method =
     3.6      Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
     3.7 -    Arith_Method | Blast_Method | Meson_Method
     3.8 +    Arith_Method | Blast_Method | Meson_Method | Algebra_Method
     3.9  
    3.10    datatype isar_proof =
    3.11      Proof of (string * typ) list * (label * term) list * isar_step list
    3.12 @@ -66,7 +66,7 @@
    3.13  
    3.14  datatype proof_method =
    3.15    Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
    3.16 -  Arith_Method | Blast_Method | Meson_Method
    3.17 +  Arith_Method | Blast_Method | Meson_Method | Algebra_Method
    3.18  
    3.19  datatype isar_proof =
    3.20    Proof of (string * typ) list * (label * term) list * isar_step list
    3.21 @@ -92,7 +92,8 @@
    3.22    | Force_Method => "force"
    3.23    | Arith_Method => "arith"
    3.24    | Blast_Method => "blast"
    3.25 -  | Meson_Method => "meson")
    3.26 +  | Meson_Method => "meson"
    3.27 +  | Algebra_Method => "algebra")
    3.28  
    3.29  fun steps_of_proof (Proof (_, _, steps)) = steps
    3.30