src/HOL/Transitive_Closure.thy
 changeset 12937 0c4fd7529467 parent 12823 9d3f5056296b child 13704 854501b1e957
```     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Feb 25 20:46:09 2002 +0100
1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Feb 25 20:48:14 2002 +0100
1.3 @@ -58,9 +58,9 @@
1.4    done
1.5
1.6  theorem rtrancl_induct [consumes 1, induct set: rtrancl]:
1.7 -  (assumes a: "(a, b) : r^*"
1.8 -    and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z")
1.9 -  "P b"
1.10 +  assumes a: "(a, b) : r^*"
1.11 +    and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z"
1.12 +  shows "P b"
1.13  proof -
1.14    from a have "a = a --> P b"
1.15      by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
1.16 @@ -151,14 +151,16 @@
1.17    done
1.18
1.19  theorem rtrancl_converseD:
1.20 -  (assumes r: "(x, y) \<in> (r^-1)^*") "(y, x) \<in> r^*"
1.21 +  assumes r: "(x, y) \<in> (r^-1)^*"
1.22 +  shows "(y, x) \<in> r^*"
1.23  proof -
1.24    from r show ?thesis
1.25      by induct (rules intro: rtrancl_trans dest!: converseD)+
1.26  qed
1.27
1.28  theorem rtrancl_converseI:
1.29 -  (assumes r: "(y, x) \<in> r^*") "(x, y) \<in> (r^-1)^*"
1.30 +  assumes r: "(y, x) \<in> r^*"
1.31 +  shows "(x, y) \<in> (r^-1)^*"
1.32  proof -
1.33    from r show ?thesis
1.34      by induct (rules intro: rtrancl_trans converseI)+
1.35 @@ -168,9 +170,9 @@
1.36    by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
1.37
1.38  theorem converse_rtrancl_induct:
1.39 -  (assumes major: "(a, b) : r^*"
1.40 -   and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y")
1.41 -    "P a"
1.42 +  assumes major: "(a, b) : r^*"
1.43 +    and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
1.44 +  shows "P a"
1.45  proof -
1.46    from rtrancl_converseI [OF major]
1.47    show ?thesis
```