tuned proofs;
authorwenzelm
Mon May 23 15:29:38 2016 +0200 (2016-05-23 ago)
changeset 631126813818baa67
parent 63111 caa0c513bbca
child 63113 fe31996e3898
tuned proofs;
src/HOL/Library/Omega_Words_Fun.thy
     1.1 --- a/src/HOL/Library/Omega_Words_Fun.thy	Mon May 23 14:56:48 2016 +0200
     1.2 +++ b/src/HOL/Library/Omega_Words_Fun.thy	Mon May 23 15:29:38 2016 +0200
     1.3 @@ -800,8 +800,8 @@
     1.4    assumes iseq: "idx_sequence idx"
     1.5      and eq: "idx m = idx n"
     1.6    shows "m = n"
     1.7 -proof (rule nat_less_cases)
     1.8 -  assume "n<m"
     1.9 +proof (cases m n rule: linorder_cases)
    1.10 +  case greater
    1.11    then obtain k where "m = Suc(n+k)"
    1.12      by (auto simp add: less_iff_Suc_add)
    1.13    with iseq have "idx n < idx m"
    1.14 @@ -809,14 +809,14 @@
    1.15    with eq show ?thesis
    1.16      by simp
    1.17  next
    1.18 -  assume "m<n"
    1.19 +  case less
    1.20    then obtain k where "n = Suc(m+k)"
    1.21      by (auto simp add: less_iff_Suc_add)
    1.22    with iseq have "idx m < idx n"
    1.23      by (simp add: idx_sequence_less)
    1.24    with eq show ?thesis
    1.25      by simp
    1.26 -qed (simp)
    1.27 +qed
    1.28  
    1.29  lemma idx_sequence_mono:
    1.30    assumes iseq: "idx_sequence idx"
    1.31 @@ -883,8 +883,8 @@
    1.32      and k: "n \<in> {idx k ..< idx (Suc k)}"
    1.33      and m: "n \<in> {idx m ..< idx (Suc m)}"
    1.34    shows "k = m"
    1.35 -proof (rule nat_less_cases)
    1.36 -  assume "k < m"
    1.37 +proof (cases k m rule: linorder_cases)
    1.38 +  case less
    1.39    hence "Suc k \<le> m" by simp
    1.40    with iseq have "idx (Suc k) \<le> idx m"
    1.41      by (rule idx_sequence_mono)
    1.42 @@ -894,7 +894,7 @@
    1.43      by simp
    1.44    thus ?thesis ..
    1.45  next
    1.46 -  assume "m < k"
    1.47 +  case greater
    1.48    hence "Suc m \<le> k" by simp
    1.49    with iseq have "idx (Suc m) \<le> idx k"
    1.50      by (rule idx_sequence_mono)
    1.51 @@ -903,7 +903,7 @@
    1.52    with m have "False"
    1.53      by simp
    1.54    thus ?thesis ..
    1.55 -qed (simp)
    1.56 +qed
    1.57  
    1.58  lemma idx_sequence_unique_interval:
    1.59    assumes iseq: "idx_sequence idx"