Moved some thms to Arith and to Trancl.

--- a/src/HOL/Lambda/Commutation.ML	Wed Oct 25 09:48:29 1995 +0100
+++ b/src/HOL/Lambda/Commutation.ML	Wed Oct 25 09:49:35 1995 +0100
@@ -8,35 +8,6 @@
 
 open Commutation;
 
-(* FIXME: move to Trancl *)
-(* FIXME: add rtrancl_idemp globally *)
-Addsimps [rtrancl_idemp];
-
-goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
-bd rtrancl_mono 1;
-bd rtrancl_mono 1;
-by(Asm_full_simp_tac 1);
-by(fast_tac eq_cs 1);
-qed "rtrancl_subset";
-
-(* FIXME: move to Trancl *)
-goal Trancl.thy "!!R. p:R ==> p:R^*";
-by(res_inst_tac [("p","p")] PairE 1);
-by(fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
-qed "r_into_rtrancl1";
-
-(* FIXME: move to Trancl *)
-goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
-by(best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl1,
-                           rtrancl_mono RS subsetD]) 1);
-qed "trancl_Un_trancl";
-
-(* FIXME: move to Trancl *)
-goal Commutation.thy "(R^=)^* = R^*";
-by(fast_tac (trancl_cs addIs [rtrancl_subset,r_into_rtrancl1]) 1);
-qed "rtrancl_reflcl";
-Addsimps [rtrancl_reflcl];
-
 (*** square ***)
 
 goalw Commutation.thy [square_def] "!!R. square R S T U ==> square S R U T";
@@ -56,12 +27,11 @@
 by(fast_tac (HOL_cs addSEs [rtrancl_into_rtrancl]) 1);
 qed "square_rtrancl";
 
-(* A big fast_tac runs out of store. Search space too large? *)
 goalw Commutation.thy [commute_def]
  "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
 bd square_reflcl 1;
 br subsetI 1;
-be r_into_rtrancl1 1;
+be r_into_rtrancl 1;
 bd square_sym 1;
 bd square_rtrancl 1;
 by(Asm_full_simp_tac 1);
@@ -120,6 +90,6 @@
 by(safe_tac HOL_cs);
 be rtrancl_induct 1;
  by(fast_tac trancl_cs 1);
