just one refute.ML;
authorwenzelm
Thu Sep 02 17:12:16 2010 +0200 (2010-09-02)
changeset 390484006f5c3f421
parent 39047 cdff476ba39e
child 39049 423b72f2d242
just one refute.ML;
src/HOL/IsaMakefile
src/HOL/Refute.thy
src/HOL/Tools/refute.ML
src/HOL/Tools/refute_isar.ML
     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