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