src/HOL/Trancl.ML
changeset 5771 7c2c8cf20221
parent 5608 a82a038a3e7a
child 6162 484adda70b65
     1.1 --- a/src/HOL/Trancl.ML	Mon Oct 26 13:05:08 1998 +0100
     1.2 +++ b/src/HOL/Trancl.ML	Wed Oct 28 11:25:38 1998 +0100
     1.3 @@ -6,9 +6,9 @@
     1.4  Theorems about the transitive closure of a relation
     1.5  *)
     1.6  
     1.7 -open Trancl;
     1.8 +(** The relation rtrancl **)
     1.9  
    1.10 -(** The relation rtrancl **)
    1.11 +section "^*";
    1.12  
    1.13  Goal "mono(%s. Id Un (r O s))";
    1.14  by (rtac monoI 1);
    1.15 @@ -195,6 +195,8 @@
    1.16  
    1.17  (**** The relation trancl ****)
    1.18  
    1.19 +section "^+";
    1.20 +
    1.21  Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
    1.22  by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
    1.23  qed "trancl_mono";
    1.24 @@ -296,6 +298,24 @@
    1.25  				  r_comp_rtrancl_eq]) 1);
    1.26  qed "trancl_converse";
    1.27  
    1.28 +Goal "(x,y) : (r^+)^-1 ==> (x,y) : (r^-1)^+";
    1.29 +by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
    1.30 +qed "trancl_converseI";
    1.31 +
    1.32 +Goal "(x,y) : (r^-1)^+ ==> (x,y) : (r^+)^-1";
    1.33 +by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
    1.34 +qed "trancl_converseD";
    1.35 +
    1.36 +val major::prems = Goal
    1.37 +    "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); \
    1.38 +\       !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]  \
    1.39 +\     ==> P(a)";
    1.40 +by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
    1.41 + by (resolve_tac prems 1);
    1.42 + be converseD 1;
    1.43 +by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
    1.44 +qed "converse_trancl_induct";
    1.45 +
    1.46  (*Unused*)
    1.47  qed_goal "irrefl_tranclI" Trancl.thy 
    1.48     "!!r. r^-1 Int r^+ = {} ==> (x, x) ~: r^+"