# HG changeset patch # User wenzelm # Date 1436478381 -7200 # Node ID f425e80a3eb02dc1ed450f0d84da40c5b4a0aeba # Parent e96b7be56d445f203f691d59013b11934fee1ac6 tuned proofs; diff -r e96b7be56d44 -r f425e80a3eb0 src/HOL/Decision_Procs/Commutative_Ring.thy --- a/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Jul 09 22:36:31 2015 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Jul 09 23:46:21 2015 +0200 @@ -194,16 +194,18 @@ lemma add_ci: "Ipol l (P \ Q) = Ipol l P + Ipol l Q" proof (induct P Q arbitrary: l rule: add.induct) case (6 x P y Q) + consider "x < y" | "x = y" | "x > y" by arith + then show ?case - proof (rule linorder_cases) - assume "x < y" - with 6 show ?case by (simp add: mkPinj_ci algebra_simps) + proof cases + case 1 + with 6 show ?thesis by (simp add: mkPinj_ci algebra_simps) next - assume "x = y" - with 6 show ?case by (simp add: mkPinj_ci) + case 2 + with 6 show ?thesis by (simp add: mkPinj_ci) next - assume "x > y" - with 6 show ?case by (simp add: mkPinj_ci algebra_simps) + case 3 + with 6 show ?thesis by (simp add: mkPinj_ci algebra_simps) qed next case (7 x P Q y R) @@ -257,13 +259,14 @@ lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n" proof (induct n arbitrary: P rule: less_induct) case (less k) + consider "k = 0" | "k > 0" by arith + then show ?case - proof (cases "k = 0") - case True + proof cases + case 1 then show ?thesis by simp next - case False - then have "k > 0" by simp + case 2 then have "k div 2 < k" by arith with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) ^ (k div 2)" by simp diff -r e96b7be56d44 -r f425e80a3eb0 src/HOL/Decision_Procs/Commutative_Ring_Complete.thy --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Thu Jul 09 22:36:31 2015 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Thu Jul 09 23:46:21 2015 +0200 @@ -39,8 +39,7 @@ apply auto apply (cases P) apply auto - apply (rename_tac pol2, case_tac pol2) - apply auto + subgoal for \ pol2 by (cases pol2) auto done lemma norm_PX1: "isnorm (PX P i Q) \ isnorm P" @@ -48,8 +47,7 @@ apply auto apply (cases P) apply auto - apply (rename_tac pol2, case_tac pol2) - apply auto + subgoal for \ pol2 by (cases pol2) auto done lemma mkPinj_cn: "y \ 0 \ isnorm Q \ isnorm (mkPinj y Q)" @@ -161,8 +159,7 @@ apply simp apply (cases P2) apply auto - apply (rename_tac pol2, case_tac pol2) - apply auto + subgoal for \ pol2 by (cases pol2) auto done next case (5 P2 i Q2 c) @@ -173,8 +170,7 @@ apply simp apply (cases P2) apply auto - apply (rename_tac pol2, case_tac pol2) - apply auto + subgoal for \ pol2 by (cases pol2) auto done next case (6 x P2 y Q2) diff -r e96b7be56d44 -r f425e80a3eb0 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Thu Jul 09 22:36:31 2015 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Thu Jul 09 23:46:21 2015 +0200 @@ -274,11 +274,10 @@ assumes "numbound0 t" shows "numbound0 (numsubst0 t a)" using assms - apply (induct a) - apply simp_all - apply (rename_tac nat a b, case_tac nat) - apply simp_all - done +proof (induct a) + case (CN n _ _) + then show ?case by (cases n) simp_all +qed simp_all lemma subst0_bound0: assumes qf: "qfree p" @@ -457,12 +456,14 @@ lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" apply (induct t s rule: numadd.induct) apply (simp_all add: Let_def) - apply (case_tac "c1 + c2 = 0") - apply (case_tac "n1 \ n2") - apply simp_all - apply (case_tac "n1 = n2") - apply (simp_all add: algebra_simps) - apply (simp add: distrib_right[symmetric]) + subgoal for n1 c1 r1 n2 c2 r2 + apply (cases "c1 + c2 = 0") + apply (cases "n1 \ n2") + apply simp_all + apply (cases "n1 = n2") + apply (simp_all add: algebra_simps) + apply (simp add: distrib_right[symmetric]) + done done lemma numadd_nb: "numbound0 t \ numbound0 s \ numbound0 (numadd (t, s))" @@ -531,12 +532,12 @@ by (cases p) auto definition conj :: "fm \ fm \ fm" - where - "conj p q = - (if p = F \ q = F then F - else if p = T then q - else if q = T then p - else And p q)" +where + "conj p q = + (if p = F \ q = F then F + else if p = T then q + else if q = T then p + else And p q)" lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)" by (cases "p = F \ q = F", simp_all add: conj_def) (cases p, simp_all) @@ -548,12 +549,12 @@ using conj_def by auto definition disj :: "fm \ fm \ fm" - where - "disj p q = - (if p = T \ q = T then T - else if p = F then q - else if q = F then p - else Or p q)" +where + "disj p q = + (if p = T \ q = T then T + else if p = F then q + else if q = F then p + else Or p q)" lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)" by (cases "p = T \ q = T", simp_all add: disj_def) (cases p, simp_all) @@ -565,12 +566,12 @@ using disj_def by auto definition imp :: "fm \ fm \ fm" - where - "imp p q = - (if p = F \ q = T then T - else if p = T then q - else if q = F then not p - else Imp p q)" +where + "imp p q = + (if p = F \ q = T then T + else if p = T then q + else if q = F then not p + else Imp p q)" lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)" by (cases "p = F \ q = T", simp_all add: imp_def, cases p) (simp_all add: not) @@ -633,188 +634,155 @@ let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp - { - fix v - assume "?sa = C v" - then have ?case using sa - by simp - } - moreover { - assume "\ (\v. ?sa = C v)" - then have ?case - using sa by (cases ?sa) (simp_all add: Let_def) - } - ultimately show ?case by blast + consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast + then show ?case + proof cases + case 1 + with sa show ?thesis by simp + next + case 2 + with sa show ?thesis by (cases ?sa) (simp_all add: Let_def) + qed next case (7 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp - { - fix v - assume "?sa = C v" - then have ?case using sa - by simp - } - moreover { - assume "\ (\v. ?sa = C v)" - then have ?case - using sa by (cases ?sa) (simp_all add: Let_def) - } - ultimately show ?case by blast + consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast + then show ?case + proof cases + case 1 + with sa show ?thesis by simp + next + case 2 + with sa show ?thesis by (cases ?sa) (simp_all add: Let_def) + qed next case (8 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp - { - fix v - assume "?sa = C v" - then have ?case using sa - by simp - } - moreover { - assume "\ (\v. ?sa = C v)" - then have ?case - using sa by (cases ?sa) (simp_all add: Let_def) - } - ultimately show ?case by blast + consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast + then show ?case + proof cases + case 1 + with sa show ?thesis by simp + next + case 2 + with sa show ?thesis by (cases ?sa) (simp_all add: Let_def) + qed next case (9 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp - { - fix v - assume "?sa = C v" - then have ?case using sa - by simp - } - moreover { - assume "\ (\v. ?sa = C v)" - then have ?case using sa - by (cases ?sa) (simp_all add: Let_def) - } - ultimately show ?case by blast + consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast + then show ?case + proof cases + case 1 + with sa show ?thesis by simp + next + case 2 + with sa show ?thesis by (cases ?sa) (simp_all add: Let_def) + qed next case (10 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp - { - fix v - assume "?sa = C v" - then have ?case - using sa by simp - } - moreover { - assume "\ (\v. ?sa = C v)" - then have ?case - using sa by (cases ?sa) (simp_all add: Let_def) - } - ultimately show ?case by blast + consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast + then show ?case + proof cases + case 1 + with sa show ?thesis by simp + next + case 2 + with sa show ?thesis by (cases ?sa) (simp_all add: Let_def) + qed next case (11 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp - { - fix v - assume "?sa = C v" - then have ?case using sa - by simp - } - moreover { - assume "\ (\v. ?sa = C v)" - then have ?case - using sa by (cases ?sa) (simp_all add: Let_def) - } - ultimately show ?case by blast + consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast + then show ?case + proof cases + case 1 + with sa show ?thesis by simp + next + case 2 + with sa show ?thesis by (cases ?sa) (simp_all add: Let_def) + qed next case (12 i a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp - { - assume "i = 0" - then have ?case using "12.hyps" - by (simp add: dvd_def Let_def) - } - moreover - { - assume i1: "abs i = 1" - from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"] - have ?case - using i1 + consider "i = 0" | "abs i = 1" | "i \ 0" "abs i \ 1" by blast + then show ?case + proof cases + case 1 + then show ?thesis + using "12.hyps" by (simp add: dvd_def Let_def) + next + case 2 + with one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"] + show ?thesis apply (cases "i = 0") apply (simp_all add: Let_def) apply (cases "i > 0") apply simp_all done - } - moreover - { - assume inz: "i \ 0" and cond: "abs i \ 1" - { - fix v - assume "?sa = C v" - then have ?case - using sa[symmetric] inz cond + next + case i: 3 + consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast + then show ?thesis + proof cases + case 1 + with sa[symmetric] i show ?thesis by (cases "abs i = 1") auto - } - moreover - { - assume "\ (\v. ?sa = C v)" + next + case 2 then have "simpfm (Dvd i a) = Dvd i ?sa" - using inz cond by (cases ?sa) (auto simp add: Let_def) - then have ?case - using sa by simp - } - ultimately have ?case by blast - } - ultimately show ?case by blast + using i by (cases ?sa) (auto simp add: Let_def) + with sa show ?thesis by simp + qed + qed next case (13 i a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp - { - assume "i = 0" - then have ?case using "13.hyps" - by (simp add: dvd_def Let_def) - } - moreover - { - assume i1: "abs i = 1" - from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"] - have ?case - using i1 + consider "i = 0" | "abs i = 1" | "i \ 0" "abs i \ 1" by blast + then show ?case + proof cases + case 1 + then show ?thesis + using "13.hyps" by (simp add: dvd_def Let_def) + next + case 2 + with one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"] + show ?thesis apply (cases "i = 0") apply (simp_all add: Let_def) apply (cases "i > 0") apply simp_all done - } - moreover - { - assume inz: "i \ 0" and cond: "abs i \ 1" - { - fix v - assume "?sa = C v" - then have ?case - using sa[symmetric] inz cond by (cases "abs i = 1") auto - } - moreover - { - assume "\ (\v. ?sa = C v)" + next + case i: 3 + consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast + then show ?thesis + proof cases + case 1 + with sa[symmetric] i show ?thesis + by (cases "abs i = 1") auto + next + case 2 then have "simpfm (NDvd i a) = NDvd i ?sa" - using inz cond by (cases ?sa) (auto simp add: Let_def) - then have ?case using sa - by simp - } - ultimately have ?case by blast - } - ultimately show ?case by blast + using i by (cases ?sa) (auto simp add: Let_def) + with sa show ?thesis by simp + qed + qed qed (simp_all add: conj disj imp iff not) lemma simpfm_bound0: "bound0 p \ bound0 (simpfm p)" @@ -861,8 +829,10 @@ qed (auto simp add: disj_def imp_def iff_def conj_def not_bn) lemma simpfm_qf: "qfree p \ qfree (simpfm p)" - by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def) - (case_tac "simpnum a", auto)+ + apply (induct p rule: simpfm.induct) + apply (auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def) + apply (case_tac "simpnum a", auto)+ + done text \Generic quantifier elimination\ function (sequential) qelim :: "fm \ (fm \ fm) \ fm" @@ -923,17 +893,16 @@ let ?j = "fst (zsplit0 a)" let ?b = "snd (zsplit0 a)" have abj: "zsplit0 a = (?j, ?b)" by simp - { - assume "m \ 0" - with 3(1)[OF abj] 3(2) have ?case + show ?case + proof (cases "m = 0") + case False + with 3(1)[OF abj] 3(2) show ?thesis by (auto simp add: Let_def split_def) - } - moreover - { - assume m0: "m = 0" + next + case m: True with abj have th: "a' = ?b \ n = i + ?j" using 3 by (simp add: Let_def split_def) - from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \ ?N ?b" + from abj 3 m have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \ ?N ?b" by blast from th have "?I x (CN 0 n a') = ?I x (CN 0 (i + ?j) ?b)" by simp @@ -941,10 +910,9 @@ by (simp add: distrib_right) finally have "?I x (CN 0 n a') = ?I x (CN 0 i a)" using th2 by simp - with th2 th have ?case using m0 + with th2 th m show ?thesis by blast - } - ultimately show ?case by blast + qed next case (4 t n a) let ?nt = "fst (zsplit0 t)" @@ -1110,7 +1078,7 @@ lemma zlfm_I: assumes qfp: "qfree p" shows "Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p \ iszlfm (zlfm p)" - (is "?I (?l p) = ?I p \ ?L (?l p)") + (is "?I (?l p) = ?I p \ ?L (?l p)") using qfp proof (induct p rule: zlfm.induct) case (5 a) @@ -1126,8 +1094,7 @@ apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r") apply auto - apply (rename_tac nat a b, case_tac nat) - apply auto + subgoal for nat a b by (cases nat) auto done next case (6 a) @@ -1143,8 +1110,7 @@ apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r") apply auto - apply (rename_tac nat a b, case_tac nat) - apply auto + subgoal for nat a b by (cases nat) auto done next case (7 a) @@ -1160,8 +1126,7 @@ apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r") apply auto - apply (rename_tac nat a b, case_tac nat) - apply auto + subgoal for nat a b by (cases nat) auto done next case (8 a) @@ -1177,8 +1142,7 @@ apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r") apply auto - apply (rename_tac nat a b, case_tac nat) - apply auto + subgoal for nat a b by (cases nat) auto done next case (9 a) @@ -1194,8 +1158,7 @@ apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r") apply auto - apply (rename_tac nat a b, case_tac nat) - apply auto + subgoal for nat a b by (cases nat) auto done next case (10 a) @@ -1211,8 +1174,7 @@ apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r") apply auto - apply (rename_tac nat a b, case_tac nat) - apply auto + subgoal for nat a b by (cases nat) auto done next case (11 j a) @@ -1224,46 +1186,36 @@ have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\t. Inum (i#bs) t" - have "j = 0 \ (j \ 0 \ ?c = 0) \ (j \ 0 \ ?c > 0) \ (j \ 0 \ ?c < 0)" + consider "j = 0" | "j \ 0" "?c = 0" | "j \ 0" "?c > 0" | "j \ 0" "?c < 0" by arith - moreover - { - assume "j = 0" + then show ?case + proof cases + case 1 then have z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) - then have ?case using 11 \j = 0\ + with 11 \j = 0\ show ?thesis by (simp del: zlfm.simps) - } - moreover - { - assume "?c = 0" and "j \ 0" - then have ?case - using zsplit0_I[OF spl, where x="i" and bs="bs"] - apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r") - apply auto - apply (rename_tac nat a b, case_tac nat) - apply auto - done - } - moreover - { - assume cp: "?c > 0" and jnz: "j \ 0" + next + case 2 + with zsplit0_I[OF spl, where x="i" and bs="bs"] show ?thesis + apply (auto simp add: Let_def split_def algebra_simps) + apply (cases "?r") + apply auto + subgoal for nat a b by (cases nat) auto + done + next + case 3 then have l: "?L (?l (Dvd j a))" by (simp add: nb Let_def split_def) - then have ?case - using Ia cp jnz by (simp add: Let_def split_def) - } - moreover - { - assume cn: "?c < 0" and jnz: "j \ 0" + with Ia 3 show ?thesis + by (simp add: Let_def split_def) + next + case 4 then have l: "?L (?l (Dvd j a))" by (simp add: nb Let_def split_def) - then have ?case - using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"] + with Ia 4 dvd_minus_iff[of "abs j" "?c*i + ?N ?r"] show ?thesis by (simp add: Let_def split_def) - } - ultimately show ?case by blast + qed next case (12 j a) let ?c = "fst (zsplit0 a)" @@ -1274,46 +1226,36 @@ have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\t. Inum (i # bs) t" - have "j = 0 \ (j \ 0 \ ?c = 0) \ (j \ 0 \ ?c > 0) \ (j \ 0 \ ?c < 0)" + consider "j = 0" | "j \ 0" "?c = 0" | "j \ 0" "?c > 0" | "j \ 0" "?c < 0" by arith - moreover - { - assume "j = 0" + then show ?case + proof cases + case 1 then have z: "zlfm (NDvd j a) = zlfm (NEq a)" by (simp add: Let_def) - then have ?case - using assms 12 \j = 0\ by (simp del: zlfm.simps) - } - moreover - { - assume "?c = 0" and "j \ 0" - then have ?case - using zsplit0_I[OF spl, where x="i" and bs="bs"] - apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r") - apply auto - apply (rename_tac nat a b, case_tac nat) - apply auto - done - } - moreover - { - assume cp: "?c > 0" and jnz: "j \ 0" + with assms 12 \j = 0\ show ?thesis + by (simp del: zlfm.simps) + next + case 2 + with zsplit0_I[OF spl, where x="i" and bs="bs"] show ?thesis + apply (auto simp add: Let_def split_def algebra_simps) + apply (cases "?r") + apply auto + subgoal for nat a b by (cases nat) auto + done + next + case 3 then have l: "?L (?l (Dvd j a))" by (simp add: nb Let_def split_def) - then have ?case using Ia cp jnz + with Ia 3 show ?thesis by (simp add: Let_def split_def) - } - moreover - { - assume cn: "?c < 0" and jnz: "j \ 0" + next + case 4 then have l: "?L (?l (Dvd j a))" by (simp add: nb Let_def split_def) - then have ?case - using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"] + with Ia 4 dvd_minus_iff[of "abs j" "?c*i + ?N ?r"] show ?thesis by (simp add: Let_def split_def) - } - ultimately show ?case by blast + qed qed auto consts minusinf :: "fm \ fm" -- \Virtual substitution of @{text "-\"}\ @@ -1508,11 +1450,15 @@ proof (induct p rule: minusinf.induct) case (1 p q) then show ?case - by auto (rule_tac x = "min z za" in exI, simp) + apply auto + subgoal for z z' by (rule exI [where x = "min z z'"]) simp + done next case (2 p q) then show ?case - by auto (rule_tac x = "min z za" in exI, simp) + apply auto + subgoal for z z' by (rule exI [where x = "min z z'"]) simp + done next case (3 c e) then have c1: "c = 1" and nb: "numbound0 e" @@ -1955,10 +1901,8 @@ by simp also have "\ \ (\k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)" by (simp add: algebra_simps) - also - fix k - have "\ \ (\k::int. c * x + Inum (x # bs) e - j * k = 0)" - using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp + also have "\ \ (\k::int. c * x + Inum (x # bs) e - j * k = 0)" + using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k" for k] ldcp by simp also have "\ \ (\k::int. c * x + Inum (x # bs) e = j * k)" by simp @@ -1988,10 +1932,8 @@ by simp also have "\ \ (\k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)" by (simp add: algebra_simps) - also - fix k - have "\ \ (\k::int. c * x + Inum (x # bs) e - j * k = 0)" - using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp + also have "\ \ (\k::int. c * x + Inum (x # bs) e - j * k = 0)" + using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k" for k] ldcp by simp also have "\ \ (\k::int. c * x + Inum (x # bs) e = j * k)" by simp @@ -2041,21 +1983,20 @@ then have p: "Ifm bbs (x # bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e" by simp_all let ?e = "Inum (x # bs) e" - { - assume "(x - d) + ?e > 0" - then have ?case + show ?case + proof (cases "(x - d) + ?e > 0") + case True + then show ?thesis using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp - } - moreover - { - assume H: "\ (x - d) + ?e > 0" + next + case False let ?v = "Neg e" have vb: "?v \ set (\ (Gt (CN 0 c e)))" by simp from 7(5)[simplified simp_thms Inum.simps \.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] have nob: "\ (\j\ {1 ..d}. x = - ?e + j)" by auto - from H p have "x + ?e > 0 \ x + ?e \ d" + from False p have "x + ?e > 0 \ x + ?e \ d" by (simp add: c1) then have "x + ?e \ 1 \ x + ?e \ d" by simp @@ -2063,32 +2004,29 @@ by simp then have "\j::int \ {1 .. d}. x = (- ?e + j)" by (simp add: algebra_simps) - with nob have ?case + with nob show ?thesis by auto - } - ultimately show ?case - by blast + qed next case (8 c e) then have p: "Ifm bbs (x # bs) (Ge (CN 0 c e))" and c1: "c = 1" and bn: "numbound0 e" by simp_all let ?e = "Inum (x # bs) e" - { - assume "(x - d) + ?e \ 0" - then have ?case + show ?case + proof (cases "(x - d) + ?e \ 0") + case True + then show ?thesis using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp - } - moreover - { - assume H: "\ (x - d) + ?e \ 0" + next + case False let ?v = "Sub (C (- 1)) e" have vb: "?v \ set (\ (Ge (CN 0 c e)))" by simp from 8(5)[simplified simp_thms Inum.simps \.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] have nob: "\ (\j\ {1 ..d}. x = - ?e - 1 + j)" by auto - from H p have "x + ?e \ 0 \ x + ?e < d" + from False p have "x + ?e \ 0 \ x + ?e < d" by (simp add: c1) then have "x + ?e +1 \ 1 \ x + ?e + 1 \ d" by simp @@ -2096,11 +2034,9 @@ by simp then have "\j::int \ {1 .. d}. x= - ?e - 1 + j" by (simp add: algebra_simps) - with nob have ?case + with nob show ?thesis by simp - } - ultimately show ?case - by blast + qed next case (3 c e) then @@ -2115,9 +2051,10 @@ from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case - using dp - by simp (erule ballE[where x="1"], - simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"]) + using dp apply simp + apply (erule ballE[where x="1"]) + apply (simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"]) + done next case (4 c e) then @@ -2129,22 +2066,19 @@ let ?v="Neg e" have vb: "?v \ set (\ (NEq (CN 0 c e)))" by simp - { - assume "x - d + Inum (((x -d)) # bs) e \ 0" - then have ?case by (simp add: c1) - } - moreover - { - assume H: "x - d + Inum ((x - d) # bs) e = 0" + show ?case + proof (cases "x - d + Inum ((x - d) # bs) e = 0") + case False + then show ?thesis by (simp add: c1) + next + case True then have "x = - Inum ((x - d) # bs) e + d" by simp then have "x = - Inum (a # bs) e + d" by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"]) - with 4(5) have ?case + with 4(5) show ?thesis using dp by simp - } - ultimately show ?case - by blast + qed next case (9 j c e) then @@ -2185,18 +2119,17 @@ lemma \': assumes lp: "iszlfm p" - and u: "d_\ p 1" - and d: "d_\ p d" - and dp: "d > 0" + and u: "d_\ p 1" + and d: "d_\ p d" + and dp: "d > 0" shows "\x. \ (\j::int \ {1 .. d}. \b \ set(\ p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \ Ifm bbs (x # bs) p \ Ifm bbs ((x - d) # bs) p" (is "\x. ?b \ ?P x \ ?P (x - d)") proof clarify fix x - assume nb: "?b" - and px: "?P x" + assume nb: "?b" and px: "?P x" then have nb2: "\ (\j::int \ {1 .. d}. \b \ Inum (a # bs) ` set (\ p). x = b + j)" by auto - from \[OF lp u d dp nb2 px] show "?P (x -d )" . + show "?P (x - d)" by (rule \[OF lp u d dp nb2 px]) qed lemma cpmi_eq: @@ -2295,16 +2228,12 @@ lemma unit: assumes qf: "qfree p" - shows "\q B d. unit p = (q, B, d) \ - ((\x. Ifm bbs (x # bs) p) \ (\x. Ifm bbs (x # bs) q)) \ + fixes q B d + assumes qBd: "unit p = (q, B, d)" + shows "((\x. Ifm bbs (x # bs) p) \ (\x. Ifm bbs (x # bs) q)) \ (Inum (i # bs)) ` set B = (Inum (i # bs)) ` set (\ q) \ d_\ q 1 \ d_\ q d \ d > 0 \ iszlfm q \ (\b\ set B. numbound0 b)" proof - - fix q B d - assume qBd: "unit p = (q,B,d)" - let ?thes = "((\x. Ifm bbs (x#bs) p) \ (\x. Ifm bbs (x#bs) q)) \ - Inum (i#bs) ` set B = Inum (i#bs) ` set (\ q) \ - d_\ q 1 \ d_\ q d \ 0 < d \ iszlfm q \ (\b\ set B. numbound0 b)" let ?I = "\x p. Ifm bbs (x#bs) p" let ?p' = "zlfm p" let ?l = "\ ?p'" @@ -2338,19 +2267,18 @@ by (simp add: simpnum_numbound0) from \_l[OF lq] have A_nb: "\b\ set ?A'. numbound0 b" by (simp add: simpnum_numbound0) - { - assume "length ?B' \ length ?A'" + show ?thesis + proof (cases "length ?B' \ length ?A'") + case True then have q: "q = ?q" and "B = ?B'" and d: "d = ?d" using qBd by (auto simp add: Let_def unit_def) with BB' B_nb have b: "?N ` (set B) = ?N ` set (\ q)" and bn: "\b\ set B. numbound0 b" by simp_all - with pq_ex dp uq dd lq q d have ?thes + with pq_ex dp uq dd lq q d show ?thesis by simp - } - moreover - { - assume "\ (length ?B' \ length ?A')" + next + case False then have q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d" using qBd by (auto simp add: Let_def unit_def) with AA' mirror_\_\[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\ q)" @@ -2363,10 +2291,9 @@ by auto from \[OF lq'] mirror_\[OF lq] q d have dq: "d_\ q d" by auto - from pqm_eq b bn uq lq' dp dq q dp d have ?thes + from pqm_eq b bn uq lq' dp dq q dp d show ?thesis by simp - } - ultimately show ?thes by blast + qed qed @@ -2389,8 +2316,8 @@ lemma cooper: assumes qf: "qfree p" - shows "((\x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \ qfree (cooper p)" - (is "(?lhs = ?rhs) \ _") + shows "(\x. Ifm bbs (x#bs) p) = Ifm bbs bs (cooper p) \ qfree (cooper p)" + (is "?lhs = ?rhs \ _") proof - let ?I = "\x p. Ifm bbs (x#bs) p" let ?q = "fst (unit p)" @@ -2466,26 +2393,24 @@ also have "\ \ Ifm bbs bs (decr (disj ?md ?qd))" by (simp only: decr [OF mdqdb]) finally have mdqd2: "?lhs \ Ifm bbs bs (decr (disj ?md ?qd))" . - { - assume mdT: "?md = T" + show ?thesis + proof (cases "?md = T") + case True then have cT: "cooper p = T" by (simp only: cooper_def unit_def split_def Let_def if_True) simp - from mdT have lhs: "?lhs" + from True have lhs: "?lhs" using mdqd by simp - from mdT have "?rhs" + from True have "?rhs" by (simp add: cooper_def unit_def split_def) - with lhs cT have ?thesis + with lhs cT show ?thesis by simp - } - moreover - { - assume mdT: "?md \ T" + next + case False then have "cooper p = decr (disj ?md ?qd)" by (simp only: cooper_def unit_def split_def Let_def if_False) - with mdqd2 decr_qf[OF mdqdb] have ?thesis + with mdqd2 decr_qf[OF mdqdb] show ?thesis by simp - } - ultimately show ?thesis by blast + qed qed definition pa :: "fm \ fm" diff -r e96b7be56d44 -r f425e80a3eb0 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Jul 09 22:36:31 2015 +0200 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Jul 09 23:46:21 2015 +0200 @@ -256,26 +256,36 @@ have xb: "x \ ?b" using xMne fxM by auto have "?a \ ?Mx" - using Max_in[OF fMx Mxne] by simp then have ainS: "?a \ S" using MxS by blast + using Max_in[OF fMx Mxne] by simp + then have ainS: "?a \ S" + using MxS by blast have "?b \ ?xM" - using Min_in[OF fxM xMne] by simp then have binS: "?b \ S" using xMS by blast + using Min_in[OF fxM xMne] by simp + then have binS: "?b \ S" + using xMS by blast have noy: "\y. ?a < y \ y < ?b \ y \ S" proof clarsimp fix y assume ay: "?a < y" and yb: "y < ?b" and yS: "y \ S" - from yS have "y \ ?Mx \ y \ ?xM" by (auto simp add: linear) + from yS have "y \ ?Mx \ y \ ?xM" + by (auto simp add: linear) then show False proof assume "y \ ?Mx" - then have "y \ ?a" using Mxne fMx by auto - with ay show ?thesis by (simp add: not_le[symmetric]) + then have "y \ ?a" + using Mxne fMx by auto + with ay show ?thesis + by (simp add: not_le[symmetric]) next assume "y \ ?xM" - then have "?b \ y" using xMne fxM by auto - with yb show ?thesis by (simp add: not_le[symmetric]) + then have "?b \ y" + using xMne fxM by auto + with yb show ?thesis + by (simp add: not_le[symmetric]) qed qed - from ainS binS noy ax xb px show ?thesis by blast + from ainS binS noy ax xb px show ?thesis + by blast qed lemma finite_set_intervals2[no_atp]: @@ -319,7 +329,8 @@ shows "(\x. (\y \ L. y < x) \ (\y \ U. x < y)) \ (\l \ L. \u \ U. l < u)" proof (simp only: atomize_eq, rule iffI) assume H: "\x. (\y\L. y < x) \ (\y\U. x < y)" - then obtain x where xL: "\y\L. y < x" and xU: "\y\U. x < y" by blast + then obtain x where xL: "\y\L. y < x" and xU: "\y\U. x < y" + by blast have "l < u" if l: "l \ L" and u: "u \ U" for l u proof - have "l < x" using xL l by blast @@ -331,13 +342,20 @@ assume H: "\l\L. \u\U. l < u" let ?ML = "Max L" let ?MU = "Min U" - from fL ne have th1: "?ML \ L" and th1': "\l\L. l \ ?ML" by auto - from fU neU have th2: "?MU \ U" and th2': "\u\U. ?MU \ u" by auto - from th1 th2 H have "?ML < ?MU" by auto - with dense obtain w where th3: "?ML < w" and th4: "w < ?MU" by blast - from th3 th1' have "\l \ L. l < w" by auto - moreover from th4 th2' have "\u \ U. w < u" by auto - ultimately show "\x. (\y\L. y < x) \ (\y\U. x < y)" by auto + from fL ne have th1: "?ML \ L" and th1': "\l\L. l \ ?ML" + by auto + from fU neU have th2: "?MU \ U" and th2': "\u\U. ?MU \ u" + by auto + from th1 th2 H have "?ML < ?MU" + by auto + with dense obtain w where th3: "?ML < w" and th4: "w < ?MU" + by blast + from th3 th1' have "\l \ L. l < w" + by auto + moreover from th4 th2' have "\u \ U. w < u" + by auto + ultimately show "\x. (\y\L. y < x) \ (\y\U. x < y)" + by auto qed lemma dlo_qe_noub[no_atp]: @@ -345,10 +363,14 @@ and fL: "finite L" shows "(\x. (\y \ L. y < x) \ (\y \ {}. x < y)) \ True" proof (simp add: atomize_eq) - from gt_ex[of "Max L"] obtain M where M: "Max L < M" by blast - from ne fL have "\x \ L. x \ Max L" by simp - with M have "\x\L. x < M" by (auto intro: le_less_trans) - then show "\x. \y\L. y < x" by blast + from gt_ex[of "Max L"] obtain M where M: "Max L < M" + by blast + from ne fL have "\x \ L. x \ Max L" + by simp + with M have "\x\L. x < M" + by (auto intro: le_less_trans) + then show "\x. \y\L. y < x" + by blast qed lemma dlo_qe_nolb[no_atp]: @@ -356,10 +378,14 @@ and fU: "finite U" shows "(\x. (\y \ {}. y < x) \ (\y \ U. x < y)) \ True" proof (simp add: atomize_eq) - from lt_ex[of "Min U"] obtain M where M: "M < Min U" by blast - from ne fU have "\x \ U. Min U \