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