src/HOL/Transitive_Closure.thy
 changeset 34909 a799687944af parent 33878 85102f57b4a8 child 34970 4c316d777461
```     1.1 --- a/src/HOL/Transitive_Closure.thy	Sun Jan 10 18:03:20 2010 +0100
1.2 +++ b/src/HOL/Transitive_Closure.thy	Sun Jan 10 18:06:30 2010 +0100
1.3 @@ -106,12 +106,8 @@
1.4  theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]:
1.5    assumes a: "r^** a b"
1.6      and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z"
1.7 -  shows "P b"
1.8 -proof -
1.9 -  from a have "a = a --> P b"
1.10 -    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
1.11 -  then show ?thesis by iprover
1.12 -qed
1.13 +  shows "P b" using a
1.14 +  by (induct x\<equiv>a b) (rule cases)+
1.15
1.16  lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set]
1.17
1.18 @@ -257,7 +253,7 @@
1.19  lemma sym_rtrancl: "sym r ==> sym (r^*)"
1.20    by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric])
1.21
1.22 -theorem converse_rtranclp_induct[consumes 1]:
1.23 +theorem converse_rtranclp_induct [consumes 1, case_names base step]:
1.24    assumes major: "r^** a b"
1.25      and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y"
1.26    shows "P a"
1.27 @@ -274,7 +270,7 @@
1.28    converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),
1.29                   consumes 1, case_names refl step]
1.30
1.31 -lemma converse_rtranclpE:
1.32 +lemma converse_rtranclpE [consumes 1, case_names base step]:
1.33    assumes major: "r^** x z"
1.34      and cases: "x=z ==> P"
1.35        "!!y. [| r x y; r^** y z |] ==> P"
1.36 @@ -352,15 +348,11 @@
1.37
1.38  text {* Nice induction rule for @{text trancl} *}
1.39  lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]:
1.40 -  assumes "r^++ a b"
1.41 +  assumes a: "r^++ a b"
1.42    and cases: "!!y. r a y ==> P y"
1.43      "!!y z. r^++ a y ==> r y z ==> P y ==> P z"
1.44 -  shows "P b"
1.45 -proof -
1.46 -  from `r^++ a b` have "a = a --> P b"
1.47 -    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
1.48 -  then show ?thesis by iprover
1.49 -qed
1.50 +  shows "P b" using a
1.51 +  by (induct x\<equiv>a b) (iprover intro: cases)+
1.52
1.53  lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set]
1.54
1.55 @@ -484,7 +476,7 @@
1.56  lemma sym_trancl: "sym r ==> sym (r^+)"
1.57    by (simp only: sym_conv_converse_eq trancl_converse [symmetric])
1.58
1.59 -lemma converse_tranclp_induct:
1.60 +lemma converse_tranclp_induct [consumes 1, case_names base step]:
1.61    assumes major: "r^++ a b"
1.62      and cases: "!!y. r y b ==> P(y)"
1.63        "!!y z.[| r y z;  r^++ z b;  P(z) |] ==> P(y)"
```