use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
authorblanchet
Wed Feb 08 01:49:33 2012 +0100 (2012-02-08)
changeset 46440d4994e2e7364
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
src/HOL/Word/Word.thy
     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.38  apply (simp add: set_conv_nth)
    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.59 -by(simp add:rotate1_def)
    1.60 -
    1.61  lemma rotate0[simp]: "rotate 0 = id"
    1.62  by(simp add:rotate_def)
    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.68 -by(simp add:rotate1_def split:list.split)
    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.74  by(simp add:rotate_drop_take)
    1.75  
    1.76  lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
    1.77 -by(simp add:rotate1_def split:list.split)
    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.84 -by(simp add:rotate1_def split:list.split) blast
    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.90  by(simp add:rotate_drop_take take_map drop_map)
    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.100 -by(simp add:rotate1_def split:list.split)
   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]