webertj@14350: (*  Title:      HOL/Tools/refute_isar.ML
webertj@14350:     ID:         $Id$
webertj@14350:     Author:     Tjark Weber
webertj@17273:     Copyright   2003-2005
webertj@14350: 
webertj@14350: Adds the 'refute' and 'refute_params' commands to Isabelle/Isar's outer
webertj@14350: syntax.
webertj@14350: *)
webertj@14350: 
webertj@14350: structure RefuteIsar =
webertj@14350: struct
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* common functions for argument parsing/scanning                            *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* both 'refute' and 'refute_params' take an optional list of arguments of   *)
webertj@14350: (* the form [name1=value1, name2=value2, ...]                                *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: 	fun repeatd delim scan = scan -- Scan.repeat (OuterParse.$$$ delim |-- scan) >> op :: || Scan.succeed [];
webertj@14350: 
webertj@14350: 	val scan_parm = (OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name));
webertj@14350: 
webertj@14350: 	val scan_parms = Scan.option (OuterParse.$$$ "[" |-- (repeatd "," scan_parm) --| OuterParse.$$$ "]");
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* set up the 'refute' command                                               *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* 'refute' takes an optional list of parameters, followed by an optional    *)
webertj@14350: (* subgoal number                                                            *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: 	val refute_scan_args = scan_parms -- (Scan.option OuterParse.nat);
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* the 'refute' command is mapped to 'Refute.refute_subgoal'                 *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: 	fun refute_trans args =
webertj@14350: 		Toplevel.keep
webertj@14350: 			(fn state =>
webertj@14350: 				(let
webertj@14350: 					val (parms, subgoal) = args
webertj@17273: 					val thy              = Toplevel.theory_of state
webertj@17273: 					val thm              = (snd o snd) (Proof.get_goal (Toplevel.proof_of state))
webertj@14350: 				in
skalberg@15570: 					Refute.refute_subgoal thy (getOpt (parms, [])) thm ((getOpt (subgoal, 1))-1)
webertj@14350: 				end)
webertj@14350: 			);
webertj@14350: 
webertj@14350: 	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
webertj@14350: 
wenzelm@17057: 	val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterKeyword.diag refute_parser;
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* set up the 'refute_params' command                                        *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* 'refute_params' takes an optional list of parameters                      *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: 	val refute_params_scan_args = scan_parms;
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* the 'refute_params' command is mapped to (multiple calls of)              *)
webertj@14350: (* 'Refute.set_default_param'; then the (new) default parameters are         *)
webertj@14350: (* displayed                                                                 *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: 	fun refute_params_trans args =
webertj@14350: 		let
webertj@14454: 			fun add_params (thy, [])    = thy
webertj@14454: 			  | add_params (thy, p::ps) = add_params (Refute.set_default_param p thy, ps)
webertj@14350: 		in
webertj@14350: 			Toplevel.theory (fn thy =>
webertj@14350: 				let
skalberg@15570: 					val thy'               = add_params (thy, (getOpt (args, [])))
webertj@14350: 					val new_default_params = Refute.get_default_params thy'
webertj@14350: 					val output             = if new_default_params=[] then "none" else (space_implode "\n" (map (fn (name,value) => name ^ "=" ^ value) new_default_params))
webertj@14350: 				in
webertj@14350: 					writeln ("Default parameters for 'refute':\n" ^ output);
webertj@14350: 					thy'
webertj@14350: 				end)
webertj@14350: 		end;
webertj@14350: 
webertj@14350: 	fun refute_params_parser tokens = (refute_params_scan_args tokens) |>> refute_params_trans;
webertj@14350: 
wenzelm@17057: 	val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl refute_params_parser;
webertj@14350: 
webertj@14350: end;
webertj@14350: 
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: (* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's  *)
webertj@14350: (* outer syntax                                                              *)
webertj@14350: (* ------------------------------------------------------------------------- *)
webertj@14350: 
webertj@14350: OuterSyntax.add_parsers [RefuteIsar.refute_cmd, RefuteIsar.refute_params_cmd];