src/HOL/Tools/refute_isar.ML
changeset 14350 41b32020d0b3
child 14454 8a8330bef1f8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/refute_isar.ML	Sat Jan 10 13:35:10 2004 +0100
     1.3 @@ -0,0 +1,102 @@
     1.4 +(*  Title:      HOL/Tools/refute_isar.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tjark Weber
     1.7 +    Copyright   2003-2004
     1.8 +
     1.9 +Adds the 'refute' and 'refute_params' commands to Isabelle/Isar's outer
    1.10 +syntax.
    1.11 +*)
    1.12 +
    1.13 +structure RefuteIsar =
    1.14 +struct
    1.15 +
    1.16 +(* ------------------------------------------------------------------------- *)
    1.17 +(* common functions for argument parsing/scanning                            *)
    1.18 +(* ------------------------------------------------------------------------- *)
    1.19 +
    1.20 +(* ------------------------------------------------------------------------- *)
    1.21 +(* both 'refute' and 'refute_params' take an optional list of arguments of   *)
    1.22 +(* the form [name1=value1, name2=value2, ...]                                *)
    1.23 +(* ------------------------------------------------------------------------- *)
    1.24 +
    1.25 +	fun repeatd delim scan = scan -- Scan.repeat (OuterParse.$$$ delim |-- scan) >> op :: || Scan.succeed [];
    1.26 +
    1.27 +	val scan_parm = (OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name));
    1.28 +
    1.29 +	val scan_parms = Scan.option (OuterParse.$$$ "[" |-- (repeatd "," scan_parm) --| OuterParse.$$$ "]");
    1.30 +
    1.31 +(* ------------------------------------------------------------------------- *)
    1.32 +(* set up the 'refute' command                                               *)
    1.33 +(* ------------------------------------------------------------------------- *)
    1.34 +
    1.35 +(* ------------------------------------------------------------------------- *)
    1.36 +(* 'refute' takes an optional list of parameters, followed by an optional    *)
    1.37 +(* subgoal number                                                            *)
    1.38 +(* ------------------------------------------------------------------------- *)
    1.39 +
    1.40 +	val refute_scan_args = scan_parms -- (Scan.option OuterParse.nat);
    1.41 +
    1.42 +(* ------------------------------------------------------------------------- *)
    1.43 +(* the 'refute' command is mapped to 'Refute.refute_subgoal'                 *)
    1.44 +(* ------------------------------------------------------------------------- *)
    1.45 +
    1.46 +	fun refute_trans args =
    1.47 +		Toplevel.keep
    1.48 +			(fn state =>
    1.49 +				(let
    1.50 +					val (parms, subgoal) = args
    1.51 +					val thy              = (Toplevel.theory_of state)
    1.52 +					val thm              = ((snd o snd) (Proof.get_goal (Toplevel.proof_of state)))
    1.53 +				in
    1.54 +					Refute.refute_subgoal thy (if_none parms []) thm ((if_none subgoal 1)-1)
    1.55 +				end)
    1.56 +			);
    1.57 +
    1.58 +	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
    1.59 +
    1.60 +	val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterSyntax.Keyword.diag refute_parser;
    1.61 +
    1.62 +(* ------------------------------------------------------------------------- *)
    1.63 +(* set up the 'refute_params' command                                        *)
    1.64 +(* ------------------------------------------------------------------------- *)
    1.65 +
    1.66 +(* ------------------------------------------------------------------------- *)
    1.67 +(* 'refute_params' takes an optional list of parameters                      *)
    1.68 +(* ------------------------------------------------------------------------- *)
    1.69 +
    1.70 +	val refute_params_scan_args = scan_parms;
    1.71 +
    1.72 +(* ------------------------------------------------------------------------- *)
    1.73 +(* the 'refute_params' command is mapped to (multiple calls of)              *)
    1.74 +(* 'Refute.set_default_param'; then the (new) default parameters are         *)
    1.75 +(* displayed                                                                 *)
    1.76 +(* ------------------------------------------------------------------------- *)
    1.77 +
    1.78 +	fun refute_params_trans args =
    1.79 +		let
    1.80 +			fun add_params (thy, []) = thy
    1.81 +				| add_params (thy, p::ps) = add_params (Refute.set_default_param p thy, ps)
    1.82 +		in
    1.83 +			Toplevel.theory (fn thy =>
    1.84 +				let
    1.85 +					val thy'               = add_params (thy, (if_none args []))
    1.86 +					val new_default_params = Refute.get_default_params thy'
    1.87 +					val output             = if new_default_params=[] then "none" else (space_implode "\n" (map (fn (name,value) => name ^ "=" ^ value) new_default_params))
    1.88 +				in
    1.89 +					writeln ("Default parameters for 'refute':\n" ^ output);
    1.90 +					thy'
    1.91 +				end)
    1.92 +		end;
    1.93 +
    1.94 +	fun refute_params_parser tokens = (refute_params_scan_args tokens) |>> refute_params_trans;
    1.95 +
    1.96 +	val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterSyntax.Keyword.thy_decl refute_params_parser;
    1.97 +
    1.98 +end;
    1.99 +
   1.100 +(* ------------------------------------------------------------------------- *)
   1.101 +(* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's  *)
   1.102 +(* outer syntax                                                              *)
   1.103 +(* ------------------------------------------------------------------------- *)
   1.104 +
   1.105 +OuterSyntax.add_parsers [RefuteIsar.refute_cmd, RefuteIsar.refute_params_cmd];