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 [2] 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"