Simplified arithmetic.
authornipkow
Wed Jan 13 08:41:28 1999 +0100 (1999-01-13)
changeset 610982b50115564c
parent 6108 2c9ed58c30ba
child 6110 15c2b571225b
Simplified arithmetic.
src/HOL/Arith.ML
src/HOL/Integ/Bin.ML
src/HOL/Nat.ML
src/HOL/NatDef.ML
src/HOL/Ord.ML
     1.1 --- a/src/HOL/Arith.ML	Tue Jan 12 17:19:53 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Jan 13 08:41:28 1999 +0100
     1.3 @@ -852,6 +852,7 @@
     1.4  val neqE = linorder_neqE;
     1.5  val notI = notI;
     1.6  val sym = sym;
     1.7 +val not_lessD = linorder_not_less RS iffD1;
     1.8  
     1.9  val mk_Eq = mk_eq;
    1.10  val mk_Trueprop = HOLogic.mk_Trueprop;
    1.11 @@ -870,7 +871,6 @@
    1.12  
    1.13  val lessD = Suc_leI;
    1.14  val not_leD = not_leE RS Suc_leI;
    1.15 -val not_lessD = leI;
    1.16  
    1.17  (* Turn term into list of summand * multiplicity plus a constant *)
    1.18  fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
     2.1 --- a/src/HOL/Integ/Bin.ML	Tue Jan 12 17:19:53 1999 +0100
     2.2 +++ b/src/HOL/Integ/Bin.ML	Wed Jan 13 08:41:28 1999 +0100
     2.3 @@ -404,7 +404,6 @@
     2.4  
     2.5  val lessD = add1_zle_eq RS iffD2;
     2.6  val not_leD = not_zleE RS lessD;
     2.7 -val not_lessD = zleI;
     2.8  
     2.9  val intT = Type("IntDef.int",[]);
    2.10  
     3.1 --- a/src/HOL/Nat.ML	Tue Jan 12 17:19:53 1999 +0100
     3.2 +++ b/src/HOL/Nat.ML	Wed Jan 13 08:41:28 1999 +0100
     3.3 @@ -52,13 +52,13 @@
     3.4   by (etac swap 1);
     3.5   by (ALLGOALS Asm_full_simp_tac);
     3.6  qed "not_gr0";
     3.7 -Addsimps [not_gr0];
     3.8 +AddIffs [not_gr0];
     3.9  
    3.10 -Goal "m<n ==> 0 < n";
    3.11 +(*Goal "m<n ==> 0 < n";
    3.12  by (dtac gr_implies_not0 1);
    3.13  by (Asm_full_simp_tac 1);
    3.14  qed "gr_implies_gr0";
    3.15 -Addsimps [gr_implies_gr0];
    3.16 +Addsimps [gr_implies_gr0];*)
    3.17  
    3.18  qed_goalw "Least_Suc" thy [Least_nat_def]
    3.19   "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
     4.1 --- a/src/HOL/NatDef.ML	Tue Jan 12 17:19:53 1999 +0100
     4.2 +++ b/src/HOL/NatDef.ML	Wed Jan 13 08:41:28 1999 +0100
     4.3 @@ -280,10 +280,10 @@
     4.4  qed "Suc_less_eq";
     4.5  Addsimps [Suc_less_eq];
     4.6  
     4.7 -Goal "~(Suc(n) < n)";
     4.8 +(*Goal "~(Suc(n) < n)";
     4.9  by (blast_tac (claset() addEs [Suc_lessD RS less_irrefl]) 1);
    4.10  qed "not_Suc_n_less_n";
    4.11 -(*Addsimps [not_Suc_n_less_n];*)
    4.12 +Addsimps [not_Suc_n_less_n];*)
    4.13  
    4.14  Goal "i<j ==> j<k --> Suc i < k";
    4.15  by (nat_ind_tac "k" 1);
    4.16 @@ -385,7 +385,7 @@
    4.17  qed "le_SucI";
    4.18  Addsimps[le_SucI];
    4.19  
    4.20 -bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
    4.21 +(*bind_thm ("le_Suc", not_Suc_n_less_n RS leI);*)
    4.22  
    4.23  Goalw [le_def] "m < n ==> m <= (n::nat)";
    4.24  by (blast_tac (claset() addEs [less_asym]) 1);
    4.25 @@ -473,32 +473,6 @@
    4.26    Not suitable as default simprules because they often lead to looping*)
    4.27  val not_less_simps = [not_less_less_Suc_eq, leD RS not_less_less_Suc_eq];
    4.28  
    4.29 -(** max
    4.30 -
    4.31 -Goalw [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)";
    4.32 -by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
    4.33 -by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
    4.34 -qed "le_max_iff_disj";
    4.35 -
    4.36 -Goalw [max_def] "!!z::nat. (max x y <= z) = (x <= z & y <= z)";
    4.37 -by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
    4.38 -by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
    4.39 -qed "max_le_iff_conj";
    4.40 -
    4.41 -
    4.42 -(** min **)
    4.43 -
    4.44 -Goalw [min_def] "!!z::nat. (z <= min x y) = (z <= x & z <= y)";
    4.45 -by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
    4.46 -by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
    4.47 -qed "le_min_iff_conj";
    4.48 -
    4.49 -Goalw [min_def] "!!z::nat. (min x y <= z) = (x <= z | y <= z)";
    4.50 -by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits) 1);
    4.51 -by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
    4.52 -qed "min_le_iff_disj";
    4.53 - **)
    4.54 -
    4.55  (** LEAST -- the least number operator **)
    4.56  
    4.57  Goal "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";
     5.1 --- a/src/HOL/Ord.ML	Tue Jan 12 17:19:53 1999 +0100
     5.2 +++ b/src/HOL/Ord.ML	Wed Jan 13 08:41:28 1999 +0100
     5.3 @@ -144,3 +144,9 @@
     5.4  
     5.5  (*** eliminates ~= in premises ***)
     5.6  bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
     5.7 +
     5.8 +Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
     5.9 +by (simp_tac (simpset() addsimps [order_less_le]) 1);
    5.10 +by (cut_facts_tac [linorder_linear] 1);
    5.11 +by (blast_tac (claset() addIs [order_antisym]) 1);
    5.12 +qed "linorder_not_less";