merged
authorpaulson
Thu Jul 12 17:23:38 2018 +0100 (2 months ago)
changeset 6861979abf4201e8d
parent 68617 75129a73aca3
parent 68618 3db8520941a4
child 68620 707437105595
child 68621 27432da24236
child 68626 330c0ec897a4
merged
     1.1 --- a/src/HOL/Nat.thy	Thu Jul 12 11:23:46 2018 +0200
     1.2 +++ b/src/HOL/Nat.thy	Thu Jul 12 17:23:38 2018 +0100
     1.3 @@ -2093,7 +2093,7 @@
     1.4  
     1.5  lemma inj_on_diff_nat:
     1.6    fixes k :: nat
     1.7 -  assumes "\<forall>n \<in> N. k \<le> n"
     1.8 +  assumes "\<And>n. n \<in> N \<Longrightarrow> k \<le> n"
     1.9    shows "inj_on (\<lambda>n. n - k) N"
    1.10  proof (rule inj_onI)
    1.11    fix x y
     2.1 --- a/src/HOL/Set_Interval.thy	Thu Jul 12 11:23:46 2018 +0200
     2.2 +++ b/src/HOL/Set_Interval.thy	Thu Jul 12 17:23:38 2018 +0100
     2.3 @@ -91,29 +91,27 @@
     2.4  
     2.5  lemma Compl_lessThan [simp]:
     2.6      "!!k:: 'a::linorder. -lessThan k = atLeast k"
     2.7 -apply (auto simp add: lessThan_def atLeast_def)
     2.8 -done
     2.9 +  by (auto simp add: lessThan_def atLeast_def)
    2.10  
    2.11  lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
    2.12 -by auto
    2.13 +  by auto
    2.14  
    2.15  lemma (in ord) greaterThan_iff [iff]: "(i \<in> greaterThan k) = (k<i)"
    2.16 -by (simp add: greaterThan_def)
    2.17 +  by (simp add: greaterThan_def)
    2.18  
    2.19  lemma Compl_greaterThan [simp]:
    2.20      "!!k:: 'a::linorder. -greaterThan k = atMost k"
    2.21    by (auto simp add: greaterThan_def atMost_def)
    2.22  
    2.23  lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
    2.24 -apply (subst Compl_greaterThan [symmetric])
    2.25 -apply (rule double_complement)
    2.26 -done
    2.27 +  apply (subst Compl_greaterThan [symmetric])
    2.28 +  apply (rule double_complement)
    2.29 +  done
    2.30  
    2.31  lemma (in ord) atLeast_iff [iff]: "(i \<in> atLeast k) = (k<=i)"
    2.32  by (simp add: atLeast_def)
    2.33  
    2.34 -lemma Compl_atLeast [simp]:
    2.35 -    "!!k:: 'a::linorder. -atLeast k = lessThan k"
    2.36 +lemma Compl_atLeast [simp]: "!!k:: 'a::linorder. -atLeast k = lessThan k"
    2.37    by (auto simp add: lessThan_def atLeast_def)
    2.38  
    2.39  lemma (in ord) atMost_iff [iff]: "(i \<in> atMost k) = (i<=k)"
    2.40 @@ -146,35 +144,25 @@
    2.41  
    2.42  lemma greaterThan_subset_iff [iff]:
    2.43       "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))"
    2.44 -apply (auto simp add: greaterThan_def)
    2.45 - apply (subst linorder_not_less [symmetric], blast)
    2.46 -done
    2.47 +  unfolding greaterThan_def by (auto simp: linorder_not_less [symmetric])
    2.48  
    2.49  lemma greaterThan_eq_iff [iff]:
    2.50       "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"
    2.51 -apply (rule iffI)
    2.52 - apply (erule equalityE)
    2.53 - apply simp_all
    2.54 -done
    2.55 +  by (auto simp: elim!: equalityE)
    2.56  
    2.57  lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))"
    2.58 -by (blast intro: order_trans)
    2.59 +  by (blast intro: order_trans)
    2.60  
    2.61  lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"
    2.62 -by (blast intro: order_antisym order_trans)
    2.63 +  by (blast intro: order_antisym order_trans)
    2.64  
    2.65  lemma lessThan_subset_iff [iff]:
    2.66       "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))"
    2.67 -apply (auto simp add: lessThan_def)
    2.68 - apply (subst linorder_not_less [symmetric], blast)
    2.69 -done
    2.70 +  unfolding lessThan_def by (auto simp: linorder_not_less [symmetric])
    2.71  
    2.72  lemma lessThan_eq_iff [iff]:
    2.73       "(lessThan x = lessThan y) = (x = (y::'a::linorder))"
    2.74 -apply (rule iffI)
    2.75 - apply (erule equalityE)
    2.76 - apply simp_all
    2.77 -done
    2.78 +  by (auto simp: elim!: equalityE)
    2.79  
    2.80  lemma lessThan_strict_subset_iff:
    2.81    fixes m n :: "'a::linorder"
    2.82 @@ -195,21 +183,17 @@
    2.83  context ord
    2.84  begin
    2.85  
    2.86 -lemma greaterThanLessThan_iff [simp]:
    2.87 -  "(i \<in> {l<..<u}) = (l < i \<and> i < u)"
    2.88 -by (simp add: greaterThanLessThan_def)
    2.89 -
    2.90 -lemma atLeastLessThan_iff [simp]:
    2.91 -  "(i \<in> {l..<u}) = (l \<le> i \<and> i < u)"
    2.92 -by (simp add: atLeastLessThan_def)
    2.93 -
    2.94 -lemma greaterThanAtMost_iff [simp]:
    2.95 -  "(i \<in> {l<..u}) = (l < i \<and> i \<le> u)"
    2.96 -by (simp add: greaterThanAtMost_def)
    2.97 -
    2.98 -lemma atLeastAtMost_iff [simp]:
    2.99 -  "(i \<in> {l..u}) = (l \<le> i \<and> i \<le> u)"
   2.100 -by (simp add: atLeastAtMost_def)
   2.101 +lemma greaterThanLessThan_iff [simp]: "(i \<in> {l<..<u}) = (l < i \<and> i < u)"
   2.102 +  by (simp add: greaterThanLessThan_def)
   2.103 +
   2.104 +lemma atLeastLessThan_iff [simp]: "(i \<in> {l..<u}) = (l \<le> i \<and> i < u)"
   2.105 +  by (simp add: atLeastLessThan_def)
   2.106 +
   2.107 +lemma greaterThanAtMost_iff [simp]: "(i \<in> {l<..u}) = (l < i \<and> i \<le> u)"
   2.108 +  by (simp add: greaterThanAtMost_def)
   2.109 +
   2.110 +lemma atLeastAtMost_iff [simp]: "(i \<in> {l..u}) = (l \<le> i \<and> i \<le> u)"
   2.111 +  by (simp add: atLeastAtMost_def)
   2.112  
   2.113  text \<open>The above four lemmas could be declared as iffs. Unfortunately this
   2.114  breaks many proofs. Since it only helps blast, it is better to leave them
   2.115 @@ -467,11 +451,11 @@
   2.116  
   2.117  lemma (in linorder) atLeastLessThan_subset_iff:
   2.118    "{a..<b} \<subseteq> {c..<d} \<Longrightarrow> b \<le> a \<or> c\<le>a \<and> b\<le>d"
   2.119 -apply (auto simp:subset_eq Ball_def)
   2.120 -apply(frule_tac x=a in spec)
   2.121 -apply(erule_tac x=d in allE)
   2.122 -apply (simp add: less_imp_le)
   2.123 -done
   2.124 +  apply (auto simp:subset_eq Ball_def not_le)
   2.125 +  apply(frule_tac x=a in spec)
   2.126 +  apply(erule_tac x=d in allE)
   2.127 +  apply (auto simp: )
   2.128 +  done
   2.129  
   2.130  lemma atLeastLessThan_inj:
   2.131    fixes a b c d :: "'a::linorder"
   2.132 @@ -718,17 +702,15 @@
   2.133  subsubsection \<open>The Constant @{term greaterThan}\<close>
   2.134  
   2.135  lemma greaterThan_0: "greaterThan 0 = range Suc"
   2.136 -apply (simp add: greaterThan_def)
   2.137 -apply (blast dest: gr0_conv_Suc [THEN iffD1])
   2.138 -done
   2.139 +  unfolding greaterThan_def
   2.140 +  by (blast dest: gr0_conv_Suc [THEN iffD1])
   2.141  
   2.142  lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
   2.143 -apply (simp add: greaterThan_def)
   2.144 -apply (auto elim: linorder_neqE)
   2.145 -done
   2.146 +  unfolding greaterThan_def
   2.147 +  by (auto elim: linorder_neqE)
   2.148  
   2.149  lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
   2.150 -by blast
   2.151 +  by blast
   2.152  
   2.153  subsubsection \<open>The Constant @{term atLeast}\<close>
   2.154  
   2.155 @@ -736,29 +718,24 @@
   2.156  by (unfold atLeast_def UNIV_def, simp)
   2.157  
   2.158  lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
   2.159 -apply (simp add: atLeast_def)
   2.160 -apply (simp add: Suc_le_eq)
   2.161 -apply (simp add: order_le_less, blast)
   2.162 -done
   2.163 +  unfolding atLeast_def by (auto simp: order_le_less Suc_le_eq)
   2.164  
   2.165  lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"
   2.166    by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)
   2.167  
   2.168  lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
   2.169 -by blast
   2.170 +  by blast
   2.171  
   2.172  subsubsection \<open>The Constant @{term atMost}\<close>
   2.173  
   2.174  lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
   2.175 -by (simp add: atMost_def)
   2.176 +  by (simp add: atMost_def)
   2.177  
   2.178  lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
   2.179 -apply (simp add: atMost_def)
   2.180 -apply (simp add: less_Suc_eq order_le_less, blast)
   2.181 -done
   2.182 +  unfolding atMost_def by (auto simp add: less_Suc_eq order_le_less)
   2.183  
   2.184  lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
   2.185 -by blast
   2.186 +  by blast
   2.187  
   2.188  subsubsection \<open>The Constant @{term atLeastLessThan}\<close>
   2.189  
   2.190 @@ -770,28 +747,24 @@
   2.191  specific concept to a more general one.\<close>
   2.192  
   2.193  lemma atLeast0LessThan [code_abbrev]: "{0::nat..<n} = {..<n}"
   2.194 -by(simp add:lessThan_def atLeastLessThan_def)
   2.195 +  by(simp add:lessThan_def atLeastLessThan_def)
   2.196  
   2.197  lemma atLeast0AtMost [code_abbrev]: "{0..n::nat} = {..n}"
   2.198 -by(simp add:atMost_def atLeastAtMost_def)
   2.199 -
   2.200 -lemma lessThan_atLeast0:
   2.201 -  "{..<n} = {0::nat..<n}"
   2.202 +  by(simp add:atMost_def atLeastAtMost_def)
   2.203 +
   2.204 +lemma lessThan_atLeast0: "{..<n} = {0::nat..<n}"
   2.205    by (simp add: atLeast0LessThan)
   2.206  
   2.207 -lemma atMost_atLeast0:
   2.208 -  "{..n} = {0::nat..n}"
   2.209 +lemma atMost_atLeast0: "{..n} = {0::nat..n}"
   2.210    by (simp add: atLeast0AtMost)
   2.211  
   2.212  lemma atLeastLessThan0: "{m..<0::nat} = {}"
   2.213 -by (simp add: atLeastLessThan_def)
   2.214 -
   2.215 -lemma atLeast0_lessThan_Suc:
   2.216 -  "{0..<Suc n} = insert n {0..<n}"
   2.217 +  by (simp add: atLeastLessThan_def)
   2.218 +
   2.219 +lemma atLeast0_lessThan_Suc: "{0..<Suc n} = insert n {0..<n}"
   2.220    by (simp add: atLeast0LessThan lessThan_Suc)
   2.221  
   2.222 -lemma atLeast0_lessThan_Suc_eq_insert_0:
   2.223 -  "{0..<Suc n} = insert 0 (Suc ` {0..<n})"
   2.224 +lemma atLeast0_lessThan_Suc_eq_insert_0: "{0..<Suc n} = insert 0 (Suc ` {0..<n})"
   2.225    by (simp add: atLeast0LessThan lessThan_Suc_eq_insert_0)
   2.226  
   2.227  
   2.228 @@ -815,19 +788,13 @@
   2.229  
   2.230  lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}"
   2.231  by (auto simp add: atLeastLessThan_def)
   2.232 -(*
   2.233 -lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}"
   2.234 -by (induct k, simp_all add: atLeastLessThanSuc)
   2.235 -
   2.236 -lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}"
   2.237 -by (auto simp add: atLeastLessThan_def)
   2.238 -*)
   2.239 +
   2.240  lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
   2.241    by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
   2.242  
   2.243  lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}"
   2.244    by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def
   2.245 -    greaterThanAtMost_def)
   2.246 +      greaterThanAtMost_def)
   2.247  
   2.248  lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}"
   2.249    by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
   2.250 @@ -846,9 +813,7 @@
   2.251    by (auto intro: set_eqI)
   2.252  
   2.253  lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
   2.254 -  apply (induct k)
   2.255 -  apply (simp_all add: atLeastLessThanSuc)
   2.256 -  done
   2.257 +  by (induct k) (simp_all add: atLeastLessThanSuc)
   2.258  
   2.259  
   2.260  subsubsection \<open>Intervals and numerals\<close>
   2.261 @@ -1123,7 +1088,7 @@
   2.262    by auto
   2.263  
   2.264  lemma image_add_int_atLeastLessThan:
   2.265 -    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
   2.266 +    "(\<lambda>x. x + (l::int)) ` {0..<u-l} = {l..<u}"
   2.267    apply (auto simp add: image_def)
   2.268    apply (rule_tac x = "x - l" in bexI)
   2.269    apply auto
   2.270 @@ -1165,25 +1130,23 @@
   2.271  
   2.272  lemma finite_greaterThanLessThan [iff]:
   2.273    fixes l :: nat shows "finite {l<..<u}"
   2.274 -by (simp add: greaterThanLessThan_def)
   2.275 +  by (simp add: greaterThanLessThan_def)
   2.276  
   2.277  lemma finite_atLeastLessThan [iff]:
   2.278    fixes l :: nat shows "finite {l..<u}"
   2.279 -by (simp add: atLeastLessThan_def)
   2.280 +  by (simp add: atLeastLessThan_def)
   2.281  
   2.282  lemma finite_greaterThanAtMost [iff]:
   2.283    fixes l :: nat shows "finite {l<..u}"
   2.284 -by (simp add: greaterThanAtMost_def)
   2.285 +  by (simp add: greaterThanAtMost_def)
   2.286  
   2.287  lemma finite_atLeastAtMost [iff]:
   2.288    fixes l :: nat shows "finite {l..u}"
   2.289 -by (simp add: atLeastAtMost_def)
   2.290 +  by (simp add: atLeastAtMost_def)
   2.291  
   2.292  text \<open>A bounded set of natural numbers is finite.\<close>
   2.293  lemma bounded_nat_set_is_finite: "(\<forall>i\<in>N. i < (n::nat)) \<Longrightarrow> finite N"
   2.294 -apply (rule finite_subset)
   2.295 - apply (rule_tac [2] finite_lessThan, auto)
   2.296 -done
   2.297 +  by (rule finite_subset [OF _ finite_lessThan]) auto
   2.298  
   2.299  text \<open>A set of natural numbers is finite iff it is bounded.\<close>
   2.300  lemma finite_nat_set_iff_bounded:
   2.301 @@ -1195,11 +1158,9 @@
   2.302    assume ?B show ?F using \<open>?B\<close> by(blast intro:bounded_nat_set_is_finite)
   2.303  qed
   2.304  
   2.305 -lemma finite_nat_set_iff_bounded_le:
   2.306 -  "finite(N::nat set) = (\<exists>m. \<forall>n\<in>N. n<=m)"
   2.307 -apply(simp add:finite_nat_set_iff_bounded)
   2.308 -apply(blast dest:less_imp_le_nat le_imp_less_Suc)
   2.309 -done
   2.310 +lemma finite_nat_set_iff_bounded_le: "finite(N::nat set) = (\<exists>m. \<forall>n\<in>N. n\<le>m)"
   2.311 +  unfolding finite_nat_set_iff_bounded
   2.312 +  by (blast dest:less_imp_le_nat le_imp_less_Suc)
   2.313  
   2.314  lemma finite_less_ub:
   2.315       "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
   2.316 @@ -1298,10 +1259,9 @@
   2.317  lemma UN_finite2_eq:
   2.318    "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n + k}. B i)) \<Longrightarrow>
   2.319      (\<Union>n. A n) = (\<Union>n. B n)"
   2.320 -  apply (rule subset_antisym)
   2.321 -   apply (rule UN_finite2_subset, blast)
   2.322 -  apply (rule UN_finite2_subset [where k=k])
   2.323 -  apply (force simp add: atLeastLessThan_add_Un [of 0])
   2.324 +  apply (rule subset_antisym [OF UN_finite_subset UN_finite2_subset])
   2.325 +   apply auto
   2.326 +  apply (force simp add: atLeastLessThan_add_Un [of 0])+
   2.327    done
   2.328  
   2.329  
   2.330 @@ -1315,7 +1275,7 @@
   2.331  
   2.332  lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l"
   2.333  proof -
   2.334 -  have "{l..<u} = (%x. x + l) ` {..<u-l}"
   2.335 +  have "{l..<u} = (\<lambda>x. x + l) ` {..<u-l}"
   2.336      apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
   2.337      apply (rule_tac x = "x - l" in exI)
   2.338      apply arith
   2.339 @@ -1349,24 +1309,24 @@
   2.340  
   2.341  lemma ex_bij_betw_nat_finite:
   2.342    "finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
   2.343 -apply(drule finite_imp_nat_seg_image_inj_on)
   2.344 -apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def)
   2.345 -done
   2.346 +  apply(drule finite_imp_nat_seg_image_inj_on)
   2.347 +  apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def)
   2.348 +  done
   2.349  
   2.350  lemma ex_bij_betw_finite_nat:
   2.351    "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
   2.352 -by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
   2.353 +  by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
   2.354  
   2.355  lemma finite_same_card_bij:
   2.356    "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> \<exists>h. bij_betw h A B"
   2.357 -apply(drule ex_bij_betw_finite_nat)
   2.358 -apply(drule ex_bij_betw_nat_finite)
   2.359 -apply(auto intro!:bij_betw_trans)
   2.360 -done
   2.361 +  apply(drule ex_bij_betw_finite_nat)
   2.362 +  apply(drule ex_bij_betw_nat_finite)
   2.363 +  apply(auto intro!:bij_betw_trans)
   2.364 +  done
   2.365  
   2.366  lemma ex_bij_betw_nat_finite_1:
   2.367    "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
   2.368 -by (rule finite_same_card_bij) auto
   2.369 +  by (rule finite_same_card_bij) auto
   2.370  
   2.371  lemma bij_betw_iff_card:
   2.372    assumes "finite A" "finite B"
   2.373 @@ -1428,26 +1388,21 @@
   2.374  
   2.375  lemma image_atLeastZeroLessThan_int: "0 \<le> u ==>
   2.376      {(0::int)..<u} = int ` {..<nat u}"
   2.377 -  apply (unfold image_def lessThan_def)
   2.378 +  unfolding image_def lessThan_def
   2.379    apply auto
   2.380    apply (rule_tac x = "nat x" in exI)
   2.381    apply (auto simp add: zless_nat_eq_int_zless [THEN sym])
   2.382    done
   2.383  
   2.384  lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
   2.385 -  apply (cases "0 \<le> u")
   2.386 -  apply (subst image_atLeastZeroLessThan_int, assumption)
   2.387 -  apply (rule finite_imageI)
   2.388 -  apply auto
   2.389 -  done
   2.390 +proof (cases "0 \<le> u")
   2.391 +  case True
   2.392 +  then show ?thesis
   2.393 +    by (auto simp: image_atLeastZeroLessThan_int)
   2.394 +qed auto
   2.395  
   2.396  lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}"
   2.397 -  apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
   2.398 -  apply (erule subst)
   2.399 -  apply (rule finite_imageI)
   2.400 -  apply (rule finite_atLeastZeroLessThan_int)
   2.401 -  apply (rule image_add_int_atLeastLessThan)
   2.402 -  done
   2.403 +  by (simp only: image_add_int_atLeastLessThan [symmetric, of l] finite_imageI finite_atLeastZeroLessThan_int)
   2.404  
   2.405  lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
   2.406    by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
   2.407 @@ -1462,32 +1417,33 @@
   2.408  subsubsection \<open>Cardinality\<close>
   2.409  
   2.410  lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
   2.411 -  apply (cases "0 \<le> u")
   2.412 -  apply (subst image_atLeastZeroLessThan_int, assumption)
   2.413 -  apply (subst card_image)
   2.414 -  apply (auto simp add: inj_on_def)
   2.415 +proof (cases "0 \<le> u")
   2.416 +  case True
   2.417 +  then show ?thesis
   2.418 +    by (auto simp: image_atLeastZeroLessThan_int card_image inj_on_def)    
   2.419 +qed auto
   2.420 +
   2.421 +lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)"
   2.422 +proof -
   2.423 +  have "card {l..<u} = card {0..<u-l}"
   2.424 +    apply (subst image_add_int_atLeastLessThan [symmetric])
   2.425 +    apply (rule card_image)
   2.426 +    apply (simp add: inj_on_def)
   2.427 +    done
   2.428 +  then show ?thesis
   2.429 +    by (simp add: card_atLeastZeroLessThan_int)
   2.430 +qed
   2.431 +
   2.432 +lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
   2.433 +  apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
   2.434 +  apply (auto simp add: algebra_simps)
   2.435    done
   2.436  
   2.437 -lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)"
   2.438 -  apply (subgoal_tac "card {l..<u} = card {0..<u-l}")
   2.439 -  apply (erule ssubst, rule card_atLeastZeroLessThan_int)
   2.440 -  apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
   2.441 -  apply (erule subst)
   2.442 -  apply (rule card_image)
   2.443 -  apply (simp add: inj_on_def)
   2.444 -  apply (rule image_add_int_atLeastLessThan)
   2.445 -  done
   2.446 -
   2.447 -lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
   2.448 -apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
   2.449 -apply (auto simp add: algebra_simps)
   2.450 -done
   2.451 -
   2.452  lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)"
   2.453 -by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
   2.454 +  by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
   2.455  
   2.456  lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))"
   2.457 -by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
   2.458 +  by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
   2.459  
   2.460  lemma finite_M_bounded_by_nat: "finite {k. P k \<and> k < (i::nat)}"
   2.461  proof -
   2.462 @@ -1496,43 +1452,44 @@
   2.463  qed
   2.464  
   2.465  lemma card_less:
   2.466 -assumes zero_in_M: "0 \<in> M"
   2.467 -shows "card {k \<in> M. k < Suc i} \<noteq> 0"
   2.468 +  assumes zero_in_M: "0 \<in> M"
   2.469 +  shows "card {k \<in> M. k < Suc i} \<noteq> 0"
   2.470  proof -
   2.471    from zero_in_M have "{k \<in> M. k < Suc i} \<noteq> {}" by auto
   2.472    with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)
   2.473  qed
   2.474  
   2.475 -lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
   2.476 -apply (rule card_bij_eq [of Suc _ _ "\<lambda>x. x - Suc 0"])
   2.477 -apply auto
   2.478 -apply (rule inj_on_diff_nat)
   2.479 -apply auto
   2.480 -apply (case_tac x)
   2.481 -apply auto
   2.482 -apply (case_tac xa)
   2.483 -apply auto
   2.484 -apply (case_tac xa)
   2.485 -apply auto
   2.486 -done
   2.487 +lemma card_less_Suc2: 
   2.488 +  assumes "0 \<notin> M" shows "card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
   2.489 +proof -
   2.490 +  have *: "\<lbrakk>j \<in> M; j < Suc i\<rbrakk> \<Longrightarrow> j - Suc 0 < i \<and> Suc (j - Suc 0) \<in> M \<and> Suc 0 \<le> j" for j
   2.491 +    by (cases j) (use assms in auto)
   2.492 +  show ?thesis
   2.493 +  proof (rule card_bij_eq)
   2.494 +    show "inj_on Suc {k. Suc k \<in> M \<and> k < i}"
   2.495 +      by force
   2.496 +    show "inj_on (\<lambda>x. x - Suc 0) {k \<in> M. k < Suc i}"
   2.497 +      by (rule inj_on_diff_nat) (use * in blast)
   2.498 +  qed (use * in auto)
   2.499 +qed
   2.500  
   2.501  lemma card_less_Suc:
   2.502 -  assumes zero_in_M: "0 \<in> M"
   2.503 +  assumes "0 \<in> M"
   2.504      shows "Suc (card {k. Suc k \<in> M \<and> k < i}) = card {k \<in> M. k < Suc i}"
   2.505  proof -
   2.506 -  from assms have a: "0 \<in> {k \<in> M. k < Suc i}" by simp
   2.507 -  hence c: "{k \<in> M. k < Suc i} = insert 0 ({k \<in> M. k < Suc i} - {0})"
   2.508 -    by (auto simp only: insert_Diff)
   2.509 -  have b: "{k \<in> M. k < Suc i} - {0} = {k \<in> M - {0}. k < Suc i}"  by auto
   2.510 -  from finite_M_bounded_by_nat[of "\<lambda>x. x \<in> M" "Suc i"]
   2.511 -  have "Suc (card {k. Suc k \<in> M \<and> k < i}) = card (insert 0 ({k \<in> M. k < Suc i} - {0}))"
   2.512 -    apply (subst card_insert)
   2.513 -    apply simp_all
   2.514 -    apply (subst b)
   2.515 -    apply (subst card_less_Suc2[symmetric])
   2.516 -    apply simp_all
   2.517 -    done
   2.518 -  with c show ?thesis by simp
   2.519 +  have "Suc (card {k. Suc k \<in> M \<and> k < i}) = Suc (card {k. Suc k \<in> M - {0} \<and> k < i})"
   2.520 +    by simp
   2.521 +  also have "\<dots> = Suc (card {k \<in> M - {0}. k < Suc i})"
   2.522 +    apply (subst card_less_Suc2)
   2.523 +    using assms by auto
   2.524 +  also have "\<dots> = Suc (card ({k \<in> M. k < Suc i} - {0}))"
   2.525 +    by (force intro: arg_cong [where f=card])
   2.526 +  also have "\<dots> = card (insert 0 ({k \<in> M. k < Suc i} - {0}))"
   2.527 +    by (simp add: card_insert)
   2.528 +  also have "... = card {k \<in> M. k < Suc i}"
   2.529 +    using assms
   2.530 +    by (force simp add: intro: arg_cong [where f=card])
   2.531 +  finally show ?thesis.
   2.532  qed
   2.533  
   2.534  
   2.535 @@ -1549,41 +1506,41 @@
   2.536    "{..<u} Un {u::'a::linorder} = {..u}"
   2.537    "(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}"
   2.538    "(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}"
   2.539 -  "(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}"
   2.540 -  "(l::'a::linorder) <= u ==> {l..<u} Un {u} = {l..u}"
   2.541 +  "(l::'a::linorder) \<le> u ==> {l} Un {l<..u} = {l..u}"
   2.542 +  "(l::'a::linorder) \<le> u ==> {l..<u} Un {u} = {l..u}"
   2.543  by auto
   2.544  
   2.545  text \<open>One- and two-sided intervals\<close>
   2.546  
   2.547  lemma ivl_disj_un_one:
   2.548    "(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}"
   2.549 -  "(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}"
   2.550 -  "(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}"
   2.551 -  "(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}"
   2.552 -  "(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}"
   2.553 +  "(l::'a::linorder) \<le> u ==> {..<l} Un {l..<u} = {..<u}"
   2.554 +  "(l::'a::linorder) \<le> u ==> {..l} Un {l<..u} = {..u}"
   2.555 +  "(l::'a::linorder) \<le> u ==> {..<l} Un {l..u} = {..u}"
   2.556 +  "(l::'a::linorder) \<le> u ==> {l<..u} Un {u<..} = {l<..}"
   2.557    "(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}"
   2.558 -  "(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}"
   2.559 -  "(l::'a::linorder) <= u ==> {l..<u} Un {u..} = {l..}"
   2.560 +  "(l::'a::linorder) \<le> u ==> {l..u} Un {u<..} = {l..}"
   2.561 +  "(l::'a::linorder) \<le> u ==> {l..<u} Un {u..} = {l..}"
   2.562  by auto
   2.563  
   2.564  text \<open>Two- and two-sided intervals\<close>
   2.565  
   2.566  lemma ivl_disj_un_two:
   2.567 -  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..<u} = {l<..<u}"
   2.568 -  "[| (l::'a::linorder) <= m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}"
   2.569 -  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..<u} = {l..<u}"
   2.570 -  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m<..<u} = {l..<u}"
   2.571 -  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..u} = {l<..u}"
   2.572 -  "[| (l::'a::linorder) <= m; m <= u |] ==> {l<..m} Un {m<..u} = {l<..u}"
   2.573 -  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..u} = {l..u}"
   2.574 -  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}"
   2.575 +  "[| (l::'a::linorder) < m; m \<le> u |] ==> {l<..<m} Un {m..<u} = {l<..<u}"
   2.576 +  "[| (l::'a::linorder) \<le> m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}"
   2.577 +  "[| (l::'a::linorder) \<le> m; m \<le> u |] ==> {l..<m} Un {m..<u} = {l..<u}"
   2.578 +  "[| (l::'a::linorder) \<le> m; m < u |] ==> {l..m} Un {m<..<u} = {l..<u}"
   2.579 +  "[| (l::'a::linorder) < m; m \<le> u |] ==> {l<..<m} Un {m..u} = {l<..u}"
   2.580 +  "[| (l::'a::linorder) \<le> m; m \<le> u |] ==> {l<..m} Un {m<..u} = {l<..u}"
   2.581 +  "[| (l::'a::linorder) \<le> m; m \<le> u |] ==> {l..<m} Un {m..u} = {l..u}"
   2.582 +  "[| (l::'a::linorder) \<le> m; m \<le> u |] ==> {l..m} Un {m<..u} = {l..u}"
   2.583  by auto
   2.584  
   2.585  lemma ivl_disj_un_two_touch:
   2.586    "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m..<u} = {l<..<u}"
   2.587 -  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m..<u} = {l..<u}"
   2.588 -  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..m} Un {m..u} = {l<..u}"
   2.589 -  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m..u} = {l..u}"
   2.590 +  "[| (l::'a::linorder) \<le> m; m < u |] ==> {l..m} Un {m..<u} = {l..<u}"
   2.591 +  "[| (l::'a::linorder) < m; m \<le> u |] ==> {l<..m} Un {m..u} = {l<..u}"
   2.592 +  "[| (l::'a::linorder) \<le> m; m \<le> u |] ==> {l..m} Un {m..u} = {l..u}"
   2.593  by auto
   2.594  
   2.595  lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch
   2.596 @@ -1635,14 +1592,11 @@
   2.597  
   2.598  subsubsection \<open>Some Subset Conditions\<close>
   2.599  
   2.600 -lemma ivl_subset [simp]:
   2.601 - "({i..<j} \<subseteq> {m..<n}) = (j \<le> i \<or> m \<le> i \<and> j \<le> (n::'a::linorder))"
   2.602 -apply(auto simp:linorder_not_le)
   2.603 -apply(rule ccontr)
   2.604 -apply(insert linorder_le_less_linear[of i n])
   2.605 -apply(clarsimp simp:linorder_not_le)
   2.606 -apply(fastforce)
   2.607 -done
   2.608 +lemma ivl_subset [simp]: "({i..<j} \<subseteq> {m..<n}) = (j \<le> i \<or> m \<le> i \<and> j \<le> (n::'a::linorder))"
   2.609 +  using linorder_class.le_less_linear[of i n]
   2.610 +  apply (auto simp: linorder_not_le)
   2.611 +   apply (force intro: leI)+
   2.612 +  done
   2.613  
   2.614  
   2.615  subsection \<open>Generic big monoid operation over intervals\<close>
   2.616 @@ -1866,14 +1820,14 @@
   2.617    "sum f {m..<Suc n} = (if n < m then 0 else sum f {m..<n} + f(n))"
   2.618    by (auto simp: ac_simps atLeastLessThanSuc)
   2.619  (*
   2.620 -lemma sum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
   2.621 +lemma sum_cl_ivl_add_one_nat: "(n::nat) \<le> m + 1 ==>
   2.622      (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
   2.623  by (auto simp:ac_simps atLeastAtMostSuc_conv)
   2.624  *)
   2.625  
   2.626  lemma sum_head:
   2.627    fixes n :: nat
   2.628 -  assumes mn: "m <= n"
   2.629 +  assumes mn: "m \<le> n"
   2.630    shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
   2.631  proof -
   2.632    from mn
   2.633 @@ -1904,24 +1858,25 @@
   2.634  lemmas sum_add_nat_ivl = sum.atLeastLessThan_concat
   2.635  
   2.636  lemma sum_diff_nat_ivl:
   2.637 -fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
   2.638 -shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
   2.639 -  sum f {m..<p} - sum f {m..<n} = sum f {n..<p}"
   2.640 -using sum_add_nat_ivl [of m n p f,symmetric]
   2.641 -apply (simp add: ac_simps)
   2.642 -done
   2.643 +  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
   2.644 +  shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> sum f {m..<p} - sum f {m..<n} = sum f {n..<p}"
   2.645 +  using sum_add_nat_ivl [of m n p f,symmetric]
   2.646 +  by (simp add: ac_simps)
   2.647  
   2.648  lemma sum_natinterval_difff:
   2.649    fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
   2.650    shows  "sum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} =
   2.651 -          (if m <= n then f m - f(n + 1) else 0)"
   2.652 +          (if m \<le> n then f m - f(n + 1) else 0)"
   2.653  by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
   2.654  
   2.655  lemma sum_nat_group: "(\<Sum>m<n::nat. sum f {m * k ..< m*k + k}) = sum f {..< n * k}"
   2.656 -  apply (subgoal_tac "k = 0 \<or> 0 < k", auto)
   2.657 -  apply (induct "n")
   2.658 -  apply (simp_all add: sum_add_nat_ivl add.commute atLeast0LessThan[symmetric])
   2.659 -  done
   2.660 +proof (cases k)
   2.661 +  case (Suc l)
   2.662 +  then have "k > 0"
   2.663 +    by auto
   2.664 +  then show ?thesis
   2.665 +    by (induct n) (simp_all add: sum_add_nat_ivl add.commute atLeast0LessThan[symmetric])
   2.666 +qed auto   
   2.667  
   2.668  lemma sum_triangle_reindex:
   2.669    fixes n :: nat
   2.670 @@ -1971,19 +1926,19 @@
   2.671  subsubsection \<open>Shifting bounds\<close>
   2.672  
   2.673  lemma sum_shift_bounds_nat_ivl:
   2.674 -  "sum f {m+k..<n+k} = sum (%i. f(i + k)){m..<n::nat}"
   2.675 +  "sum f {m+k..<n+k} = sum (\<lambda>i. f(i + k)){m..<n::nat}"
   2.676  by (induct "n", auto simp:atLeastLessThanSuc)
   2.677  
   2.678  lemma sum_shift_bounds_cl_nat_ivl:
   2.679 -  "sum f {m+k..n+k} = sum (%i. f(i + k)){m..n::nat}"
   2.680 +  "sum f {m+k..n+k} = sum (\<lambda>i. f(i + k)){m..n::nat}"
   2.681    by (rule sum.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
   2.682  
   2.683  corollary sum_shift_bounds_cl_Suc_ivl:
   2.684 -  "sum f {Suc m..Suc n} = sum (%i. f(Suc i)){m..n}"
   2.685 +  "sum f {Suc m..Suc n} = sum (\<lambda>i. f(Suc i)){m..n}"
   2.686  by (simp add:sum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
   2.687  
   2.688  corollary sum_shift_bounds_Suc_ivl:
   2.689 -  "sum f {Suc m..<Suc n} = sum (%i. f(Suc i)){m..<n}"
   2.690 +  "sum f {Suc m..<Suc n} = sum (\<lambda>i. f(Suc i)){m..<n}"
   2.691  by (simp add:sum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
   2.692  
   2.693  context comm_monoid_add
   2.694 @@ -2008,8 +1963,7 @@
   2.695      using \<open>f 0 = 0\<close> by simp
   2.696  qed
   2.697  
   2.698 -lemma sum_shift_lb_Suc0_0:
   2.699 -  "sum f {Suc 0..k} = sum f {0..k}"
   2.700 +lemma sum_shift_lb_Suc0_0: "sum f {Suc 0..k} = sum f {0..k}"
   2.701  proof (cases k)
   2.702    case 0
   2.703    with \<open>f 0 = 0\<close> show ?thesis
   2.704 @@ -2054,7 +2008,7 @@
   2.705    shows "(\<Sum>i\<le>n. f i) = f 0 + (\<Sum>i<n. f (Suc i))"
   2.706  by (metis atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost atLeastSucAtMost_greaterThanAtMost le0 sum_head sum_shift_bounds_Suc_ivl)
   2.707  
   2.708 -lemma sum_last_plus: fixes n::nat shows "m <= n \<Longrightarrow> (\<Sum>i = m..n. f i) = f n + (\<Sum>i = m..<n. f i)"
   2.709 +lemma sum_last_plus: fixes n::nat shows "m \<le> n \<Longrightarrow> (\<Sum>i = m..n. f i) = f n + (\<Sum>i = m..<n. f i)"
   2.710    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost add.commute)
   2.711  
   2.712  lemma sum_Suc_diff:
   2.713 @@ -2436,19 +2390,19 @@
   2.714  subsubsection \<open>Shifting bounds\<close>
   2.715  
   2.716  lemma prod_shift_bounds_nat_ivl:
   2.717 -  "prod f {m+k..<n+k} = prod (%i. f(i + k)){m..<n::nat}"
   2.718 +  "prod f {m+k..<n+k} = prod (\<lambda>i. f(i + k)){m..<n::nat}"
   2.719  by (induct "n", auto simp:atLeastLessThanSuc)
   2.720  
   2.721  lemma prod_shift_bounds_cl_nat_ivl:
   2.722 -  "prod f {m+k..n+k} = prod (%i. f(i + k)){m..n::nat}"
   2.723 +  "prod f {m+k..n+k} = prod (\<lambda>i. f(i + k)){m..n::nat}"
   2.724    by (rule prod.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
   2.725  
   2.726  corollary prod_shift_bounds_cl_Suc_ivl:
   2.727 -  "prod f {Suc m..Suc n} = prod (%i. f(Suc i)){m..n}"
   2.728 +  "prod f {Suc m..Suc n} = prod (\<lambda>i. f(Suc i)){m..n}"
   2.729  by (simp add:prod_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
   2.730  
   2.731  corollary prod_shift_bounds_Suc_ivl:
   2.732 -  "prod f {Suc m..<Suc n} = prod (%i. f(Suc i)){m..<n}"
   2.733 +  "prod f {Suc m..<Suc n} = prod (\<lambda>i. f(Suc i)){m..<n}"
   2.734  by (simp add:prod_shift_bounds_nat_ivl[where k="Suc 0", simplified])
   2.735  
   2.736  lemma prod_lessThan_Suc [simp]: "prod f {..<Suc n} = prod f {..<n} * f n"
     3.1 --- a/src/HOL/Transitive_Closure.thy	Thu Jul 12 11:23:46 2018 +0200
     3.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Jul 12 17:23:38 2018 +0100
     3.3 @@ -83,7 +83,7 @@
     3.4  subsection \<open>Reflexive-transitive closure\<close>
     3.5  
     3.6  lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) (=)) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"
     3.7 -  by (auto simp add: fun_eq_iff)
     3.8 +  by (auto simp: fun_eq_iff)
     3.9  
    3.10  lemma r_into_rtrancl [intro]: "\<And>p. p \<in> r \<Longrightarrow> p \<in> r\<^sup>*"
    3.11    \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close>
    3.12 @@ -156,18 +156,16 @@
    3.13      (base) "a = b"
    3.14    | (step) y where "(a, y) \<in> r\<^sup>*" and "(y, b) \<in> r"
    3.15    \<comment> \<open>elimination of \<open>rtrancl\<close> -- by induction on a special formula\<close>
    3.16 -  apply (subgoal_tac "a = b \<or> (\<exists>y. (a, y) \<in> r\<^sup>* \<and> (y, b) \<in> r)")
    3.17 -   apply (rule_tac [2] major [THEN rtrancl_induct])
    3.18 -    prefer 2 apply blast
    3.19 -   prefer 2 apply blast
    3.20 -  apply (erule asm_rl exE disjE conjE base step)+
    3.21 -  done
    3.22 +proof -
    3.23 +  have "a = b \<or> (\<exists>y. (a, y) \<in> r\<^sup>* \<and> (y, b) \<in> r)"
    3.24 +    by (rule major [THEN rtrancl_induct]) blast+
    3.25 +  then show ?thesis
    3.26 +    by (auto intro: base step)
    3.27 +qed
    3.28  
    3.29  lemma rtrancl_Int_subset: "Id \<subseteq> s \<Longrightarrow> (r\<^sup>* \<inter> s) O r \<subseteq> s \<Longrightarrow> r\<^sup>* \<subseteq> s"
    3.30 -  apply (rule subsetI)
    3.31 -  apply auto
    3.32 -  apply (erule rtrancl_induct)
    3.33 -  apply auto
    3.34 +  apply clarify
    3.35 +  apply (erule rtrancl_induct, auto)
    3.36    done
    3.37  
    3.38  lemma converse_rtranclp_into_rtranclp: "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c"
    3.39 @@ -193,14 +191,11 @@
    3.40    done
    3.41  
    3.42  lemma rtrancl_subset_rtrancl: "r \<subseteq> s\<^sup>* \<Longrightarrow> r\<^sup>* \<subseteq> s\<^sup>*"
    3.43 -  apply (drule rtrancl_mono)
    3.44 -  apply simp
    3.45 -  done
    3.46 +by (drule rtrancl_mono, simp)
    3.47  
    3.48  lemma rtranclp_subset: "R \<le> S \<Longrightarrow> S \<le> R\<^sup>*\<^sup>* \<Longrightarrow> S\<^sup>*\<^sup>* = R\<^sup>*\<^sup>*"
    3.49    apply (drule rtranclp_mono)
    3.50 -  apply (drule rtranclp_mono)
    3.51 -  apply simp
    3.52 +  apply (drule rtranclp_mono, simp)
    3.53    done
    3.54  
    3.55  lemmas rtrancl_subset = rtranclp_subset [to_set]
    3.56 @@ -216,21 +211,10 @@
    3.57  lemmas rtrancl_reflcl [simp] = rtranclp_reflclp [to_set]
    3.58  
    3.59  lemma rtrancl_r_diff_Id: "(r - Id)\<^sup>* = r\<^sup>*"
    3.60 -  apply (rule sym)
    3.61 -  apply (rule rtrancl_subset)
    3.62 -   apply blast
    3.63 -  apply clarify
    3.64 -  apply (rename_tac a b)
    3.65 -  apply (case_tac "a = b")
    3.66 -   apply blast
    3.67 -  apply blast
    3.68 -  done
    3.69 +  by (rule rtrancl_subset [symmetric]) auto
    3.70  
    3.71  lemma rtranclp_r_diff_Id: "(inf r (\<noteq>))\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*"
    3.72 -  apply (rule sym)
    3.73 -  apply (rule rtranclp_subset)
    3.74 -   apply blast+
    3.75 -  done
    3.76 +  by (rule rtranclp_subset [symmetric]) auto
    3.77  
    3.78  theorem rtranclp_converseD:
    3.79    assumes "(r\<inverse>\<inverse>)\<^sup>*\<^sup>* x y"
    3.80 @@ -272,12 +256,12 @@
    3.81    assumes major: "r\<^sup>*\<^sup>* x z"
    3.82      and cases: "x = z \<Longrightarrow> P" "\<And>y. r x y \<Longrightarrow> r\<^sup>*\<^sup>* y z \<Longrightarrow> P"
    3.83    shows P
    3.84 -  apply (subgoal_tac "x = z \<or> (\<exists>y. r x y \<and> r\<^sup>*\<^sup>* y z)")
    3.85 -   apply (rule_tac [2] major [THEN converse_rtranclp_induct])
    3.86 -    prefer 2 apply iprover
    3.87 -   prefer 2 apply iprover
    3.88 -  apply (erule asm_rl exE disjE conjE cases)+
    3.89 -  done
    3.90 +proof -
    3.91 +  have "x = z \<or> (\<exists>y. r x y \<and> r\<^sup>*\<^sup>* y z)"
    3.92 +    by (rule_tac major [THEN converse_rtranclp_induct]) iprover+
    3.93 +  then show ?thesis
    3.94 +    by (auto intro: cases)
    3.95 +qed
    3.96  
    3.97  lemmas converse_rtranclE = converse_rtranclpE [to_set]
    3.98  
    3.99 @@ -360,8 +344,7 @@
   3.100  
   3.101  lemma rtranclp_into_tranclp2: "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
   3.102    \<comment> \<open>intro rule from \<open>r\<close> and \<open>rtrancl\<close>\<close>
   3.103 -  apply (erule rtranclp.cases)
   3.104 -   apply iprover
   3.105 +  apply (erule rtranclp.cases, iprover)
   3.106    apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1])
   3.107      apply (simp | rule r_into_rtranclp)+
   3.108    done
   3.109 @@ -401,10 +384,8 @@
   3.110    using assms by cases simp_all
   3.111  
   3.112  lemma trancl_Int_subset: "r \<subseteq> s \<Longrightarrow> (r\<^sup>+ \<inter> s) O r \<subseteq> s \<Longrightarrow> r\<^sup>+ \<subseteq> s"
   3.113 -  apply (rule subsetI)
   3.114 -  apply auto
   3.115 -  apply (erule trancl_induct)
   3.116 -   apply auto
   3.117 +  apply clarify
   3.118 +  apply (erule trancl_induct, auto)
   3.119    done
   3.120  
   3.121  lemma trancl_unfold: "r\<^sup>+ = r \<union> r\<^sup>+ O r"
   3.122 @@ -438,10 +419,8 @@
   3.123  
   3.124  lemma trancl_id [simp]: "trans r \<Longrightarrow> r\<^sup>+ = r"
   3.125    apply auto
   3.126 -  apply (erule trancl_induct)
   3.127 -   apply assumption
   3.128 -  apply (unfold trans_def)
   3.129 -  apply blast
   3.130 +  apply (erule trancl_induct, assumption)
   3.131 +  apply (unfold trans_def, blast)
   3.132    done
   3.133  
   3.134  lemma rtranclp_tranclp_tranclp:
   3.135 @@ -485,16 +464,14 @@
   3.136      and cases: "\<And>y. r y b \<Longrightarrow> P y" "\<And>y z. r y z \<Longrightarrow> r\<^sup>+\<^sup>+ z b \<Longrightarrow> P z \<Longrightarrow> P y"
   3.137    shows "P a"
   3.138    apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major])
   3.139 -   apply (rule cases)
   3.140 -   apply (erule conversepD)
   3.141 +   apply (blast intro: cases)
   3.142    apply (blast intro: assms dest!: tranclp_converseD)
   3.143    done
   3.144  
   3.145  lemmas converse_trancl_induct = converse_tranclp_induct [to_set]
   3.146  
   3.147  lemma tranclpD: "R\<^sup>+\<^sup>+ x y \<Longrightarrow> \<exists>z. R x z \<and> R\<^sup>*\<^sup>* z y"
   3.148 -  apply (erule converse_tranclp_induct)
   3.149 -   apply auto
   3.150 +  apply (erule converse_tranclp_induct, auto)
   3.151    apply (blast intro: rtranclp_trans)
   3.152    done
   3.153  
   3.154 @@ -537,8 +514,7 @@
   3.155    by (induct rule: rtrancl_induct) auto
   3.156  
   3.157  lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A \<Longrightarrow> r\<^sup>+ \<subseteq> A \<times> A"
   3.158 -  apply (rule subsetI)
   3.159 -  apply (simp only: split_tupled_all)
   3.160 +  apply (clarsimp simp:)
   3.161    apply (erule tranclE)
   3.162     apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+
   3.163    done
   3.164 @@ -552,13 +528,19 @@
   3.165  lemmas reflcl_trancl [simp] = reflclp_tranclp [to_set]
   3.166  
   3.167  lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*"
   3.168 -  apply safe
   3.169 -   apply (drule trancl_into_rtrancl, simp)
   3.170 -  apply (erule rtranclE, safe)
   3.171 -   apply (rule r_into_trancl, simp)
   3.172 -  apply (rule rtrancl_into_trancl1)
   3.173 -   apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast)
   3.174 -  done
   3.175 +proof -
   3.176 +  have "(a, b) \<in> (r\<^sup>=)\<^sup>+ \<Longrightarrow> (a, b) \<in> r\<^sup>*" for a b
   3.177 +    by (force dest: trancl_into_rtrancl)
   3.178 +  moreover have "(a, b) \<in> (r\<^sup>=)\<^sup>+" if "(a, b) \<in> r\<^sup>*" for a b
   3.179 +    using that
   3.180 +  proof (cases a b rule: rtranclE)
   3.181 +    case step
   3.182 +    show ?thesis
   3.183 +      by (rule rtrancl_into_trancl1) (use step in auto)
   3.184 +  qed auto
   3.185 +  ultimately show ?thesis 
   3.186 +    by auto
   3.187 +qed
   3.188  
   3.189  lemma rtrancl_trancl_reflcl [code]: "r\<^sup>* = (r\<^sup>+)\<^sup>="
   3.190    by simp
   3.191 @@ -570,7 +552,7 @@
   3.192    by (rule subst [OF reflcl_trancl]) simp
   3.193  
   3.194  lemma rtranclpD: "R\<^sup>*\<^sup>* a b \<Longrightarrow> a = b \<or> a \<noteq> b \<and> R\<^sup>+\<^sup>+ a b"
   3.195 -  by (force simp add: reflclp_tranclp [symmetric] simp del: reflclp_tranclp)
   3.196 +  by (force simp: reflclp_tranclp [symmetric] simp del: reflclp_tranclp)
   3.197  
   3.198  lemmas rtranclD = rtranclpD [to_set]
   3.199  
   3.200 @@ -585,19 +567,20 @@
   3.201  
   3.202  lemma trancl_insert: "(insert (y, x) r)\<^sup>+ = r\<^sup>+ \<union> {(a, b). (a, y) \<in> r\<^sup>* \<and> (x, b) \<in> r\<^sup>*}"
   3.203    \<comment> \<open>primitive recursion for \<open>trancl\<close> over finite relations\<close>
   3.204 -  apply (rule equalityI)
   3.205 -   apply (rule subsetI)
   3.206 -   apply (simp only: split_tupled_all)
   3.207 -   apply (erule trancl_induct, blast)
   3.208 -   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)
   3.209 -  apply (rule subsetI)
   3.210 -  apply (blast intro: trancl_mono rtrancl_mono
   3.211 -      [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   3.212 -  done
   3.213 +proof -
   3.214 +  have "\<And>a b. (a, b) \<in> (insert (y, x) r)\<^sup>+ \<Longrightarrow>
   3.215 +           (a, b) \<in> r\<^sup>+ \<union> {(a, b). (a, y) \<in> r\<^sup>* \<and> (x, b) \<in> r\<^sup>*}"
   3.216 +    by (erule trancl_induct) (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)+
   3.217 +  moreover have "r\<^sup>+ \<union> {(a, b). (a, y) \<in> r\<^sup>* \<and> (x, b) \<in> r\<^sup>*}  \<subseteq> (insert (y, x) r)\<^sup>+"
   3.218 +    by (blast intro: trancl_mono rtrancl_mono [THEN [2] rev_subsetD]
   3.219 +                     rtrancl_trancl_trancl rtrancl_into_trancl2)
   3.220 +  ultimately show ?thesis
   3.221 +    by auto
   3.222 +qed
   3.223  
   3.224  lemma trancl_insert2:
   3.225    "(insert (a, b) r)\<^sup>+ = r\<^sup>+ \<union> {(x, y). ((x, a) \<in> r\<^sup>+ \<or> x = a) \<and> ((b, y) \<in> r\<^sup>+ \<or> y = b)}"
   3.226 -  by (auto simp add: trancl_insert rtrancl_eq_or_trancl)
   3.227 +  by (auto simp: trancl_insert rtrancl_eq_or_trancl)
   3.228  
   3.229  lemma rtrancl_insert: "(insert (a,b) r)\<^sup>* = r\<^sup>* \<union> {(x, y). (x, a) \<in> r\<^sup>* \<and> (b, y) \<in> r\<^sup>*}"
   3.230    using trancl_insert[of a b r]
   3.231 @@ -636,28 +619,30 @@
   3.232  lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r"
   3.233    unfolding Domain_converse [symmetric] by (simp add: trancl_converse [symmetric])
   3.234  
   3.235 -lemma Not_Domain_rtrancl: "x \<notin> Domain R \<Longrightarrow> (x, y) \<in> R\<^sup>* \<longleftrightarrow> x = y"
   3.236 -  apply auto
   3.237 -  apply (erule rev_mp)
   3.238 -  apply (erule rtrancl_induct)
   3.239 -   apply auto
   3.240 -  done
   3.241 +lemma Not_Domain_rtrancl: 
   3.242 +  assumes "x \<notin> Domain R" shows "(x, y) \<in> R\<^sup>* \<longleftrightarrow> x = y"
   3.243 +proof -
   3.244 +have "(x, y) \<in> R\<^sup>* \<Longrightarrow> x = y"
   3.245 +  by (erule rtrancl_induct) (use assms in auto)
   3.246 +  then show ?thesis
   3.247 +    by auto
   3.248 +qed
   3.249  
   3.250  lemma trancl_subset_Field2: "r\<^sup>+ \<subseteq> Field r \<times> Field r"
   3.251    apply clarify
   3.252    apply (erule trancl_induct)
   3.253 -   apply (auto simp add: Field_def)
   3.254 +   apply (auto simp: Field_def)
   3.255    done
   3.256  
   3.257  lemma finite_trancl[simp]: "finite (r\<^sup>+) = finite r"
   3.258 -  apply auto
   3.259 -   prefer 2
   3.260 +proof
   3.261 +  show "finite (r\<^sup>+) \<Longrightarrow> finite r"
   3.262 +    by (blast intro: r_into_trancl' finite_subset)
   3.263 +  show "finite r \<Longrightarrow> finite (r\<^sup>+)"
   3.264     apply (rule trancl_subset_Field2 [THEN finite_subset])
   3.265 -   apply (rule finite_SigmaI)
   3.266 -    prefer 3
   3.267 -    apply (blast intro: r_into_trancl' finite_subset)
   3.268 -   apply (auto simp add: finite_Field)
   3.269 +   apply (auto simp: finite_Field)
   3.270    done
   3.271 +qed
   3.272  
   3.273  lemma finite_rtrancl_Image[simp]: assumes "finite R" "finite A" shows "finite (R\<^sup>* `` A)"
   3.274  proof (rule ccontr)
   3.275 @@ -670,13 +655,20 @@
   3.276    be merged with main body.\<close>
   3.277  
   3.278  lemma single_valued_confluent:
   3.279 -  "single_valued r \<Longrightarrow> (x, y) \<in> r\<^sup>* \<Longrightarrow> (x, z) \<in> r\<^sup>* \<Longrightarrow> (y, z) \<in> r\<^sup>* \<or> (z, y) \<in> r\<^sup>*"
   3.280 -  apply (erule rtrancl_induct)
   3.281 -   apply simp
   3.282 -  apply (erule disjE)
   3.283 -   apply (blast elim:converse_rtranclE dest:single_valuedD)
   3.284 -  apply (blast intro:rtrancl_trans)
   3.285 -  done
   3.286 +  assumes "single_valued r" and xy: "(x, y) \<in> r\<^sup>*" and xz: "(x, z) \<in> r\<^sup>*"
   3.287 +  shows "(y, z) \<in> r\<^sup>* \<or> (z, y) \<in> r\<^sup>*"
   3.288 +  using xy
   3.289 +proof (induction rule: rtrancl_induct)
   3.290 +  case base
   3.291 +  show ?case
   3.292 +    by (simp add: assms)   
   3.293 +next
   3.294 +  case (step y z)
   3.295 +  with xz \<open>single_valued r\<close> show ?case
   3.296 +    apply (auto simp: elim: converse_rtranclE dest: single_valuedD)
   3.297 +    apply (blast intro: rtrancl_trans)
   3.298 +    done
   3.299 +qed
   3.300  
   3.301  lemma r_r_into_trancl: "(a, b) \<in> R \<Longrightarrow> (b, c) \<in> R \<Longrightarrow> (a, c) \<in> R\<^sup>+"
   3.302    by (fast intro: trancl_trans)
   3.303 @@ -824,16 +816,18 @@
   3.304    by (fact relpow_Suc_D2' [to_pred])
   3.305  
   3.306  lemma relpow_E2:
   3.307 -  "(x, z) \<in> R ^^ n \<Longrightarrow>
   3.308 -    (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) \<Longrightarrow>
   3.309 -    (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P) \<Longrightarrow> P"
   3.310 -  apply (cases n)
   3.311 -   apply simp
   3.312 -  apply (rename_tac nat)
   3.313 -  apply (cut_tac n=nat and R=R in relpow_Suc_D2')
   3.314 -  apply simp
   3.315 -  apply blast
   3.316 -  done
   3.317 +  assumes "(x, z) \<in> R ^^ n" "n = 0 \<Longrightarrow> x = z \<Longrightarrow> P"
   3.318 +          "\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P"
   3.319 +      shows "P"
   3.320 +proof (cases n)
   3.321 +  case 0
   3.322 +  with assms show ?thesis
   3.323 +    by simp
   3.324 +next
   3.325 +  case (Suc m)
   3.326 +  with assms relpow_Suc_D2' [of m R] show ?thesis
   3.327 +    by force
   3.328 +qed
   3.329  
   3.330  lemma relpowp_E2:
   3.331    "(P ^^ n) x z \<Longrightarrow>
   3.332 @@ -915,22 +909,23 @@
   3.333    by (simp add: rtranclp_is_Sup_relpowp)
   3.334  
   3.335  lemma trancl_power: "p \<in> R\<^sup>+ \<longleftrightarrow> (\<exists>n > 0. p \<in> R ^^ n)"
   3.336 -  apply (cases p)
   3.337 -  apply simp
   3.338 -  apply (rule iffI)
   3.339 -   apply (drule tranclD2)
   3.340 -   apply (clarsimp simp: rtrancl_is_UN_relpow)
   3.341 -   apply (rule_tac x="Suc x" in exI)
   3.342 -   apply (clarsimp simp: relcomp_unfold)
   3.343 -   apply fastforce
   3.344 -  apply clarsimp
   3.345 -  apply (case_tac n)
   3.346 -   apply simp
   3.347 -  apply clarsimp
   3.348 -  apply (drule relpow_imp_rtrancl)
   3.349 -  apply (drule rtrancl_into_trancl1)
   3.350 -   apply auto
   3.351 -  done
   3.352 +proof -
   3.353 +  have "((a, b) \<in> R\<^sup>+) = (\<exists>n>0. (a, b) \<in> R ^^ n)" for a b
   3.354 +  proof safe
   3.355 +    show "(a, b) \<in> R\<^sup>+ \<Longrightarrow> \<exists>n>0. (a, b) \<in> R ^^ n"
   3.356 +      apply (drule tranclD2)
   3.357 +      apply (fastforce simp: rtrancl_is_UN_relpow relcomp_unfold)
   3.358 +      done
   3.359 +    show "(a, b) \<in> R\<^sup>+" if "n > 0" "(a, b) \<in> R ^^ n" for n
   3.360 +    proof (cases n)
   3.361 +      case (Suc m)
   3.362 +      with that show ?thesis
   3.363 +        by (auto simp: dest: relpow_imp_rtrancl rtrancl_into_trancl1)
   3.364 +    qed (use that in auto)
   3.365 +  qed
   3.366 +  then show ?thesis
   3.367 +    by (cases p) auto
   3.368 +qed
   3.369  
   3.370  lemma tranclp_power: "(P\<^sup>+\<^sup>+) x y \<longleftrightarrow> (\<exists>n > 0. (P ^^ n) x y)"
   3.371    using trancl_power [to_pred, of P "(x, y)"] by simp
   3.372 @@ -1070,8 +1065,7 @@
   3.373    fixes R :: "('a \<times> 'a) set"
   3.374    assumes "finite R"
   3.375    shows "R^^k \<subseteq> (UN n:{n. n \<le> card R}. R^^n)"
   3.376 -  apply (cases k)
   3.377 -   apply force
   3.378 +  apply (cases k, force)
   3.379    apply (use relpow_finite_bounded1[OF assms, of k] in auto)
   3.380    done
   3.381  
   3.382 @@ -1088,7 +1082,7 @@
   3.383    shows "finite (R O S)"
   3.384  proof-
   3.385    have "R O S = (\<Union>(x, y)\<in>R. \<Union>(u, v)\<in>S. if u = y then {(x, v)} else {})"
   3.386 -    by (force simp add: split_def image_constant_conv split: if_splits)
   3.387 +    by (force simp: split_def image_constant_conv split: if_splits)
   3.388    then show ?thesis
   3.389      using assms by clarsimp
   3.390  qed
   3.391 @@ -1166,7 +1160,7 @@
   3.392    by (auto simp: Let_def)
   3.393  
   3.394  lemma finite_trancl_ntranl: "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R"
   3.395 -  by (cases "card R") (auto simp add: trancl_finite_eq_relpow relpow_empty ntrancl_def)
   3.396 +  by (cases "card R") (auto simp: trancl_finite_eq_relpow relpow_empty ntrancl_def)
   3.397  
   3.398  
   3.399  subsection \<open>Acyclic relations\<close>