author wenzelm Mon May 23 15:29:38 2016 +0200 (2016-05-23 ago) changeset 63112 6813818baa67 parent 63111 caa0c513bbca child 63113 fe31996e3898
tuned proofs;
```     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.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.22    with iseq have "idx m < idx n"
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"
```