author | blanchet |
Tue, 31 Aug 2010 21:01:47 +0200 | |
changeset 38944 | 827c98e8ba8b |
parent 36960 | 01594f816e3a |
child 39048 | 4006f5c3f421 |
permissions | -rw-r--r-- |
14350 | 1 |
(* Title: HOL/Tools/refute_isar.ML |
2 |
Author: Tjark Weber |
|
22092 | 3 |
Copyright 2003-2007 |
14350 | 4 |
|
32855 | 5 |
Outer syntax commands 'refute' and 'refute_params'. |
14350 | 6 |
*) |
7 |
||
32855 | 8 |
structure Refute_Isar: sig end = |
14350 | 9 |
struct |
10 |
||
32855 | 11 |
(* argument parsing *) |
14350 | 12 |
|
32855 | 13 |
(*optional list of arguments of the form [name1=value1, name2=value2, ...]*) |
14350 | 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 | 17 |
|
18 |
||
32855 | 19 |
(* 'refute' command *) |
14350 | 20 |
|
32855 | 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 | 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 | 31 |
|
32 |
||
32855 | 33 |
(* 'refute_params' command *) |
14350 | 34 |
|
32855 | 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 | 38 |
(scan_parms >> (fn parms => |
39 |
Toplevel.theory (fn thy => |
|
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 | 42 |
val output = |
43 |
(case Refute.get_default_params thy' of |
|
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 | 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 | 48 |
|
49 |
end; |
|
50 |