author blanchet Wed Feb 08 01:49:33 2012 +0100 (2012-02-08) changeset 46440 d4994e2e7364 parent 46439 2388be11cb50 child 46441 992a1688303f
use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
 src/HOL/List.thy file | annotate | diff | revisions src/HOL/Word/Word.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/List.thy	Wed Feb 08 00:55:06 2012 +0100
1.2 +++ b/src/HOL/List.thy	Wed Feb 08 01:49:33 2012 +0100
1.3 @@ -206,9 +206,9 @@
1.4    length :: "'a list \<Rightarrow> nat" where
1.5    "length \<equiv> size"
1.6
1.7 -definition
1.8 -  rotate1 :: "'a list \<Rightarrow> 'a list" where
1.9 -  "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
1.10 +primrec rotate1 :: "'a list \<Rightarrow> 'a list" where
1.11 +  "rotate1 [] = []" |
1.12 +  "rotate1 (x # xs) = xs @ [x]"
1.13
1.14  definition
1.15    rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
1.16 @@ -265,8 +265,8 @@
1.17  @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
1.18  @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
1.19  @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
1.20 -@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
1.21 -@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def eval_nat_numeral)}\\
1.22 +@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
1.23 +@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
1.24  @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
1.25  @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
1.26  @{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)}
1.27 @@ -2880,7 +2880,7 @@
1.28  by (metis distinct_remdups finite_list set_remdups)
1.29
1.30  lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
1.31 -by (induct x, auto)
1.32 +by (induct x, auto)
1.33
1.34  lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
1.35  by (induct x, auto)
1.36 @@ -2967,7 +2967,7 @@
1.37  apply (case_tac j, simp)
1.39   apply (case_tac j)
1.40 -apply (clarsimp simp add: set_conv_nth, simp)
1.41 +apply (clarsimp simp add: set_conv_nth, simp)
1.42  apply (rule conjI)
1.43  (*TOO SLOW
1.44  apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
1.45 @@ -2999,7 +2999,7 @@
1.46      case False with Cons show ?thesis by simp
1.47    next
1.48      case True with Cons.prems
1.49 -    have "card (set xs) = Suc (length xs)"
1.50 +    have "card (set xs) = Suc (length xs)"
1.51        by (simp add: card_insert_if split: split_if_asm)
1.52      moreover have "card (set xs) \<le> length xs" by (rule card_length)
1.53      ultimately have False by simp
1.54 @@ -3590,9 +3590,6 @@
1.55
1.56  subsubsection{*@{text rotate1} and @{text rotate}*}
1.57
1.58 -lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
1.60 -
1.61  lemma rotate0[simp]: "rotate 0 = id"
1.63
1.64 @@ -3619,7 +3616,7 @@
1.65  done
1.66
1.67  lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
1.69 +by (cases xs) simp_all
1.70
1.71  lemma rotate_drop_take:
1.72    "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
1.73 @@ -3642,13 +3639,13 @@
1.75
1.76  lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
1.78 +by (cases xs) simp_all
1.79
1.80  lemma length_rotate[simp]: "length(rotate n xs) = length xs"
1.81  by (induct n arbitrary: xs) (simp_all add:rotate_def)
1.82
1.83  lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
1.85 +by (cases xs) auto
1.86
1.87  lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
1.88  by (induct n) (simp_all add:rotate_def)
1.89 @@ -3657,13 +3654,13 @@
1.91
1.92  lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
1.93 -by (cases xs) (auto simp add:rotate1_def)
1.94 +by (cases xs) auto
1.95
1.96  lemma set_rotate[simp]: "set(rotate n xs) = set xs"
1.97  by (induct n) (simp_all add:rotate_def)
1.98
1.99  lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
1.101 +by (cases xs) auto
1.102
1.103  lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
1.104  by (induct n) (simp_all add:rotate_def)
```
```     2.1 --- a/src/HOL/Word/Word.thy	Wed Feb 08 00:55:06 2012 +0100
2.2 +++ b/src/HOL/Word/Word.thy	Wed Feb 08 01:49:33 2012 +0100
2.3 @@ -3942,7 +3942,7 @@
2.4      rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
2.5    apply (unfold map2_def)
2.6    apply (cases xs)
2.7 -   apply (cases ys, auto simp add : rotate1_def)+
2.8 +   apply (cases ys, auto)+
2.9    done
2.10
2.11  lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
```