# HG changeset patch
# User berghofe
# Date 1263143190 -3600
# Node ID a799687944af75724cae223f5d99828660ac90d0
# Parent  d546e75631bb68568a2c759a2605689e9bc4bbd6
Tuned some proofs; nicer case names for some of the induction / cases rules.

diff -r d546e75631bb -r a799687944af src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sun Jan 10 18:03:20 2010 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sun Jan 10 18:06:30 2010 +0100
@@ -106,12 +106,8 @@
 theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]:
   assumes a: "r^** a b"
     and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z"
-  shows "P b"
-proof -
-  from a have "a = a --> P b"
-    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
-  then show ?thesis by iprover
-qed
+  shows "P b" using a
+  by (induct x\<equiv>a b) (rule cases)+
 
 lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set]
 
@@ -257,7 +253,7 @@
 lemma sym_rtrancl: "sym r ==> sym (r^*)"
   by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric])
 
-theorem converse_rtranclp_induct[consumes 1]:
+theorem converse_rtranclp_induct [consumes 1, case_names base step]:
   assumes major: "r^** a b"
     and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y"
   shows "P a"
@@ -274,7 +270,7 @@
   converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),
                  consumes 1, case_names refl step]
 
-lemma converse_rtranclpE:
+lemma converse_rtranclpE [consumes 1, case_names base step]:
   assumes major: "r^** x z"
     and cases: "x=z ==> P"
       "!!y. [| r x y; r^** y z |] ==> P"
@@ -352,15 +348,11 @@
 
 text {* Nice induction rule for @{text trancl} *}
 lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]:
-  assumes "r^++ a b"
+  assumes a: "r^++ a b"
   and cases: "!!y. r a y ==> P y"
     "!!y z. r^++ a y ==> r y z ==> P y ==> P z"
-  shows "P b"
-proof -
-  from `r^++ a b` have "a = a --> P b"
-    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
-  then show ?thesis by iprover
-qed
+  shows "P b" using a
+  by (induct x\<equiv>a b) (iprover intro: cases)+
 
 lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set]
 
@@ -484,7 +476,7 @@
 lemma sym_trancl: "sym r ==> sym (r^+)"
   by (simp only: sym_conv_converse_eq trancl_converse [symmetric])
 
-lemma converse_tranclp_induct:
+lemma converse_tranclp_induct [consumes 1, case_names base step]:
   assumes major: "r^++ a b"
     and cases: "!!y. r y b ==> P(y)"
       "!!y z.[| r y z;  r^++ z b;  P(z) |] ==> P(y)"