src/HOL/Tools/refute_isar.ML
author Philipp Meyer
Wed Sep 30 11:33:59 2009 +0200 (2009-09-30)
changeset 32866 1238cbb7c08f
parent 32857 394d37f19e0a
child 33291 93f0238151f6
permissions -rw-r--r--
atp_minimal using chain_ths again
webertj@14350
     1
(*  Title:      HOL/Tools/refute_isar.ML
webertj@14350
     2
    Author:     Tjark Weber
webertj@22092
     3
    Copyright   2003-2007
webertj@14350
     4
wenzelm@32855
     5
Outer syntax commands 'refute' and 'refute_params'.
webertj@14350
     6
*)
webertj@14350
     7
wenzelm@32855
     8
structure Refute_Isar: sig end =
webertj@14350
     9
struct
webertj@14350
    10
wenzelm@32855
    11
(* argument parsing *)
webertj@14350
    12
wenzelm@32855
    13
(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
webertj@14350
    14
wenzelm@32855
    15
val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
webertj@14350
    16
wenzelm@32855
    17
val scan_parms = Scan.optional
wenzelm@32855
    18
  (OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
webertj@14350
    19
webertj@14350
    20
wenzelm@32855
    21
(* 'refute' command *)
webertj@14350
    22
wenzelm@32855
    23
val _ =
wenzelm@32855
    24
  OuterSyntax.improper_command "refute"
wenzelm@32855
    25
    "try to find a model that refutes a given subgoal" OuterKeyword.diag
wenzelm@32857
    26
    (scan_parms -- Scan.optional OuterParse.nat 1 >>
wenzelm@32857
    27
      (fn (parms, i) =>
wenzelm@32857
    28
        Toplevel.keep (fn state =>
wenzelm@32857
    29
          let
wenzelm@32857
    30
            val thy = Toplevel.theory_of state;
wenzelm@32857
    31
            val (_, st) = Proof.flat_goal (Toplevel.proof_of state);
wenzelm@32857
    32
          in Refute.refute_goal thy parms st i end)));
webertj@14350
    33
webertj@14350
    34
wenzelm@32855
    35
(* 'refute_params' command *)
webertj@14350
    36
wenzelm@32855
    37
val _ =
wenzelm@32855
    38
  OuterSyntax.command "refute_params"
wenzelm@32855
    39
    "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl
wenzelm@32855
    40
    (scan_parms >> (fn parms =>
wenzelm@32855
    41
      Toplevel.theory (fn thy =>
wenzelm@32855
    42
        let
wenzelm@32857
    43
          val thy' = fold Refute.set_default_param parms thy;
wenzelm@32855
    44
          val output =
wenzelm@32855
    45
            (case Refute.get_default_params thy' of
wenzelm@32855
    46
              [] => "none"
wenzelm@32857
    47
            | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
wenzelm@32855
    48
          val _ = writeln ("Default parameters for 'refute':\n" ^ output);
wenzelm@32857
    49
        in thy' end)));
webertj@14350
    50
webertj@14350
    51
end;
webertj@14350
    52