src/HOL/Transitive_Closure.thy
 changeset 17589 58eeffd73be1 parent 16514 090c6a98c704 child 17876 b9c92f384109
```     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Sep 22 23:55:42 2005 +0200
1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Sep 22 23:56:15 2005 +0200
1.3 @@ -74,8 +74,8 @@
1.4    shows "P b"
1.5  proof -
1.6    from a have "a = a --> P b"
1.7 -    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
1.8 -  thus ?thesis by rules
1.9 +    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
1.10 +  thus ?thesis by iprover
1.11  qed
1.12
1.13  lemmas rtrancl_induct2 =
1.14 @@ -88,7 +88,7 @@
1.15    fix x y z
1.16    assume "(x, y) \<in> r\<^sup>*"
1.17    assume "(y, z) \<in> r\<^sup>*"
1.18 -  thus "(x, z) \<in> r\<^sup>*" by induct (rules!)+
1.19 +  thus "(x, z) \<in> r\<^sup>*" by induct (iprover!)+
1.20  qed
1.21
1.22  lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
1.23 @@ -112,7 +112,7 @@
1.24
1.25  lemma converse_rtrancl_into_rtrancl:
1.26    "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
1.27 -  by (rule rtrancl_trans) rules+
1.28 +  by (rule rtrancl_trans) iprover+
1.29
1.30  text {*
1.31    \medskip More @{term "r^*"} equations and inclusions.
1.32 @@ -158,7 +158,7 @@
1.33    shows "(y, x) \<in> r^*"
1.34  proof -
1.35    from r show ?thesis
1.36 -    by induct (rules intro: rtrancl_trans dest!: converseD)+
1.37 +    by induct (iprover intro: rtrancl_trans dest!: converseD)+
1.38  qed
1.39
1.40  theorem rtrancl_converseI:
1.41 @@ -166,7 +166,7 @@
1.42    shows "(x, y) \<in> (r^-1)^*"
1.43  proof -
1.44    from r show ?thesis
1.45 -    by induct (rules intro: rtrancl_trans converseI)+
1.46 +    by induct (iprover intro: rtrancl_trans converseI)+
1.47  qed
1.48
1.49  lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
1.50 @@ -179,7 +179,7 @@
1.51  proof -
1.52    from rtrancl_converseI [OF major]
1.53    show ?thesis
1.54 -    by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
1.55 +    by induct (iprover intro: cases dest!: converseD rtrancl_converseD)+
1.56  qed
1.57
1.58  lemmas converse_rtrancl_induct2 =
1.59 @@ -197,8 +197,8 @@
1.60    show ?thesis
1.61      apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
1.62       apply (rule_tac  major [THEN converse_rtrancl_induct])
1.63 -      prefer 2 apply rules
1.64 -     prefer 2 apply rules
1.65 +      prefer 2 apply iprover
1.66 +     prefer 2 apply iprover
1.67      apply (erule asm_rl exE disjE conjE prems)+
1.68      done
1.69  qed
1.70 @@ -221,7 +221,7 @@
1.71  lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
1.72    apply (simp only: split_tupled_all)
1.73    apply (erule trancl.induct)
1.74 -  apply (rules dest: subsetD)+
1.75 +  apply (iprover dest: subsetD)+
1.76    done
1.77
1.78  lemma r_into_trancl': "!!p. p : r ==> p : r^+"
1.79 @@ -232,15 +232,15 @@
1.80  *}
1.81
1.82  lemma trancl_into_rtrancl: "(a, b) \<in> r^+ ==> (a, b) \<in> r^*"
1.83 -  by (erule trancl.induct) rules+
1.84 +  by (erule trancl.induct) iprover+
1.85
1.86  lemma rtrancl_into_trancl1: assumes r: "(a, b) \<in> r^*"
1.87    shows "!!c. (b, c) \<in> r ==> (a, c) \<in> r^+" using r
1.88 -  by induct rules+
1.89 +  by induct iprover+
1.90
1.91  lemma rtrancl_into_trancl2: "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+"
1.92    -- {* intro rule from @{text r} and @{text rtrancl} *}
1.93 -  apply (erule rtranclE, rules)
1.94 +  apply (erule rtranclE, iprover)
1.95    apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
1.96     apply (assumption | rule r_into_rtrancl)+
1.97    done
1.98 @@ -253,8 +253,8 @@
1.99    -- {* Nice induction rule for @{text trancl} *}
1.100  proof -
1.101    from a have "a = a --> P b"
1.102 -    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
1.103 -  thus ?thesis by rules
1.104 +    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
1.105 +  thus ?thesis by iprover
1.106  qed
1.107
1.108  lemma trancl_trans_induct:
1.109 @@ -267,7 +267,7 @@
1.110    assume major: "(x,y) : r^+"
1.111    case rule_context
1.112    show ?thesis
1.113 -    by (rules intro: r_into_trancl major [THEN trancl_induct] prems)
1.114 +    by (iprover intro: r_into_trancl major [THEN trancl_induct] prems)
1.115  qed
1.116
1.117  inductive_cases tranclE: "(a, b) : r^+"
1.118 @@ -281,14 +281,14 @@
1.119    fix x y z
1.120    assume "(x, y) \<in> r^+"
1.121    assume "(y, z) \<in> r^+"
1.122 -  thus "(x, z) \<in> r^+" by induct (rules!)+
1.123 +  thus "(x, z) \<in> r^+" by induct (iprover!)+
1.124  qed
1.125
1.126  lemmas trancl_trans = trans_trancl [THEN transD, standard]
1.127
1.128  lemma rtrancl_trancl_trancl: assumes r: "(x, y) \<in> r^*"
1.129    shows "!!z. (y, z) \<in> r^+ ==> (x, z) \<in> r^+" using r
1.130 -  by induct (rules intro: trancl_trans)+
1.131 +  by induct (iprover intro: trancl_trans)+
1.132
1.133  lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+"
1.134    by (erule transD [OF trans_trancl r_into_trancl])
1.135 @@ -309,13 +309,13 @@
1.136  lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x, y) \<in> (r^-1)^+"
1.137    apply (drule converseD)
1.138    apply (erule trancl.induct)
1.139 -  apply (rules intro: converseI trancl_trans)+
1.140 +  apply (iprover intro: converseI trancl_trans)+
1.141    done
1.142
1.143  lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
1.144    apply (rule converseI)
1.145    apply (erule trancl.induct)
1.146 -  apply (rules dest: converseD intro: trancl_trans)+
1.147 +  apply (iprover dest: converseD intro: trancl_trans)+
1.148    done
1.149
1.150  lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"
```