src/HOL/Transitive_Closure.thy
 changeset 14404 4952c5a92e04 parent 14398 c5c47703f763 child 14565 c6dc17aab88a
```     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Feb 20 14:22:51 2004 +0100
1.2 +++ b/src/HOL/Transitive_Closure.thy	Sat Feb 21 08:43:08 2004 +0100
1.3 @@ -70,11 +70,10 @@
1.4    thus ?thesis by rules
1.5  qed
1.6
1.7 -ML_setup {*
1.8 -  bind_thm ("rtrancl_induct2", split_rule
1.9 -    (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] (thm "rtrancl_induct")));
1.10 -*}
1.11 -
1.12 +lemmas rtrancl_induct2 =
1.13 +  rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
1.14 +                 consumes 1, case_names refl step]
1.15 +
1.16  lemma trans_rtrancl: "trans(r^*)"
1.17    -- {* transitivity of transitive closure!! -- by induction *}
1.18  proof (rule transI)
1.19 @@ -165,7 +164,7 @@
1.20  lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
1.21    by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
1.22
1.23 -theorem converse_rtrancl_induct:
1.24 +theorem converse_rtrancl_induct[consumes 1]:
1.25    assumes major: "(a, b) : r^*"
1.26      and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
1.27    shows "P a"
1.28 @@ -175,10 +174,9 @@
1.29      by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
1.30  qed
1.31
1.32 -ML_setup {*
1.33 -  bind_thm ("converse_rtrancl_induct2", split_rule
1.34 -    (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")] (thm "converse_rtrancl_induct")));
1.35 -*}
1.36 +lemmas converse_rtrancl_induct2 =
1.37 +  converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
1.38 +                 consumes 1, case_names refl step]
1.39
1.40  lemma converse_rtranclE:
1.41    "[| (x,z):r^*;
```