src/HOL/Transitive_Closure.thy

--- a/src/HOL/Transitive_Closure.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -74,8 +74,8 @@
   shows "P b"
 proof -
   from a have "a = a --> P b"
-    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
-  thus ?thesis by rules
+    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
+  thus ?thesis by iprover
 qed
 
 lemmas rtrancl_induct2 =
@@ -88,7 +88,7 @@
   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!)+
+  thus "(x, z) \<in> r\<^sup>*" by induct (iprover!)+
 qed
 
 lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
@@ -112,7 +112,7 @@
 
 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+
+  by (rule rtrancl_trans) iprover+
 
 text {*
   \medskip More @{term "r^*"} equations and inclusions.
@@ -158,7 +158,7 @@
   shows "(y, x) \<in> r^*"
 proof -
   from r show ?thesis
-    by induct (rules intro: rtrancl_trans dest!: converseD)+
+    by induct (iprover intro: rtrancl_trans dest!: converseD)+
 qed
 
 theorem rtrancl_converseI:
@@ -166,7 +166,7 @@
   shows "(x, y) \<in> (r^-1)^*"
 proof -
   from r show ?thesis
-    by induct (rules intro: rtrancl_trans converseI)+
+    by induct (iprover intro: rtrancl_trans converseI)+
 qed
 
 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
@@ -179,7 +179,7 @@
 proof -
   from rtrancl_converseI [OF major]
   show ?thesis
-    by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
+    by induct (iprover intro: cases dest!: converseD rtrancl_converseD)+
 qed
 
 lemmas converse_rtrancl_induct2 =
@@ -197,8 +197,8 @@
   show ?thesis
     apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
      apply (rule_tac [2] major [THEN converse_rtrancl_induct])
-      prefer 2 apply rules
-     prefer 2 apply rules
+      prefer 2 apply iprover
+     prefer 2 apply iprover
     apply (erule asm_rl exE disjE conjE prems)+
     done
 qed
@@ -221,7 +221,7 @@
 lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
   apply (simp only: split_tupled_all)
   apply (erule trancl.induct)
-  apply (rules dest: subsetD)+
+  apply (iprover dest: subsetD)+
   done
 
 lemma r_into_trancl': "!!p. p : r ==> p : r^+"
@@ -232,15 +232,15 @@
 *}
 
 lemma trancl_into_rtrancl: "(a, b) \<in> r^+ ==> (a, b) \<in> r^*"
-  by (erule trancl.induct) rules+
+  by (erule trancl.induct) iprover+
 
 lemma rtrancl_into_trancl1: assumes r: "(a, b) \<in> r^*"
   shows "!!c. (b, c) \<in> r ==> (a, c) \<in> r^+" using r
-  by induct rules+
+  by induct iprover+
 
 lemma rtrancl_into_trancl2: "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+"
   -- {* intro rule from @{text r} and @{text rtrancl} *}
-  apply (erule rtranclE, rules)
+  apply (erule rtranclE, iprover)
   apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
    apply (assumption | rule r_into_rtrancl)+
   done
@@ -253,8 +253,8 @@
   -- {* Nice induction rule for @{text trancl} *}
 proof -
   from a have "a = a --> P b"
-    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
-  thus ?thesis by rules
+    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
+  thus ?thesis by iprover
 qed
 
 lemma trancl_trans_induct:
@@ -267,7 +267,7 @@
   assume major: "(x,y) : r^+"
   case rule_context
   show ?thesis
-    by (rules intro: r_into_trancl major [THEN trancl_induct] prems)
+    by (iprover intro: r_into_trancl major [THEN trancl_induct] prems)
 qed
 
 inductive_cases tranclE: "(a, b) : r^+"
@@ -281,14 +281,14 @@
   fix x y z
   assume "(x, y) \<in> r^+"
   assume "(y, z) \<in> r^+"
-  thus "(x, z) \<in> r^+" by induct (rules!)+
+  thus "(x, z) \<in> r^+" by induct (iprover!)+
 qed
 
 lemmas trancl_trans = trans_trancl [THEN transD, standard]
 
 lemma rtrancl_trancl_trancl: assumes r: "(x, y) \<in> r^*"
   shows "!!z. (y, z) \<in> r^+ ==> (x, z) \<in> r^+" using r
-  by induct (rules intro: trancl_trans)+
+  by induct (iprover intro: trancl_trans)+
 
 lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+"
   by (erule transD [OF trans_trancl r_into_trancl])
@@ -309,13 +309,13 @@
 lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x, y) \<in> (r^-1)^+"
   apply (drule converseD)
   apply (erule trancl.induct)
-  apply (rules intro: converseI trancl_trans)+
+  apply (iprover intro: converseI trancl_trans)+
   done
 
 lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
   apply (rule converseI)
   apply (erule trancl.induct)
-  apply (rules dest: converseD intro: trancl_trans)+
+  apply (iprover dest: converseD intro: trancl_trans)+
   done
 
 lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"