# HG changeset patch
# User nipkow
# Date 881423319 -3600
# Node ID 2cba48b0f1c4e5e564465fab9f86092949b79d97
# Parent  407f786d305979ee8f71a3c9bfb2756f9f0cb70b
Cleaned up arithmetic mess.

diff -r 407f786d3059 -r 2cba48b0f1c4 src/HOLCF/IOA/NTP/Impl.ML
--- a/src/HOLCF/IOA/NTP/Impl.ML	Fri Dec 05 18:46:18 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.ML	Sat Dec 06 16:48:39 1997 +0100
@@ -111,8 +111,8 @@
 by (rtac impI 1);
 by (REPEAT (etac conjE 1));
 by (asm_simp_tac (simpset() addsimps [hdr_sum_def, Multiset.count_def,
-                               Multiset.countm_nonempty_def]
-                     setloop (split_tac [expand_if])) 1);
+                                      Multiset.countm_nonempty_def]
+                            addsplits [expand_if]) 1);
 (* detour 2 *)
 by (tac 1);
 by (tac_ren 1);
@@ -121,16 +121,13 @@
 by (asm_full_simp_tac (simpset() addsimps [Impl.hdr_sum_def, 
                                          Multiset.count_def,
                                          Multiset.countm_nonempty_def,
-                                         Multiset.delm_nonempty_def,
-                                         left_plus_cancel,
-                                         left_plus_cancel_inside_succ,
-                                         unzero_less]
-                               setloop (split_tac [expand_if])) 1);
+                                         Multiset.delm_nonempty_def]
+                                 addsplits [expand_if]) 1);
 by (rtac allI 1);
 by (rtac conjI 1);
 by (rtac impI 1);
 by (hyp_subst_tac 1);
-by (rtac (pred_suc RS mp RS sym RS iffD2) 1);
+by (rtac (pred_suc RS iffD1) 1);
 by (dtac less_le_trans 1);
 by (cut_facts_tac [rewrite_rule[Packet.hdr_def]
                    eq_packet_imp_eq_hdr RS countm_props] 1);;
@@ -199,8 +196,7 @@
   by (rtac impI 1);
   by (rtac impI 1);
   by (REPEAT (etac conjE 1));
-  by (dres_inst_tac [("k","count (rsch s) (~sbit(sen s))")] 
-                     (standard(leq_add_leq RS mp)) 1);
+  by (dres_inst_tac [("k","count (rsch s) (~sbit(sen s))")] le_imp_add_le 1);
   by (Asm_full_simp_tac 1);
 
   (* 1 *)
@@ -211,8 +207,7 @@
   by (rtac impI 1);
   by (REPEAT (etac conjE 1));
   by (fold_tac  [rewrite_rule[Packet.hdr_def]Impl.hdr_sum_def]);
-  by (dres_inst_tac [("k","hdr_sum (srch s) (sbit(sen s))")] 
-                     (standard(leq_add_leq RS mp)) 1);
+  by (dres_inst_tac [("k","hdr_sum (srch s) (sbit(sen s))")] le_imp_add_le 1);
   by (Asm_full_simp_tac 1);
 qed "inv2";
 
@@ -267,7 +262,7 @@
                                 (inv1 RS invariantE) RS conjunct2] 1);
   by (asm_full_simp_tac (simpset() addsimps
                          [hdr_sum_def, Multiset.count_def]) 1);
-  by (rtac (less_eq_add_cong RS mp RS mp) 1);
+  by (rtac add_le_mono 1);
   by (rtac countm_props 1);
   by (Simp_tac 1);
   by (rtac countm_props 1);
@@ -331,7 +326,7 @@
   by (Asm_full_simp_tac 1);
   by (eres_inst_tac [("x","m")] allE 1);
   by (dtac less_le_trans 1);
-  by (dtac (left_add_leq RS mp) 1);
+  by (dtac add_leD1 1);
   by (Asm_full_simp_tac 1);
   by (Asm_full_simp_tac 1);
 qed "inv4";
diff -r 407f786d3059 -r 2cba48b0f1c4 src/HOLCF/IOA/NTP/Lemmas.ML
--- a/src/HOLCF/IOA/NTP/Lemmas.ML	Fri Dec 05 18:46:18 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Sat Dec 06 16:48:39 1997 +0100
@@ -3,9 +3,6 @@
     Author:     Tobias Nipkow & Konrad Slind
     Copyright   1994  TU Muenchen
 
-(Mostly) Arithmetic lemmas
-Should realy go in Arith.ML.
-Also: Get rid of all the --> in favour of ==> !!!
 *)
 
 (* Logic *)
