# 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]