A few lemmas and some Adds.
authornipkow
Mon Feb 21 10:20:38 2000 +0100 (2000-02-21)
changeset 8265187cada50e19
parent 8264 fffae6147cf7
child 8266 4bc79ed1233b
A few lemmas and some Adds.
src/HOL/Relation.ML
src/HOL/Trancl.ML
src/HOL/WF.ML
     1.1 --- a/src/HOL/Relation.ML	Sun Feb 20 09:32:06 2000 +0100
     1.2 +++ b/src/HOL/Relation.ML	Mon Feb 21 10:20:38 2000 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4  Goalw [Id_def] "(a,b):Id = (a=b)";
     1.5  by (Blast_tac 1);
     1.6  qed "pair_in_Id_conv";
     1.7 -Addsimps [pair_in_Id_conv];
     1.8 +AddIffs [pair_in_Id_conv];
     1.9  
    1.10  Goalw [refl_def] "reflexive Id";
    1.11  by Auto_tac;
     2.1 --- a/src/HOL/Trancl.ML	Sun Feb 20 09:32:06 2000 +0100
     2.2 +++ b/src/HOL/Trancl.ML	Mon Feb 21 10:20:38 2000 +0100
     2.3 @@ -142,6 +142,17 @@
     2.4  qed "rtrancl_reflcl";
     2.5  Addsimps [rtrancl_reflcl];
     2.6  
     2.7 +Goal "(r - Id)^* = r^*";
     2.8 +br sym 1;
     2.9 +br rtrancl_subset 1;
    2.10 + by (Blast_tac 1);
    2.11 +by (Clarify_tac 1);
    2.12 +by(rename_tac "a b" 1);
    2.13 +by(case_tac "a=b" 1);
    2.14 + by (Blast_tac 1);
    2.15 +by(blast_tac (claset() addSIs [r_into_rtrancl]) 1);
    2.16 +qed "rtrancl_r_diff_Id";
    2.17 +
    2.18  Goal "(x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
    2.19  by (rtac converseI 1);
    2.20  by (etac rtrancl_induct 1);
    2.21 @@ -347,10 +358,7 @@
    2.22  Goal "(r^+)^= = r^*";
    2.23  by Safe_tac;
    2.24  by  (etac trancl_into_rtrancl 1);
    2.25 -by (etac rtranclE 1);
    2.26 -by  (Auto_tac );
    2.27 -by (etac rtrancl_into_trancl1 1);
    2.28 -by (assume_tac 1);
    2.29 +by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
    2.30  qed "reflcl_trancl";
    2.31  Addsimps[reflcl_trancl];
    2.32  
     3.1 --- a/src/HOL/WF.ML	Sun Feb 20 09:32:06 2000 +0100
     3.2 +++ b/src/HOL/WF.ML	Mon Feb 21 10:20:38 2000 +0100
     3.3 @@ -230,6 +230,19 @@
     3.4  Goalw [acyclic_def] "acyclic(r^-1) = acyclic r";
     3.5  by (simp_tac (simpset() addsimps [trancl_converse]) 1);
     3.6  qed "acyclic_converse";
     3.7 +AddIffs [acyclic_converse];
     3.8 +
     3.9 +Goalw [acyclic_def,antisym_def] "acyclic r ==> antisym(r^*)";
    3.10 +by(blast_tac (claset() addEs [rtranclE]
    3.11 +     addIs [rtrancl_into_trancl1,rtrancl_trancl_trancl]) 1);
    3.12 +qed "acyclic_impl_antisym_rtrancl";
    3.13 +
    3.14 +(* Other direction:
    3.15 +acyclic = no loops
    3.16 +antisym = only self loops
    3.17 +Goalw [acyclic_def,antisym_def] "antisym(r^* ) ==> acyclic(r - Id)";
    3.18 +==> "antisym(r^* ) = acyclic(r - Id)";
    3.19 +*)
    3.20  
    3.21  Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r";
    3.22  by (blast_tac (claset() addIs [trancl_mono]) 1);