src/HOL/Transitive_Closure.thy

 consts
   rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^*)" [1000] 999)
 
 inductive "r^*"
   intros
-    rtrancl_refl [intro!, simp]: "(a, a) : r^*"
-    rtrancl_into_rtrancl: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
+    rtrancl_refl [intro!, CPure.intro!, simp]: "(a, a) : r^*"
+    rtrancl_into_rtrancl [CPure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
 
 constdefs
   trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
   "r^+ ==  r O rtrancl r"
 

   apply (erule rtrancl.induct)
    apply (rule_tac [2] rtrancl_into_rtrancl)
     apply blast+
   done
 
-theorem rtrancl_induct [consumes 1]:
+theorem rtrancl_induct [consumes 1, induct set: rtrancl]:
   (assumes a: "(a, b) : r^*"
     and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z")
   "P b"
 proof -
   from a have "a = a --> P b"
-    by (induct "%x y. x = a --> P y" a b rule: rtrancl.induct)
-      (rules intro: cases)+
+    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
   thus ?thesis by rules
 qed
 
 ML_setup {*
   bind_thm ("rtrancl_induct2", split_rule
     (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] (thm "rtrancl_induct")));
 *}
 
 lemma trans_rtrancl: "trans(r^*)"
   -- {* transitivity of transitive closure!! -- by induction *}
-  apply (unfold trans_def)
-  apply safe
-  apply (erule_tac b = z in rtrancl_induct)
-   apply (blast intro: rtrancl_into_rtrancl)+
-  done
+proof (rule transI)
+  fix x y z
+  assume "(x, y) \<in> r\<^sup>*"
+  assume "(y, z) \<in> r\<^sup>*"
+  thus "(x, z) \<in> r\<^sup>*" by induct (rules!)+
+qed
 
 lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
 
 lemma rtranclE:
   "[| (a::'a,b) : r^*;  (a = b) ==> P;

       prefer 2 apply (blast!)
     apply (erule asm_rl exE disjE conjE prems)+
     done
 qed
 
-lemmas converse_rtrancl_into_rtrancl = r_into_rtrancl [THEN rtrancl_trans, standard]
+lemma converse_rtrancl_into_rtrancl:
+  "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
+  by (rule rtrancl_trans) rules+
 
 text {*
   \medskip More @{term "r^*"} equations and inclusions.
 *}
 

   apply (case_tac "a = b")
    apply blast
   apply (blast intro!: r_into_rtrancl)
   done
 
-lemma rtrancl_converseD: "(x, y) \<in> (r^-1)^* ==> (y, x) \<in> r^*"
-  apply (erule rtrancl_induct)
-   apply (rule rtrancl_refl)
-  apply (blast intro: rtrancl_trans)
-  done
-
-lemma rtrancl_converseI: "(y, x) \<in> r^* ==> (x, y) \<in> (r^-1)^*"
-  apply (erule rtrancl_induct)
-   apply (rule rtrancl_refl)
-  apply (blast intro: rtrancl_trans)
-  done
+theorem rtrancl_converseD:
+  (assumes r: "(x, y) \<in> (r^-1)^*") "(y, x) \<in> r^*"
+proof -
+  from r show ?thesis
+    by induct (rules intro: rtrancl_trans dest!: converseD)+
+qed
+
+theorem rtrancl_converseI:
+  (assumes r: "(y, x) \<in> r^*") "(x, y) \<in> (r^-1)^*"
+proof -
+  from r show ?thesis
+    by induct (rules intro: rtrancl_trans converseI)+
+qed
 
 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
   by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
 
-lemma converse_rtrancl_induct:
-  "[| (a,b) : r^*; P(b);
-      !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]
-    ==> P(a)"
-proof -
-  assume major: "(a,b) : r^*"
-  case rule_context
-  show ?thesis
-    apply (rule major [THEN rtrancl_converseI, THEN rtrancl_induct])
-     apply assumption
-    apply (blast! dest!: rtrancl_converseD)
-  done
+theorem converse_rtrancl_induct:
+  (assumes major: "(a, b) : r^*"
+   and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y")
+    "P a"
+proof -
+  from rtrancl_converseI [OF major]
+  show ?thesis
+    by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
 qed
 
 ML_setup {*
   bind_thm ("converse_rtrancl_induct2", split_rule
     (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")] (thm "converse_rtrancl_induct")));

   rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
   rtrancl_trancl_trancl trancl_rtrancl_trancl
 
 declare trancl_into_rtrancl [elim]
 
-declare rtrancl_induct [induct set: rtrancl]
 declare rtranclE [cases set: rtrancl]
 declare trancl_induct [induct set: trancl]
 declare tranclE [cases set: trancl]
 
 end