# HG changeset patch
# User blanchet
# Date 1328662173 -3600
# Node ID d4994e2e73649b4bdd8250d4ee4c648f7b09f10c
# Parent  2388be11cb50c90694e9e0c99f81634b0520e5b6
use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")

diff -r 2388be11cb50 -r d4994e2e7364 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 08 00:55:06 2012 +0100
+++ b/src/HOL/List.thy	Wed Feb 08 01:49:33 2012 +0100
@@ -206,9 +206,9 @@
   length :: "'a list \<Rightarrow> nat" where
   "length \<equiv> size"
 
-definition
-  rotate1 :: "'a list \<Rightarrow> 'a list" where
-  "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
+primrec rotate1 :: "'a list \<Rightarrow> 'a list" where
+  "rotate1 [] = []" |
+  "rotate1 (x # xs) = xs @ [x]"
 
 definition
   rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -265,8 +265,8 @@
 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
-@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
-@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def eval_nat_numeral)}\\
+@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
+@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
 @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
 @{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)}
@@ -2880,7 +2880,7 @@
 by (metis distinct_remdups finite_list set_remdups)
 
 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
-by (induct x, auto) 
+by (induct x, auto)
 
 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
 by (induct x, auto)
@@ -2967,7 +2967,7 @@
 apply (case_tac j, simp)
 apply (simp add: set_conv_nth)
  apply (case_tac j)
-apply (clarsimp simp add: set_conv_nth, simp) 
+apply (clarsimp simp add: set_conv_nth, simp)
 apply (rule conjI)
 (*TOO SLOW
 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
@@ -2999,7 +2999,7 @@
     case False with Cons show ?thesis by simp
   next
     case True with Cons.prems
-    have "card (set xs) = Suc (length xs)" 
+    have "card (set xs) = Suc (length xs)"
       by (simp add: card_insert_if split: split_if_asm)
     moreover have "card (set xs) \<le> length xs" by (rule card_length)
     ultimately have False by simp
@@ -3590,9 +3590,6 @@
 
 subsubsection{*@{text rotate1} and @{text rotate}*}
 
-lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
-by(simp add:rotate1_def)
-
 lemma rotate0[simp]: "rotate 0 = id"
 by(simp add:rotate_def)
 
@@ -3619,7 +3616,7 @@
 done
 
 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
-by(simp add:rotate1_def split:list.split)
+by (cases xs) simp_all
 
 lemma rotate_drop_take:
   "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
@@ -3642,13 +3639,13 @@
 by(simp add:rotate_drop_take)
 
 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
-by(simp add:rotate1_def split:list.split)
+by (cases xs) simp_all
 
 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
 by (induct n arbitrary: xs) (simp_all add:rotate_def)
 
 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
-by(simp add:rotate1_def split:list.split) blast
+by (cases xs) auto
 
 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
 by (induct n) (simp_all add:rotate_def)
@@ -3657,13 +3654,13 @@
 by(simp add:rotate_drop_take take_map drop_map)
 
 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
-by (cases xs) (auto simp add:rotate1_def)
+by (cases xs) auto
 
 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
 by (induct n) (simp_all add:rotate_def)
 
 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
-by(simp add:rotate1_def split:list.split)
+by (cases xs) auto
 
 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
 by (induct n) (simp_all add:rotate_def)
diff -r 2388be11cb50 -r d4994e2e7364 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Feb 08 00:55:06 2012 +0100
+++ b/src/HOL/Word/Word.thy	Wed Feb 08 01:49:33 2012 +0100
@@ -3942,7 +3942,7 @@
     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" 
   apply (unfold map2_def)
   apply (cases xs)
-   apply (cases ys, auto simp add : rotate1_def)+
+   apply (cases ys, auto)+
   done
 
 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]