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