# HG changeset patch
# User paulson
# Date 907924259 -7200
# Node ID 77e9ab9cd7b1623a465b5ac39685d54a4e6d5ea9
# Parent  4813dd0fe6e5cd191a412081028ecd79f14f9060
polymorphic versions of nat_neq_iff and nat_neqE

diff -r 4813dd0fe6e5 -r 77e9ab9cd7b1 src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Thu Oct 08 11:59:17 1998 +0200
+++ b/src/HOL/Lambda/Eta.ML	Fri Oct 09 11:10:59 1998 +0200
@@ -44,7 +44,7 @@
 by (asm_full_simp_tac (addsplit (simpset())) 2);
 by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
                       addsplits [nat.split]) 1);
-by (safe_tac (HOL_cs addSEs [nat_neqE]));
+by (safe_tac (HOL_cs addSEs [linorder_neqE]));
 by (ALLGOALS trans_tac);
 qed "free_subst";
 Addsimps [free_subst];
@@ -119,7 +119,7 @@
 Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
 by (induct_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (addsplit (simpset()))));
-by (safe_tac (HOL_cs addSEs [nat_neqE]));
+by (safe_tac (HOL_cs addSEs [linorder_neqE]));
 by (ALLGOALS trans_tac);
 qed_spec_mp "subst_Var_Suc";
 Addsimps [subst_Var_Suc];
@@ -163,7 +163,7 @@
 by (induct_tac "s" 1);
   by (Simp_tac 1);
   by (SELECT_GOAL(safe_tac HOL_cs)1);
-   by (etac nat_neqE 1);
+   by (etac linorder_neqE 1);
     by (res_inst_tac [("x","Var nat")] exI 1);
     by (Asm_simp_tac 1);
    by (res_inst_tac [("x","Var(nat-1)")] exI 1);
diff -r 4813dd0fe6e5 -r 77e9ab9cd7b1 src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu Oct 08 11:59:17 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Oct 09 11:10:59 1998 +0200
@@ -131,7 +131,7 @@
 Addsimps [deltas_concat];
 
 goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
-by (etac nat_neqE 1);
+by (etac linorder_neqE 1);
 by (ALLGOALS trans_tac);
 val lemma = result();
 
diff -r 4813dd0fe6e5 -r 77e9ab9cd7b1 src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Thu Oct 08 11:59:17 1998 +0200
+++ b/src/HOL/Ord.ML	Fri Oct 09 11:10:59 1998 +0200
@@ -121,4 +121,10 @@
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "min_le_iff_disj";
 
+Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
+by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
+by Auto_tac;
+qed "linorder_neq_iff";
 
+(*** eliminates ~= in premises ***)
+bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
diff -r 4813dd0fe6e5 -r 77e9ab9cd7b1 src/HOL/UNITY/Channel.ML
--- a/src/HOL/UNITY/Channel.ML	Thu Oct 08 11:59:17 1998 +0200
+++ b/src/HOL/UNITY/Channel.ML	Fri Oct 09 11:10:59 1998 +0200
@@ -33,7 +33,7 @@
 by (Blast_tac 1);
 by Safe_tac;
 by (auto_tac (claset() addDs [minSet_eq_SomeD], 
-	      simpset() addsimps [le_def, nat_neq_iff]));
+	      simpset() addsimps [le_def, linorder_neq_iff]));
 qed "minSet_greaterThan";
 
 
diff -r 4813dd0fe6e5 -r 77e9ab9cd7b1 src/HOL/UNITY/LessThan.ML
--- a/src/HOL/UNITY/LessThan.ML	Thu Oct 08 11:59:17 1998 +0200
+++ b/src/HOL/UNITY/LessThan.ML	Fri Oct 09 11:10:59 1998 +0200
@@ -50,7 +50,7 @@
 Addsimps [greaterThan_0];
 
 Goalw [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
-by (auto_tac (claset() addEs [nat_neqE], simpset()));
+by (auto_tac (claset() addEs [linorder_neqE], simpset()));
 qed "greaterThan_Suc";
 
 Goal "(INT m. greaterThan m) = {}";
diff -r 4813dd0fe6e5 -r 77e9ab9cd7b1 src/HOL/UNITY/Token.ML
--- a/src/HOL/UNITY/Token.ML	Thu Oct 08 11:59:17 1998 +0200
+++ b/src/HOL/UNITY/Token.ML	Fri Oct 09 11:10:59 1998 +0200
@@ -56,10 +56,10 @@
 by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
 by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, Suc_leI, less_imp_le,
                                       diff_add_assoc]) 2);
-by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
+by (full_simp_tac (simpset() addsimps [linorder_neq_iff]) 1);
 by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1);
 by (auto_tac (claset(), 
-              simpset() addsimps [diff_add_assoc2, nat_neq_iff, 
+              simpset() addsimps [diff_add_assoc2, linorder_neq_iff, 
                                   Suc_le_eq, Suc_diff_Suc, less_imp_diff_less, 
                                   add_diff_less, mod_less, mod_geq]));
 by (etac subst 1);