# HG changeset patch # User nipkow # Date 951124838 -3600 # Node ID 187cada50e19f66da3b831386d9a0da1066f21f0 # Parent fffae6147cf7ac620fa6a47916cde226a16f7828 A few lemmas and some Adds. diff -r fffae6147cf7 -r 187cada50e19 src/HOL/Relation.ML --- a/src/HOL/Relation.ML Sun Feb 20 09:32:06 2000 +0100 +++ b/src/HOL/Relation.ML Mon Feb 21 10:20:38 2000 +0100 @@ -21,7 +21,7 @@ Goalw [Id_def] "(a,b):Id = (a=b)"; by (Blast_tac 1); qed "pair_in_Id_conv"; -Addsimps [pair_in_Id_conv]; +AddIffs [pair_in_Id_conv]; Goalw [refl_def] "reflexive Id"; by Auto_tac; diff -r fffae6147cf7 -r 187cada50e19 src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Sun Feb 20 09:32:06 2000 +0100 +++ b/src/HOL/Trancl.ML Mon Feb 21 10:20:38 2000 +0100 @@ -142,6 +142,17 @@ qed "rtrancl_reflcl"; Addsimps [rtrancl_reflcl]; +Goal "(r - Id)^* = r^*"; +br sym 1; +br rtrancl_subset 1; + by (Blast_tac 1); +by (Clarify_tac 1); +by(rename_tac "a b" 1); +by(case_tac "a=b" 1); + by (Blast_tac 1); +by(blast_tac (claset() addSIs [r_into_rtrancl]) 1); +qed "rtrancl_r_diff_Id"; + Goal "(x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1"; by (rtac converseI 1); by (etac rtrancl_induct 1); @@ -347,10 +358,7 @@ Goal "(r^+)^= = r^*"; by Safe_tac; by (etac trancl_into_rtrancl 1); -by (etac rtranclE 1); -by (Auto_tac ); -by (etac rtrancl_into_trancl1 1); -by (assume_tac 1); +by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1); qed "reflcl_trancl"; Addsimps[reflcl_trancl]; diff -r fffae6147cf7 -r 187cada50e19 src/HOL/WF.ML --- a/src/HOL/WF.ML Sun Feb 20 09:32:06 2000 +0100 +++ b/src/HOL/WF.ML Mon Feb 21 10:20:38 2000 +0100 @@ -230,6 +230,19 @@ Goalw [acyclic_def] "acyclic(r^-1) = acyclic r"; by (simp_tac (simpset() addsimps [trancl_converse]) 1); qed "acyclic_converse"; +AddIffs [acyclic_converse]; + +Goalw [acyclic_def,antisym_def] "acyclic r ==> antisym(r^*)"; +by(blast_tac (claset() addEs [rtranclE] + addIs [rtrancl_into_trancl1,rtrancl_trancl_trancl]) 1); +qed "acyclic_impl_antisym_rtrancl"; + +(* Other direction: +acyclic = no loops +antisym = only self loops +Goalw [acyclic_def,antisym_def] "antisym(r^* ) ==> acyclic(r - Id)"; +==> "antisym(r^* ) = acyclic(r - Id)"; +*) Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r"; by (blast_tac (claset() addIs [trancl_mono]) 1);