# HG changeset patch
# User nipkow
# Date 1115188570 -7200
# Node ID b6e3455489137cd1bce1e47f4f0df102ef92a81a
# Parent  c79fa63504c8c45ebdf993fd3d7fc6cb98055378
Fixing a problem with lin.arith.

diff -r c79fa63504c8 -r b6e345548913 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue May 03 15:37:41 2005 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed May 04 08:36:10 2005 +0200
@@ -278,6 +278,7 @@
 
 
 lemmas zless_linear = linorder_less_linear [where 'a = int]
+lemmas linorder_neqE_int = linorder_neqE[where 'a = int]
 
 
 lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
diff -r c79fa63504c8 -r b6e345548913 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Tue May 03 15:37:41 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy	Wed May 04 08:36:10 2005 +0200
@@ -565,10 +565,10 @@
 
 val nat_bin_arith_setup =
  [Fast_Arith.map_data 
-   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
+   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
      {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
       inj_thms = inj_thms,
-      lessD = lessD,
+      lessD = lessD, neqE = neqE,
       simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
                                   not_neg_number_of_Pls,
                                   neg_number_of_Min,neg_number_of_BIT]})]
diff -r c79fa63504c8 -r b6e345548913 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Tue May 03 15:37:41 2005 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Wed May 04 08:36:10 2005 +0200
@@ -514,11 +514,12 @@
 in
 
 val int_arith_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
+ [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms,
     inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
     lessD = lessD @ [zless_imp_add1_zle],
+    neqE = thm "linorder_neqE_int" :: neqE,
     simpset = simpset addsimps add_rules
                       addsimprocs simprocs
                       addcongs [if_weak_cong]}),
diff -r c79fa63504c8 -r b6e345548913 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Tue May 03 15:37:41 2005 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Wed May 04 08:36:10 2005 +0200
@@ -544,9 +544,9 @@
 in
 
 val nat_simprocs_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
+ [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
-    inj_thms = inj_thms, lessD = lessD,
+    inj_thms = inj_thms, lessD = lessD, neqE = neqE,
     simpset = simpset addsimps add_rules
                       addsimprocs simprocs})];
 
diff -r c79fa63504c8 -r b6e345548913 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Tue May 03 15:37:41 2005 +0200
+++ b/src/HOL/Nat.ML	Wed May 04 08:36:10 2005 +0200
@@ -236,3 +236,4 @@
 val zero_less_diff = thm "zero_less_diff";
 val zero_less_mult_iff = thm "zero_less_mult_iff";
 val zero_reorient = thm "zero_reorient";
+val linorder_neqE_nat = thm "linorder_neqE_nat";
\ No newline at end of file
diff -r c79fa63504c8 -r b6e345548913 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue May 03 15:37:41 2005 +0200
+++ b/src/HOL/Nat.thy	Wed May 04 08:36:10 2005 +0200
@@ -443,6 +443,8 @@
     (assumption |
       rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
 
+lemmas linorder_neqE_nat = linorder_neqE[where 'a = nat]
+
 lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
   by (blast elim!: less_SucE)
 
diff -r c79fa63504c8 -r b6e345548913 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Tue May 03 15:37:41 2005 +0200
+++ b/src/HOL/arith_data.ML	Wed May 04 08:36:10 2005 +0200
@@ -173,7 +173,6 @@
 struct
 val ccontr = ccontr;
 val conjI = conjI;
-val neqE = linorder_neqE;
 val notI = notI;
 val sym = sym;
 val not_lessD = linorder_not_less RS iffD1;
@@ -418,12 +417,13 @@
 
 val init_lin_arith_data =
  Fast_Arith.setup @
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset = _} =>
+ [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
    {add_mono_thms = add_mono_thms @
     add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
     mult_mono_thms = mult_mono_thms,
     inj_thms = inj_thms,
     lessD = lessD @ [Suc_leI],
+    neqE = [linorder_neqE_nat],
     simpset = HOL_basic_ss addsimps add_rules
                    addsimprocs [ab_group_add_cancel.sum_conv, 
                                 ab_group_add_cancel.rel_conv]