@@ -13,10 +10,6 @@
   by(fast_tac (claset() addDs prems) 1);
 qed "imp_conj_lemma";
 
-goal HOL.thy "(P --> (? x. Q(x))) = (? x. P --> Q(x))";
-  by(Fast_tac 1);
-qed "imp_ex_equiv";
-
 goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
   by (Fast_tac 1);
 qed "fork_lemma";
@@ -29,20 +22,6 @@
   by (Fast_tac 1);
 qed "neg_flip";
 
-goal HOL.thy "P --> Q(M) --> Q(if P then M else N)";
-  by (rtac impI 1); 
-  by (rtac impI 1);
-  by (rtac (expand_if RS iffD2) 1);
-  by (Fast_tac 1);
-qed "imp_true_decompose";
-
-goal HOL.thy "(~P) --> Q(N) --> Q(if P then M else N)";
-  by (rtac impI 1); 
-  by (rtac impI 1);
-  by (rtac (expand_if RS iffD2) 1);
-  by (Fast_tac 1);
-qed "imp_false_decompose";
-
 
 (* Sets *)
 val set_lemmas =
@@ -53,159 +32,12 @@
          "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
 
 
-(* Arithmetic *)	(* FIXME cleanup *)
-
-goal Arith.thy "n ~= 0 --> Suc(m+pred(n)) = m+n";
-  by (nat_ind_tac "n" 1);
-  by (REPEAT(Simp_tac 1));
-val Suc_pred_lemma = store_thm("Suc_pred_lemma", result() RS mp);
-
-goal Arith.thy "((m::nat) + n = m + p) = (n = p)";
-  by (nat_ind_tac "m" 1);
-  by (Simp_tac 1);
-  by (Asm_simp_tac 1);
-qed "left_plus_cancel";
-
-goal Arith.thy "((x::nat) + y = Suc(x + z)) = (y = Suc(z))";
-  by (nat_ind_tac "x" 1);
-  by (Simp_tac 1);
-  by (Asm_simp_tac 1);
-qed "left_plus_cancel_inside_succ";
-
-goal Arith.thy "(x ~= 0) = (? y. x = Suc(y))";
-  by (nat_ind_tac "x" 1);
-  by (Simp_tac 1);
-  by (Asm_simp_tac 1);
-qed "nonzero_is_succ";
-
-goal Arith.thy "(m::nat) < n --> m + p < n + p";
-  by (nat_ind_tac "p" 1);
-  by (Simp_tac 1);
-  by (Asm_simp_tac 1);
-qed "less_add_same_less";
-
-goal Arith.thy "(x::nat)<= y --> x<=y+k";
-  by (nat_ind_tac "k" 1);
-  by (Simp_tac 1);
-  by (Asm_full_simp_tac 1);
-qed "leq_add_leq";
-
-goal Arith.thy "(x::nat) + y <= z --> x <= z";
-  by (nat_ind_tac "y" 1);
-  by (Simp_tac 1);
-  by (Asm_simp_tac 1);
-  by (rtac impI 1);
-  by (dtac Suc_leD 1);
-  by (Fast_tac 1);
-qed "left_add_leq";
-
-goal Arith.thy "(A::nat) < B --> C < D --> A + C < B + D";
- by (rtac impI 1);
- by (rtac impI 1);
- by (rtac less_trans 1);
- by (rtac (less_add_same_less RS mp) 1);
- by (assume_tac 1);
- by (rtac (add_commute RS ssubst)1);;
- by (res_inst_tac [("m1","B")] (add_commute RS ssubst) 1);
- by (rtac (less_add_same_less RS mp) 1);
- by (assume_tac 1);
-qed "less_add_cong";
+(* Arithmetic *)
 
