src/HOL/Tools/refute_isar.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 36960 01594f816e3a
child 39048 4006f5c3f421
permissions -rw-r--r--
tuned titles
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
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 34120
diff changeset
    15
val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 34120
diff changeset
    16
val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    17
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    18
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    19
(* 'refute' command *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    20
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    21
val _ =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 34120
diff changeset
    22
  Outer_Syntax.improper_command "refute"
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 34120
diff changeset
    23
    "try to find a model that refutes a given subgoal" Keyword.diag
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 34120
diff changeset
    24
    (scan_parms -- Scan.optional Parse.nat 1 >>
32857
394d37f19e0a Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents: 32855
diff changeset
    25
      (fn (parms, i) =>
394d37f19e0a Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents: 32855
diff changeset
    26
        Toplevel.keep (fn state =>
394d37f19e0a Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents: 32855
diff changeset
    27
          let
34120
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 33291
diff changeset
    28
            val ctxt = Toplevel.context_of state;
33291
93f0238151f6 back to Proof.raw_goal;
wenzelm
parents: 32857
diff changeset
    29
            val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
34120
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 33291
diff changeset
    30
          in Refute.refute_goal ctxt parms st i end)));
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    31
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    32
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    33
(* 'refute_params' command *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    34
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    35
val _ =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 34120
diff changeset
    36
  Outer_Syntax.command "refute_params"
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 34120
diff changeset
    37
    "show/store default parameters for the 'refute' command" Keyword.thy_decl
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    38
    (scan_parms >> (fn parms =>
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    39
      Toplevel.theory (fn thy =>
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    40
        let
32857
394d37f19e0a Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents: 32855
diff changeset
    41
          val thy' = fold Refute.set_default_param parms thy;
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    42
          val output =
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    43
            (case Refute.get_default_params thy' of
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    44
              [] => "none"
32857
394d37f19e0a Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents: 32855
diff changeset
    45
            | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    46
          val _ = writeln ("Default parameters for 'refute':\n" ^ output);
32857
394d37f19e0a Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents: 32855
diff changeset
    47
        in thy' end)));
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    48
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    49
end;
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    50