--- a/src/HOL/Decision_Procs/Ferrack.thy Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Feb 25 14:25:52 2011 +0100
@@ -39,10 +39,6 @@
with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
qed
-lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
-using Nat.gr0_conv_Suc
-by clarsimp
-
(*********************************************************************************)
(**** SHADOW SYNTAX AND SEMANTICS ****)
@@ -240,7 +236,7 @@
assumes nb: "numbound0 a"
shows "Inum (b#bs) a = Inum (b'#bs) a"
using nb
-by (induct a) (simp_all add: nth_pos2)
+by (induct a) simp_all
primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
"bound0 T = True"
@@ -263,7 +259,7 @@
assumes bp: "bound0 p"
shows "Ifm (b#bs) p = Ifm (b'#bs) p"
using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
-by (induct p) (auto simp add: nth_pos2)
+by (induct p) auto
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
by (cases p, auto)
@@ -316,12 +312,12 @@
lemma decrnum: assumes nb: "numbound0 t"
shows "Inum (x#bs) t = Inum bs (decrnum t)"
- using nb by (induct t rule: decrnum.induct, simp_all add: nth_pos2)
+ using nb by (induct t rule: decrnum.induct, simp_all)
lemma decr: assumes nb: "bound0 p"
shows "Ifm (x#bs) p = Ifm bs (decr p)"
using nb
- by (induct p rule: decr.induct, simp_all add: nth_pos2 decrnum)
+ by (induct p rule: decr.induct, simp_all add: decrnum)
lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
by (induct p, simp_all)
@@ -1420,7 +1416,7 @@
also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
-qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2)
+qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"])
lemma uset_l:
assumes lp: "isrlfm p"
@@ -1436,7 +1432,7 @@
proof-
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")
using lp nmi ex
- by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
+ by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
then obtain s m where smU: "(s,m) \<in> set (uset p)" and mx: "real m * x \<ge> ?N a s" by blast
from uset_l[OF lp] smU have mp: "real m > 0" by auto
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"
@@ -1452,7 +1448,7 @@
proof-
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")
using lp nmi ex
- by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2)
+ by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
then obtain s m where smU: "(s,m) \<in> set (uset p)" and mx: "real m * x \<le> ?N a s" by blast
from uset_l[OF lp] smU have mp: "real m > 0" by auto
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"
@@ -1563,7 +1559,7 @@
hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps)
thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"]
by (simp add: algebra_simps)
-qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
+qed (auto simp add: numbound0_I[where bs="bs" and b="y" and b'="x"])
lemma finite_set_intervals:
assumes px: "P (x::real)"
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Feb 25 14:25:52 2011 +0100
@@ -67,7 +67,7 @@
assumes nb: "tmbound0 a"
shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
using nb
-by (induct a rule: tm.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto)
primrec tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *) where
"tmbound n (CP c) = True"
@@ -105,10 +105,10 @@
lemma decrtm0: assumes nb: "tmbound0 t"
shows "Itm vs (x#bs) t = Itm vs bs (decrtm0 t)"
- using nb by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
+ using nb by (induct t rule: decrtm0.induct, simp_all)
lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t"
- by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
+ by (induct t rule: decrtm0.induct, simp_all)
primrec decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" where
"decrtm m (CP c) = (CP c)"
@@ -175,10 +175,10 @@
| "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
lemma tmsubst0:
shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
- by (induct a rule: tm.induct) (auto simp add: nth_pos2)
+ by (induct a rule: tm.induct) auto
lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
- by (induct a rule: tm.induct) (auto simp add: nth_pos2)
+ by (induct a rule: tm.induct) auto
primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where
"tmsubst n t (CP c) = CP c"
@@ -193,7 +193,7 @@
lemma tmsubst: assumes nb: "tmboundslt (length bs) a" and nlt: "n \<le> length bs"
shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a"
using nb nlt
-by (induct a rule: tm.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto)
lemma tmsubst_nb0: assumes tnb: "tmbound0 t"
shows "tmbound0 (tmsubst 0 t a)"
@@ -534,7 +534,7 @@
assumes bp: "bound0 p"
shows "Ifm vs (b#bs) p = Ifm vs (b'#bs) p"
using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
-by (induct p rule: bound0.induct,auto simp add: nth_pos2)
+by (induct p rule: bound0.induct,auto)
primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *) where
"bound m T = True"
@@ -1585,7 +1585,7 @@
proof-
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)"
using lp nmi ex
- apply (induct p rule: minusinf.induct, auto simp add: eq le lt nth_pos2 polyneg_norm)
+ apply (induct p rule: minusinf.induct, auto simp add: eq le lt polyneg_norm)
apply (auto simp add: linorder_not_less order_le_less)
done
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
@@ -1618,7 +1618,7 @@
proof-
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)"
using lp nmi ex
- apply (induct p rule: minusinf.induct, auto simp add: eq le lt nth_pos2 polyneg_norm)
+ apply (induct p rule: minusinf.induct, auto simp add: eq le lt polyneg_norm)
apply (auto simp add: linorder_not_less order_le_less)
done
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
@@ -1798,7 +1798,7 @@
from yne c eq_divide_eq[of "y" "- ?Nt x s" "?N c"] have ?case
by (simp add: field_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric]) }
ultimately show ?case by blast
-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"])
+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"])
lemma one_plus_one_pos[simp]: "(1::'a::{linordered_field}) + 1 > 0"
proof-
@@ -2468,10 +2468,6 @@
with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
qed
-lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
-using Nat.gr0_conv_Suc
-by clarsimp
-
lemma simpfm_lin: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Fri Feb 25 14:25:52 2011 +0100
@@ -210,11 +210,6 @@
"poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
| "poly_deriv p = 0\<^sub>p"
- (* Verification *)
-lemma nth_pos2[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
-using Nat.gr0_conv_Suc
-by clarsimp
-
subsection{* Semantics of the polynomial representation *}
primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
--- a/src/HOL/Hoare_Parallel/Graph.thy Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/Hoare_Parallel/Graph.thy Fri Feb 25 14:25:52 2011 +0100
@@ -140,11 +140,8 @@
apply simp
apply(subgoal_tac "(length path - Suc m) + nat \<le> length path")
prefer 2 apply arith
-apply(drule nth_drop)
-apply simp
apply(subgoal_tac "length path - Suc m + nat = length path - Suc 0")
prefer 2 apply arith
-apply simp
apply clarify
apply(case_tac "i")
apply(force simp add: nth_list_update)
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Fri Feb 25 14:25:52 2011 +0100
@@ -111,8 +111,6 @@
apply simp
apply clarify
apply simp
- apply(case_tac j,simp)
- apply simp
apply simp
apply(rule conjI)
apply clarify
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Fri Feb 25 14:25:52 2011 +0100
@@ -871,12 +871,8 @@
apply(simp add:comm_def)
apply clarify
apply(erule_tac x="Suc(length xs + i)" in allE,simp)
-apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift del:map.simps)
- apply(simp add:last_length)
- apply(erule mp)
- apply(case_tac "last xs")
- apply(simp add:lift_def)
-apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
+apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift last_conv_nth lift_def split_def)
+apply(simp add:Cons_lift_append nth_append snd_lift)
done
lemma While_sound_aux [rule_format]:
--- a/src/HOL/Hoare_Parallel/RG_Tran.thy Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Tran.thy Fri Feb 25 14:25:52 2011 +0100
@@ -130,8 +130,6 @@
lemma last_length: "((a#xs)!(length xs))=last (a#xs)"
apply simp
apply(induct xs,simp+)
-apply(case_tac xs)
-apply simp_all
done
lemma div_seq [rule_format]: "list \<in> cptn_mod \<Longrightarrow>
@@ -304,10 +302,10 @@
apply(erule CptnEnv)
apply(erule CptnComp,simp)
apply(rule CptnComp)
- apply(erule CondT,simp)
+ apply(erule CondT,simp)
apply(rule CptnComp)
- apply(erule CondF,simp)
---{* Seq1 *}
+ apply(erule CondF,simp)
+--{* Seq1 *}
apply(erule cptn.cases,simp_all)
apply(rule CptnOne)
apply clarify
@@ -332,37 +330,27 @@
apply(drule_tac P=P1 in lift_is_cptn)
apply(simp add:lift_def)
apply simp
-apply(case_tac "xs\<noteq>[]")
- apply(drule_tac P=P1 in last_lift)
- apply(rule last_fst_esp)
- apply (simp add:last_length)
- apply(simp add:Cons_lift del:map.simps)
- apply(rule conjI, clarify, simp)
- apply(case_tac "(((Some P0, s) # xs) ! length xs)")
- apply clarify
- apply (simp add:lift_def last_length)
-apply (simp add:last_length)
+apply(simp split: split_if_asm)
+apply(frule_tac P=P1 in last_lift)
+ apply(rule last_fst_esp)
+ apply (simp add:last_length)
+apply(simp add:Cons_lift lift_def split_def last_conv_nth)
--{* While1 *}
apply(rule CptnComp)
-apply(rule WhileT,simp)
+ apply(rule WhileT,simp)
apply(drule_tac P="While b P" in lift_is_cptn)
apply(simp add:lift_def)
--{* While2 *}
apply(rule CptnComp)
-apply(rule WhileT,simp)
+ apply(rule WhileT,simp)
apply(rule cptn_append_is_cptn)
-apply(drule_tac P="While b P" in lift_is_cptn)
+ apply(drule_tac P="While b P" in lift_is_cptn)
apply(simp add:lift_def)
apply simp
-apply(case_tac "xs\<noteq>[]")
- apply(drule_tac P="While b P" in last_lift)
- apply(rule last_fst_esp,simp add:last_length)
- apply(simp add:Cons_lift del:map.simps)
- apply(rule conjI, clarify, simp)
- apply(case_tac "(((Some P, s) # xs) ! length xs)")
- apply clarify
- apply (simp add:last_length lift_def)
-apply simp
+apply(simp split: split_if_asm)
+apply(frule_tac P="While b P" in last_lift)
+ apply(rule last_fst_esp,simp add:last_length)
+apply(simp add:Cons_lift lift_def split_def last_conv_nth)
done
theorem cptn_iff_cptn_mod: "(c \<in> cptn) = (c \<in> cptn_mod)"
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Fri Feb 25 14:25:52 2011 +0100
@@ -421,11 +421,6 @@
apply (induct xs arbitrary: a i j)
apply simp
apply simp
-apply (case_tac j)
-apply simp
-apply auto
-apply (case_tac nat)
-apply auto
done
(* suffices that j \<le> length xs and length ys *)
@@ -443,7 +438,6 @@
apply (case_tac i', auto)
apply (erule_tac x="Suc i'" in allE, auto)
apply (erule_tac x="i' - 1" in allE, auto)
- apply (case_tac i', auto)
apply (erule_tac x="Suc i'" in allE, auto)
done
qed
@@ -459,11 +453,9 @@
lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
apply (induct xs arbitrary: i j k)
-apply auto
+apply simp
apply (case_tac k)
apply auto
-apply (case_tac i)
-apply auto
done
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}"
--- a/src/HOL/List.thy Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/List.thy Fri Feb 25 14:25:52 2011 +0100
@@ -1321,6 +1321,9 @@
declare nth.simps [simp del]
+lemma nth_Cons_pos[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
+by(auto simp: Nat.gr0_conv_Suc)
+
lemma nth_append:
"(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
apply (induct xs arbitrary: n, simp)
--- a/src/HOL/Word/Bool_List_Representation.thy Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Fri Feb 25 14:25:52 2011 +0100
@@ -308,12 +308,7 @@
apply clarsimp
apply clarsimp
apply (case_tac w rule: bin_exhaust)
- apply clarsimp
- apply (case_tac "n - m")
- apply arith
apply simp
- apply (rule_tac f = "%n. bl ! n" in arg_cong)
- apply arith
done
lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"