src/HOL/Tools/refute.ML
changeset 39048 4006f5c3f421
parent 39047 cdff476ba39e
child 39049 423b72f2d242
--- a/src/HOL/Tools/refute.ML	Thu Sep 02 16:45:21 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Sep 02 17:12:16 2010 +0200
@@ -3257,5 +3257,47 @@
    add_printer "stlc" stlc_printer #>
    add_printer "IDT"  IDT_printer;
 
+
+
+(** outer syntax commands 'refute' and 'refute_params' **)
+
+(* argument parsing *)
+
+(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
+
+val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
+val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
+
+
+(* 'refute' command *)
+
+val _ =
+  Outer_Syntax.improper_command "refute"
+    "try to find a model that refutes a given subgoal" Keyword.diag
+    (scan_parms -- Scan.optional Parse.nat 1 >>
+      (fn (parms, i) =>
+        Toplevel.keep (fn state =>
+          let
+            val ctxt = Toplevel.context_of state;
+            val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
+          in refute_goal ctxt parms st i end)));
+
+
+(* 'refute_params' command *)
+
+val _ =
+  Outer_Syntax.command "refute_params"
+    "show/store default parameters for the 'refute' command" Keyword.thy_decl
+    (scan_parms >> (fn parms =>
+      Toplevel.theory (fn thy =>
+        let
+          val thy' = fold set_default_param parms thy;
+          val output =
+            (case get_default_params thy' of
+              [] => "none"
+            | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
+          val _ = writeln ("Default parameters for 'refute':\n" ^ output);
+        in thy' end)));
+
 end;