# HG changeset patch
# User wenzelm
# Date 1211115871 -7200
# Node ID 9cd13e810998d61f75f0a32fe319a7325940b093
# Parent  1fe801f9cfc9a47c3881890c498f2313dae08434
renamed type decompT to decomp;
refute: proper context for trace_ex;
some attempts to improve readability;

diff -r 1fe801f9cfc9 -r 9cd13e810998 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Sun May 18 15:04:27 2008 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sun May 18 15:04:31 2008 +0200
@@ -11,8 +11,6 @@
 the term.
 *)
 
-(* Debugging: set Fast_Arith.trace *)
-
 (*** Data needed for setting up the linear arithmetic package ***)
 
 signature LIN_ARITH_LOGIC =
@@ -49,8 +47,8 @@
 signature LIN_ARITH_DATA =
 sig
   (*internal representation of linear (in-)equations:*)
-  type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool
-  val decomp: Proof.context -> term -> decompT option
+  type decomp = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool
+  val decomp: Proof.context -> term -> decomp option
   val domain_is_nat: term -> bool
 
   (*preprocessing, performed on a representation of subgoals as list of premises:*)
@@ -349,7 +347,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun allpairs f xs ys =
-  List.concat (map (fn x => map (fn y => f x y) ys) xs);
+  maps (fn x => map (fn y => f x y) ys) xs;
 
 fun extract_first p =
   let fun extract xs (y::ys) = if p y then (SOME y,xs@ys)
@@ -606,7 +604,7 @@
 (*        failure as soon as a case could not be refuted; i.e. delay further *)
 (*        splitting until after a refutation for other cases has been found. *)
 
-fun split_items ctxt do_pre (Ts, terms) : (typ list * (LA_Data.decompT * int) list) list =
+fun split_items ctxt do_pre (Ts, terms) : (typ list * (LA_Data.decomp * int) list) list =
 let
   (* splits inequalities '~=' into '<' and '>'; this corresponds to *)
   (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic    *)
@@ -616,11 +614,11 @@
   (*        better (i.e. less likely to break when neqE changes)    *)
   (*        implementation should *test* which theorem from neqE    *)
   (*        can be applied, and split the premise accordingly.      *)
-  fun elim_neq (ineqs : (LA_Data.decompT option * bool) list) :
-               (LA_Data.decompT option * bool) list list =
+  fun elim_neq (ineqs : (LA_Data.decomp option * bool) list) :
+               (LA_Data.decomp option * bool) list list =
   let
-    fun elim_neq' nat_only ([] : (LA_Data.decompT option * bool) list) :
-                  (LA_Data.decompT option * bool) list list =
+    fun elim_neq' nat_only ([] : (LA_Data.decomp option * bool) list) :
+                  (LA_Data.decomp option * bool) list list =
           [[]]
       | elim_neq' nat_only ((NONE, is_nat) :: ineqs) =
           map (cons (NONE, is_nat)) (elim_neq' nat_only ineqs)
@@ -633,8 +631,7 @@
             map (cons ineq) (elim_neq' nat_only ineqs)
   in
     ineqs |> elim_neq' true
-          |> map (elim_neq' false)
-          |> List.concat
+          |> maps (elim_neq' false)
   end
 
   fun number_hyps _ []             = []
@@ -659,56 +656,53 @@
   result
 end;
 
-fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decompT, _)) : term list =
+fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decomp, _)) : term list =
     union_term (map fst lhs) (union_term (map fst rhs) ats);
 
-fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decompT, _)) :
+fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _)) :
   (bool * term) list =
   union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats);
 
-fun discr (initems : (LA_Data.decompT * int) list) : bool list =
+fun discr (initems : (LA_Data.decomp * int) list) : bool list =
   map fst (Library.foldl add_datoms ([],initems));
 
 fun refutes ctxt params show_ex :
-  (typ list * (LA_Data.decompT * int) list) list -> injust list -> injust list option =
-let
-  fun refute ((Ts : typ list, initems : (LA_Data.decompT * int) list)::initemss)
-             (js : injust list) : injust list option =
-    let
-      val atoms = Library.foldl add_atoms ([], initems)
-      val n = length atoms
-      val mkleq = mklineq n atoms
-      val ixs = 0 upto (n - 1)
-      val iatoms = atoms ~~ ixs
-      val natlineqs = List.mapPartial (mknat Ts ixs) iatoms
-      val ineqs = map mkleq initems @ natlineqs
-    in case elim (ineqs, []) of
-         Success j =>
-           (trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")");
-            refute initemss (js@[j]))
-       | Failure hist =>
-           (if not show_ex then
-              ()
-            else let
-              (* invent names for bound variables that are new, i.e. in Ts,  *)
-              (* but not in params; we assume that Ts still contains (map    *)
-              (* snd params) as a suffix                                     *)
-              val new_count = length Ts - length params - 1
-              val new_names = map Name.bound (0 upto new_count)
-              val params'   = (new_names @ map fst params) ~~ Ts
-            in
-              trace_ex ctxt params' atoms (discr initems) n hist
-            end; NONE)
-    end
-    | refute [] js = SOME js
-in refute end;
+    (typ list * (LA_Data.decomp * int) list) list -> injust list -> injust list option =
+  let
+    fun refute ((Ts, initems : (LA_Data.decomp * int) list) :: initemss) (js: injust list) =
+          let
+            val atoms = Library.foldl add_atoms ([], initems)
+            val n = length atoms
+            val mkleq = mklineq n atoms
+            val ixs = 0 upto (n - 1)
+            val iatoms = atoms ~~ ixs
+            val natlineqs = List.mapPartial (mknat Ts ixs) iatoms
+            val ineqs = map mkleq initems @ natlineqs
+          in case elim (ineqs, []) of
+               Success j =>
+                 (trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")");
+                  refute initemss (js @ [j]))
+             | Failure hist =>
+                 (if not show_ex then ()
+                  else
+                    let
+                      val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params)
+                      val (more_names, ctxt'') = ctxt' |> Variable.variant_fixes
+                        (Name.invents (Variable.names_of ctxt') Name.uu (length Ts - length params))
+                      val params' = (more_names @ param_names) ~~ Ts
+                    in
+                      trace_ex ctxt'' params' atoms (discr initems) n hist
+                    end; NONE)
+          end
+      | refute [] js = SOME js
+  in refute end;
 
 fun refute ctxt params show_ex do_pre terms : injust list option =
   refutes ctxt params show_ex (split_items ctxt do_pre (map snd params, terms)) [];
 
 fun count P xs = length (filter P xs);
 
-fun prove ctxt (params : (string * Term.typ) list) show_ex do_pre Hs concl : injust list option =
+fun prove ctxt params show_ex do_pre Hs concl : injust list option =
   let
     val _ = trace_msg "prove:"
     (* append the negated conclusion to 'Hs' -- this corresponds to     *)
@@ -850,7 +844,7 @@
 fun lin_arith_simproc ss concl =
   let
     val ctxt = Simplifier.the_context ss
-    val thms = List.concat (map LA_Logic.atomize (Simplifier.prems_of_ss ss))
+    val thms = maps LA_Logic.atomize (Simplifier.prems_of_ss ss)
     val Hs = map Thm.prop_of thms
     val Tconcl = LA_Logic.mk_Trueprop concl
   in