# HG changeset patch
# User nipkow
# Date 1022746372 -7200
# Node ID e5434b822a961088ebaddf6ea17a8d40b0de0de6
# Parent  ef8ed6adcb383626eb6114a01a3cc939147d6397
Modifications due to enhanced linear arithmetic.

diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/Hoare/Examples.ML	Thu May 30 10:12:52 2002 +0200
@@ -30,10 +30,8 @@
 by (hoare_tac (K all_tac) 1);
 (*Now prove the verification conditions*)
 by   Auto_tac;
-by    (etac gcd_nnn 4);
-by   (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3);
-by  (force_tac (claset(),
-               simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2);
+by    (etac gcd_nnn 3);
+by   (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 2);
 by (asm_simp_tac (simpset() addsimps [gcd_diff_r,less_imp_le]) 1);
 qed "Euclid_GCD";
 
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/HoareParallel/Gar_Coll.thy
--- a/src/HOL/HoareParallel/Gar_Coll.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/HoareParallel/Gar_Coll.thy	Thu May 30 10:12:52 2002 +0200
@@ -124,8 +124,6 @@
 apply(simp_all add:collector_defs Graph_defs)
 apply safe
 apply(simp_all add:nth_list_update)
-   apply (erule less_SucE)
-    apply simp+
   apply (erule less_SucE)
    apply simp+
  apply(drule le_imp_less_or_eq)
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/HoareParallel/Mul_Gar_Coll.thy
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Thu May 30 10:12:52 2002 +0200
@@ -93,7 +93,6 @@
 apply interfree_aux
 apply safe
 apply(simp_all add: nth_list_update)
-apply force+
 done
 
 lemma Mul_interfree_Redirect_Edge_Color_Target: 
@@ -112,7 +111,6 @@
 apply interfree_aux
 apply safe
 apply(simp_all add:nth_list_update)
-apply (drule not_sym,force)+
 done
 
 lemma Mul_interfree_Color_Target_Color_Target: 
@@ -122,7 +120,6 @@
 apply interfree_aux
 apply safe
 apply(simp_all add: nth_list_update)
-apply (drule not_sym,force)
 done
 
 lemmas mul_mutator_interfree = 
@@ -138,7 +135,6 @@
 apply(tactic {* TRYALL (interfree_aux_tac) *})
 apply(tactic {* ALLGOALS Clarify_tac *})
 apply (simp_all add:nth_list_update)
-apply force+
 done
 
 subsubsection {* Modular Parameterized Mutators *}
@@ -154,7 +150,7 @@
 apply oghoare
 apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
 apply(erule Mul_Mutator)
-apply(simp add:Mul_interfree_Mutator_Mutator) 
+apply(simp add:Mul_interfree_Mutator_Mutator)
 apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
 done
 
@@ -204,8 +200,6 @@
 apply(simp_all add:mul_collector_defs Graph_defs)
 apply safe
 apply(simp_all add:nth_list_update)
-   apply (erule less_SucE)
-    apply simp+
   apply (erule less_SucE)
    apply simp+
  apply(drule le_imp_less_or_eq)
@@ -1288,4 +1282,4 @@
 apply(simp add:Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append)
 done
 
-end
\ No newline at end of file
+end
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/HoareParallel/OG_Examples.thy
--- a/src/HOL/HoareParallel/OG_Examples.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Thu May 30 10:12:52 2002 +0200
@@ -136,6 +136,7 @@
  COEND
   .{False}." 
 apply oghoare
+--{* 20 vc *}
 apply auto
 done
 
@@ -169,7 +170,9 @@
 apply oghoare
 --{* 35 vc *}
 apply simp_all
+--{* 21 vc *}
 apply(tactic {* ALLGOALS Clarify_tac *})
+--{* 11 vc *}
 apply simp_all
 apply(tactic {* ALLGOALS Clarify_tac *})
 --{* 11 subgoals left *}
@@ -194,17 +197,12 @@
 apply force
 --{* 5 subgoals left *}
 prefer 5
-apply(rule conjI)
- apply clarify
-prefer 2
-apply(case_tac "j=i")
- apply simp
-apply simp
---{* 4 subgoals left *}
 apply(tactic {* ALLGOALS (case_tac "j=k") *})
+--{* 10 subgoals left *}
 apply simp_all
 apply(erule_tac x=i in allE)
 apply force
+--{* 9 subgoals left *}
 apply(case_tac "j=l")
  apply simp
  apply(erule_tac x=k in allE)
@@ -224,18 +222,21 @@
 apply force
 apply force
 apply force
+--{* 5 subgoals left *}
 apply(erule_tac x=k in allE)
 apply(erule_tac x=l in allE)
 apply(case_tac "j=l")
  apply force
 apply force
 apply force
+--{* 3 subgoals left *}
 apply(erule_tac x=k in allE)
 apply(erule_tac x=l in allE)
 apply(case_tac "j=l")
  apply force
 apply force
 apply force
+--{* 1 subgoals left *}
 apply(erule_tac x=k in allE)
 apply(erule_tac x=l in allE)
 apply(case_tac "j=l")
@@ -482,10 +483,7 @@
    COEND 
     .{\<forall>i < n. \<acute>A!i = 0}."
 apply oghoare
-apply simp_all
-  apply force+
-apply clarify
-apply (simp add:nth_list_update)
+apply force+
 done
 
 subsubsection {* Increment a Variable in Parallel *}
@@ -508,7 +506,7 @@
 apply(subgoal_tac "n - j = Suc(n- Suc j)")
   apply simp
 apply arith
-done 
+done
 
 lemma Example2_lemma2_aux2: 
   "!!b. j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
@@ -564,4 +562,4 @@
 apply(force intro: Example2_lemma3)
 done
 
-end
\ No newline at end of file
+end
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/HoareParallel/OG_Tactics.thy
--- a/src/HOL/HoareParallel/OG_Tactics.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/HoareParallel/OG_Tactics.thy	Thu May 30 10:12:52 2002 +0200
@@ -265,8 +265,7 @@
 \<and> (x#xs) ! 0=x \<and> (x#xs) ! Suc n = xs ! n"
 by simp
 lemma le_Suc_eq_insert: "{i. i <Suc n} = insert n {i. i< n}"
-apply auto
-by arith
+by auto
 lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps"
 lemmas my_simp_list = list_lemmas fst_conv snd_conv
 not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc Suc_Suc_eq
@@ -498,4 +497,4 @@
     (Method.SIMPLE_METHOD' HEADGOAL (disjE_Tac (K all_tac))) *}
   "verification condition generator for interference freedom tests"
 
-end
\ No newline at end of file
+end
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/HoareParallel/RG_Examples.thy
--- a/src/HOL/HoareParallel/RG_Examples.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Thu May 30 10:12:52 2002 +0200
@@ -147,7 +147,10 @@
     apply simp
    apply clarify
    apply simp
-   apply(case_tac j,simp,simp)
+   apply(subgoal_tac "j=0")
+    apply (rotate_tac -1)
+    apply simp
+   apply arith
   apply clarify
   apply(case_tac i,simp,simp)
  apply clarify   
@@ -324,7 +327,7 @@
     apply force
    apply(rule Basic)
       apply force
-     apply force
+     apply fastsimp
     apply force
    apply force
   apply(rule Basic)
@@ -340,7 +343,7 @@
      apply(erule_tac x=j in allE)
      apply force
     apply clarsimp
-    apply force
+    apply fastsimp
 apply force+
 done
 
@@ -399,4 +402,4 @@
 apply force+
 done
 
-end
\ No newline at end of file
+end
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Thu May 30 10:12:52 2002 +0200
@@ -1,4 +1,3 @@
-
 header {* \section{The Proof System} *}
 
 theory RG_Hoare = RG_Tran:
@@ -1143,8 +1142,7 @@
 apply(case_tac "i-length xs")
  apply arith
 apply(simp add:nth_append del:map.simps last.simps)
-apply(rule conjI,clarify,arith)
-apply clarify
+apply(rotate_tac -3)
 apply(subgoal_tac "i- Suc (length xs)=nat")
  prefer 2
  apply arith
@@ -1281,7 +1279,6 @@
  apply(case_tac "i=ib",simp)
   apply(erule etran.elims,simp)
  apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp)
- apply(erule disjE,arith)
  apply(case_tac "ia=m",simp)
   apply(erule etran.elims,simp)
  apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE)
@@ -1325,7 +1322,6 @@
 apply(case_tac "i=ia",simp)
  apply(erule etran.elims,simp)
 apply(erule_tac x="ia" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp)
- apply(erule disjE,arith)
 apply(erule_tac x=j and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
 apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
 apply(simp add:same_state_def)
@@ -1514,4 +1510,4 @@
   apply(assumption+) 
 done
 
-end
\ No newline at end of file
+end
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/HoareParallel/RG_Tran.thy
--- a/src/HOL/HoareParallel/RG_Tran.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Tran.thy	Thu May 30 10:12:52 2002 +0200
@@ -1,4 +1,3 @@
-
 header {* \section{Operational Semantics} *}
 
 theory RG_Tran = RG_Com:
@@ -617,7 +616,6 @@
    apply simp
    apply(case_tac j,simp)
     apply(rule tl_zero)
-      apply(drule_tac t=l in not_sym,simp)
       apply(erule_tac x=l in allE, erule impE, assumption, 
             erule_tac x=1 and P="\<lambda>j.  (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
       apply(force elim:etran.elims intro:Env)
@@ -654,7 +652,6 @@
     apply(erule_tac x=l  in allE, erule impE, assumption,
           erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
     apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp)
-    apply(drule not_sym,erule impE,assumption )
     apply(erule etran.elims,simp)
    apply(rule tl_zero)
     apply force
@@ -669,7 +666,6 @@
     apply(erule_tac x=ia  in allE, erule impE, assumption,
     erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
     apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp)
-    apply(drule not_sym,erule impE,assumption)
     apply(force elim:etran.elims intro:Env)
    apply force
   apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
@@ -858,7 +854,6 @@
   apply clarify
   apply(rule_tac x=i in exI,simp)
  apply clarify
- apply(drule not_sym,simp)
  apply(rule Env)
 apply simp
 apply(erule_tac x=nat and P="\<lambda>j. ?H j \<longrightarrow> (?P j \<or> ?Q j)" in allE,simp)
@@ -1075,4 +1070,4 @@
 apply(force intro:aux_if)
 done
 
-end
\ No newline at end of file
+end
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/Hyperreal/MacLaurin.ML
--- a/src/HOL/Hyperreal/MacLaurin.ML	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.ML	Thu May 30 10:12:52 2002 +0200
@@ -443,8 +443,6 @@
 
 Goal "d < (4::nat) ==> d = 0 | d = 1 | d = 2 | d = 3";
 by (case_tac "d" 1 THEN Auto_tac);
-by (case_tac "nat" 1 THEN Auto_tac);
-by (case_tac "nata" 1 THEN Auto_tac);
 qed "lemma_exhaust_less_4";
 
 bind_thm ("real_mult_le_lemma",
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/Integ/IntArith.ML	Thu May 30 10:12:52 2002 +0200
@@ -40,7 +40,6 @@
 by (etac impE 1);
  by (asm_full_simp_tac (simpset() addsimps [zabs_def] 
                                  addsplits [split_if_asm]) 1);
- by (arith_tac 1);
 by (blast_tac (claset() addIs [le_SucI]) 1);
 val lemma = result();
 
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu May 30 10:12:52 2002 +0200
@@ -79,7 +79,7 @@
 lemma Sigma_Suc2:
     "m = n + 2 ==> A <*> below m =
       (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"
-  by (auto simp add: below_def) arith
+  by (auto simp add: below_def)
 
 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2
 
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/Lambda/Eta.thy	Thu May 30 10:12:52 2002 +0200
@@ -69,9 +69,6 @@
    prefer 2
    apply simp
   apply (simp add: diff_Suc subst_Var split: nat.split)
-  apply clarify
-  apply (erule linorder_neqE)
-  apply simp_all
   done
 
 lemma free_eta [rule_format]:
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Thu May 30 10:12:52 2002 +0200
@@ -150,7 +150,6 @@
     apply (simp_all
       add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
       split: nat.split)
-  apply (auto simp add: linorder_neq_iff)
   done
 
 
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu May 30 10:12:52 2002 +0200
@@ -64,8 +64,6 @@
  by (Asm_full_simp_tac 1);
  by (blast_tac (claset() addDs [in_set_butlastD]) 1);
 by (Asm_simp_tac 1);
-by (rtac conjI 1);
- by (Blast_tac 1);
 by (strip_tac 1);
 by (etac allE 1);
 by (etac impE 1);
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/Library/Primes.thy	Thu May 30 10:12:52 2002 +0200
@@ -185,7 +185,6 @@
   apply (auto simp add: prime_def)
   apply (case_tac m)
    apply (auto dest!: dvd_imp_le)
-  apply arith
   done
 
 text {*
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/List.thy	Thu May 30 10:12:52 2002 +0200
@@ -531,7 +531,6 @@
  apply simp_all
 apply(erule ssubst)
 apply auto
-apply arith
 done
 
 lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)"
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu May 30 10:12:52 2002 +0200
@@ -174,8 +174,7 @@
 
 lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
   apply (cases "x=n0")
-  apply (auto simp add: intervall_def) 
-  apply arith
+  apply (auto simp add: intervall_def)
   done
 
 lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x" 
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/NumberTheory/Chinese.thy
--- a/src/HOL/NumberTheory/Chinese.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy	Thu May 30 10:12:52 2002 +0200
@@ -185,14 +185,11 @@
      apply (rule_tac [!] funprod_zgcd)
      apply safe
      apply simp_all
-    apply (subgoal_tac [3] "ia \<le> n")
-     prefer 4
-     apply arith
-     apply (subgoal_tac "i<n")
-     prefer 2
-     apply arith
-    apply (case_tac [2] i)
-     apply simp_all
+   apply (subgoal_tac "i<n")
+    prefer 2
+    apply arith
+   apply (case_tac [2] i)
+    apply simp_all
   done
 
 lemma aux:
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/NumberTheory/EulerFermat.thy
--- a/src/HOL/NumberTheory/EulerFermat.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy	Thu May 30 10:12:52 2002 +0200
@@ -340,10 +340,10 @@
   apply (subst RRset2norRR_eq_norR [symmetric])
     apply (rule_tac [3] inj_func_bijR)
       apply auto
-      apply (unfold zcongm_def)
-      apply (rule_tac [3] RRset2norRR_correct1)
-        apply (rule_tac [6] RRset2norRR_inj)
-         apply (auto intro: order_less_le [THEN iffD2]
+     apply (unfold zcongm_def)
+     apply (rule_tac [2] RRset2norRR_correct1)
+       apply (rule_tac [5] RRset2norRR_inj)
+        apply (auto intro: order_less_le [THEN iffD2]
 	   simp add: noX_is_RRset)
   apply (unfold noXRRset_def norRRset_def)
   apply (rule finite_imageI)
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/NumberTheory/IntPrimes.thy
--- a/src/HOL/NumberTheory/IntPrimes.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Thu May 30 10:12:52 2002 +0200
@@ -264,12 +264,10 @@
 lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
   apply (frule_tac b = n and a = m in pos_mod_sign)
   apply (simp add: zgcd_def zabs_def nat_mod_distrib)
-  apply (cut_tac a = "-m" and b = n in zmod_zminus1_eq_if)
   apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
   apply (frule_tac a = m in pos_mod_bound)
-  apply (simp add: nat_diff_distrib)
-  apply (rule gcd_diff2)
-  apply (simp add: nat_le_eq_zle)
+  apply (simp add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
+  apply (simp add: gcd_non_0 nat_mod_distrib [symmetric])
   done
 
 lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)"
@@ -707,7 +705,6 @@
    prefer 2
    apply (frule_tac a = "r'" in pos_mod_sign)
    apply auto
-   apply arith
   apply (rule exI)
   apply (rule exI)
   apply (subst xzgcda.simps)
@@ -727,7 +724,6 @@
    prefer 2
    apply (frule_tac a = "r'" in pos_mod_sign)
    apply auto
-   apply arith
   apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp)
   apply (subst xzgcda.simps)
   apply auto
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/NumberTheory/WilsonRuss.thy
--- a/src/HOL/NumberTheory/WilsonRuss.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy	Thu May 30 10:12:52 2002 +0200
@@ -344,7 +344,6 @@
    apply safe
      apply (rule_tac x = "2" in exI)
      apply auto
-  apply arith
   done
 
 theorem Wilson_Russ:
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/TLA/TLA.ML
--- a/src/HOL/TLA/TLA.ML	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/TLA/TLA.ML	Thu May 30 10:12:52 2002 +0200
@@ -999,8 +999,6 @@
  by (etac STL4E 1); 
  by (rtac DmdImpl 1);
  by (clarsimp_tac (temp_css addsimps2 [angle_def]) 1);
- by (rtac nat_less_cases 1);
- by Auto_tac;
 by (rtac (temp_use wf_box_dmd_decrease) 1);
 by (auto_tac (temp_css addSEs2 [STL4E,DmdImplE]));
 qed "nat_box_dmd_decrease";
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/ex/AVL.ML
--- a/src/HOL/ex/AVL.ML	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/ex/AVL.ML	Thu May 30 10:12:52 2002 +0200
@@ -93,7 +93,6 @@
 by (case_tac "tree1" 1);
  by (Asm_simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [max_def]) 1);
-by (arith_tac 1);
 qed_spec_mp "height_rl_rot";
 
 
diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/ex/BinEx.thy
--- a/src/HOL/ex/BinEx.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/ex/BinEx.thy	Thu May 30 10:12:52 2002 +0200
@@ -342,18 +342,35 @@
   apply (erule normal.induct)
      apply auto
   done
-
+(*
 lemma bin_minus_normal: "w \<in> normal ==> bin_minus w \<in> normal"
   apply (erule normal.induct)
      apply (simp_all add: bin_minus_BIT)
   apply (rule normal.intros)
-  apply assumption
+   apply assumption
   apply (simp add: normal_Pls_eq_0)
   apply (simp only: number_of_minus iszero_def zminus_equation [of _ "0"])
+
+The previous command should have finished the proof but the lin-arith
+procedure at the end of simplificatioon fails.
+Problem: lin-arith correctly derives the contradictory thm
+"number_of w + 1 + - 0 \<le> 0 + number_of w"  [..]
+which its local simplification setup should turn into False.
+But on the way we get
+
+Procedure "int_add_eval_numerals" produced rewrite rule:
+number_of ?v3 + 1 \<equiv> number_of (bin_add ?v3 (Pls BIT True))
+
+and eventually we arrive not at false but at
+
+"\<not> neg (number_of (bin_add w (bin_minus (bin_add w (Pls BIT True)))))"
+
+The next 2 commands should now be obsolete:
   apply (rule not_sym)
   apply simp
   done
 
+needs the previous thm:
 lemma bin_mult_normal [rule_format]:
     "w \<in> normal ==> z \<in> normal --> bin_mult w z \<in> normal"
   apply (erule normal.induct)
@@ -361,5 +378,5 @@
   apply (safe dest!: normal_BIT_D)
   apply (simp add: bin_add_normal)
   done
-
+*)
 end