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