# HG changeset patch # User nipkow # Date 1298640352 -3600 # Node ID 15d76ed6ea67534e15ffc16a36f00e5d1bf546b2 # Parent c27b0b37041aa8f00fc1e03d1722ccc52e9bb523# Parent d8f76db6a2070be026b73ca57def84e8a0175e91 merged diff -r c27b0b37041a -r 15d76ed6ea67 src/HOL/Decision_Procs/Ferrack.thy --- 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 "\x\set xs. \y\set xs. P x y" by blast qed -lemma nth_pos2: "0 < n \ (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 \ 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 \ 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 \ qfree (decr p)" by (induct p, simp_all) @@ -1420,7 +1416,7 @@ also have "\ = (real c *?t + ?n* (?N x e) \ 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 "\ (s,m) \ set (uset p). real m * x \ Inum (a#bs) s " (is "\ (s,m) \ ?U p. real m *x \ ?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) \ set (uset p)" and mx: "real m * x \ ?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 \ ?N a s / real m" @@ -1452,7 +1448,7 @@ proof- have "\ (s,m) \ set (uset p). real m * x \ Inum (a#bs) s " (is "\ (s,m) \ ?U p. real m *x \ ?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) \ set (uset p)" and mx: "real m * x \ ?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 \ ?N a s / real m" @@ -1563,7 +1559,7 @@ hence "y* real c + ?N x e \ 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)" diff -r c27b0b37041a -r 15d76ed6ea67 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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 \ tm \ 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 \ tm \ 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 \ 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 \ tm \ tm \ tm" where "tmsubst n t (CP c) = CP c" @@ -193,7 +193,7 @@ lemma tmsubst: assumes nb: "tmboundslt (length bs) a" and nlt: "n \ 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 \ fm \ bool" (* A Formula is independent of Bound n *) where "bound m T = True" @@ -1585,7 +1585,7 @@ proof- have "\ (c,s) \ set (uset p). (Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s) \ (Ipoly vs c > 0 \ Ipoly vs c * x \ - 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) \ set (uset p)" and x: "(Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s) \ (Ipoly vs c > 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s)" by blast @@ -1618,7 +1618,7 @@ proof- have "\ (c,s) \ set (uset p). (Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s) \ (Ipoly vs c > 0 \ Ipoly vs c * x \ - 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) \ set (uset p)" and x: "(Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s) \ (Ipoly vs c > 0 \ Ipoly vs c * x \ - 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 "\x\set xs. \y\set xs. P x y" by blast qed -lemma nth_pos2: "0 < n \ (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 \ islin (simpfm p)" by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin) diff -r c27b0b37041a -r 15d76ed6ea67 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- 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 \ (x#xs) ! n = xs ! (n - 1)" -using Nat.gr0_conv_Suc -by clarsimp - subsection{* Semantics of the polynomial representation *} primrec Ipoly :: "'a list \ poly \ 'a::{field_char_0, field_inverse_zero, power}" where diff -r c27b0b37041a -r 15d76ed6ea67 src/HOL/Hoare_Parallel/Graph.thy --- 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 \ 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) diff -r c27b0b37041a -r 15d76ed6ea67 src/HOL/Hoare_Parallel/RG_Examples.thy --- 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 diff -r c27b0b37041a -r 15d76ed6ea67 src/HOL/Hoare_Parallel/RG_Hoare.thy --- 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]: diff -r c27b0b37041a -r 15d76ed6ea67 src/HOL/Hoare_Parallel/RG_Tran.thy --- 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 \ cptn_mod \ @@ -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\[]") - 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\[]") - 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 \ cptn) = (c \ cptn_mod)" diff -r c27b0b37041a -r 15d76ed6ea67 src/HOL/Imperative_HOL/ex/Sublist.thy --- 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 \ 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': "\ k < j - i; j \ length xs \ \ (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. \k. i \ k \ k < j \ k < List.length xs \ x = xs ! k}" diff -r c27b0b37041a -r 15d76ed6ea67 src/HOL/List.thy --- 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 \ (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) diff -r c27b0b37041a -r 15d76ed6ea67 src/HOL/Word/Bool_List_Representation.thy --- 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)"