src/HOL/Tools/refute_isar.ML
author wenzelm
Fri, 02 Oct 2009 20:51:32 +0200
changeset 32855 7da2447fadf2
parent 26931 aa226d8405a8
child 32857 394d37f19e0a
permissions -rw-r--r--
misc tuning and simplification;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     1
(*  Title:      HOL/Tools/refute_isar.ML
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     2
    Author:     Tjark Weber
22092
ab3dfcef6489 reformatted to 80 chars/line
webertj
parents: 17273
diff changeset
     3
    Copyright   2003-2007
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     4
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
     5
Outer syntax commands 'refute' and 'refute_params'.
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     6
*)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     7
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
     8
structure Refute_Isar: sig end =
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     9
struct
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    10
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    11
(* argument parsing *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    12
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    13
(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    14
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    15
val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    16
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    17
val scan_parms = Scan.optional
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    18
  (OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    19
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    20
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    21
(* 'refute' command *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    22
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    23
val _ =
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    24
  OuterSyntax.improper_command "refute"
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    25
    "try to find a model that refutes a given subgoal" OuterKeyword.diag
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    26
    (scan_parms -- Scan.optional OuterParse.nat 1 >> (fn (parms, subgoal) =>
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    27
      Toplevel.keep (fn state =>
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    28
        let
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    29
          val thy = Toplevel.theory_of state
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    30
          val st = (snd o snd) (Proof.get_goal (Toplevel.proof_of state))
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    31
        in
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    32
          Refute.refute_subgoal thy parms st (subgoal - 1)
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    33
        end)));
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    34
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    35
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    36
(* 'refute_params' command *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    37
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    38
val _ =
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    39
  OuterSyntax.command "refute_params"
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    40
    "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    41
    (scan_parms >> (fn parms =>
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    42
      Toplevel.theory (fn thy =>
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    43
        let
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    44
          val thy' = fold Refute.set_default_param parms thy
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    45
          val output =
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    46
            (case Refute.get_default_params thy' of
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    47
              [] => "none"
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    48
            | new_defaults => cat_lines (map (fn (name, value) => name ^ "=" ^ value) new_defaults))
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    49
          val _ = writeln ("Default parameters for 'refute':\n" ^ output);
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    50
        in thy' end)))
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    51
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    52
end;
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    53