- by(slow_tac (rel_cs addIs [r_into_rtrancl]
-                     addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
+by(slow_tac (rel_cs addIs [r_into_rtrancl]
+                    addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
 qed "Church_Rosser_confluent";

--- a/src/HOL/Lambda/Commutation.thy	Wed Oct 25 09:48:29 1995 +0100
+++ b/src/HOL/Lambda/Commutation.thy	Wed Oct 25 09:49:35 1995 +0100
@@ -9,7 +9,6 @@
 Commutation = Trancl +
 
 consts
-  reflcl  :: "('a*'a)set => ('a*'a)set"               ("(_^=)" [100] 100)
   square  :: "[('a*'a)set,('a*'a)set,('a*'a)set,('a*'a)set] => bool"
   commute :: "[('a*'a)set,('a*'a)set] => bool"
   confluent, diamond, Church_Rosser :: "('a*'a)set => bool"
@@ -25,7 +24,6 @@
   !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
 
 translations
-  "r^="   == "r Un id"
   "confluent R" == "diamond(R^*)"
 
 end

--- a/src/HOL/Lambda/Eta.ML	Wed Oct 25 09:48:29 1995 +0100
+++ b/src/HOL/Lambda/Eta.ML	Wed Oct 25 09:49:35 1995 +0100
@@ -4,16 +4,14 @@
     Copyright   1995 TU Muenchen
 
 Eta reduction,
-confluence ot eta,
+confluence of eta,
 commutation of beta/eta,
 confluence of beta+eta
 *)
 
 open Eta;
 
-(* FIXME: add Suc_pred glovbally *)
-Addsimps (Suc_pred :: eta.intrs);
-
+Addsimps eta.intrs;
 
 val eta_cases = map (eta.mk_cases db.simps)
     ["Fun s -e> z","s @ t -e> u","Var i -e> t"];
@@ -21,37 +19,17 @@
 val beta_cases = map (beta.mk_cases db.simps)
     ["s @ t -> u","Var i -> t"];
 
-(* FIXME: add r_into_rtrancl to trancl_cs ???
-          build on lambda_ss which should build on trancl_cs *)
-val eta_cs = trancl_cs addIs ([e-mail])
+val eta_cs = lambda_cs addIs eta.intrs
                        addSEs (beta_cases@eta_cases);
 
 (*** Arithmetic lemmas ***)
 
-goal Nat.thy "~ Suc n <= n";
-by(simp_tac (simpset_of "Nat" addsimps [le_def]) 1);
-qed "Suc_n_not_le_n";
-
-(* FIXME: move into Nat.ML *)
-goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
-by(nat_ind_tac "i" 1);
-by(ALLGOALS(Asm_simp_tac));
-qed "le_0";
-Addsimps [le_0];
-
 goal HOL.thy "!!P. P ==> P=True";
 by(fast_tac HOL_cs 1);
 qed "True_eq";
 
 Addsimps [less_not_sym RS True_eq];
 
-(* FIXME: move into Nat.ML *)
-goal Arith.thy "!!i. i<j ==> j<k --> Suc i < k";
-by(nat_ind_tac "k" 1);
-by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
-by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
-bind_thm("less_trans_Suc",result() RS mp);
-
 goal Arith.thy "i < j --> pred i < j";
 by(nat_ind_tac "j" 1);
 by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
@@ -224,7 +202,7 @@
 by(db.induct_tac "u" 1);
 by(ALLGOALS(asm_simp_tac (addsplit (!simpset))));
 by(fast_tac (eta_cs addIs [r_into_rtrancl]) 1);
-by(fast_tac (eta_cs addIs [rtrancl_eta_App]) 1);
+by(fast_tac (eta_cs addSIs [rtrancl_eta_App]) 1);
 by(fast_tac (eta_cs addSIs [rtrancl_eta_Fun,eta_lift]) 1);
 bind_thm("rtrancl_eta_subst", result() RS spec RS spec RS spec RS mp);
 

--- a/src/HOL/Lambda/Lambda.ML	Wed Oct 25 09:48:29 1995 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Wed Oct 25 09:49:35 1995 +0100
@@ -32,18 +32,14 @@
 by(fast_tac (HOL_cs addIs prems) 1);
 qed "leqE";
 
-goal Arith.thy "!!i. i < j ==> Suc(pred j) = j";
-by(fast_tac (HOL_cs addEs [lessE] addss !simpset) 1);
-qed "Suc_pred";
-
 goal Arith.thy "!!i. Suc i < j ==> i < pred j ";
 by (resolve_tac [Suc_less_SucD] 1);
-by (asm_simp_tac (!simpset addsimps [Suc_pred]) 1);
+by (Asm_simp_tac 1);
 qed "lt_pred";
 
 goal Arith.thy "!!i. [| i < Suc j; k < i |] ==> pred i < j ";
 by (resolve_tac [Suc_less_SucD] 1);
-by (asm_simp_tac (!simpset addsimps [Suc_pred]) 1);
+by (Asm_simp_tac 1);
 qed "gt_pred";
 
 
@@ -54,7 +50,8 @@
 Delsimps [less_Suc_eq, subst_Var];
 Addsimps ([if_not_P, not_less_eq] @ beta.intrs);
 
-val lambda_cs = HOL_cs addSIs beta.intrs;
+(* don't add r_into_rtrancl! *)
+val lambda_cs = trancl_cs addSIs beta.intrs;
 
 (*** Congruence rules for ->> ***)
 
@@ -74,8 +71,8 @@
 qed "rtrancl_beta_AppR";
 
 goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
-by (fast_tac (lambda_cs addIs
-                [rtrancl_beta_AppL,rtrancl_beta_AppR,rtrancl_trans]) 1);
+by (fast_tac (lambda_cs addSIs [rtrancl_beta_AppL,rtrancl_beta_AppR]
+                        addIs  [rtrancl_trans]) 1);
 qed "rtrancl_beta_App";
 
 (*** subst and lift ***)
@@ -116,7 +113,7 @@
 by (Asm_full_simp_tac 1);
 by (eres_inst_tac [("j","nat")] leqE 1);
 by (asm_full_simp_tac (addsplit(!simpset)
-                       addsimps [less_SucI,gt_pred,Suc_pred]) 1);
+                       addsimps [less_SucI,gt_pred]) 1);
 by (hyp_subst_tac 1);
 by (Asm_simp_tac 1);
 by (forw_inst_tac [("j","j")] lt_trans2 1);
@@ -136,7 +133,7 @@
 by (eres_inst_tac [("i","j")] leqE 1);
 by (forward_tac  [lt_trans1] 1 THEN assume_tac 1);
 by (ALLGOALS(asm_full_simp_tac
-               (!simpset addsimps [Suc_pred,less_SucI,gt_pred])));
+               (!simpset addsimps [less_SucI,gt_pred])));
 by (hyp_subst_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1);
 by(split_tac [expand_if] 1);
@@ -161,12 +158,12 @@
 by(Asm_full_simp_tac 1);
 by (forward_tac [lessI RS less_trans] 1);
 by (eresolve_tac [leqE] 1);
-by (asm_simp_tac (!simpset addsimps [Suc_pred,lt_pred]) 2);
+by (asm_simp_tac (!simpset addsimps [lt_pred]) 2);
 by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1);
 by (forw_inst_tac [("i","i")] (lessI RS less_trans) 1);
-by (asm_simp_tac (!simpset addsimps [Suc_pred,lt_pred]) 1);
+by (asm_simp_tac (!simpset addsimps [lt_pred]) 1);
 by (eres_inst_tac [("i","nat")] leqE 1);
-by (asm_full_simp_tac (!simpset addsimps [Suc_pred,less_SucI]) 2);
+by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 2);
 by (excluded_middle_tac "nat < i" 1);
 by (Asm_full_simp_tac 1);
 by (eres_inst_tac [("j","nat")] leqE 1);