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)"