-goal Arith.thy "(A::nat) <= B --> C <= D --> A + C <= B + D";
-  by (rtac impI 1);
-  by (rtac impI 1);
-  by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
-  by (safe_tac (claset()));
-  by (rtac (less_add_cong RS mp RS mp) 1);
-  by (assume_tac 1);
-  by (assume_tac 1);
-  by (rtac (less_add_same_less RS mp) 1);
-  by (assume_tac 1);
-  by (rtac (add_commute RS ssubst)1);;
-  by (res_inst_tac [("m1","B")] (add_commute RS ssubst) 1);
-  by (rtac (less_add_same_less RS mp) 1);
-  by (assume_tac 1);
-qed "less_eq_add_cong";
-
-goal Arith.thy "(w <= y) --> ((x::nat) + y <= z) --> (x + w <= z)";
-  by (rtac impI 1); 
-  by (dtac (less_eq_add_cong RS mp) 1);
-  by (cut_facts_tac [le_refl] 1);
-  by (dres_inst_tac [("P","x<=x")] mp 1);by (assume_tac 1);
-  by (asm_full_simp_tac (simpset() delsimprocs nat_cancel addsimps [add_commute]) 1);
-  by (rtac impI 1);
-  by (etac le_trans 1);
-  by (assume_tac 1);
-qed "leq_add_left_cong";
-
-goal Arith.thy "(? x. y = Suc(x)) = (~(y = 0))";
-  by (nat_ind_tac "y" 1);
-  by (Simp_tac 1);
-  by (rtac iffI 1);
-  by (Asm_full_simp_tac 1);
-  by (Fast_tac 1);
-qed "suc_not_zero";
-
-goal Arith.thy "Suc(x) <= y --> (? z. y = Suc(z))";
-  by (rtac impI 1);
-  by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
-  by (safe_tac (claset()));
-  by (Fast_tac 2);
-  by (asm_simp_tac (simpset() addsimps [suc_not_zero]) 1);
-qed "suc_leq_suc";
-
-goal Arith.thy "~0<n --> n = 0";
-  by (nat_ind_tac "n" 1);
-  by (Auto_tac ());
-qed "zero_eq";
-
-goal Arith.thy "x < Suc(y) --> x<=y";
-  by (nat_ind_tac "n" 1);
-  by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
-  by (safe_tac (claset()));
-  by (etac less_imp_le 1);
-qed "less_suc_imp_leq";
-
-goal Arith.thy "0<x --> Suc(pred(x)) = x";
-  by (nat_ind_tac "x" 1);
-  by (Simp_tac 1);
-  by (Asm_simp_tac 1);
-qed "suc_pred_id";
-
-goal Arith.thy "0<x --> (pred(x) = y) = (x = Suc(y))";
-  by (nat_ind_tac "x" 1);
-  by (Simp_tac 1);
-  by (Asm_simp_tac 1);
+goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
+by(asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
+by(Blast_tac 1);
 qed "pred_suc";
 
-goal Arith.thy "(x ~= 0) = (0<x)";
-  by (nat_ind_tac "x" 1);
-  by (Simp_tac 1);
-  by (Asm_simp_tac 1);
-qed "unzero_less";
 
-(* Odd proof. Why do induction? *)
-goal Arith.thy "((x::nat) = y + z) --> (y <= x)";
-  by (nat_ind_tac "y" 1);
-  by (Simp_tac 1);
-  by (simp_tac (simpset() addsimps [le_refl RS (leq_add_leq RS mp)]) 1);
-qed "plus_leq_lem";
-
-(* Lists *)
-
-val list_ss = simpset_of List.thy;
-
-goal List.thy "(xs @ (y#ys)) ~= []";
-  by (list.induct_tac "xs" 1);
-  by (simp_tac list_ss 1);
-  by (asm_simp_tac list_ss 1);
-qed "append_cons";
-
-goal List.thy "(x ~= hd(xs@ys)) = (x ~= (if xs = [] then hd ys else hd xs))";
-  by (list.induct_tac "xs" 1);
-  by (simp_tac list_ss 1);
-  by (asm_full_simp_tac list_ss 1);
-qed "not_hd_append";
-
-
-Addsimps ([append_cons,not_hd_append,Suc_pred_lemma] @ set_lemmas);
+Addsimps (hd_append :: set_lemmas);
diff -r 407f786d3059 -r 2cba48b0f1c4 src/HOLCF/IOA/NTP/Multiset.ML
--- a/src/HOLCF/IOA/NTP/Multiset.ML	Fri Dec 05 18:46:18 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Multiset.ML	Sat Dec 06 16:48:39 1997 +0100
@@ -42,7 +42,7 @@
   by (res_inst_tac [("M","M")] Multiset.induction 1);
   by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
   by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
-  by (etac (less_eq_add_cong RS mp RS mp) 1);
+  by (etac add_le_mono 1);
   by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]
                                   setloop (split_tac [expand_if])) 1);
 qed "countm_props";
@@ -76,9 +76,8 @@
                            Multiset.countm_empty_def]) 1);
   by (asm_simp_tac (simpset() addsimps 
                       [eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def,
-                       Multiset.countm_nonempty_def,pos_count_imp_pos_countm,
-                       suc_pred_id]
-                    setloop (split_tac [expand_if])) 1);
+                       Multiset.countm_nonempty_def,pos_count_imp_pos_countm]
+                    addsplits [expand_if]) 1);
 qed "countm_done_delm";