src/HOL/Tools/refute_isar.ML
author webertj
Fri Jan 19 21:20:10 2007 +0100 (2007-01-19)
changeset 22092 ab3dfcef6489
parent 17273 e95f7141ba2f
child 24867 e5b55d7be9bb
permissions -rw-r--r--
reformatted to 80 chars/line
webertj@14350
     1
(*  Title:      HOL/Tools/refute_isar.ML
webertj@14350
     2
    ID:         $Id$
webertj@14350
     3
    Author:     Tjark Weber
webertj@22092
     4
    Copyright   2003-2007
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@22092
    22
	fun repeatd delim scan = scan -- Scan.repeat (OuterParse.$$$ delim |-- scan)
webertj@22092
    23
		>> op :: || Scan.succeed [];
webertj@14350
    24
webertj@22092
    25
	val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
webertj@14350
    26
webertj@22092
    27
	val scan_parms = Scan.option
webertj@22092
    28
		(OuterParse.$$$ "[" |-- (repeatd "," scan_parm) --| OuterParse.$$$ "]");
webertj@14350
    29
webertj@14350
    30
(* ------------------------------------------------------------------------- *)
webertj@14350
    31
(* set up the 'refute' command                                               *)
webertj@14350
    32
(* ------------------------------------------------------------------------- *)
webertj@14350
    33
webertj@14350
    34
(* ------------------------------------------------------------------------- *)
webertj@14350
    35
(* 'refute' takes an optional list of parameters, followed by an optional    *)
webertj@14350
    36
(* subgoal number                                                            *)
webertj@14350
    37
(* ------------------------------------------------------------------------- *)
webertj@14350
    38
webertj@14350
    39
	val refute_scan_args = scan_parms -- (Scan.option OuterParse.nat);
webertj@14350
    40
webertj@14350
    41
(* ------------------------------------------------------------------------- *)
webertj@14350
    42
(* the 'refute' command is mapped to 'Refute.refute_subgoal'                 *)
webertj@14350
    43
(* ------------------------------------------------------------------------- *)
webertj@14350
    44
webertj@14350
    45
	fun refute_trans args =
webertj@22092
    46
		Toplevel.keep (fn state =>
webertj@22092
    47
			let
webertj@22092
    48
				val (parms_opt, subgoal_opt) = args
webertj@22092
    49
				val parms   = Option.getOpt (parms_opt, [])
webertj@22092
    50
				val subgoal = Option.getOpt (subgoal_opt, 1) - 1
webertj@22092
    51
				val thy     = Toplevel.theory_of state
webertj@22092
    52
				val thm     = (snd o snd) (Proof.get_goal (Toplevel.proof_of state))
webertj@22092
    53
			in
webertj@22092
    54
				Refute.refute_subgoal thy parms thm subgoal
webertj@22092
    55
			end);
webertj@14350
    56
webertj@14350
    57
	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
webertj@14350
    58
webertj@22092
    59
	val refute_cmd = OuterSyntax.improper_command "refute"
webertj@22092
    60
		"try to find a model that refutes a given subgoal"
webertj@22092
    61
		OuterKeyword.diag refute_parser;
webertj@14350
    62
webertj@14350
    63
(* ------------------------------------------------------------------------- *)
webertj@14350
    64
(* set up the 'refute_params' command                                        *)
webertj@14350
    65
(* ------------------------------------------------------------------------- *)
webertj@14350
    66
webertj@14350
    67
(* ------------------------------------------------------------------------- *)
webertj@14350
    68
(* 'refute_params' takes an optional list of parameters                      *)
webertj@14350
    69
(* ------------------------------------------------------------------------- *)
webertj@14350
    70
webertj@14350
    71
	val refute_params_scan_args = scan_parms;
webertj@14350
    72
webertj@14350
    73
(* ------------------------------------------------------------------------- *)
webertj@14350
    74
(* the 'refute_params' command is mapped to (multiple calls of)              *)
webertj@14350
    75
(* 'Refute.set_default_param'; then the (new) default parameters are         *)
webertj@14350
    76
(* displayed                                                                 *)
webertj@14350
    77
(* ------------------------------------------------------------------------- *)
webertj@14350
    78
webertj@14350
    79
	fun refute_params_trans args =
webertj@14350
    80
		let
webertj@22092
    81
			fun add_params thy [] =
webertj@22092
    82
				thy
webertj@22092
    83
			  | add_params thy (p::ps) =
webertj@22092
    84
				add_params (Refute.set_default_param p thy) ps
webertj@14350
    85
		in
webertj@14350
    86
			Toplevel.theory (fn thy =>
webertj@14350
    87
				let
webertj@22092
    88
					val thy'               = add_params thy (getOpt (args, []))
webertj@14350
    89
					val new_default_params = Refute.get_default_params thy'
webertj@22092
    90
					val output             = if new_default_params=[] then
webertj@22092
    91
							"none"
webertj@22092
    92
						else
webertj@22092
    93
							space_implode "\n" (map (fn (name, value) => name ^ "=" ^ value)
webertj@22092
    94
								new_default_params)
webertj@14350
    95
				in
webertj@14350
    96
					writeln ("Default parameters for 'refute':\n" ^ output);
webertj@14350
    97
					thy'
webertj@14350
    98
				end)
webertj@14350
    99
		end;
webertj@14350
   100
webertj@22092
   101
	fun refute_params_parser tokens =
webertj@22092
   102
		(refute_params_scan_args tokens) |>> refute_params_trans;
webertj@14350
   103
webertj@22092
   104
	val refute_params_cmd = OuterSyntax.command "refute_params"
webertj@22092
   105
		"show/store default parameters for the 'refute' command"
webertj@22092
   106
		OuterKeyword.thy_decl refute_params_parser;
webertj@14350
   107
webertj@14350
   108
end;
webertj@14350
   109
webertj@14350
   110
(* ------------------------------------------------------------------------- *)
webertj@14350
   111
(* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's  *)
webertj@14350
   112
(* outer syntax                                                              *)
webertj@14350
   113
(* ------------------------------------------------------------------------- *)
webertj@14350
   114
webertj@14350
   115
OuterSyntax.add_parsers [RefuteIsar.refute_cmd, RefuteIsar.refute_params_cmd];