added simp lemma nth_Cons_pos to List
authornipkow
Fri Feb 25 14:25:41 2011 +0100 (2011-02-25)
changeset 41842d8f76db6a207
parent 41840 f69045fdc836
child 41843 15d76ed6ea67
added simp lemma nth_Cons_pos to List
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Hoare_Parallel/Graph.thy
src/HOL/Hoare_Parallel/RG_Examples.thy
src/HOL/Hoare_Parallel/RG_Hoare.thy
src/HOL/Hoare_Parallel/RG_Tran.thy
src/HOL/Imperative_HOL/ex/Sublist.thy
src/HOL/List.thy
src/HOL/Word/Bool_List_Representation.thy
     1.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Feb 25 08:46:52 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Feb 25 14:25:41 2011 +0100
     1.3 @@ -39,10 +39,6 @@
     1.4    with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
     1.5  qed
     1.6  
     1.7 -lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
     1.8 -using Nat.gr0_conv_Suc
     1.9 -by clarsimp
    1.10 -
    1.11  
    1.12    (*********************************************************************************)
    1.13    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    1.14 @@ -240,7 +236,7 @@
    1.15    assumes nb: "numbound0 a"
    1.16    shows "Inum (b#bs) a = Inum (b'#bs) a"
    1.17  using nb
    1.18 -by (induct a) (simp_all add: nth_pos2)
    1.19 +by (induct a) simp_all
    1.20  
    1.21  primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
    1.22    "bound0 T = True"
    1.23 @@ -263,7 +259,7 @@
    1.24    assumes bp: "bound0 p"
    1.25    shows "Ifm (b#bs) p = Ifm (b'#bs) p"
    1.26  using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
    1.27 -by (induct p) (auto simp add: nth_pos2)
    1.28 +by (induct p) auto
    1.29  
    1.30  lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
    1.31  by (cases p, auto)
    1.32 @@ -316,12 +312,12 @@
    1.33  
    1.34  lemma decrnum: assumes nb: "numbound0 t"
    1.35    shows "Inum (x#bs) t = Inum bs (decrnum t)"
    1.36 -  using nb by (induct t rule: decrnum.induct, simp_all add: nth_pos2)
    1.37 +  using nb by (induct t rule: decrnum.induct, simp_all)
    1.38  
    1.39  lemma decr: assumes nb: "bound0 p"
    1.40    shows "Ifm (x#bs) p = Ifm bs (decr p)"
    1.41    using nb 
    1.42 -  by (induct p rule: decr.induct, simp_all add: nth_pos2 decrnum)
    1.43 +  by (induct p rule: decr.induct, simp_all add: decrnum)
    1.44  
    1.45  lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
    1.46  by (induct p, simp_all)
    1.47 @@ -1420,7 +1416,7 @@
    1.48    also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
    1.49      using np by simp 
    1.50    finally show ?case using nbt nb by (simp add: algebra_simps)
    1.51 -qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2)
    1.52 +qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"])
    1.53  
    1.54  lemma uset_l:
    1.55    assumes lp: "isrlfm p"
    1.56 @@ -1436,7 +1432,7 @@
    1.57  proof-
    1.58    have "\<exists> (s,m) \<in> set (uset p). real m * x \<ge> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<ge> ?N a s")
    1.59      using lp nmi ex
    1.60 -    by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
    1.61 +    by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
    1.62    then obtain s m where smU: "(s,m) \<in> set (uset p)" and mx: "real m * x \<ge> ?N a s" by blast
    1.63    from uset_l[OF lp] smU have mp: "real m > 0" by auto
    1.64    from pos_divide_le_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \<ge> ?N a s / real m" 
    1.65 @@ -1452,7 +1448,7 @@
    1.66  proof-
    1.67    have "\<exists> (s,m) \<in> set (uset p). real m * x \<le> Inum (a#bs) s " (is "\<exists> (s,m) \<in> ?U p. real m *x \<le> ?N a s")
    1.68      using lp nmi ex
    1.69 -    by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
    1.70 +    by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
    1.71    then obtain s m where smU: "(s,m) \<in> set (uset p)" and mx: "real m * x \<le> ?N a s" by blast
    1.72    from uset_l[OF lp] smU have mp: "real m > 0" by auto
    1.73    from pos_le_divide_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \<le> ?N a s / real m" 
    1.74 @@ -1563,7 +1559,7 @@
    1.75    hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
    1.76    thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 
    1.77      by (simp add: algebra_simps)
    1.78 -qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
    1.79 +qed (auto simp add: numbound0_I[where bs="bs" and b="y" and b'="x"])
    1.80  
    1.81  lemma finite_set_intervals:
    1.82    assumes px: "P (x::real)" 
     2.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 25 08:46:52 2011 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 25 14:25:41 2011 +0100
     2.3 @@ -67,7 +67,7 @@
     2.4    assumes nb: "tmbound0 a"
     2.5    shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
     2.6  using nb
     2.7 -by (induct a rule: tm.induct,auto simp add: nth_pos2)
     2.8 +by (induct a rule: tm.induct,auto)
     2.9  
    2.10  primrec tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *) where
    2.11    "tmbound n (CP c) = True"
    2.12 @@ -105,10 +105,10 @@
    2.13  
    2.14  lemma decrtm0: assumes nb: "tmbound0 t"
    2.15    shows "Itm vs (x#bs) t = Itm vs bs (decrtm0 t)"
    2.16 -  using nb by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
    2.17 +  using nb by (induct t rule: decrtm0.induct, simp_all)
    2.18  
    2.19  lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t"
    2.20 -  by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
    2.21 +  by (induct t rule: decrtm0.induct, simp_all)
    2.22  
    2.23  primrec decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" where
    2.24    "decrtm m (CP c) = (CP c)"
    2.25 @@ -175,10 +175,10 @@
    2.26  | "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
    2.27  lemma tmsubst0:
    2.28    shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
    2.29 -  by (induct a rule: tm.induct) (auto simp add: nth_pos2)
    2.30 +  by (induct a rule: tm.induct) auto
    2.31  
    2.32  lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
    2.33 -  by (induct a rule: tm.induct) (auto simp add: nth_pos2)
    2.34 +  by (induct a rule: tm.induct) auto
    2.35  
    2.36  primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where
    2.37    "tmsubst n t (CP c) = CP c"
    2.38 @@ -193,7 +193,7 @@
    2.39  lemma tmsubst: assumes nb: "tmboundslt (length bs) a" and nlt: "n \<le> length bs"
    2.40    shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a"
    2.41  using nb nlt
    2.42 -by (induct a rule: tm.induct,auto simp add: nth_pos2)
    2.43 +by (induct a rule: tm.induct,auto)
    2.44  
    2.45  lemma tmsubst_nb0: assumes tnb: "tmbound0 t"
    2.46  shows "tmbound0 (tmsubst 0 t a)"
    2.47 @@ -534,7 +534,7 @@
    2.48    assumes bp: "bound0 p"
    2.49    shows "Ifm vs (b#bs) p = Ifm vs (b'#bs) p"
    2.50  using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
    2.51 -by (induct p rule: bound0.induct,auto simp add: nth_pos2)
    2.52 +by (induct p rule: bound0.induct,auto)
    2.53  
    2.54  primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *) where
    2.55    "bound m T = True"
    2.56 @@ -1585,7 +1585,7 @@
    2.57  proof-
    2.58    have "\<exists> (c,s) \<in> set (uset p). (Ipoly vs c < 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s) \<or>  (Ipoly vs c > 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s)" 
    2.59      using lp nmi ex
    2.60 -    apply (induct p rule: minusinf.induct, auto simp add: eq le lt nth_pos2 polyneg_norm)
    2.61 +    apply (induct p rule: minusinf.induct, auto simp add: eq le lt polyneg_norm)
    2.62      apply (auto simp add: linorder_not_less order_le_less)
    2.63      done 
    2.64    then obtain c s where csU: "(c,s) \<in> set (uset p)" and x: "(Ipoly vs c < 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s) \<or>  (Ipoly vs c > 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s)" by blast
    2.65 @@ -1618,7 +1618,7 @@
    2.66  proof-
    2.67    have "\<exists> (c,s) \<in> set (uset p). (Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s) \<or>  (Ipoly vs c > 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s)" 
    2.68      using lp nmi ex
    2.69 -    apply (induct p rule: minusinf.induct, auto simp add: eq le lt nth_pos2 polyneg_norm)
    2.70 +    apply (induct p rule: minusinf.induct, auto simp add: eq le lt polyneg_norm)
    2.71      apply (auto simp add: linorder_not_less order_le_less)
    2.72      done 
    2.73    then obtain c s where csU: "(c,s) \<in> set (uset p)" and x: "(Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s) \<or>  (Ipoly vs c > 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s)" by blast
    2.74 @@ -1798,7 +1798,7 @@
    2.75      from yne c eq_divide_eq[of "y" "- ?Nt x s" "?N c"] have ?case
    2.76        by (simp add: field_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric]) }
    2.77    ultimately show ?case by blast
    2.78 -qed (auto simp add: nth_pos2 tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"] bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
    2.79 +qed (auto simp add: tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"] bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
    2.80  
    2.81  lemma one_plus_one_pos[simp]: "(1::'a::{linordered_field}) + 1 > 0"
    2.82  proof-
    2.83 @@ -2468,10 +2468,6 @@
    2.84    with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
    2.85  qed
    2.86  
    2.87 -lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
    2.88 -using Nat.gr0_conv_Suc
    2.89 -by clarsimp
    2.90 -
    2.91  lemma simpfm_lin:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    2.92    shows "qfree p \<Longrightarrow> islin (simpfm p)"
    2.93    by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)
     3.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Feb 25 08:46:52 2011 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Feb 25 14:25:41 2011 +0100
     3.3 @@ -210,11 +210,6 @@
     3.4    "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
     3.5  | "poly_deriv p = 0\<^sub>p"
     3.6  
     3.7 -  (* Verification *)
     3.8 -lemma nth_pos2[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
     3.9 -using Nat.gr0_conv_Suc
    3.10 -by clarsimp
    3.11 -
    3.12  subsection{* Semantics of the polynomial representation *}
    3.13  
    3.14  primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
     4.1 --- a/src/HOL/Hoare_Parallel/Graph.thy	Fri Feb 25 08:46:52 2011 +0100
     4.2 +++ b/src/HOL/Hoare_Parallel/Graph.thy	Fri Feb 25 14:25:41 2011 +0100
     4.3 @@ -140,11 +140,8 @@
     4.4  apply simp
     4.5  apply(subgoal_tac "(length path - Suc m) + nat \<le> length path")
     4.6   prefer 2 apply arith
     4.7 -apply(drule nth_drop)
     4.8 -apply simp
     4.9  apply(subgoal_tac "length path - Suc m + nat = length path - Suc 0")
    4.10   prefer 2 apply arith 
    4.11 -apply simp
    4.12  apply clarify
    4.13  apply(case_tac "i")
    4.14   apply(force simp add: nth_list_update)
     5.1 --- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Fri Feb 25 08:46:52 2011 +0100
     5.2 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Fri Feb 25 14:25:41 2011 +0100
     5.3 @@ -111,8 +111,6 @@
     5.4       apply simp
     5.5      apply clarify
     5.6      apply simp
     5.7 -    apply(case_tac j,simp)
     5.8 -    apply simp
     5.9     apply simp
    5.10     apply(rule conjI)
    5.11      apply clarify
     6.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Fri Feb 25 08:46:52 2011 +0100
     6.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Fri Feb 25 14:25:41 2011 +0100
     6.3 @@ -871,12 +871,8 @@
     6.4   apply(simp add:comm_def)
     6.5  apply clarify
     6.6  apply(erule_tac x="Suc(length xs + i)" in allE,simp)
     6.7 -apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift del:map.simps)
     6.8 - apply(simp add:last_length)
     6.9 - apply(erule mp)
    6.10 - apply(case_tac "last xs")
    6.11 - apply(simp add:lift_def)
    6.12 -apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
    6.13 +apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift last_conv_nth lift_def split_def)
    6.14 +apply(simp add:Cons_lift_append nth_append snd_lift)
    6.15  done
    6.16  
    6.17  lemma While_sound_aux [rule_format]: 
     7.1 --- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Fri Feb 25 08:46:52 2011 +0100
     7.2 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Fri Feb 25 14:25:41 2011 +0100
     7.3 @@ -130,8 +130,6 @@
     7.4  lemma last_length: "((a#xs)!(length xs))=last (a#xs)"
     7.5  apply simp
     7.6  apply(induct xs,simp+)
     7.7 -apply(case_tac xs)
     7.8 -apply simp_all
     7.9  done
    7.10  
    7.11  lemma div_seq [rule_format]: "list \<in> cptn_mod \<Longrightarrow>
    7.12 @@ -304,10 +302,10 @@
    7.13         apply(erule CptnEnv)
    7.14        apply(erule CptnComp,simp)
    7.15       apply(rule CptnComp)
    7.16 -     apply(erule CondT,simp)
    7.17 +      apply(erule CondT,simp)
    7.18      apply(rule CptnComp)
    7.19 -    apply(erule CondF,simp)
    7.20 ---{* Seq1 *}   
    7.21 +     apply(erule CondF,simp)
    7.22 +--{* Seq1 *}
    7.23  apply(erule cptn.cases,simp_all)
    7.24    apply(rule CptnOne)
    7.25   apply clarify
    7.26 @@ -332,37 +330,27 @@
    7.27    apply(drule_tac P=P1 in lift_is_cptn)
    7.28    apply(simp add:lift_def)
    7.29   apply simp
    7.30 -apply(case_tac "xs\<noteq>[]")
    7.31 - apply(drule_tac P=P1 in last_lift)
    7.32 -  apply(rule last_fst_esp)
    7.33 -  apply (simp add:last_length)
    7.34 - apply(simp add:Cons_lift del:map.simps)
    7.35 - apply(rule conjI, clarify, simp)
    7.36 - apply(case_tac "(((Some P0, s) # xs) ! length xs)")
    7.37 - apply clarify
    7.38 - apply (simp add:lift_def last_length)
    7.39 -apply (simp add:last_length)
    7.40 +apply(simp split: split_if_asm)
    7.41 +apply(frule_tac P=P1 in last_lift)
    7.42 + apply(rule last_fst_esp)
    7.43 + apply (simp add:last_length)
    7.44 +apply(simp add:Cons_lift lift_def split_def last_conv_nth)
    7.45  --{* While1 *}
    7.46  apply(rule CptnComp)
    7.47 -apply(rule WhileT,simp)
    7.48 + apply(rule WhileT,simp)
    7.49  apply(drule_tac P="While b P" in lift_is_cptn)
    7.50  apply(simp add:lift_def)
    7.51  --{* While2 *}
    7.52  apply(rule CptnComp)
    7.53 -apply(rule WhileT,simp)
    7.54 + apply(rule WhileT,simp)
    7.55  apply(rule cptn_append_is_cptn)
    7.56 -apply(drule_tac P="While b P" in lift_is_cptn)
    7.57 +  apply(drule_tac P="While b P" in lift_is_cptn)
    7.58    apply(simp add:lift_def)
    7.59   apply simp
    7.60 -apply(case_tac "xs\<noteq>[]")
    7.61 - apply(drule_tac P="While b P" in last_lift)
    7.62 -  apply(rule last_fst_esp,simp add:last_length)
    7.63 - apply(simp add:Cons_lift del:map.simps)
    7.64 - apply(rule conjI, clarify, simp)
    7.65 - apply(case_tac "(((Some P, s) # xs) ! length xs)")
    7.66 - apply clarify
    7.67 - apply (simp add:last_length lift_def)
    7.68 -apply simp
    7.69 +apply(simp split: split_if_asm)
    7.70 +apply(frule_tac P="While b P" in last_lift)
    7.71 + apply(rule last_fst_esp,simp add:last_length)
    7.72 +apply(simp add:Cons_lift lift_def split_def last_conv_nth)
    7.73  done
    7.74  
    7.75  theorem cptn_iff_cptn_mod: "(c \<in> cptn) = (c \<in> cptn_mod)"
     8.1 --- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Fri Feb 25 08:46:52 2011 +0100
     8.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Fri Feb 25 14:25:41 2011 +0100
     8.3 @@ -421,11 +421,6 @@
     8.4  apply (induct xs arbitrary: a i j)
     8.5  apply simp
     8.6  apply simp
     8.7 -apply (case_tac j)
     8.8 -apply simp
     8.9 -apply auto
    8.10 -apply (case_tac nat)
    8.11 -apply auto
    8.12  done
    8.13  
    8.14  (* suffices that j \<le> length xs and length ys *) 
    8.15 @@ -443,7 +438,6 @@
    8.16      apply (case_tac i', auto)
    8.17      apply (erule_tac x="Suc i'" in allE, auto)
    8.18      apply (erule_tac x="i' - 1" in allE, auto)
    8.19 -    apply (case_tac i', auto)
    8.20      apply (erule_tac x="Suc i'" in allE, auto)
    8.21      done
    8.22  qed
    8.23 @@ -459,11 +453,9 @@
    8.24  
    8.25  lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
    8.26  apply (induct xs arbitrary: i j k)
    8.27 -apply auto
    8.28 +apply simp
    8.29  apply (case_tac k)
    8.30  apply auto
    8.31 -apply (case_tac i)
    8.32 -apply auto
    8.33  done
    8.34  
    8.35  lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
     9.1 --- a/src/HOL/List.thy	Fri Feb 25 08:46:52 2011 +0100
     9.2 +++ b/src/HOL/List.thy	Fri Feb 25 14:25:41 2011 +0100
     9.3 @@ -1321,6 +1321,9 @@
     9.4  
     9.5  declare nth.simps [simp del]
     9.6  
     9.7 +lemma nth_Cons_pos[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
     9.8 +by(auto simp: Nat.gr0_conv_Suc)
     9.9 +
    9.10  lemma nth_append:
    9.11    "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
    9.12  apply (induct xs arbitrary: n, simp)
    10.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 25 08:46:52 2011 +0100
    10.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 25 14:25:41 2011 +0100
    10.3 @@ -308,12 +308,7 @@
    10.4     apply clarsimp
    10.5    apply clarsimp
    10.6    apply (case_tac w rule: bin_exhaust)
    10.7 -  apply clarsimp
    10.8 -  apply (case_tac "n - m")
    10.9 -   apply arith
   10.10    apply simp
   10.11 -  apply (rule_tac f = "%n. bl ! n" in arg_cong) 
   10.12 -  apply arith
   10.13    done
   10.14    
   10.15  lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"