1.1 --- a/src/HOL/IsaMakefile Thu Sep 02 16:45:21 2010 +0200
1.2 +++ b/src/HOL/IsaMakefile Thu Sep 02 17:12:16 2010 +0200
1.3 @@ -209,7 +209,6 @@
1.4 Tools/primrec.ML \
1.5 Tools/prop_logic.ML \
1.6 Tools/refute.ML \
1.7 - Tools/refute_isar.ML \
1.8 Tools/rewrite_hol_proof.ML \
1.9 Tools/sat_funcs.ML \
1.10 Tools/sat_solver.ML \
2.1 --- a/src/HOL/Refute.thy Thu Sep 02 16:45:21 2010 +0200
2.2 +++ b/src/HOL/Refute.thy Thu Sep 02 17:12:16 2010 +0200
2.3 @@ -9,9 +9,7 @@
2.4
2.5 theory Refute
2.6 imports Hilbert_Choice List
2.7 -uses
2.8 - "Tools/refute.ML"
2.9 - "Tools/refute_isar.ML"
2.10 +uses "Tools/refute.ML"
2.11 begin
2.12
2.13 setup Refute.setup
2.14 @@ -92,16 +90,14 @@
2.15 (* ------------------------------------------------------------------------- *)
2.16 (* FILES *)
2.17 (* *)
2.18 -(* HOL/Tools/prop_logic.ML Propositional logic *)
2.19 -(* HOL/Tools/sat_solver.ML SAT solvers *)
2.20 -(* HOL/Tools/refute.ML Translation HOL -> propositional logic and *)
2.21 -(* Boolean assignment -> HOL model *)
2.22 -(* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *)
2.23 -(* syntax *)
2.24 -(* HOL/Refute.thy This file: loads the ML files, basic setup, *)
2.25 -(* documentation *)
2.26 -(* HOL/SAT.thy Sets default parameters *)
2.27 -(* HOL/ex/RefuteExamples.thy Examples *)
2.28 +(* HOL/Tools/prop_logic.ML Propositional logic *)
2.29 +(* HOL/Tools/sat_solver.ML SAT solvers *)
2.30 +(* HOL/Tools/refute.ML Translation HOL -> propositional logic and *)
2.31 +(* Boolean assignment -> HOL model *)
2.32 +(* HOL/Refute.thy This file: loads the ML files, basic setup, *)
2.33 +(* documentation *)
2.34 +(* HOL/SAT.thy Sets default parameters *)
2.35 +(* HOL/ex/Refute_Examples.thy Examples *)
2.36 (* ------------------------------------------------------------------------- *)
2.37 \end{verbatim}
2.38 *}
3.1 --- a/src/HOL/Tools/refute.ML Thu Sep 02 16:45:21 2010 +0200
3.2 +++ b/src/HOL/Tools/refute.ML Thu Sep 02 17:12:16 2010 +0200
3.3 @@ -3257,5 +3257,47 @@
3.4 add_printer "stlc" stlc_printer #>
3.5 add_printer "IDT" IDT_printer;
3.6
3.7 +
3.8 +
3.9 +(** outer syntax commands 'refute' and 'refute_params' **)
3.10 +
3.11 +(* argument parsing *)
3.12 +
3.13 +(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
3.14 +
3.15 +val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
3.16 +val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
3.17 +
3.18 +
3.19 +(* 'refute' command *)
3.20 +
3.21 +val _ =
3.22 + Outer_Syntax.improper_command "refute"
3.23 + "try to find a model that refutes a given subgoal" Keyword.diag
3.24 + (scan_parms -- Scan.optional Parse.nat 1 >>
3.25 + (fn (parms, i) =>
3.26 + Toplevel.keep (fn state =>
3.27 + let
3.28 + val ctxt = Toplevel.context_of state;
3.29 + val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
3.30 + in refute_goal ctxt parms st i end)));
3.31 +
3.32 +
3.33 +(* 'refute_params' command *)
3.34 +
3.35 +val _ =
3.36 + Outer_Syntax.command "refute_params"
3.37 + "show/store default parameters for the 'refute' command" Keyword.thy_decl
3.38 + (scan_parms >> (fn parms =>
3.39 + Toplevel.theory (fn thy =>
3.40 + let
3.41 + val thy' = fold set_default_param parms thy;
3.42 + val output =
3.43 + (case get_default_params thy' of
3.44 + [] => "none"
3.45 + | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
3.46 + val _ = writeln ("Default parameters for 'refute':\n" ^ output);
3.47 + in thy' end)));
3.48 +
3.49 end;
3.50
4.1 --- a/src/HOL/Tools/refute_isar.ML Thu Sep 02 16:45:21 2010 +0200
4.2 +++ b/src/HOL/Tools/refute_isar.ML Thu Sep 02 17:12:16 2010 +0200
4.3 @@ -2,49 +2,6 @@
4.4 Author: Tjark Weber
4.5 Copyright 2003-2007
4.6
4.7 -Outer syntax commands 'refute' and 'refute_params'.
4.8 -*)
4.9 -
4.10 -structure Refute_Isar: sig end =
4.11 -struct
4.12 -
4.13 -(* argument parsing *)
4.14 -
4.15 -(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
4.16 -
4.17 -val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
4.18 -val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
4.19 -
4.20 -
4.21 -(* 'refute' command *)
4.22 -
4.23 -val _ =
4.24 - Outer_Syntax.improper_command "refute"
4.25 - "try to find a model that refutes a given subgoal" Keyword.diag
4.26 - (scan_parms -- Scan.optional Parse.nat 1 >>
4.27 - (fn (parms, i) =>
4.28 - Toplevel.keep (fn state =>
4.29 - let
4.30 - val ctxt = Toplevel.context_of state;
4.31 - val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
4.32 - in Refute.refute_goal ctxt parms st i end)));
4.33 -
4.34 -
4.35 -(* 'refute_params' command *)
4.36 -
4.37 -val _ =
4.38 - Outer_Syntax.command "refute_params"
4.39 - "show/store default parameters for the 'refute' command" Keyword.thy_decl
4.40 - (scan_parms >> (fn parms =>
4.41 - Toplevel.theory (fn thy =>
4.42 - let
4.43 - val thy' = fold Refute.set_default_param parms thy;
4.44 - val output =
4.45 - (case Refute.get_default_params thy' of
4.46 - [] => "none"
4.47 - | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
4.48 - val _ = writeln ("Default parameters for 'refute':\n" ^ output);
4.49 - in thy' end)));
4.50
4.51 end;
4.52