author nipkow Fri Feb 25 14:25:52 2011 +0100 (2011-02-25) changeset 41843 15d76ed6ea67 parent 41841 c27b0b37041a parent 41842 d8f76db6a207 child 41844 b933142e02d0 child 41849 1a65b780bd56
merged
```     1.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Feb 25 12:16:18 2011 +0100
1.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Feb 25 14:25:52 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.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 12:16:18 2011 +0100
2.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 25 14:25:52 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 12:16:18 2011 +0100
3.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Feb 25 14:25:52 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 12:16:18 2011 +0100
4.2 +++ b/src/HOL/Hoare_Parallel/Graph.thy	Fri Feb 25 14:25:52 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")
```
```     5.1 --- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Fri Feb 25 12:16:18 2011 +0100
5.2 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Fri Feb 25 14:25:52 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 12:16:18 2011 +0100
6.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Fri Feb 25 14:25:52 2011 +0100
6.3 @@ -871,12 +871,8 @@
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.9 - apply(erule mp)
6.10 - apply(case_tac "last xs")
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.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 12:16:18 2011 +0100
7.2 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Fri Feb 25 14:25:52 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.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.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.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.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.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.59   apply simp
7.60 -apply(case_tac "xs\<noteq>[]")
7.61 - apply(drule_tac P="While b P" in last_lift)
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.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 12:16:18 2011 +0100
8.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Fri Feb 25 14:25:52 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 12:16:18 2011 +0100
9.2 +++ b/src/HOL/List.thy	Fri Feb 25 14:25:52 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 12:16:18 2011 +0100
10.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 25 14:25:52 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)"
```