added rtranclIs
authornipkow
Mon Oct 09 19:49:58 2000 +0200 (2000-10-09)
changeset 101799d5678e6bf34
parent 10178 aecb5bf6f76f
child 10180 149878bae19c
added rtranclIs
src/HOL/Induct/Comb.ML
src/HOL/Lambda/Commutation.thy
src/HOL/Trancl.ML
src/HOL/UNITY/Reach.ML
     1.1 --- a/src/HOL/Induct/Comb.ML	Mon Oct 09 19:20:55 2000 +0200
     1.2 +++ b/src/HOL/Induct/Comb.ML	Mon Oct 09 19:49:58 2000 +0200
     1.3 @@ -65,12 +65,12 @@
     1.4  
     1.5  Goal "x ---> y ==> x#z ---> y#z";
     1.6  by (etac rtrancl_induct 1);
     1.7 -by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
     1.8 +by (ALLGOALS (blast_tac (claset() addIs rtranclIs)));
     1.9  qed "Ap_reduce1";
    1.10  
    1.11  Goal "x ---> y ==> z#x ---> z#y";
    1.12  by (etac rtrancl_induct 1);
    1.13 -by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
    1.14 +by (ALLGOALS (blast_tac (claset() addIs rtranclIs)));
    1.15  qed "Ap_reduce2";
    1.16  
    1.17  (** Counterexample to the diamond property for -1-> **)
     2.1 --- a/src/HOL/Lambda/Commutation.thy	Mon Oct 09 19:20:55 2000 +0200
     2.2 +++ b/src/HOL/Lambda/Commutation.thy	Mon Oct 09 19:49:58 2000 +0200
     2.3 @@ -132,7 +132,7 @@
     2.4         rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
     2.5    apply (erule rtrancl_induct)
     2.6     apply blast
     2.7 -  apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)
     2.8 +  apply (blast del: rtrancl_refl intro: rtranclIs)
     2.9    done
    2.10  
    2.11 -end
    2.12 \ No newline at end of file
    2.13 +end
     3.1 --- a/src/HOL/Trancl.ML	Mon Oct 09 19:20:55 2000 +0200
     3.2 +++ b/src/HOL/Trancl.ML	Mon Oct 09 19:49:58 2000 +0200
     3.3 @@ -97,7 +97,7 @@
     3.4  qed "rtranclE";
     3.5  
     3.6  bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
     3.7 -
     3.8 +bind_thms("rtranclIs", [r_into_rtrancl, rtrancl_trans]);
     3.9  
    3.10  (*** More r^* equations and inclusions ***)
    3.11  
    3.12 @@ -106,14 +106,14 @@
    3.13  by (etac r_into_rtrancl 2);
    3.14  by (etac rtrancl_induct 1);
    3.15  by (rtac rtrancl_refl 1);
    3.16 -by (blast_tac (claset() addIs [rtrancl_trans]) 1);
    3.17 +by (blast_tac (claset() addIs rtranclIs) 1);
    3.18  qed "rtrancl_idemp";
    3.19  Addsimps [rtrancl_idemp];
    3.20  
    3.21  Goal "R^* O R^* = R^*";
    3.22  by (rtac set_ext 1);
    3.23  by (split_all_tac 1);
    3.24 -by (blast_tac (claset() addIs [rtrancl_trans]) 1);
    3.25 +by (blast_tac (claset() addIs rtranclIs) 1);
    3.26  qed "rtrancl_idemp_self_comp";
    3.27  Addsimps [rtrancl_idemp_self_comp];
    3.28  
    3.29 @@ -153,13 +153,13 @@
    3.30  Goal "(x,y) : (r^-1)^* ==> (y,x) : r^*";
    3.31  by (etac rtrancl_induct 1);
    3.32  by (rtac rtrancl_refl 1);
    3.33 -by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
    3.34 +by (blast_tac (claset() addIs rtranclIs) 1);
    3.35  qed "rtrancl_converseD";
    3.36  
    3.37  Goal "(y,x) : r^* ==> (x,y) : (r^-1)^*";
    3.38  by (etac rtrancl_induct 1);
    3.39  by (rtac rtrancl_refl 1);
    3.40 -by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
    3.41 +by (blast_tac (claset() addIs rtranclIs) 1);
    3.42  qed "rtrancl_converseI";
    3.43  
    3.44  Goal "(r^-1)^* = (r^*)^-1";
    3.45 @@ -288,7 +288,7 @@
    3.46  bind_thm ("trancl_trans", trans_trancl RS transD);
    3.47  
    3.48  Goalw [trancl_def] "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
    3.49 -by (blast_tac (claset() addIs [rtrancl_trans,r_into_rtrancl]) 1);
    3.50 +by (blast_tac (claset() addIs rtranclIs) 1);
    3.51  qed "rtrancl_trancl_trancl";
    3.52  
    3.53  (* "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+" *)
     4.1 --- a/src/HOL/UNITY/Reach.ML	Mon Oct 09 19:20:55 2000 +0200
     4.2 +++ b/src/HOL/UNITY/Reach.ML	Mon Oct 09 19:49:58 2000 +0200
     4.3 @@ -31,7 +31,7 @@
     4.4  
     4.5  Goal "Rprg : Always reach_invariant";
     4.6  by (always_tac 1);
     4.7 -by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
     4.8 +by (blast_tac (claset() addIs rtranclIs) 1);
     4.9  qed "reach_invariant";
    4.10  
    4.11  
    4.12 @@ -42,7 +42,7 @@
    4.13       "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
    4.14  by (rtac equalityI 1);
    4.15  by (auto_tac (claset() addSIs [ext], simpset()));
    4.16 -by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2);
    4.17 +by (blast_tac (claset() addIs rtranclIs) 2);
    4.18  by (etac rtrancl_induct 1);
    4.19  by Auto_tac;
    4.20  qed "fixedpoint_invariant_correct";