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