Refined arithmetic.
authornipkow
Wed Jan 13 12:16:34 1999 +0100 (1999-01-13)
changeset 6115c70bce7deb0f
parent 6114 45958e54d72e
child 6116 8ba2f25610f7
Refined arithmetic.
src/HOL/Arith.ML
src/HOL/Integ/IntDef.ML
src/HOL/Nat.ML
src/HOL/NatDef.ML
src/HOL/Ord.ML
src/HOL/UNITY/Network.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Jan 13 12:08:51 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Jan 13 12:16:34 1999 +0100
     1.3 @@ -966,7 +966,7 @@
     1.4  *)
     1.5  val nat_arith_tac =
     1.6    refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
     1.7 -             ((REPEAT o etac nat_neqE) THEN' fast_nat_arith_tac);
     1.8 +             ((REPEAT_DETERM o etac nat_neqE) THEN' fast_nat_arith_tac);
     1.9  
    1.10  (*---------------------------------------------------------------------------*)
    1.11  (* End of proof procedures. Now go and USE them!                             *)
     2.1 --- a/src/HOL/Integ/IntDef.ML	Wed Jan 13 12:08:51 1999 +0100
     2.2 +++ b/src/HOL/Integ/IntDef.ML	Wed Jan 13 12:16:34 1999 +0100
     2.3 @@ -533,8 +533,6 @@
     2.4  by (simp_tac (simpset() addsimps [integ_le_less]) 1);
     2.5  qed "zle_refl";
     2.6  
     2.7 -AddIffs [le_refl];
     2.8 -
     2.9  Goalw [zle_def] "z < w ==> z <= (w::int)";
    2.10  by (blast_tac (claset() addEs [zless_asym]) 1);
    2.11  qed "zless_imp_zle";
     3.1 --- a/src/HOL/Nat.ML	Wed Jan 13 12:08:51 1999 +0100
     3.2 +++ b/src/HOL/Nat.ML	Wed Jan 13 12:16:34 1999 +0100
     3.3 @@ -54,12 +54,6 @@
     3.4  qed "not_gr0";
     3.5  AddIffs [not_gr0];
     3.6  
     3.7 -(*Goal "m<n ==> 0 < n";
     3.8 -by (dtac gr_implies_not0 1);
     3.9 -by (Asm_full_simp_tac 1);
    3.10 -qed "gr_implies_gr0";
    3.11 -Addsimps [gr_implies_gr0];*)
    3.12 -
    3.13  qed_goalw "Least_Suc" thy [Least_nat_def]
    3.14   "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    3.15   (fn _ => [
     4.1 --- a/src/HOL/NatDef.ML	Wed Jan 13 12:08:51 1999 +0100
     4.2 +++ b/src/HOL/NatDef.ML	Wed Jan 13 12:16:34 1999 +0100
     4.3 @@ -418,8 +418,6 @@
     4.4  by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
     4.5  qed "le_refl";
     4.6  
     4.7 -AddIffs [le_refl];
     4.8 -
     4.9  
    4.10  Goal "[| i <= j; j < k |] ==> i < (k::nat)";
    4.11  by (blast_tac (claset() addSDs [le_imp_less_or_eq]
     5.1 --- a/src/HOL/Ord.ML	Wed Jan 13 12:08:51 1999 +0100
     5.2 +++ b/src/HOL/Ord.ML	Wed Jan 13 12:16:34 1999 +0100
     5.3 @@ -27,7 +27,7 @@
     5.4  
     5.5  (** Reflexivity **)
     5.6  
     5.7 -Addsimps [order_refl];
     5.8 +AddIffs [order_refl];
     5.9  
    5.10  (*This form is useful with the classical reasoner*)
    5.11  Goal "!!x::'a::order. x = y ==> x <= y";
     6.1 --- a/src/HOL/UNITY/Network.ML	Wed Jan 13 12:08:51 1999 +0100
     6.2 +++ b/src/HOL/UNITY/Network.ML	Wed Jan 13 12:16:34 1999 +0100
     6.3 @@ -45,7 +45,7 @@
     6.4  by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1);
     6.5  by (assume_tac 1);
     6.6  by (ALLGOALS Asm_full_simp_tac);
     6.7 -by (Blast_tac 1);
     6.8 +by (blast_tac (claset() delrules [le0]) 1);
     6.9  by (Clarify_tac 1);
    6.10  by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
    6.11  		  "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);