src/HOL/Transitive_Closure.thy
changeset 14208 144f45277d5a
parent 13867 1fdecd15437f
child 14337 e13731554e50
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Sep 26 10:34:28 2003 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Sep 26 10:34:57 2003 +0200
     1.3 @@ -57,8 +57,7 @@
     1.4    apply (rule subsetI)
     1.5    apply (simp only: split_tupled_all)
     1.6    apply (erule rtrancl.induct)
     1.7 -   apply (rule_tac [2] rtrancl_into_rtrancl)
     1.8 -    apply blast+
     1.9 +   apply (rule_tac [2] rtrancl_into_rtrancl, blast+)
    1.10    done
    1.11  
    1.12  theorem rtrancl_induct [consumes 1, induct set: rtrancl]:
    1.13 @@ -126,15 +125,11 @@
    1.14    done
    1.15  
    1.16  lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*"
    1.17 -  apply (drule rtrancl_mono)
    1.18 -  apply simp
    1.19 -  done
    1.20 +by (drule rtrancl_mono, simp)
    1.21  
    1.22  lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> R^* ==> S^* = R^*"
    1.23    apply (drule rtrancl_mono)
    1.24 -  apply (drule rtrancl_mono)
    1.25 -  apply simp
    1.26 -  apply blast
    1.27 +  apply (drule rtrancl_mono, simp, blast)
    1.28    done
    1.29  
    1.30  lemma rtrancl_Un_rtrancl: "(R^* \<union> S^*)^* = (R \<union> S)^*"
    1.31 @@ -145,12 +140,9 @@
    1.32  
    1.33  lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*"
    1.34    apply (rule sym)
    1.35 -  apply (rule rtrancl_subset)
    1.36 -   apply blast
    1.37 -  apply clarify
    1.38 +  apply (rule rtrancl_subset, blast, clarify)
    1.39    apply (rename_tac a b)
    1.40 -  apply (case_tac "a = b")
    1.41 -   apply blast
    1.42 +  apply (case_tac "a = b", blast)
    1.43    apply (blast intro!: r_into_rtrancl)
    1.44    done
    1.45  
    1.46 @@ -239,8 +231,7 @@
    1.47  
    1.48  lemma rtrancl_into_trancl2: "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+"
    1.49    -- {* intro rule from @{text r} and @{text rtrancl} *}
    1.50 -  apply (erule rtranclE)
    1.51 -   apply rules
    1.52 +  apply (erule rtranclE, rules)
    1.53    apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
    1.54     apply (assumption | rule r_into_rtrancl)+
    1.55    done
    1.56 @@ -296,8 +287,7 @@
    1.57    apply (rule equalityI)
    1.58     apply (rule subsetI)
    1.59     apply (simp only: split_tupled_all)
    1.60 -   apply (erule trancl_induct)
    1.61 -    apply blast
    1.62 +   apply (erule trancl_induct, blast)
    1.63     apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)
    1.64    apply (rule subsetI)
    1.65    apply (blast intro: trancl_mono rtrancl_mono
    1.66 @@ -336,8 +326,7 @@
    1.67  qed
    1.68  
    1.69  lemma tranclD: "(x, y) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> R^*"
    1.70 -  apply (erule converse_trancl_induct)
    1.71 -   apply auto
    1.72 +  apply (erule converse_trancl_induct, auto)
    1.73    apply (blast intro: rtrancl_trans)
    1.74    done
    1.75  
    1.76 @@ -349,8 +338,7 @@
    1.77  
    1.78  lemma trancl_subset_Sigma_aux:
    1.79      "(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A"
    1.80 -  apply (erule rtrancl_induct)
    1.81 -   apply auto
    1.82 +  apply (erule rtrancl_induct, auto)
    1.83    done
    1.84  
    1.85  lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"
    1.86 @@ -368,15 +356,11 @@
    1.87  
    1.88  lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"
    1.89    apply safe
    1.90 -   apply (drule trancl_into_rtrancl)
    1.91 -   apply simp
    1.92 -  apply (erule rtranclE)
    1.93 -   apply safe
    1.94 -   apply (rule r_into_trancl)
    1.95 -   apply simp
    1.96 +   apply (drule trancl_into_rtrancl, simp)
    1.97 +  apply (erule rtranclE, safe)
    1.98 +   apply (rule r_into_trancl, simp)
    1.99    apply (rule rtrancl_into_trancl1)
   1.100 -   apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD])
   1.101 -  apply fast
   1.102 +   apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast)
   1.103    done
   1.104  
   1.105  lemma trancl_empty [simp]: "{}^+ = {}"
   1.106 @@ -433,8 +417,7 @@
   1.107    apply (drule tranclD)
   1.108    apply (erule exE, erule conjE)
   1.109    apply (drule rtrancl_trans, assumption)
   1.110 -  apply (drule rtrancl_into_trancl2, assumption)
   1.111 -  apply assumption
   1.112 +  apply (drule rtrancl_into_trancl2, assumption, assumption)
   1.113    done
   1.114  
   1.115  lemmas transitive_closure_trans [trans] =