--- 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 \<oplus> 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
--- 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 \<dots> pol2 by (cases pol2) auto
done
lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
@@ -48,8 +47,7 @@
apply auto
apply (cases P)
apply auto
- apply (rename_tac pol2, case_tac pol2)
- apply auto
+ subgoal for \<dots> pol2 by (cases pol2) auto
done
lemma mkPinj_cn: "y \<noteq> 0 \<Longrightarrow> isnorm Q \<Longrightarrow> 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 \<dots> 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 \<dots> pol2 by (cases pol2) auto
done
next
case (6 x P2 y Q2)
--- 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 \<le> 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 \<le> 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 \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"
@@ -531,12 +532,12 @@
by (cases p) auto
definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
- where
- "conj p q =
- (if p = F \<or> 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 \<or> 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 \<or> q = F", simp_all add: conj_def) (cases p, simp_all)
@@ -548,12 +549,12 @@
using conj_def by auto
definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
- where
- "disj p q =
- (if p = T \<or> 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 \<or> 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 \<or> q = T", simp_all add: disj_def) (cases p, simp_all)
@@ -565,12 +566,12 @@
using disj_def by auto
definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
- where
- "imp p q =
- (if p = F \<or> 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 \<or> 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 \<or> 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 "\<not> (\<exists>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" | "\<not> (\<exists>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 "\<not> (\<exists>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" | "\<not> (\<exists>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 "\<not> (\<exists>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" | "\<not> (\<exists>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 "\<not> (\<exists>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" | "\<not> (\<exists>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 "\<not> (\<exists>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" | "\<not> (\<exists>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 "\<not> (\<exists>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" | "\<not> (\<exists>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 \<noteq> 0" "abs i \<noteq> 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 \<noteq> 0" and cond: "abs i \<noteq> 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" | "\<not> (\<exists>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 "\<not> (\<exists>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 \<noteq> 0" "abs i \<noteq> 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 \<noteq> 0" and cond: "abs i \<noteq> 1"
- {
- fix v
- assume "?sa = C v"
- then have ?case
- using sa[symmetric] inz cond by (cases "abs i = 1") auto
- }
- moreover
- {
- assume "\<not> (\<exists>v. ?sa = C v)"
+ next
+ case i: 3
+ consider v where "?sa = C v" | "\<not> (\<exists>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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<open>Generic quantifier elimination\<close>
function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> 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 \<noteq> 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 \<and> 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) \<and> ?N ?b"
+ from abj 3 m have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?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 \<and> iszlfm (zlfm p)"
- (is "?I (?l p) = ?I p \<and> ?L (?l p)")
+ (is "?I (?l p) = ?I p \<and> ?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 = "\<lambda>t. Inum (i#bs) t"
- have "j = 0 \<or> (j \<noteq> 0 \<and> ?c = 0) \<or> (j \<noteq> 0 \<and> ?c > 0) \<or> (j \<noteq> 0 \<and> ?c < 0)"
+ consider "j = 0" | "j \<noteq> 0" "?c = 0" | "j \<noteq> 0" "?c > 0" | "j \<noteq> 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 \<open>j = 0\<close>
+ with 11 \<open>j = 0\<close> show ?thesis
by (simp del: zlfm.simps)
- }
- moreover
- {
- assume "?c = 0" and "j \<noteq> 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 \<noteq> 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 \<noteq> 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 = "\<lambda>t. Inum (i # bs) t"
- have "j = 0 \<or> (j \<noteq> 0 \<and> ?c = 0) \<or> (j \<noteq> 0 \<and> ?c > 0) \<or> (j \<noteq> 0 \<and> ?c < 0)"
+ consider "j = 0" | "j \<noteq> 0" "?c = 0" | "j \<noteq> 0" "?c > 0" | "j \<noteq> 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 \<open>j = 0\<close> by (simp del: zlfm.simps)
- }
- moreover
- {
- assume "?c = 0" and "j \<noteq> 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 \<noteq> 0"
+ with assms 12 \<open>j = 0\<close> 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 \<noteq> 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 \<Rightarrow> fm" -- \<open>Virtual substitution of @{text "-\<infinity>"}\<close>
@@ -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 "\<dots> \<longleftrightarrow> (\<exists>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 "\<dots> \<longleftrightarrow> (\<exists>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 "\<dots> \<longleftrightarrow> (\<exists>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 "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
by simp
@@ -1988,10 +1932,8 @@
by simp
also have "\<dots> \<longleftrightarrow> (\<exists>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 "\<dots> \<longleftrightarrow> (\<exists>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 "\<dots> \<longleftrightarrow> (\<exists>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 "\<dots> \<longleftrightarrow> (\<exists>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: "\<not> (x - d) + ?e > 0"
+ next
+ case False
let ?v = "Neg e"
have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))"
by simp
from 7(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)"
by auto
- from H p have "x + ?e > 0 \<and> x + ?e \<le> d"
+ from False p have "x + ?e > 0 \<and> x + ?e \<le> d"
by (simp add: c1)
then have "x + ?e \<ge> 1 \<and> x + ?e \<le> d"
by simp
@@ -2063,32 +2004,29 @@
by simp
then have "\<exists>j::int \<in> {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 \<ge> 0"
- then have ?case
+ show ?case
+ proof (cases "(x - d) + ?e \<ge> 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: "\<not> (x - d) + ?e \<ge> 0"
+ next
+ case False
let ?v = "Sub (C (- 1)) e"
have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))"
by simp
from 8(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e - 1 + j)"
by auto
- from H p have "x + ?e \<ge> 0 \<and> x + ?e < d"
+ from False p have "x + ?e \<ge> 0 \<and> x + ?e < d"
by (simp add: c1)
then have "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"
by simp
@@ -2096,11 +2034,9 @@
by simp
then have "\<exists>j::int \<in> {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 \<in> set (\<beta> (NEq (CN 0 c e)))"
by simp
- {
- assume "x - d + Inum (((x -d)) # bs) e \<noteq> 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 \<beta>':
assumes lp: "iszlfm p"
- and u: "d_\<beta> p 1"
- and d: "d_\<delta> p d"
- and dp: "d > 0"
+ and u: "d_\<beta> p 1"
+ and d: "d_\<delta> p d"
+ and dp: "d > 0"
shows "\<forall>x. \<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow>
Ifm bbs (x # bs) p \<longrightarrow> Ifm bbs ((x - d) # bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
proof clarify
fix x
- assume nb: "?b"
- and px: "?P x"
+ assume nb: "?b" and px: "?P x"
then have nb2: "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
by auto
- from \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
+ show "?P (x - d)" by (rule \<beta>[OF lp u d dp nb2 px])
qed
lemma cpmi_eq:
@@ -2295,16 +2228,12 @@
lemma unit:
assumes qf: "qfree p"
- shows "\<And>q B d. unit p = (q, B, d) \<Longrightarrow>
- ((\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) q)) \<and>
+ fixes q B d
+ assumes qBd: "unit p = (q, B, d)"
+ shows "((\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) q)) \<and>
(Inum (i # bs)) ` set B = (Inum (i # bs)) ` set (\<beta> q) \<and> d_\<beta> q 1 \<and> d_\<delta> q d \<and> d > 0 \<and>
iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
proof -
- fix q B d
- assume qBd: "unit p = (q,B,d)"
- let ?thes = "((\<exists>x. Ifm bbs (x#bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) q)) \<and>
- Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and>
- d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
let ?I = "\<lambda>x p. Ifm bbs (x#bs) p"
let ?p' = "zlfm p"
let ?l = "\<zeta> ?p'"
@@ -2338,19 +2267,18 @@
by (simp add: simpnum_numbound0)
from \<alpha>_l[OF lq] have A_nb: "\<forall>b\<in> set ?A'. numbound0 b"
by (simp add: simpnum_numbound0)
- {
- assume "length ?B' \<le> length ?A'"
+ show ?thesis
+ proof (cases "length ?B' \<le> 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 (\<beta> q)" and bn: "\<forall>b\<in> 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 "\<not> (length ?B' \<le> 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_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
@@ -2363,10 +2291,9 @@
by auto
from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq: "d_\<delta> 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 "((\<exists>x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \<and> qfree (cooper p)"
- (is "(?lhs = ?rhs) \<and> _")
+ shows "(\<exists>x. Ifm bbs (x#bs) p) = Ifm bbs bs (cooper p) \<and> qfree (cooper p)"
+ (is "?lhs = ?rhs \<and> _")
proof -
let ?I = "\<lambda>x p. Ifm bbs (x#bs) p"
let ?q = "fst (unit p)"
@@ -2466,26 +2393,24 @@
also have "\<dots> \<longleftrightarrow> Ifm bbs bs (decr (disj ?md ?qd))"
by (simp only: decr [OF mdqdb])
finally have mdqd2: "?lhs \<longleftrightarrow> 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 \<noteq> 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 \<Rightarrow> fm"
--- 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 \<le> ?b"
using xMne fxM by auto
have "?a \<in> ?Mx"
- using Max_in[OF fMx Mxne] by simp then have ainS: "?a \<in> S" using MxS by blast
+ using Max_in[OF fMx Mxne] by simp
+ then have ainS: "?a \<in> S"
+ using MxS by blast
have "?b \<in> ?xM"
- using Min_in[OF fxM xMne] by simp then have binS: "?b \<in> S" using xMS by blast
+ using Min_in[OF fxM xMne] by simp
+ then have binS: "?b \<in> S"
+ using xMS by blast
have noy: "\<forall>y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
proof clarsimp
fix y
assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
- from yS have "y \<in> ?Mx \<or> y \<in> ?xM" by (auto simp add: linear)
+ from yS have "y \<in> ?Mx \<or> y \<in> ?xM"
+ by (auto simp add: linear)
then show False
proof
assume "y \<in> ?Mx"
- then have "y \<le> ?a" using Mxne fMx by auto
- with ay show ?thesis by (simp add: not_le[symmetric])
+ then have "y \<le> ?a"
+ using Mxne fMx by auto
+ with ay show ?thesis
+ by (simp add: not_le[symmetric])
next
assume "y \<in> ?xM"
- then have "?b \<le> y" using xMne fxM by auto
- with yb show ?thesis by (simp add: not_le[symmetric])
+ then have "?b \<le> 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 "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> (\<forall>l \<in> L. \<forall>u \<in> U. l < u)"
proof (simp only: atomize_eq, rule iffI)
assume H: "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)"
- then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < y" by blast
+ then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < y"
+ by blast
have "l < u" if l: "l \<in> L" and u: "u \<in> U" for l u
proof -
have "l < x" using xL l by blast
@@ -331,13 +342,20 @@
assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l < u"
let ?ML = "Max L"
let ?MU = "Min U"
- from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<le> ?ML" by auto
- from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<le> 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 "\<forall>l \<in> L. l < w" by auto
- moreover from th4 th2' have "\<forall>u \<in> U. w < u" by auto
- ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" by auto
+ from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<le> ?ML"
+ by auto
+ from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<le> 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 "\<forall>l \<in> L. l < w"
+ by auto
+ moreover from th4 th2' have "\<forall>u \<in> U. w < u"
+ by auto
+ ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)"
+ by auto
qed
lemma dlo_qe_noub[no_atp]:
@@ -345,10 +363,14 @@
and fL: "finite L"
shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> 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 "\<forall>x \<in> L. x \<le> Max L" by simp
- with M have "\<forall>x\<in>L. x < M" by (auto intro: le_less_trans)
- then show "\<exists>x. \<forall>y\<in>L. y < x" by blast
+ from gt_ex[of "Max L"] obtain M where M: "Max L < M"
+ by blast
+ from ne fL have "\<forall>x \<in> L. x \<le> Max L"
+ by simp
+ with M have "\<forall>x\<in>L. x < M"
+ by (auto intro: le_less_trans)
+ then show "\<exists>x. \<forall>y\<in>L. y < x"
+ by blast
qed
lemma dlo_qe_nolb[no_atp]:
@@ -356,10 +378,14 @@
and fU: "finite U"
shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> 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 "\<forall>x \<in> U. Min U \<le> x" by simp
- with M have "\<forall>x\<in>U. M < x" by (auto intro: less_le_trans)
- then show "\<exists>x. \<forall>y\<in>U. x < y" by blast
+ from lt_ex[of "Min U"] obtain M where M: "M < Min U"
+ by blast
+ from ne fU have "\<forall>x \<in> U. Min U \<le> x"
+ by simp
+ with M have "\<forall>x\<in>U. M < x"
+ by (auto intro: less_le_trans)
+ then show "\<exists>x. \<forall>y\<in>U. x < y"
+ by blast
qed
lemma exists_neq[no_atp]: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x"
@@ -386,14 +412,15 @@
lemmas weak_dnf_simps[no_atp] = simp_thms dnf
lemma nnf_simps[no_atp]:
- "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)"
- "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
- "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
- "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))"
- "(\<not> \<not>(P)) = P"
+ "(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)"
+ "(\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)"
+ "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
+ "(P \<longleftrightarrow> Q) \<longleftrightarrow> ((P \<and> Q) \<or> (\<not> P \<and> \<not> Q))"
+ "(\<not> \<not> P) \<longleftrightarrow> P"
by blast+
-lemma ex_distrib[no_atp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
+lemma ex_distrib[no_atp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))"
+ by blast
lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
@@ -431,14 +458,18 @@
and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
proof -
- from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
- by blast
- from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast
- from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
+ from ex1 ex2 obtain z1 and z2
+ where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+ and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+ by blast
+ from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z"
+ by blast
+ from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z"
+ by simp_all
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" if H: "z \<sqsubset> x" for x
using less_trans[OF zz1 H] less_trans[OF zz2 H] z1 zz1 z2 zz2 by auto
- then show ?thesis by blast
+ then show ?thesis
+ by blast
qed
lemma pinf_disj[no_atp]:
@@ -446,13 +477,18 @@
and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
proof-
- from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
- from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast
- from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
+ from ex1 ex2 obtain z1 and z2
+ where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+ and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+ by blast
+ from gt_ex obtain z where z: "ord.max less_eq z1 z2 \<sqsubset> z"
+ by blast
+ from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z"
+ by simp_all
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" if H: "z \<sqsubset> x" for x
using less_trans[OF zz1 H] less_trans[OF zz2 H] z1 zz1 z2 zz2 by auto
- then show ?thesis by blast
+ then show ?thesis
+ by blast
qed
lemma pinf_ex[no_atp]:
@@ -460,9 +496,12 @@
and p1: P1
shows "\<exists>x. P x"
proof -
- from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
- from gt_ex obtain x where x: "z \<sqsubset> x" by blast
- from z x p1 show ?thesis by blast
+ from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)"
+ by blast
+ from gt_ex obtain x where x: "z \<sqsubset> x"
+ by blast
+ from z x p1 show ?thesis
+ by blast
qed
end
@@ -473,7 +512,8 @@
assumes lt_ex: "\<exists>y. less y x"
begin
-lemma le_ex[no_atp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
+lemma le_ex[no_atp]: "\<exists>y. y \<sqsubseteq> x"
+ using lt_ex by auto
text \<open>Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}\<close>
@@ -482,14 +522,18 @@
and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
proof -
- from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+ from ex1 ex2 obtain z1 and z2
+ where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
by blast
- from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast
- from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
+ from lt_ex obtain z where z: "z \<sqsubset> ord.min less_eq z1 z2"
+ by blast
+ from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2"
+ by simp_all
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" if H: "x \<sqsubset> z" for x
using less_trans[OF H zz1] less_trans[OF H zz2] z1 zz1 z2 zz2 by auto
- then show ?thesis by blast
+ then show ?thesis
+ by blast
qed
lemma minf_disj[no_atp]:
@@ -497,13 +541,18 @@
and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
proof -
- from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
- from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast
- from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
+ from ex1 ex2 obtain z1 and z2
+ where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+ and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+ by blast
+ from lt_ex obtain z where z: "z \<sqsubset> ord.min less_eq z1 z2"
+ by blast
+ from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2"
+ by simp_all
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" if H: "x \<sqsubset> z" for x
using less_trans[OF H zz1] less_trans[OF H zz2] z1 zz1 z2 zz2 by auto
- then show ?thesis by blast
+ then show ?thesis
+ by blast
qed
lemma minf_ex[no_atp]:
@@ -511,9 +560,12 @@
and p1: P1
shows "\<exists>x. P x"
proof -
- from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
- from lt_ex obtain x where x: "x \<sqsubset> z" by blast
- from z x p1 show ?thesis by blast
+ from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)"
+ by blast
+ from lt_ex obtain x where x: "x \<sqsubset> z"
+ by blast
+ from z x p1 show ?thesis
+ by blast
qed
end
@@ -526,12 +578,17 @@
begin
sublocale dlo: unbounded_dense_linorder
- apply unfold_locales
- using gt_ex lt_ex between_less
- apply auto
- apply (rule_tac x="between x y" in exI)
- apply simp
- done
+proof (unfold_locales, goals)
+ case (1 x y)
+ then show ?case
+ using between_less [of x y] by auto
+next
+ case 2
+ then show ?case by (rule lt_ex)
+next
+ case 3
+ then show ?case by (rule gt_ex)
+qed
lemma rinf_U[no_atp]:
assumes fU: "finite U"