Moved some thms to Arith and to Trancl.
authornipkow
Wed Oct 25 09:49:35 1995 +0100 (1995-10-25)
changeset 1302ddfdcc9ce667
parent 1301 42782316d510
child 1303 010be89a7541
Moved some thms to Arith and to Trancl.
src/HOL/Lambda/Commutation.ML
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Lambda.ML
     1.1 --- a/src/HOL/Lambda/Commutation.ML	Wed Oct 25 09:48:29 1995 +0100
     1.2 +++ b/src/HOL/Lambda/Commutation.ML	Wed Oct 25 09:49:35 1995 +0100
     1.3 @@ -8,35 +8,6 @@
     1.4  
     1.5  open Commutation;
     1.6  
     1.7 -(* FIXME: move to Trancl *)
     1.8 -(* FIXME: add rtrancl_idemp globally *)
     1.9 -Addsimps [rtrancl_idemp];
    1.10 -
    1.11 -goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
    1.12 -bd rtrancl_mono 1;
    1.13 -bd rtrancl_mono 1;
    1.14 -by(Asm_full_simp_tac 1);
    1.15 -by(fast_tac eq_cs 1);
    1.16 -qed "rtrancl_subset";
    1.17 -
    1.18 -(* FIXME: move to Trancl *)
    1.19 -goal Trancl.thy "!!R. p:R ==> p:R^*";
    1.20 -by(res_inst_tac [("p","p")] PairE 1);
    1.21 -by(fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
    1.22 -qed "r_into_rtrancl1";
    1.23 -
    1.24 -(* FIXME: move to Trancl *)
    1.25 -goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
    1.26 -by(best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl1,
    1.27 -                           rtrancl_mono RS subsetD]) 1);
    1.28 -qed "trancl_Un_trancl";
    1.29 -
    1.30 -(* FIXME: move to Trancl *)
    1.31 -goal Commutation.thy "(R^=)^* = R^*";
    1.32 -by(fast_tac (trancl_cs addIs [rtrancl_subset,r_into_rtrancl1]) 1);
    1.33 -qed "rtrancl_reflcl";
    1.34 -Addsimps [rtrancl_reflcl];
    1.35 -
    1.36  (*** square ***)
    1.37  
    1.38  goalw Commutation.thy [square_def] "!!R. square R S T U ==> square S R U T";
    1.39 @@ -56,12 +27,11 @@
    1.40  by(fast_tac (HOL_cs addSEs [rtrancl_into_rtrancl]) 1);
    1.41  qed "square_rtrancl";
    1.42  
    1.43 -(* A big fast_tac runs out of store. Search space too large? *)
    1.44  goalw Commutation.thy [commute_def]
    1.45   "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
    1.46  bd square_reflcl 1;
    1.47  br subsetI 1;
    1.48 -be r_into_rtrancl1 1;
    1.49 +be r_into_rtrancl 1;
    1.50  bd square_sym 1;
    1.51  bd square_rtrancl 1;
    1.52  by(Asm_full_simp_tac 1);
    1.53 @@ -120,6 +90,6 @@
    1.54  by(safe_tac HOL_cs);
    1.55  be rtrancl_induct 1;
    1.56   by(fast_tac trancl_cs 1);
    1.57 - by(slow_tac (rel_cs addIs [r_into_rtrancl]
    1.58 -                     addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
    1.59 +by(slow_tac (rel_cs addIs [r_into_rtrancl]
    1.60 +                    addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
    1.61  qed "Church_Rosser_confluent";
     2.1 --- a/src/HOL/Lambda/Commutation.thy	Wed Oct 25 09:48:29 1995 +0100
     2.2 +++ b/src/HOL/Lambda/Commutation.thy	Wed Oct 25 09:49:35 1995 +0100
     2.3 @@ -9,7 +9,6 @@
     2.4  Commutation = Trancl +
     2.5  
     2.6  consts
     2.7 -  reflcl  :: "('a*'a)set => ('a*'a)set"               ("(_^=)" [100] 100)
     2.8    square  :: "[('a*'a)set,('a*'a)set,('a*'a)set,('a*'a)set] => bool"
     2.9    commute :: "[('a*'a)set,('a*'a)set] => bool"
    2.10    confluent, diamond, Church_Rosser :: "('a*'a)set => bool"
    2.11 @@ -25,7 +24,6 @@
    2.12    !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
    2.13  
    2.14  translations
    2.15 -  "r^="   == "r Un id"
    2.16    "confluent R" == "diamond(R^*)"
    2.17  
    2.18  end
     3.1 --- a/src/HOL/Lambda/Eta.ML	Wed Oct 25 09:48:29 1995 +0100
     3.2 +++ b/src/HOL/Lambda/Eta.ML	Wed Oct 25 09:49:35 1995 +0100
     3.3 @@ -4,16 +4,14 @@
     3.4      Copyright   1995 TU Muenchen
     3.5  
     3.6  Eta reduction,
     3.7 -confluence ot eta,
     3.8 +confluence of eta,
     3.9  commutation of beta/eta,
    3.10  confluence of beta+eta
    3.11  *)
    3.12  
    3.13  open Eta;
    3.14  
    3.15 -(* FIXME: add Suc_pred glovbally *)
    3.16 -Addsimps (Suc_pred :: eta.intrs);
    3.17 -
    3.18 +Addsimps eta.intrs;
    3.19  
    3.20  val eta_cases = map (eta.mk_cases db.simps)
    3.21      ["Fun s -e> z","s @ t -e> u","Var i -e> t"];
    3.22 @@ -21,37 +19,17 @@
    3.23  val beta_cases = map (beta.mk_cases db.simps)
    3.24      ["s @ t -> u","Var i -> t"];
    3.25  
    3.26 -(* FIXME: add r_into_rtrancl to trancl_cs ???
    3.27 -          build on lambda_ss which should build on trancl_cs *)
    3.28 -val eta_cs = trancl_cs addIs (beta.intrs@eta.intrs)
    3.29 +val eta_cs = lambda_cs addIs eta.intrs
    3.30                         addSEs (beta_cases@eta_cases);
    3.31  
    3.32  (*** Arithmetic lemmas ***)
    3.33  
    3.34 -goal Nat.thy "~ Suc n <= n";
    3.35 -by(simp_tac (simpset_of "Nat" addsimps [le_def]) 1);
    3.36 -qed "Suc_n_not_le_n";
    3.37 -
    3.38 -(* FIXME: move into Nat.ML *)
    3.39 -goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
    3.40 -by(nat_ind_tac "i" 1);
    3.41 -by(ALLGOALS(Asm_simp_tac));
    3.42 -qed "le_0";
    3.43 -Addsimps [le_0];
    3.44 -
    3.45  goal HOL.thy "!!P. P ==> P=True";
    3.46  by(fast_tac HOL_cs 1);
    3.47  qed "True_eq";
    3.48  
    3.49  Addsimps [less_not_sym RS True_eq];
    3.50  
    3.51 -(* FIXME: move into Nat.ML *)
    3.52 -goal Arith.thy "!!i. i<j ==> j<k --> Suc i < k";
    3.53 -by(nat_ind_tac "k" 1);
    3.54 -by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
    3.55 -by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
    3.56 -bind_thm("less_trans_Suc",result() RS mp);
    3.57 -
    3.58  goal Arith.thy "i < j --> pred i < j";
    3.59  by(nat_ind_tac "j" 1);
    3.60  by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
    3.61 @@ -224,7 +202,7 @@
    3.62  by(db.induct_tac "u" 1);
    3.63  by(ALLGOALS(asm_simp_tac (addsplit (!simpset))));
    3.64  by(fast_tac (eta_cs addIs [r_into_rtrancl]) 1);
    3.65 -by(fast_tac (eta_cs addIs [rtrancl_eta_App]) 1);
    3.66 +by(fast_tac (eta_cs addSIs [rtrancl_eta_App]) 1);
    3.67  by(fast_tac (eta_cs addSIs [rtrancl_eta_Fun,eta_lift]) 1);
    3.68  bind_thm("rtrancl_eta_subst", result() RS spec RS spec RS spec RS mp);
    3.69  
     4.1 --- a/src/HOL/Lambda/Lambda.ML	Wed Oct 25 09:48:29 1995 +0100
     4.2 +++ b/src/HOL/Lambda/Lambda.ML	Wed Oct 25 09:49:35 1995 +0100
     4.3 @@ -32,18 +32,14 @@
     4.4  by(fast_tac (HOL_cs addIs prems) 1);
     4.5  qed "leqE";
     4.6  
     4.7 -goal Arith.thy "!!i. i < j ==> Suc(pred j) = j";
     4.8 -by(fast_tac (HOL_cs addEs [lessE] addss !simpset) 1);
     4.9 -qed "Suc_pred";
    4.10 -
    4.11  goal Arith.thy "!!i. Suc i < j ==> i < pred j ";
    4.12  by (resolve_tac [Suc_less_SucD] 1);
    4.13 -by (asm_simp_tac (!simpset addsimps [Suc_pred]) 1);
    4.14 +by (Asm_simp_tac 1);
    4.15  qed "lt_pred";
    4.16  
    4.17  goal Arith.thy "!!i. [| i < Suc j; k < i |] ==> pred i < j ";
    4.18  by (resolve_tac [Suc_less_SucD] 1);
    4.19 -by (asm_simp_tac (!simpset addsimps [Suc_pred]) 1);
    4.20 +by (Asm_simp_tac 1);
    4.21  qed "gt_pred";
    4.22  
    4.23  
    4.24 @@ -54,7 +50,8 @@
    4.25  Delsimps [less_Suc_eq, subst_Var];
    4.26  Addsimps ([if_not_P, not_less_eq] @ beta.intrs);
    4.27  
    4.28 -val lambda_cs = HOL_cs addSIs beta.intrs;
    4.29 +(* don't add r_into_rtrancl! *)
    4.30 +val lambda_cs = trancl_cs addSIs beta.intrs;
    4.31  
    4.32  (*** Congruence rules for ->> ***)
    4.33  
    4.34 @@ -74,8 +71,8 @@
    4.35  qed "rtrancl_beta_AppR";
    4.36  
    4.37  goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
    4.38 -by (fast_tac (lambda_cs addIs
    4.39 -                [rtrancl_beta_AppL,rtrancl_beta_AppR,rtrancl_trans]) 1);
    4.40 +by (fast_tac (lambda_cs addSIs [rtrancl_beta_AppL,rtrancl_beta_AppR]
    4.41 +                        addIs  [rtrancl_trans]) 1);
    4.42  qed "rtrancl_beta_App";
    4.43  
    4.44  (*** subst and lift ***)
    4.45 @@ -116,7 +113,7 @@
    4.46  by (Asm_full_simp_tac 1);
    4.47  by (eres_inst_tac [("j","nat")] leqE 1);
    4.48  by (asm_full_simp_tac (addsplit(!simpset)
    4.49 -                       addsimps [less_SucI,gt_pred,Suc_pred]) 1);
    4.50 +                       addsimps [less_SucI,gt_pred]) 1);
    4.51  by (hyp_subst_tac 1);
    4.52  by (Asm_simp_tac 1);
    4.53  by (forw_inst_tac [("j","j")] lt_trans2 1);
    4.54 @@ -136,7 +133,7 @@
    4.55  by (eres_inst_tac [("i","j")] leqE 1);
    4.56  by (forward_tac  [lt_trans1] 1 THEN assume_tac 1);
    4.57  by (ALLGOALS(asm_full_simp_tac
    4.58 -               (!simpset addsimps [Suc_pred,less_SucI,gt_pred])));
    4.59 +               (!simpset addsimps [less_SucI,gt_pred])));
    4.60  by (hyp_subst_tac 1);
    4.61  by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1);
    4.62  by(split_tac [expand_if] 1);
    4.63 @@ -161,12 +158,12 @@
    4.64  by(Asm_full_simp_tac 1);
    4.65  by (forward_tac [lessI RS less_trans] 1);
    4.66  by (eresolve_tac [leqE] 1);
    4.67 -by (asm_simp_tac (!simpset addsimps [Suc_pred,lt_pred]) 2);
    4.68 +by (asm_simp_tac (!simpset addsimps [lt_pred]) 2);
    4.69  by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1);
    4.70  by (forw_inst_tac [("i","i")] (lessI RS less_trans) 1);
    4.71 -by (asm_simp_tac (!simpset addsimps [Suc_pred,lt_pred]) 1);
    4.72 +by (asm_simp_tac (!simpset addsimps [lt_pred]) 1);
    4.73  by (eres_inst_tac [("i","nat")] leqE 1);
    4.74 -by (asm_full_simp_tac (!simpset addsimps [Suc_pred,less_SucI]) 2);
    4.75 +by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 2);
    4.76  by (excluded_middle_tac "nat < i" 1);
    4.77  by (Asm_full_simp_tac 1);
    4.78  by (eres_inst_tac [("j","nat")] leqE 1);