src/HOL/Tools/refute_isar.ML
author haftmann
Fri Dec 16 09:00:11 2005 +0100 (2005-12-16)
changeset 18418 bf448d999b7e
parent 17273 e95f7141ba2f
child 22092 ab3dfcef6489
permissions -rw-r--r--
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
     1 (*  Title:      HOL/Tools/refute_isar.ML
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2003-2005
     5 
     6 Adds the 'refute' and 'refute_params' commands to Isabelle/Isar's outer
     7 syntax.
     8 *)
     9 
    10 structure RefuteIsar =
    11 struct
    12 
    13 (* ------------------------------------------------------------------------- *)
    14 (* common functions for argument parsing/scanning                            *)
    15 (* ------------------------------------------------------------------------- *)
    16 
    17 (* ------------------------------------------------------------------------- *)
    18 (* both 'refute' and 'refute_params' take an optional list of arguments of   *)
    19 (* the form [name1=value1, name2=value2, ...]                                *)
    20 (* ------------------------------------------------------------------------- *)
    21 
    22 	fun repeatd delim scan = scan -- Scan.repeat (OuterParse.$$$ delim |-- scan) >> op :: || Scan.succeed [];
    23 
    24 	val scan_parm = (OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name));
    25 
    26 	val scan_parms = Scan.option (OuterParse.$$$ "[" |-- (repeatd "," scan_parm) --| OuterParse.$$$ "]");
    27 
    28 (* ------------------------------------------------------------------------- *)
    29 (* set up the 'refute' command                                               *)
    30 (* ------------------------------------------------------------------------- *)
    31 
    32 (* ------------------------------------------------------------------------- *)
    33 (* 'refute' takes an optional list of parameters, followed by an optional    *)
    34 (* subgoal number                                                            *)
    35 (* ------------------------------------------------------------------------- *)
    36 
    37 	val refute_scan_args = scan_parms -- (Scan.option OuterParse.nat);
    38 
    39 (* ------------------------------------------------------------------------- *)
    40 (* the 'refute' command is mapped to 'Refute.refute_subgoal'                 *)
    41 (* ------------------------------------------------------------------------- *)
    42 
    43 	fun refute_trans args =
    44 		Toplevel.keep
    45 			(fn state =>
    46 				(let
    47 					val (parms, subgoal) = args
    48 					val thy              = Toplevel.theory_of state
    49 					val thm              = (snd o snd) (Proof.get_goal (Toplevel.proof_of state))
    50 				in
    51 					Refute.refute_subgoal thy (getOpt (parms, [])) thm ((getOpt (subgoal, 1))-1)
    52 				end)
    53 			);
    54 
    55 	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
    56 
    57 	val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterKeyword.diag refute_parser;
    58 
    59 (* ------------------------------------------------------------------------- *)
    60 (* set up the 'refute_params' command                                        *)
    61 (* ------------------------------------------------------------------------- *)
    62 
    63 (* ------------------------------------------------------------------------- *)
    64 (* 'refute_params' takes an optional list of parameters                      *)
    65 (* ------------------------------------------------------------------------- *)
    66 
    67 	val refute_params_scan_args = scan_parms;
    68 
    69 (* ------------------------------------------------------------------------- *)
    70 (* the 'refute_params' command is mapped to (multiple calls of)              *)
    71 (* 'Refute.set_default_param'; then the (new) default parameters are         *)
    72 (* displayed                                                                 *)
    73 (* ------------------------------------------------------------------------- *)
    74 
    75 	fun refute_params_trans args =
    76 		let
    77 			fun add_params (thy, [])    = thy
    78 			  | add_params (thy, p::ps) = add_params (Refute.set_default_param p thy, ps)
    79 		in
    80 			Toplevel.theory (fn thy =>
    81 				let
    82 					val thy'               = add_params (thy, (getOpt (args, [])))
    83 					val new_default_params = Refute.get_default_params thy'
    84 					val output             = if new_default_params=[] then "none" else (space_implode "\n" (map (fn (name,value) => name ^ "=" ^ value) new_default_params))
    85 				in
    86 					writeln ("Default parameters for 'refute':\n" ^ output);
    87 					thy'
    88 				end)
    89 		end;
    90 
    91 	fun refute_params_parser tokens = (refute_params_scan_args tokens) |>> refute_params_trans;
    92 
    93 	val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl refute_params_parser;
    94 
    95 end;
    96 
    97 (* ------------------------------------------------------------------------- *)
    98 (* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's  *)
    99 (* outer syntax                                                              *)
   100 (* ------------------------------------------------------------------------- *)
   101 
   102 OuterSyntax.add_parsers [RefuteIsar.refute_cmd, RefuteIsar.refute_params_cmd];