Mercurialisabelle / file revision
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Tools/refute_isar.ML
author wenzelm
Wed Feb 15 21:34:55 2006 +0100 (2006-02-15)
changeset 19046 bc5c6c9b114e
parent 17273 e95f7141ba2f
child 22092 ab3dfcef6489
permissions -rw-r--r--
removed distinct, renamed gen_distinct to distinct; 
     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];
isabelle