# HG changeset patch
# User nipkow
# Date 1115188665 -7200
# Node ID 7ef183f3fc9804772143cb9001a3a1c4069c6ac3
# Parent  b6e3455489137cd1bce1e47f4f0df102ef92a81a
neqE applies even if the type is not one which partakes in linear arithmetic.
This lead to confusion. Now there are multiple type specific neqE.

diff -r b6e345548913 -r 7ef183f3fc98 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed May 04 08:36:10 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed May 04 08:37:45 2005 +0200
@@ -25,7 +25,6 @@
 sig
   val conjI:		thm
   val ccontr:           thm (* (~ P ==> False) ==> P *)
-  val neqE:             thm (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *)
   val notI:             thm (* (P ==> False) ==> ~ P *)
   val not_lessD:        thm (* ~(m < n) ==> n <= m *)
   val not_leD:          thm (* ~(m <= n) ==> n < m *)
@@ -72,9 +71,9 @@
 sig
   val setup: (theory -> theory) list
   val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
-                 lessD: thm list, simpset: Simplifier.simpset}
+                 lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
                  -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
-                     lessD: thm list, simpset: Simplifier.simpset})
+                     lessD: thm list, neqE: thm list, simpset: Simplifier.simpset})
                 -> theory -> theory
   val trace           : bool ref
   val fast_arith_neq_limit: int ref
@@ -96,21 +95,22 @@
 struct
   val name = "Provers/fast_lin_arith";
   type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
-            lessD: thm list, simpset: Simplifier.simpset};
+            lessD: thm list, neqE: thm list, simpset: Simplifier.simpset};
 
   val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
-               lessD = [], simpset = Simplifier.empty_ss};
+               lessD = [], neqE = [], simpset = Simplifier.empty_ss};
   val copy = I;
   val prep_ext = I;
 
   fun merge ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
-              lessD = lessD1, simpset = simpset1},
+              lessD = lessD1, neqE=neqE1, simpset = simpset1},
              {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
-              lessD = lessD2, simpset = simpset2}) =
+              lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
     {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
      mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2),
      inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
      lessD = Drule.merge_rules (lessD1, lessD2),
+     neqE = Drule.merge_rules (neqE1, neqE2),
      simpset = Simplifier.merge_ss (simpset1, simpset2)};
 
   fun print _ _ = ();
@@ -419,7 +419,8 @@
  exception FalseE of thm
 in
 fun mkthm sg asms just =
-  let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} = Data.get_sg sg;
+  let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
+          Data.get_sg sg;
       val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
                             map fst lhs  union  (map fst rhs  union  ats))
                         ([], List.mapPartial (fn thm => if Thm.no_prems thm
@@ -621,7 +622,8 @@
 fun refute_tac(i,justs) =
   fn state =>
     let val sg = #sign(rep_thm state)
-        fun just1 j = REPEAT_DETERM(etac LA_Logic.neqE i) THEN
+        val {neqE, ...} = Data.get_sg sg;
+        fun just1 j = REPEAT_DETERM(eresolve_tac neqE i) THEN
                       METAHYPS (fn asms => rtac (mkthm sg asms j) 1) i
     in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN
        EVERY(map just1 justs)
@@ -685,14 +687,17 @@
     val (_,ct2) = Thm.dest_comb Ict2
 in (ct1,ct2) end;
 
-fun splitasms asms =
-let fun split(asms',[]) = Tip(rev asms')
+fun splitasms sg asms =
+let val {neqE, ...}  = Data.get_sg sg;
+    fun split(asms',[]) = Tip(rev asms')
       | split(asms',asm::asms) =
-      let val spl = asm COMP LA_Logic.neqE
-          val (ct1,ct2) = extract(cprop_of spl)
-          val thm1 = assume ct1 and thm2 = assume ct2
-      in Spl(spl,ct1,split(asms',asms@[thm1]),ct2,split(asms',asms@[thm2])) end
-      handle THM _ => split(asm::asms', asms)
+      (case get_first (fn th => SOME(asm COMP th) handle THM _ => NONE) neqE
+       of SOME spl =>
+          let val (ct1,ct2) = extract(cprop_of spl)
+              val thm1 = assume ct1 and thm2 = assume ct2
+          in Spl(spl,ct1,split(asms',asms@[thm1]),ct2,split(asms',asms@[thm2]))
+          end
+       | NONE => split(asm::asms', asms))
 in split([],asms) end;
 
 fun fwdproof sg (Tip asms) (j::js) = (mkthm sg asms j, js)
@@ -708,7 +713,7 @@
 let val nTconcl = LA_Logic.neg_prop Tconcl
     val cnTconcl = cterm_of sg nTconcl
     val nTconclthm = assume cnTconcl
-    val tree = splitasms (thms @ [nTconclthm])
+    val tree = splitasms sg (thms @ [nTconclthm])
     val (thm,_) = fwdproof sg tree js
     val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
 in SOME(LA_Logic.mk_Eq((implies_intr cnTconcl thm) COMP contr)) end