# HG changeset patch
# User wenzelm
# Date 1254512517 -7200
# Node ID 394d37f19e0a7f535a2a4a9abcc085a989ac1e94
# Parent  92d9555ac790ef4d418d9bcaafb88bccf2e4d684
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
command 'refute': Proof.flat_goal provides standard view on internally structured Isar goal, suitable for (semi)automated tools;

diff -r 92d9555ac790 -r 394d37f19e0a src/HOL/Refute.thy
--- a/src/HOL/Refute.thy	Fri Oct 02 21:39:06 2009 +0200
+++ b/src/HOL/Refute.thy	Fri Oct 02 21:41:57 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Refute.thy
-    ID:         $Id$
     Author:     Tjark Weber
     Copyright   2003-2007
 
diff -r 92d9555ac790 -r 394d37f19e0a src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Oct 02 21:39:06 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Oct 02 21:41:57 2009 +0200
@@ -51,9 +51,8 @@
   (* tries to find a model for a formula: *)
   val satisfy_term   : theory -> (string * string) list -> Term.term -> unit
   (* tries to find a model that refutes a formula: *)
-  val refute_term    : theory -> (string * string) list -> Term.term -> unit
-  val refute_subgoal :
-    theory -> (string * string) list -> Thm.thm -> int -> unit
+  val refute_term : theory -> (string * string) list -> term -> unit
+  val refute_goal : theory -> (string * string) list -> thm -> int -> unit
 
   val setup : theory -> theory
 
@@ -1355,16 +1354,11 @@
   end;
 
 (* ------------------------------------------------------------------------- *)
-(* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
-(* params        : list of '(name, value)' pairs used to override default    *)
-(*                 parameters                                                *)
-(* subgoal       : 0-based index specifying the subgoal number               *)
+(* refute_goal                                                               *)
 (* ------------------------------------------------------------------------- *)
 
-  (* theory -> (string * string) list -> Thm.thm -> int -> unit *)
-
-  fun refute_subgoal thy params thm subgoal =
-    refute_term thy params (List.nth (Thm.prems_of thm, subgoal));
+  fun refute_goal thy params st i =
+    refute_term thy params (Logic.get_goal (Thm.prop_of st) i);
 
 
 (* ------------------------------------------------------------------------- *)
diff -r 92d9555ac790 -r 394d37f19e0a src/HOL/Tools/refute_isar.ML
--- a/src/HOL/Tools/refute_isar.ML	Fri Oct 02 21:39:06 2009 +0200
+++ b/src/HOL/Tools/refute_isar.ML	Fri Oct 02 21:41:57 2009 +0200
@@ -23,14 +23,13 @@
 val _ =
   OuterSyntax.improper_command "refute"
     "try to find a model that refutes a given subgoal" OuterKeyword.diag
-    (scan_parms -- Scan.optional OuterParse.nat 1 >> (fn (parms, subgoal) =>
-      Toplevel.keep (fn state =>
-        let
-          val thy = Toplevel.theory_of state
-          val st = (snd o snd) (Proof.get_goal (Toplevel.proof_of state))
-        in
-          Refute.refute_subgoal thy parms st (subgoal - 1)
-        end)));
+    (scan_parms -- Scan.optional OuterParse.nat 1 >>
+      (fn (parms, i) =>
+        Toplevel.keep (fn state =>
+          let
+            val thy = Toplevel.theory_of state;
+            val (_, st) = Proof.flat_goal (Toplevel.proof_of state);
+          in Refute.refute_goal thy parms st i end)));
 
 
 (* 'refute_params' command *)
@@ -41,13 +40,13 @@
     (scan_parms >> (fn parms =>
       Toplevel.theory (fn thy =>
         let
-          val thy' = fold Refute.set_default_param parms thy
+          val thy' = fold Refute.set_default_param parms thy;
           val output =
             (case Refute.get_default_params thy' of
               [] => "none"
-            | new_defaults => cat_lines (map (fn (name, value) => name ^ "=" ^ value) new_defaults))
+            | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
           val _ = writeln ("Default parameters for 'refute':\n" ^ output);
-        in thy' end)))
+        in thy' end)));
 
 end;