src/HOL/Tools/refute_isar.ML
author blanchet
Mon, 14 Dec 2009 12:14:12 +0100
changeset 34120 f9920a3ddf50
parent 33291 93f0238151f6
child 36960 01594f816e3a
permissions -rw-r--r--
added "no_assms" option to Refute, and include structured proof assumptions by default; will do the same for Quickcheck unless there are objections
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
34120
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 33291
diff changeset
    15
val scan_parm =
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 33291
diff changeset
    16
  OuterParse.name
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 33291
diff changeset
    17
  -- (Scan.optional (OuterParse.$$$ "=" |-- OuterParse.name) "true")
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    18
val scan_parms = Scan.optional
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    19
  (OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    20
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    21
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    22
(* 'refute' command *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    23
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    24
val _ =
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    25
  OuterSyntax.improper_command "refute"
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    26
    "try to find a model that refutes a given subgoal" OuterKeyword.diag
32857
394d37f19e0a Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents: 32855
diff changeset
    27
    (scan_parms -- Scan.optional OuterParse.nat 1 >>
394d37f19e0a Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents: 32855
diff changeset
    28
      (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
    29
        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
    30
          let
34120
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 33291
diff changeset
    31
            val ctxt = Toplevel.context_of state;
33291
93f0238151f6 back to Proof.raw_goal;
wenzelm
parents: 32857
diff changeset
    32
            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
    33
          in Refute.refute_goal ctxt parms st i 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
32857
394d37f19e0a Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents: 32855
diff changeset
    44
          val thy' = fold Refute.set_default_param parms thy;
32855
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"
32857
394d37f19e0a Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents: 32855
diff changeset
    48
            | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
32855
7da2447fadf2 misc tuning and simplification;
wenzelm
parents: 26931
diff changeset
    49
          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
    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