# HG changeset patch
# User bulwahn
# Date 1291629163 -3600
# Node ID 6604115019bf1f3bfa8e379580dd5a352924a523
# Parent  3208d3b0a3ddc9baf6f8c2c25d055b0df92c0749
adding filtering, sytactic welltyping, and sledgehammer method in mutabelle

diff -r 3208d3b0a3dd -r 6604115019bf src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Dec 06 09:34:57 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Dec 06 10:52:43 2010 +0100
@@ -24,6 +24,9 @@
 
 val solve_direct_mtd : mtd
 val try_mtd : mtd
+
+val sledgehammer_mtd : mtd
+
 (*
 val refute_mtd : mtd
 val nitpick_mtd : mtd
@@ -143,7 +146,7 @@
 
 fun invoke_try thy t =
   let
-    val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) 
+    val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
   in
     case Try.invoke_try NONE state of
       true => (Solved, ([], NONE))
@@ -152,6 +155,17 @@
 
 val try_mtd = ("try", invoke_try)
 
+(** sledgehammer **)
+
+fun invoke_sledgehammer thy t =
+  if can (Goal.prove_global thy (Term.add_free_names t [])  [] t)
+      (fn {context, ...} => Sledgehammer_Tactics.sledgehammer_with_metis_tac context 1) then
+    (Solved, ([], NONE))
+  else
+    (Unsolved, ([], NONE))
+
+val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer)
+
 (*
 fun invoke_refute thy t =
   let
@@ -287,7 +301,14 @@
  @{const_name "Pure.term"},
  @{const_name "top_class.top"},
  (*@{const_name "HOL.equal"},*)
- @{const_name "Quotient.Quot_True"}
+ @{const_name "Quotient.Quot_True"},
+ @{const_name "equal_fun_inst.equal_fun"},
+ @{const_name "equal_bool_inst.equal_bool"},
+ @{const_name "ord_fun_inst.less_eq_fun"},
+ @{const_name "ord_fun_inst.less_fun"},
+ @{const_name Metis.fequal},
+ @{const_name Meson.skolem},
+ @{const_name transfer_morphism}
  (*@{const_name "==>"}, @{const_name "=="}*)]
 
 val forbidden_mutant_consts =
@@ -426,11 +447,12 @@
       else
         mutants
     val mutants = mutants
-          |> take_random max_mutants
           |> map Mutabelle.freeze |> map freezeT
 (*          |> filter (not o is_forbidden_mutant) *)
           |> List.mapPartial (try (Sign.cert_term thy))
-          |> List.filter (is_some o try (cterm_of thy))
+          |> List.filter (is_some o try (Thm.cterm_of thy))
+          |> List.filter (is_some o try (Syntax.check_term (ProofContext.init_global thy)))
+          |> take_random max_mutants
     val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
   in
     create_entry thy thm exec mutants mtds