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;