author bulwahn Mon, 06 Dec 2010 10:52:43 +0100 changeset 40971 6604115019bf parent 40970 3208d3b0a3dd child 40972 ce78ef6a909b
adding filtering, sytactic welltyping, and sledgehammer method in mutabelle
```--- 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```