summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 11 Jul 2015 21:32:06 +0200 | |

changeset 60711 | 799044496769 |

parent 60710 | 07089a750d2a |

child 60712 | 3ba16d28449d |

tuned proofs;

--- a/src/HOL/Decision_Procs/Ferrack.thy Sat Jul 11 00:14:54 2015 +0200 +++ b/src/HOL/Decision_Procs/Ferrack.thy Sat Jul 11 21:32:06 2015 +0200 @@ -1702,490 +1702,758 @@ lemma lin_dense: assumes lp: "isrlfm p" - and noS: "\<forall>t. l < t \<and> t< u \<longrightarrow> t \<notin> (\<lambda>(t,n). Inum (x#bs) t / real n) ` set (uset p)" - (is "\<forall>t. _ \<and> _ \<longrightarrow> t \<notin> (\<lambda>(t,n). ?N x t / real n ) ` (?U p)") - and lx: "l < x" and xu:"x < u" and px:" Ifm (x#bs) p" - and ly: "l < y" and yu: "y < u" + and noS: "\<forall>t. l < t \<and> t< u \<longrightarrow> t \<notin> (\<lambda>(t,n). Inum (x#bs) t / real n) ` set (uset p)" + (is "\<forall>t. _ \<and> _ \<longrightarrow> t \<notin> (\<lambda>(t,n). ?N x t / real n ) ` (?U p)") + and lx: "l < x" + and xu:"x < u" + and px:" Ifm (x#bs) p" + and ly: "l < y" and yu: "y < u" shows "Ifm (y#bs) p" -using lp px noS + using lp px noS proof (induct p rule: isrlfm.induct) - case (5 c e) then have cp: "real c > 0" and nb: "numbound0 e" by simp+ - from 5 have "x * real c + ?N x e < 0" by (simp add: algebra_simps) + case (5 c e) + then have cp: "real c > 0" and nb: "numbound0 e" + by simp_all + from 5 have "x * real c + ?N x e < 0" + by (simp add: algebra_simps) then have pxc: "x < (- ?N x e) / real c" by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"]) - from 5 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto - then have "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto - moreover {assume y: "y < (-?N x e)/ real c" + from 5 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" + by auto + with ly yu have yne: "y \<noteq> - ?N x e / real c" + by auto + then consider "y < (-?N x e)/ real c" | "y > (- ?N x e) / real c" + by atomize_elim auto + then show ?case + proof cases + case y: 1 + then have "y * real c < - ?N x e" + by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) + then have "real c * y + ?N x e < 0" + by (simp add: algebra_simps) + then show ?thesis + using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp + next + case y: 2 + with yu have eu: "u > (- ?N x e) / real c" + by auto + with noSc ly yu have "(- ?N x e) / real c \<le> l" + by (cases "(- ?N x e) / real c > l") auto + with lx pxc have False + by auto + then show ?thesis .. + qed +next + case (6 c e) + then have cp: "real c > 0" and nb: "numbound0 e" + by simp_all + from 6 have "x * real c + ?N x e \<le> 0" + by (simp add: algebra_simps) + then have pxc: "x \<le> (- ?N x e) / real c" + by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) + from 6 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" + by auto + with ly yu have yne: "y \<noteq> - ?N x e / real c" + by auto + then consider "y < (- ?N x e) / real c" | "y > (-?N x e) / real c" + by atomize_elim auto + then show ?case + proof cases + case y: 1 then have "y * real c < - ?N x e" by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - then have "real c * y + ?N x e < 0" by (simp add: algebra_simps) - then have ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} - moreover {assume y: "y > (- ?N x e) / real c" - with yu have eu: "u > (- ?N x e) / real c" by auto - with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) - with lx pxc have "False" by auto - then have ?case by simp } - ultimately show ?case by blast + then have "real c * y + ?N x e < 0" + by (simp add: algebra_simps) + then show ?thesis + using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp + next + case y: 2 + with yu have eu: "u > (- ?N x e) / real c" + by auto + with noSc ly yu have "(- ?N x e) / real c \<le> l" + by (cases "(- ?N x e) / real c > l") auto + with lx pxc have False + by auto + then show ?thesis .. + qed next - case (6 c e) then have cp: "real c > 0" and nb: "numbound0 e" by simp + - from 6 have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps) - then have pxc: "x \<le> (- ?N x e) / real c" - by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) - from 6 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto - then have "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto - moreover {assume y: "y < (-?N x e)/ real c" - then have "y * real c < - ?N x e" - by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - then have "real c * y + ?N x e < 0" by (simp add: algebra_simps) - then have ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} - moreover {assume y: "y > (- ?N x e) / real c" - with yu have eu: "u > (- ?N x e) / real c" by auto - with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) - with lx pxc have "False" by auto - then have ?case by simp } - ultimately show ?case by blast -next - case (7 c e) then have cp: "real c > 0" and nb: "numbound0 e" by simp+ - from 7 have "x * real c + ?N x e > 0" by (simp add: algebra_simps) + case (7 c e) + then have cp: "real c > 0" and nb: "numbound0 e" + by simp_all + from 7 have "x * real c + ?N x e > 0" + by (simp add: algebra_simps) then have pxc: "x > (- ?N x e) / real c" by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"]) - from 7 have noSc: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto - then have "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto - moreover {assume y: "y > (-?N x e)/ real c" + from 7 have noSc: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" + by auto + with ly yu have yne: "y \<noteq> - ?N x e / real c" + by auto + then consider "y > (- ?N x e) / real c" | "y < (-?N x e) / real c" + by atomize_elim auto + then show ?case + proof cases + case 1 + then have "y * real c > - ?N x e" + by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) + then have "real c * y + ?N x e > 0" + by (simp add: algebra_simps) + then show ?thesis + using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp + next + case 2 + with ly have eu: "l < (- ?N x e) / real c" + by auto + with noSc ly yu have "(- ?N x e) / real c \<ge> u" + by (cases "(- ?N x e) / real c > l") auto + with xu pxc have False by auto + then show ?thesis .. + qed +next + case (8 c e) + then have cp: "real c > 0" and nb: "numbound0 e" + by simp_all + from 8 have "x * real c + ?N x e \<ge> 0" + by (simp add: algebra_simps) + then have pxc: "x \<ge> (- ?N x e) / real c" + by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) + from 8 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" + by auto + with ly yu have yne: "y \<noteq> - ?N x e / real c" + by auto + then consider "y > (- ?N x e) / real c" | "y < (-?N x e) / real c" + by atomize_elim auto + then show ?case + proof cases + case 1 then have "y * real c > - ?N x e" by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) then have "real c * y + ?N x e > 0" by (simp add: algebra_simps) - then have ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} - moreover {assume y: "y < (- ?N x e) / real c" - with ly have eu: "l < (- ?N x e) / real c" by auto - with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) - with xu pxc have "False" by auto - then have ?case by simp } - ultimately show ?case by blast + then show ?thesis + using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp + next + case 2 + with ly have eu: "l < (- ?N x e) / real c" + by auto + with noSc ly yu have "(- ?N x e) / real c \<ge> u" + by (cases "(- ?N x e) / real c > l") auto + with xu pxc have False + by auto + then show ?thesis .. + qed next - case (8 c e) then have cp: "real c > 0" and nb: "numbound0 e" by simp+ - from 8 have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps) - then have pxc: "x \<ge> (- ?N x e) / real c" - by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) - from 8 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto - then have "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto - moreover {assume y: "y > (-?N x e)/ real c" - then have "y * real c > - ?N x e" - by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - then have "real c * y + ?N x e > 0" by (simp add: algebra_simps) - then have ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} - moreover {assume y: "y < (- ?N x e) / real c" - with ly have eu: "l < (- ?N x e) / real c" by auto - with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) - with xu pxc have "False" by auto - then have ?case by simp } - ultimately show ?case by blast -next - case (3 c e) then have cp: "real c > 0" and nb: "numbound0 e" by simp+ - from cp have cnz: "real c \<noteq> 0" by simp - from 3 have "x * real c + ?N x e = 0" by (simp add: algebra_simps) + case (3 c e) + then have cp: "real c > 0" and nb: "numbound0 e" + by simp_all + from cp have cnz: "real c \<noteq> 0" + by simp + from 3 have "x * real c + ?N x e = 0" + by (simp add: algebra_simps) then have pxc: "x = (- ?N x e) / real c" by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"]) - from 3 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto - with pxc show ?case by simp + from 3 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" + by auto + with lx xu have yne: "x \<noteq> - ?N x e / real c" + by auto + with pxc show ?case + by simp next - case (4 c e) then have cp: "real c > 0" and nb: "numbound0 e" by simp+ - from cp have cnz: "real c \<noteq> 0" by simp - from 4 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto + case (4 c e) + then have cp: "real c > 0" and nb: "numbound0 e" + by simp_all + from cp have cnz: "real c \<noteq> 0" + by simp + from 4 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" + by auto + with ly yu have yne: "y \<noteq> - ?N x e / real c" + by auto then have "y* real c \<noteq> -?N x e" by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp - then have "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps) + then have "y* real c + ?N x e \<noteq> 0" + by (simp add: algebra_simps) then show ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by (simp add: algebra_simps) qed (auto simp add: numbound0_I[where bs="bs" and b="y" and b'="x"]) lemma finite_set_intervals: - assumes px: "P (x::real)" - and lx: "l \<le> x" and xu: "x \<le> u" - and linS: "l\<in> S" and uinS: "u \<in> S" - and fS:"finite S" and lS: "\<forall>x\<in> S. l \<le> x" and Su: "\<forall>x\<in> S. x \<le> u" + fixes x :: real + assumes px: "P x" + and lx: "l \<le> x" + and xu: "x \<le> u" + and linS: "l\<in> S" + and uinS: "u \<in> S" + and fS: "finite S" + and lS: "\<forall>x\<in> S. l \<le> x" + and Su: "\<forall>x\<in> S. x \<le> u" shows "\<exists>a \<in> S. \<exists>b \<in> S. (\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x" proof - let ?Mx = "{y. y\<in> S \<and> y \<le> x}" let ?xM = "{y. y\<in> S \<and> x \<le> y}" let ?a = "Max ?Mx" let ?b = "Min ?xM" - have MxS: "?Mx \<subseteq> S" by blast - then have fMx: "finite ?Mx" using fS finite_subset by auto - from lx linS have linMx: "l \<in> ?Mx" by blast - then have Mxne: "?Mx \<noteq> {}" by blast - have xMS: "?xM \<subseteq> S" by blast - then have fxM: "finite ?xM" using fS finite_subset by auto - from xu uinS have linxM: "u \<in> ?xM" by blast - then have xMne: "?xM \<noteq> {}" by blast - have ax:"?a \<le> x" using Mxne fMx by auto - 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 - have "?b \<in> ?xM" 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) + have MxS: "?Mx \<subseteq> S" + by blast + then have fMx: "finite ?Mx" + using fS finite_subset by auto + from lx linS have linMx: "l \<in> ?Mx" + by blast + then have Mxne: "?Mx \<noteq> {}" + by blast + have xMS: "?xM \<subseteq> S" + by blast + then have fxM: "finite ?xM" + using fS finite_subset by auto + from xu uinS have linxM: "u \<in> ?xM" + by blast + then have xMne: "?xM \<noteq> {}" + by blast + have ax:"?a \<le> x" + using Mxne fMx by auto + 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 + have "?b \<in> ?xM" + 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 - moreover {assume "y \<in> ?Mx" then have "y \<le> ?a" using Mxne fMx by auto with ay have "False" by simp} - moreover {assume "y \<in> ?xM" then have "y \<ge> ?b" using xMne fxM by auto with yb have "False" by simp} - ultimately show "False" by blast + from yS consider "y \<in> ?Mx" | "y \<in> ?xM" + by atomize_elim auto + then show False + proof cases + case 1 + then have "y \<le> ?a" + using Mxne fMx by auto + with ay show ?thesis by simp + next + case 2 + then have "y \<ge> ?b" + using xMne fxM by auto + with yb show ?thesis by simp + 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 rinf_uset: assumes lp: "isrlfm p" - and nmi: "\<not> (Ifm (x#bs) (minusinf p))" (is "\<not> (Ifm (x#bs) (?M p))") - and npi: "\<not> (Ifm (x#bs) (plusinf p))" (is "\<not> (Ifm (x#bs) (?P p))") - and ex: "\<exists>x. Ifm (x#bs) p" (is "\<exists>x. ?I x p") - shows "\<exists>(l,n) \<in> set (uset p). \<exists>(s,m) \<in> set (uset p). ?I ((Inum (x#bs) l / real n + Inum (x#bs) s / real m) / 2) p" + and nmi: "\<not> (Ifm (x # bs) (minusinf p))" (is "\<not> (Ifm (x # bs) (?M p))") + and npi: "\<not> (Ifm (x # bs) (plusinf p))" (is "\<not> (Ifm (x # bs) (?P p))") + and ex: "\<exists>x. Ifm (x # bs) p" (is "\<exists>x. ?I x p") + shows "\<exists>(l,n) \<in> set (uset p). \<exists>(s,m) \<in> set (uset p). + ?I ((Inum (x#bs) l / real n + Inum (x#bs) s / real m) / 2) p" proof - - let ?N = "\<lambda>x t. Inum (x#bs) t" + let ?N = "\<lambda>x t. Inum (x # bs) t" let ?U = "set (uset p)" - from ex obtain a where pa: "?I a p" by blast + from ex obtain a where pa: "?I a p" + by blast from bound0_I[OF rminusinf_bound0[OF lp], where bs="bs" and b="x" and b'="a"] nmi - have nmi': "\<not> (?I a (?M p))" by simp + have nmi': "\<not> (?I a (?M p))" + by simp from bound0_I[OF rplusinf_bound0[OF lp], where bs="bs" and b="x" and b'="a"] npi - have npi': "\<not> (?I a (?P p))" by simp + have npi': "\<not> (?I a (?P p))" + by simp have "\<exists>(l,n) \<in> set (uset p). \<exists>(s,m) \<in> set (uset p). ?I ((?N a l/real n + ?N a s /real m) / 2) p" proof - let ?M = "(\<lambda>(t,c). ?N a t / real c) ` ?U" - have fM: "finite ?M" by auto + have fM: "finite ?M" + by auto from rminusinf_uset[OF lp nmi pa] rplusinf_uset[OF lp npi pa] - have "\<exists>(l,n) \<in> set (uset p). \<exists>(s,m) \<in> set (uset p). a \<le> ?N x l / real n \<and> a \<ge> ?N x s / real m" by blast - then obtain "t" "n" "s" "m" where - tnU: "(t,n) \<in> ?U" and smU: "(s,m) \<in> ?U" - and xs1: "a \<le> ?N x s / real m" and tx1: "a \<ge> ?N x t / real n" by blast - from uset_l[OF lp] tnU smU numbound0_I[where bs="bs" and b="x" and b'="a"] xs1 tx1 have xs: "a \<le> ?N a s / real m" and tx: "a \<ge> ?N a t / real n" by auto - from tnU have Mne: "?M \<noteq> {}" by auto - then have Une: "?U \<noteq> {}" by simp + have "\<exists>(l,n) \<in> set (uset p). \<exists>(s,m) \<in> set (uset p). a \<le> ?N x l / real n \<and> a \<ge> ?N x s / real m" + by blast + then obtain "t" "n" "s" "m" + where tnU: "(t,n) \<in> ?U" + and smU: "(s,m) \<in> ?U" + and xs1: "a \<le> ?N x s / real m" + and tx1: "a \<ge> ?N x t / real n" + by blast + from uset_l[OF lp] tnU smU numbound0_I[where bs="bs" and b="x" and b'="a"] xs1 tx1 + have xs: "a \<le> ?N a s / real m" and tx: "a \<ge> ?N a t / real n" + by auto + from tnU have Mne: "?M \<noteq> {}" + by auto + then have Une: "?U \<noteq> {}" + by simp let ?l = "Min ?M" let ?u = "Max ?M" - have linM: "?l \<in> ?M" using fM Mne by simp - have uinM: "?u \<in> ?M" using fM Mne by simp - have tnM: "?N a t / real n \<in> ?M" using tnU by auto - have smM: "?N a s / real m \<in> ?M" using smU by auto - have lM: "\<forall>t\<in> ?M. ?l \<le> t" using Mne fM by auto - have Mu: "\<forall>t\<in> ?M. t \<le> ?u" using Mne fM by auto - have "?l \<le> ?N a t / real n" using tnM Mne by simp then have lx: "?l \<le> a" using tx by simp - have "?N a s / real m \<le> ?u" using smM Mne by simp then have xu: "a \<le> ?u" using xs by simp + have linM: "?l \<in> ?M" + using fM Mne by simp + have uinM: "?u \<in> ?M" + using fM Mne by simp + have tnM: "?N a t / real n \<in> ?M" + using tnU by auto + have smM: "?N a s / real m \<in> ?M" + using smU by auto + have lM: "\<forall>t\<in> ?M. ?l \<le> t" + using Mne fM by auto + have Mu: "\<forall>t\<in> ?M. t \<le> ?u" + using Mne fM by auto + have "?l \<le> ?N a t / real n" + using tnM Mne by simp + then have lx: "?l \<le> a" + using tx by simp + have "?N a s / real m \<le> ?u" + using smM Mne by simp + then have xu: "a \<le> ?u" + using xs by simp from finite_set_intervals2[where P="\<lambda>x. ?I x p",OF pa lx xu linM uinM fM lM Mu] - have "(\<exists>s\<in> ?M. ?I s p) \<or> - (\<exists>t1\<in> ?M. \<exists>t2 \<in> ?M. (\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M) \<and> t1 < a \<and> a < t2 \<and> ?I a p)" . - moreover { fix u assume um: "u\<in> ?M" and pu: "?I u p" - then have "\<exists>(tu,nu) \<in> ?U. u = ?N a tu / real nu" by auto - then obtain "tu" "nu" where tuU: "(tu,nu) \<in> ?U" and tuu:"u= ?N a tu / real nu" by blast - have "(u + u) / 2 = u" by auto with pu tuu - have "?I (((?N a tu / real nu) + (?N a tu / real nu)) / 2) p" by simp - with tuU have ?thesis by blast} - moreover{ - assume "\<exists>t1\<in> ?M. \<exists>t2 \<in> ?M. (\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M) \<and> t1 < a \<and> a < t2 \<and> ?I a p" - then obtain t1 and t2 where t1M: "t1 \<in> ?M" and t2M: "t2\<in> ?M" - and noM: "\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M" and t1x: "t1 < a" and xt2: "a < t2" and px: "?I a p" + consider u where "u \<in> ?M" "?I u p" + | t1 t2 where "t1 \<in> ?M" "t2 \<in> ?M" "\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M" "t1 < a" "a < t2" "?I a p" + by blast + then show ?thesis + proof cases + case 1 + note um = \<open>u \<in> ?M\<close> and pu = \<open>?I u p\<close> + then have "\<exists>(tu,nu) \<in> ?U. u = ?N a tu / real nu" + by auto + then obtain tu nu where tuU: "(tu, nu) \<in> ?U" and tuu: "u= ?N a tu / real nu" by blast - from t1M have "\<exists>(t1u,t1n) \<in> ?U. t1 = ?N a t1u / real t1n" by auto - then obtain "t1u" "t1n" where t1uU: "(t1u,t1n) \<in> ?U" and t1u: "t1 = ?N a t1u / real t1n" by blast - from t2M have "\<exists>(t2u,t2n) \<in> ?U. t2 = ?N a t2u / real t2n" by auto - then obtain "t2u" "t2n" where t2uU: "(t2u,t2n) \<in> ?U" and t2u: "t2 = ?N a t2u / real t2n" by blast - from t1x xt2 have t1t2: "t1 < t2" by simp + have "(u + u) / 2 = u" + by auto + with pu tuu have "?I (((?N a tu / real nu) + (?N a tu / real nu)) / 2) p" + by simp + with tuU show ?thesis by blast + next + case 2 + note t1M = \<open>t1 \<in> ?M\<close> and t2M = \<open>t2\<in> ?M\<close> + and noM = \<open>\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M\<close> + and t1x = \<open>t1 < a\<close> and xt2 = \<open>a < t2\<close> and px = \<open>?I a p\<close> + from t1M have "\<exists>(t1u,t1n) \<in> ?U. t1 = ?N a t1u / real t1n" + by auto + then obtain t1u t1n where t1uU: "(t1u, t1n) \<in> ?U" and t1u: "t1 = ?N a t1u / real t1n" + by blast + from t2M have "\<exists>(t2u,t2n) \<in> ?U. t2 = ?N a t2u / real t2n" + by auto + then obtain t2u t2n where t2uU: "(t2u, t2n) \<in> ?U" and t2u: "t2 = ?N a t2u / real t2n" + by blast + from t1x xt2 have t1t2: "t1 < t2" + by simp let ?u = "(t1 + t2) / 2" - from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2" by auto + from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2" + by auto from lin_dense[OF lp noM t1x xt2 px t1lu ut2] have "?I ?u p" . - with t1uU t2uU t1u t2u have ?thesis by blast} - ultimately show ?thesis by blast + with t1uU t2uU t1u t2u show ?thesis + by blast + qed qed - then obtain "l" "n" "s" "m" where lnU: "(l,n) \<in> ?U" and smU:"(s,m) \<in> ?U" - and pu: "?I ((?N a l / real n + ?N a s / real m) / 2) p" by blast - from lnU smU uset_l[OF lp] have nbl: "numbound0 l" and nbs: "numbound0 s" by auto + then obtain l n s m where lnU: "(l, n) \<in> ?U" and smU:"(s, m) \<in> ?U" + and pu: "?I ((?N a l / real n + ?N a s / real m) / 2) p" + by blast + from lnU smU uset_l[OF lp] have nbl: "numbound0 l" and nbs: "numbound0 s" + by auto from numbound0_I[OF nbl, where bs="bs" and b="a" and b'="x"] numbound0_I[OF nbs, where bs="bs" and b="a" and b'="x"] pu - have "?I ((?N x l / real n + ?N x s / real m) / 2) p" by simp - with lnU smU - show ?thesis by auto + have "?I ((?N x l / real n + ?N x s / real m) / 2) p" + by simp + with lnU smU show ?thesis + by auto qed + + (* The Ferrante - Rackoff Theorem *) theorem fr_eq: assumes lp: "isrlfm p" - shows "(\<exists>x. Ifm (x#bs) p) = ((Ifm (x#bs) (minusinf p)) \<or> (Ifm (x#bs) (plusinf p)) \<or> (\<exists>(t,n) \<in> set (uset p). \<exists>(s,m) \<in> set (uset p). Ifm ((((Inum (x#bs) t)/ real n + (Inum (x#bs) s) / real m) /2)#bs) p))" - (is "(\<exists>x. ?I x p) = (?M \<or> ?P \<or> ?F)" is "?E = ?D") + shows "(\<exists>x. Ifm (x#bs) p) \<longleftrightarrow> + Ifm (x # bs) (minusinf p) \<or> Ifm (x # bs) (plusinf p) \<or> + (\<exists>(t,n) \<in> set (uset p). \<exists>(s,m) \<in> set (uset p). + Ifm ((((Inum (x # bs) t) / real n + (Inum (x # bs) s) / real m) / 2) # bs) p)" + (is "(\<exists>x. ?I x p) \<longleftrightarrow> (?M \<or> ?P \<or> ?F)" is "?E = ?D") proof assume px: "\<exists>x. ?I x p" - have "?M \<or> ?P \<or> (\<not> ?M \<and> \<not> ?P)" by blast - moreover {assume "?M \<or> ?P" then have "?D" by blast} - moreover {assume nmi: "\<not> ?M" and npi: "\<not> ?P" - from rinf_uset[OF lp nmi npi] have "?F" using px by blast then have "?D" by blast} - ultimately show "?D" by blast + consider "?M \<or> ?P" | "\<not> ?M" "\<not> ?P" by blast + then show ?D + proof cases + case 1 + then show ?thesis by blast + next + case 2 + from rinf_uset[OF lp this] have ?F + using px by blast + then show ?thesis by blast + qed next - assume "?D" - moreover {assume m:"?M" from rminusinf_ex[OF lp m] have "?E" .} - moreover {assume p: "?P" from rplusinf_ex[OF lp p] have "?E" . } - moreover {assume f:"?F" then have "?E" by blast} - ultimately show "?E" by blast + assume ?D + then consider ?M | ?P | ?F by blast + then show ?E + proof cases + case 1 + from rminusinf_ex[OF lp this] show ?thesis . + next + case 2 + from rplusinf_ex[OF lp this] show ?thesis . + next + case 3 + then show ?thesis by blast + qed qed lemma fr_equsubst: assumes lp: "isrlfm p" - shows "(\<exists>x. Ifm (x#bs) p) = ((Ifm (x#bs) (minusinf p)) \<or> (Ifm (x#bs) (plusinf p)) \<or> (\<exists>(t,k) \<in> set (uset p). \<exists>(s,l) \<in> set (uset p). Ifm (x#bs) (usubst p (Add(Mul l t) (Mul k s) , 2*k*l))))" - (is "(\<exists>x. ?I x p) = (?M \<or> ?P \<or> ?F)" is "?E = ?D") + shows "(\<exists>x. Ifm (x # bs) p) \<longleftrightarrow> + (Ifm (x # bs) (minusinf p) \<or> Ifm (x # bs) (plusinf p) \<or> + (\<exists>(t,k) \<in> set (uset p). \<exists>(s,l) \<in> set (uset p). + Ifm (x#bs) (usubst p (Add (Mul l t) (Mul k s), 2 * k * l))))" + (is "(\<exists>x. ?I x p) \<longleftrightarrow> ?M \<or> ?P \<or> ?F" is "?E = ?D") proof assume px: "\<exists>x. ?I x p" - have "?M \<or> ?P \<or> (\<not> ?M \<and> \<not> ?P)" by blast - moreover {assume "?M \<or> ?P" then have "?D" by blast} - moreover {assume nmi: "\<not> ?M" and npi: "\<not> ?P" - let ?f ="\<lambda>(t,n). Inum (x#bs) t / real n" - let ?N = "\<lambda>t. Inum (x#bs) t" - {fix t n s m assume "(t,n)\<in> set (uset p)" and "(s,m) \<in> set (uset p)" - with uset_l[OF lp] have tnb: "numbound0 t" and np:"real n > 0" and snb: "numbound0 s" and mp:"real m > 0" + consider "?M \<or> ?P" | "\<not> ?M" "\<not> ?P" by blast + then show ?D + proof cases + case 1 + then show ?thesis by blast + next + case 2 + let ?f = "\<lambda>(t,n). Inum (x # bs) t / real n" + let ?N = "\<lambda>t. Inum (x # bs) t" + { + fix t n s m + assume "(t, n) \<in> set (uset p)" and "(s, m) \<in> set (uset p)" + with uset_l[OF lp] have tnb: "numbound0 t" + and np: "real n > 0" and snb: "numbound0 s" and mp: "real m > 0" by auto let ?st = "Add (Mul m t) (Mul n s)" - from np mp have mnp: "real (2*n*m) > 0" by (simp add: mult.commute) - from tnb snb have st_nb: "numbound0 ?st" by simp - have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" + from np mp have mnp: "real (2 * n * m) > 0" + by (simp add: mult.commute) + from tnb snb have st_nb: "numbound0 ?st" + by simp + have st: "(?N t / real n + ?N s / real m) / 2 = ?N ?st / real (2 * n * m)" using mnp mp np by (simp add: algebra_simps add_divide_distrib) from usubst_I[OF lp mnp st_nb, where x="x" and bs="bs"] - have "?I x (usubst p (?st,2*n*m)) = ?I ((?N t / real n + ?N s / real m) /2) p" by (simp only: st[symmetric])} - with rinf_uset[OF lp nmi npi px] have "?F" by blast then have "?D" by blast} - ultimately show "?D" by blast + have "?I x (usubst p (?st, 2 * n * m)) = ?I ((?N t / real n + ?N s / real m) / 2) p" + by (simp only: st[symmetric]) + } + with rinf_uset[OF lp 2 px] have ?F + by blast + then show ?thesis + by blast + qed next - assume "?D" - moreover {assume m:"?M" from rminusinf_ex[OF lp m] have "?E" .} - moreover {assume p: "?P" from rplusinf_ex[OF lp p] have "?E" . } - moreover {fix t k s l assume "(t,k) \<in> set (uset p)" and "(s,l) \<in> set (uset p)" - and px:"?I x (usubst p (Add (Mul l t) (Mul k s), 2*k*l))" - with uset_l[OF lp] have tnb: "numbound0 t" and np:"real k > 0" and snb: "numbound0 s" and mp:"real l > 0" by auto + assume ?D + then consider ?M | ?P | t k s l where "(t, k) \<in> set (uset p)" "(s, l) \<in> set (uset p)" + "?I x (usubst p (Add (Mul l t) (Mul k s), 2 * k * l))" + by blast + then show ?E + proof cases + case 1 + from rminusinf_ex[OF lp this] show ?thesis . + next + case 2 + from rplusinf_ex[OF lp this] show ?thesis . + next + case 3 + with uset_l[OF lp] have tnb: "numbound0 t" and np: "real k > 0" + and snb: "numbound0 s" and mp: "real l > 0" + by auto let ?st = "Add (Mul l t) (Mul k s)" - from np mp have mnp: "real (2*k*l) > 0" by (simp add: mult.commute) - from tnb snb have st_nb: "numbound0 ?st" by simp - from usubst_I[OF lp mnp st_nb, where bs="bs"] px have "?E" by auto} - ultimately show "?E" by blast + from np mp have mnp: "real (2 * k * l) > 0" + by (simp add: mult.commute) + from tnb snb have st_nb: "numbound0 ?st" + by simp + from usubst_I[OF lp mnp st_nb, where bs="bs"] + \<open>?I x (usubst p (Add (Mul l t) (Mul k s), 2 * k * l))\<close> show ?thesis + by auto + qed qed (* Implement the right hand side of Ferrante and Rackoff's Theorem. *) -definition ferrack :: "fm \<Rightarrow> fm" where - "ferrack p = (let p' = rlfm (simpfm p); mp = minusinf p'; pp = plusinf p' - in if (mp = T \<or> pp = T) then T else - (let U = remdups(map simp_num_pair - (map (\<lambda>((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2*n*m)) - (alluopairs (uset p')))) - in decr (disj mp (disj pp (evaldjf (simpfm \<circ> (usubst p')) U)))))" +definition ferrack :: "fm \<Rightarrow> fm" +where + "ferrack p = + (let + p' = rlfm (simpfm p); + mp = minusinf p'; + pp = plusinf p' + in + if mp = T \<or> pp = T then T + else + (let U = remdups (map simp_num_pair + (map (\<lambda>((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2 * n * m)) + (alluopairs (uset p')))) + in decr (disj mp (disj pp (evaldjf (simpfm \<circ> usubst p') U)))))" lemma uset_cong_aux: - assumes Ul: "\<forall>(t,n) \<in> set U. numbound0 t \<and> n >0" - shows "((\<lambda>(t,n). Inum (x#bs) t /real n) ` (set (map (\<lambda>((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2*n*m)) (alluopairs U)))) = ((\<lambda>((t,n),(s,m)). (Inum (x#bs) t /real n + Inum (x#bs) s /real m)/2) ` (set U \<times> set U))" + assumes Ul: "\<forall>(t,n) \<in> set U. numbound0 t \<and> n > 0" + shows "((\<lambda>(t,n). Inum (x # bs) t / real n) ` + (set (map (\<lambda>((t,n),(s,m)). (Add (Mul m t) (Mul n s), 2 * n * m)) (alluopairs U)))) = + ((\<lambda>((t,n),(s,m)). (Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) ` (set U \<times> set U))" (is "?lhs = ?rhs") -proof(auto) +proof auto fix t n s m - assume "((t,n),(s,m)) \<in> set (alluopairs U)" - then have th: "((t,n),(s,m)) \<in> (set U \<times> set U)" + assume "((t, n), (s, m)) \<in> set (alluopairs U)" + then have th: "((t, n), (s, m)) \<in> set U \<times> set U" using alluopairs_set1[where xs="U"] by blast - let ?N = "\<lambda>t. Inum (x#bs) t" - let ?st= "Add (Mul m t) (Mul n s)" - from Ul th have mnz: "m \<noteq> 0" by auto - from Ul th have nnz: "n \<noteq> 0" by auto - have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mnz nnz by (simp add: algebra_simps add_divide_distrib) - - then show "(real m * Inum (x # bs) t + real n * Inum (x # bs) s) / - (2 * real n * real m) - \<in> (\<lambda>((t, n), s, m). - (Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) ` - (set U \<times> set U)"using mnz nnz th + let ?N = "\<lambda>t. Inum (x # bs) t" + let ?st = "Add (Mul m t) (Mul n s)" + from Ul th have mnz: "m \<noteq> 0" + by auto + from Ul th have nnz: "n \<noteq> 0" + by auto + have st: "(?N t / real n + ?N s / real m) / 2 = ?N ?st / real (2 * n * m)" + using mnz nnz by (simp add: algebra_simps add_divide_distrib) + then show "(real m * Inum (x # bs) t + real n * Inum (x # bs) s) / (2 * real n * real m) + \<in> (\<lambda>((t, n), s, m). (Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) ` + (set U \<times> set U)" + using mnz nnz th apply (auto simp add: th add_divide_distrib algebra_simps split_def image_def) - by (rule_tac x="(s,m)" in bexI,simp_all) - (rule_tac x="(t,n)" in bexI,simp_all add: mult.commute) + apply (rule_tac x="(s,m)" in bexI) + apply simp_all + apply (rule_tac x="(t,n)" in bexI) + apply (simp_all add: mult.commute) + done next fix t n s m - assume tnU: "(t,n) \<in> set U" and smU:"(s,m) \<in> set U" - let ?N = "\<lambda>t. Inum (x#bs) t" - let ?st= "Add (Mul m t) (Mul n s)" - from Ul smU have mnz: "m \<noteq> 0" by auto - from Ul tnU have nnz: "n \<noteq> 0" by auto - have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mnz nnz by (simp add: algebra_simps add_divide_distrib) - let ?P = "\<lambda>(t',n') (s',m'). (Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2" - have Pc:"\<forall>a b. ?P a b = ?P b a" - by auto - from Ul alluopairs_set1 have Up:"\<forall>((t,n),(s,m)) \<in> set (alluopairs U). n \<noteq> 0 \<and> m \<noteq> 0" by blast - from alluopairs_ex[OF Pc, where xs="U"] tnU smU - have th':"\<exists>((t',n'),(s',m')) \<in> set (alluopairs U). ?P (t',n') (s',m')" - by blast - then obtain t' n' s' m' where ts'_U: "((t',n'),(s',m')) \<in> set (alluopairs U)" - and Pts': "?P (t',n') (s',m')" by blast - from ts'_U Up have mnz': "m' \<noteq> 0" and nnz': "n'\<noteq> 0" by auto - let ?st' = "Add (Mul m' t') (Mul n' s')" - have st': "(?N t' / real n' + ?N s' / real m')/2 = ?N ?st' / real (2*n'*m')" - using mnz' nnz' by (simp add: algebra_simps add_divide_distrib) - from Pts' have - "(Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2" by simp - also have "\<dots> = ((\<lambda>(t, n). Inum (x # bs) t / real n) ((\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t',n'),(s',m'))))" by (simp add: st') - finally show "(Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2 - \<in> (\<lambda>(t, n). Inum (x # bs) t / real n) ` - (\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ` - set (alluopairs U)" - using ts'_U by blast + assume tnU: "(t, n) \<in> set U" and smU: "(s, m) \<in> set U" + let ?N = "\<lambda>t. Inum (x # bs) t" + let ?st = "Add (Mul m t) (Mul n s)" + from Ul smU have mnz: "m \<noteq> 0" + by auto + from Ul tnU have nnz: "n \<noteq> 0" + by auto + have st: "(?N t / real n + ?N s / real m) / 2 = ?N ?st / real (2 * n * m)" + using mnz nnz by (simp add: algebra_simps add_divide_distrib) + let ?P = "\<lambda>(t',n') (s',m'). (Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = + (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m') / 2" + have Pc:"\<forall>a b. ?P a b = ?P b a" + by auto + from Ul alluopairs_set1 have Up:"\<forall>((t,n),(s,m)) \<in> set (alluopairs U). n \<noteq> 0 \<and> m \<noteq> 0" + by blast + from alluopairs_ex[OF Pc, where xs="U"] tnU smU + have th':"\<exists>((t',n'),(s',m')) \<in> set (alluopairs U). ?P (t',n') (s',m')" + by blast + then obtain t' n' s' m' where ts'_U: "((t',n'),(s',m')) \<in> set (alluopairs U)" + and Pts': "?P (t', n') (s', m')" + by blast + from ts'_U Up have mnz': "m' \<noteq> 0" and nnz': "n'\<noteq> 0" + by auto + let ?st' = "Add (Mul m' t') (Mul n' s')" + have st': "(?N t' / real n' + ?N s' / real m') / 2 = ?N ?st' / real (2 * n' * m')" + using mnz' nnz' by (simp add: algebra_simps add_divide_distrib) + from Pts' have "(Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2 = + (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m') / 2" + by simp + also have "\<dots> = (\<lambda>(t, n). Inum (x # bs) t / real n) + ((\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t', n'), (s', m')))" + by (simp add: st') + finally show "(Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2 + \<in> (\<lambda>(t, n). Inum (x # bs) t / real n) ` + (\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ` set (alluopairs U)" + using ts'_U by blast qed lemma uset_cong: assumes lp: "isrlfm p" - and UU': "((\<lambda>(t,n). Inum (x#bs) t /real n) ` U') = ((\<lambda>((t,n),(s,m)). (Inum (x#bs) t /real n + Inum (x#bs) s /real m)/2) ` (U \<times> U))" (is "?f ` U' = ?g ` (U\<times>U)") - and U: "\<forall>(t,n) \<in> U. numbound0 t \<and> n > 0" - and U': "\<forall>(t,n) \<in> U'. numbound0 t \<and> n > 0" - shows "(\<exists>(t,n) \<in> U. \<exists>(s,m) \<in> U. Ifm (x#bs) (usubst p (Add (Mul m t) (Mul n s),2*n*m))) = (\<exists>(t,n) \<in> U'. Ifm (x#bs) (usubst p (t,n)))" - (is "?lhs = ?rhs") + and UU': "((\<lambda>(t,n). Inum (x # bs) t / real n) ` U') = + ((\<lambda>((t,n),(s,m)). (Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) ` (U \<times> U))" + (is "?f ` U' = ?g ` (U \<times> U)") + and U: "\<forall>(t,n) \<in> U. numbound0 t \<and> n > 0" + and U': "\<forall>(t,n) \<in> U'. numbound0 t \<and> n > 0" + shows "(\<exists>(t,n) \<in> U. \<exists>(s,m) \<in> U. Ifm (x # bs) (usubst p (Add (Mul m t) (Mul n s), 2 * n * m))) = + (\<exists>(t,n) \<in> U'. Ifm (x # bs) (usubst p (t, n)))" + (is "?lhs \<longleftrightarrow> ?rhs") proof - assume ?lhs - then obtain t n s m where tnU: "(t,n) \<in> U" and smU:"(s,m) \<in> U" and - Pst: "Ifm (x#bs) (usubst p (Add (Mul m t) (Mul n s),2*n*m))" by blast - let ?N = "\<lambda>t. Inum (x#bs) t" - from tnU smU U have tnb: "numbound0 t" and np: "n > 0" - and snb: "numbound0 s" and mp:"m > 0" by auto - let ?st= "Add (Mul m t) (Mul n s)" - from np mp have mnp: "real (2*n*m) > 0" + show ?rhs if ?lhs + proof - + from that obtain t n s m where tnU: "(t, n) \<in> U" and smU: "(s, m) \<in> U" + and Pst: "Ifm (x # bs) (usubst p (Add (Mul m t) (Mul n s), 2 * n * m))" + by blast + let ?N = "\<lambda>t. Inum (x#bs) t" + from tnU smU U have tnb: "numbound0 t" and np: "n > 0" + and snb: "numbound0 s" and mp: "m > 0" + by auto + let ?st = "Add (Mul m t) (Mul n s)" + from np mp have mnp: "real (2 * n * m) > 0" by (simp add: mult.commute real_of_int_mult[symmetric] del: real_of_int_mult) - from tnb snb have stnb: "numbound0 ?st" by simp - have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mp np by (simp add: algebra_simps add_divide_distrib) - from tnU smU UU' have "?g ((t,n),(s,m)) \<in> ?f ` U'" by blast - then have "\<exists>(t',n') \<in> U'. ?g ((t,n),(s,m)) = ?f (t',n')" - by auto (rule_tac x="(a,b)" in bexI, auto) - then obtain t' n' where tnU': "(t',n') \<in> U'" and th: "?g ((t,n),(s,m)) = ?f (t',n')" by blast - from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto - from usubst_I[OF lp mnp stnb, where bs="bs" and x="x"] Pst - have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" by simp - from conjunct1[OF usubst_I[OF lp np' tnb', where bs="bs" and x="x"], symmetric] th[simplified split_def fst_conv snd_conv,symmetric] Pst2[simplified st[symmetric]] - have "Ifm (x # bs) (usubst p (t', n')) " by (simp only: st) - then show ?rhs using tnU' by auto -next - assume ?rhs - then obtain t' n' where tnU': "(t',n') \<in> U'" and Pt': "Ifm (x # bs) (usubst p (t', n'))" - by blast - from tnU' UU' have "?f (t',n') \<in> ?g ` (U\<times>U)" by blast - then have "\<exists>((t,n),(s,m)) \<in> (U\<times>U). ?f (t',n') = ?g ((t,n),(s,m))" - by auto (rule_tac x="(a,b)" in bexI, auto) - then obtain t n s m where tnU: "(t,n) \<in> U" and smU:"(s,m) \<in> U" and - th: "?f (t',n') = ?g((t,n),(s,m)) "by blast - let ?N = "\<lambda>t. Inum (x#bs) t" - from tnU smU U have tnb: "numbound0 t" and np: "n > 0" - and snb: "numbound0 s" and mp:"m > 0" by auto - let ?st= "Add (Mul m t) (Mul n s)" - from np mp have mnp: "real (2*n*m) > 0" + from tnb snb have stnb: "numbound0 ?st" + by simp + have st: "(?N t / real n + ?N s / real m) / 2 = ?N ?st / real (2 * n * m)" + using mp np by (simp add: algebra_simps add_divide_distrib) + from tnU smU UU' have "?g ((t, n), (s, m)) \<in> ?f ` U'" + by blast + then have "\<exists>(t',n') \<in> U'. ?g ((t, n), (s, m)) = ?f (t', n')" + apply auto + apply (rule_tac x="(a, b)" in bexI) + apply auto + done + then obtain t' n' where tnU': "(t',n') \<in> U'" and th: "?g ((t, n), (s, m)) = ?f (t', n')" + by blast + from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" + by auto + from usubst_I[OF lp mnp stnb, where bs="bs" and x="x"] Pst + have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" + by simp + from conjunct1[OF usubst_I[OF lp np' tnb', where bs="bs" and x="x"], symmetric] + th[simplified split_def fst_conv snd_conv,symmetric] Pst2[simplified st[symmetric]] + have "Ifm (x # bs) (usubst p (t', n'))" + by (simp only: st) + then show ?thesis + using tnU' by auto + qed + show ?lhs if ?rhs + proof - + from that obtain t' n' where tnU': "(t', n') \<in> U'" and Pt': "Ifm (x # bs) (usubst p (t', n'))" + by blast + from tnU' UU' have "?f (t', n') \<in> ?g ` (U \<times> U)" + by blast + then have "\<exists>((t,n),(s,m)) \<in> U \<times> U. ?f (t', n') = ?g ((t, n), (s, m))" + apply auto + apply (rule_tac x="(a,b)" in bexI) + apply auto + done + then obtain t n s m where tnU: "(t, n) \<in> U" and smU: "(s, m) \<in> U" and + th: "?f (t', n') = ?g ((t, n), (s, m))" + by blast + let ?N = "\<lambda>t. Inum (x # bs) t" + from tnU smU U have tnb: "numbound0 t" and np: "n > 0" + and snb: "numbound0 s" and mp: "m > 0" + by auto + let ?st = "Add (Mul m t) (Mul n s)" + from np mp have mnp: "real (2 * n * m) > 0" by (simp add: mult.commute real_of_int_mult[symmetric] del: real_of_int_mult) - from tnb snb have stnb: "numbound0 ?st" by simp - have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" - using mp np by (simp add: algebra_simps add_divide_distrib) - from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto - from usubst_I[OF lp np' tnb', where bs="bs" and x="x",simplified th[simplified split_def fst_conv snd_conv] st] Pt' - have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" by simp - with usubst_I[OF lp mnp stnb, where x="x" and bs="bs"] tnU smU show ?lhs by blast + from tnb snb have stnb: "numbound0 ?st" + by simp + have st: "(?N t / real n + ?N s / real m) / 2 = ?N ?st / real (2 * n * m)" + using mp np by (simp add: algebra_simps add_divide_distrib) + from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" + by auto + from usubst_I[OF lp np' tnb', where bs="bs" and x="x",simplified + th[simplified split_def fst_conv snd_conv] st] Pt' + have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" + by simp + with usubst_I[OF lp mnp stnb, where x="x" and bs="bs"] tnU smU + show ?thesis by blast + qed qed lemma ferrack: assumes qf: "qfree p" - shows "qfree (ferrack p) \<and> ((Ifm bs (ferrack p)) = (\<exists>x. Ifm (x#bs) p))" - (is "_ \<and> (?rhs = ?lhs)") + shows "qfree (ferrack p) \<and> (Ifm bs (ferrack p) \<longleftrightarrow> (\<exists>x. Ifm (x # bs) p))" + (is "_ \<and> (?rhs \<longleftrightarrow> ?lhs)") proof - - let ?I = "\<lambda>x p. Ifm (x#bs) p" + let ?I = "\<lambda>x p. Ifm (x # bs) p" fix x - let ?N = "\<lambda>t. Inum (x#bs) t" + let ?N = "\<lambda>t. Inum (x # bs) t" let ?q = "rlfm (simpfm p)" let ?U = "uset ?q" let ?Up = "alluopairs ?U" - let ?g = "\<lambda>((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2*n*m)" + let ?g = "\<lambda>((t,n),(s,m)). (Add (Mul m t) (Mul n s), 2 * n * m)" let ?S = "map ?g ?Up" let ?SS = "map simp_num_pair ?S" let ?Y = "remdups ?SS" - let ?f= "(\<lambda>(t,n). ?N t / real n)" - let ?h = "\<lambda>((t,n),(s,m)). (?N t/real n + ?N s/ real m) /2" - let ?F = "\<lambda>p. \<exists>a \<in> set (uset p). \<exists>b \<in> set (uset p). ?I x (usubst p (?g(a,b)))" + let ?f = "\<lambda>(t,n). ?N t / real n" + let ?h = "\<lambda>((t,n),(s,m)). (?N t / real n + ?N s / real m) / 2" + let ?F = "\<lambda>p. \<exists>a \<in> set (uset p). \<exists>b \<in> set (uset p). ?I x (usubst p (?g (a, b)))" let ?ep = "evaldjf (simpfm \<circ> (usubst ?q)) ?Y" - from rlfm_I[OF simpfm_qf[OF qf]] have lq: "isrlfm ?q" by blast - from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp + from rlfm_I[OF simpfm_qf[OF qf]] have lq: "isrlfm ?q" + by blast + from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<subseteq> set ?U \<times> set ?U" + by simp from uset_l[OF lq] have U_l: "\<forall>(t,n) \<in> set ?U. numbound0 t \<and> n > 0" . from U_l UpU - have "\<forall>((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto - then have Snb: "\<forall>(t,n) \<in> set ?S. numbound0 t \<and> n > 0 " by auto + have "\<forall>((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" + by auto + then have Snb: "\<forall>(t,n) \<in> set ?S. numbound0 t \<and> n > 0 " + by auto have Y_l: "\<forall>(t,n) \<in> set ?Y. numbound0 t \<and> n > 0" proof - - { fix t n assume tnY: "(t,n) \<in> set ?Y" - then have "(t,n) \<in> set ?SS" by simp - then have "\<exists>(t',n') \<in> set ?S. simp_num_pair (t',n') = (t,n)" - by (auto simp add: split_def simp del: map_map) - (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all) - then obtain t' n' where tn'S: "(t',n') \<in> set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast - from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto - from simp_num_pair_l[OF tnb np tns] - have "numbound0 t \<and> n > 0" . } + have "numbound0 t \<and> n > 0" if tnY: "(t, n) \<in> set ?Y" for t n + proof - + from that have "(t,n) \<in> set ?SS" + by simp + then have "\<exists>(t',n') \<in> set ?S. simp_num_pair (t', n') = (t, n)" + apply (auto simp add: split_def simp del: map_map) + apply (rule_tac x="((aa,ba),(ab,bb))" in bexI) + apply simp_all + done + then obtain t' n' where tn'S: "(t', n') \<in> set ?S" and tns: "simp_num_pair (t', n') = (t, n)" + by blast + from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" + by auto + from simp_num_pair_l[OF tnb np tns] show ?thesis . + qed then show ?thesis by blast qed have YU: "(?f ` set ?Y) = (?h ` (set ?U \<times> set ?U))" proof - - from simp_num_pair_ci[where bs="x#bs"] have - "\<forall>x. (?f \<circ> simp_num_pair) x = ?f x" by auto - then have th: "?f \<circ> simp_num_pair = ?f" using ext by blast - have "(?f ` set ?Y) = ((?f \<circ> simp_num_pair) ` set ?S)" by (simp add: comp_assoc image_comp) - also have "\<dots> = (?f ` set ?S)" by (simp add: th) - also have "\<dots> = ((?f \<circ> ?g) ` set ?Up)" + from simp_num_pair_ci[where bs="x#bs"] have "\<forall>x. (?f \<circ> simp_num_pair) x = ?f x" + by auto + then have th: "?f \<circ> simp_num_pair = ?f" + by auto + have "(?f ` set ?Y) = ((?f \<circ> simp_num_pair) ` set ?S)" + by (simp add: comp_assoc image_comp) + also have "\<dots> = ?f ` set ?S" + by (simp add: th) + also have "\<dots> = (?f \<circ> ?g) ` set ?Up" by (simp only: set_map o_def image_comp) - also have "\<dots> = (?h ` (set ?U \<times> set ?U))" - using uset_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_comp] by blast + also have "\<dots> = ?h ` (set ?U \<times> set ?U)" + using uset_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_comp] + by blast finally show ?thesis . qed - have "\<forall>(t,n) \<in> set ?Y. bound0 (simpfm (usubst ?q (t,n)))" + have "\<forall>(t,n) \<in> set ?Y. bound0 (simpfm (usubst ?q (t, n)))" proof - - { fix t n assume tnY: "(t,n) \<in> set ?Y" - with Y_l have tnb: "numbound0 t" and np: "real n > 0" by auto - from usubst_I[OF lq np tnb] - have "bound0 (usubst ?q (t,n))" by simp then have "bound0 (simpfm (usubst ?q (t,n)))" - using simpfm_bound0 by simp} + have "bound0 (simpfm (usubst ?q (t, n)))" if tnY: "(t,n) \<in> set ?Y" for t n + proof - + from Y_l that have tnb: "numbound0 t" and np: "real n > 0" + by auto + from usubst_I[OF lq np tnb] have "bound0 (usubst ?q (t, n))" + by simp + then show ?thesis + using simpfm_bound0 by simp + qed then show ?thesis by blast qed - then have ep_nb: "bound0 ?ep" using evaldjf_bound0[where xs="?Y" and f="simpfm \<circ> (usubst ?q)"] by auto + then have ep_nb: "bound0 ?ep" + using evaldjf_bound0[where xs="?Y" and f="simpfm \<circ> (usubst ?q)"] by auto let ?mp = "minusinf ?q" let ?pp = "plusinf ?q" let ?M = "?I x ?mp" let ?P = "?I x ?pp" let ?res = "disj ?mp (disj ?pp ?ep)" - from rminusinf_bound0[OF lq] rplusinf_bound0[OF lq] ep_nb - have nbth: "bound0 ?res" by auto + from rminusinf_bound0[OF lq] rplusinf_bound0[OF lq] ep_nb have nbth: "bound0 ?res" + by auto - from conjunct1[OF rlfm_I[OF simpfm_qf[OF qf]]] simpfm - - have th: "?lhs = (\<exists>x. ?I x ?q)" by auto + from conjunct1[OF rlfm_I[OF simpfm_qf[OF qf]]] simpfm have th: "?lhs = (\<exists>x. ?I x ?q)" + by auto from th fr_equsubst[OF lq, where bs="bs" and x="x"] have lhfr: "?lhs = (?M \<or> ?P \<or> ?F ?q)" by (simp only: split_def fst_conv snd_conv) also have "\<dots> = (?M \<or> ?P \<or> (\<exists>(t,n) \<in> set ?Y. ?I x (simpfm (usubst ?q (t,n)))))" - using uset_cong[OF lq YU U_l Y_l] by (simp only: split_def fst_conv snd_conv simpfm) + using uset_cong[OF lq YU U_l Y_l] by (simp only: split_def fst_conv snd_conv simpfm) also have "\<dots> = (Ifm (x#bs) ?res)" using evaldjf_ex[where ps="?Y" and bs = "x#bs" and f="simpfm \<circ> (usubst ?q)",symmetric] by (simp add: split_def pair_collapse) - finally have lheq: "?lhs = (Ifm bs (decr ?res))" using decr[OF nbth] by blast - then have lr: "?lhs = ?rhs" apply (unfold ferrack_def Let_def) + finally have lheq: "?lhs = Ifm bs (decr ?res)" + using decr[OF nbth] by blast + then have lr: "?lhs = ?rhs" + unfolding ferrack_def Let_def by (cases "?mp = T \<or> ?pp = T", auto) (simp add: disj_def)+ - from decr_qf[OF nbth] have "qfree (ferrack p)" by (auto simp add: Let_def ferrack_def) - with lr show ?thesis by blast + from decr_qf[OF nbth] have "qfree (ferrack p)" + by (auto simp add: Let_def ferrack_def) + with lr show ?thesis + by blast qed -definition linrqe:: "fm \<Rightarrow> fm" where - "linrqe p = qelim (prep p) ferrack" +definition linrqe:: "fm \<Rightarrow> fm" + where "linrqe p = qelim (prep p) ferrack" theorem linrqe: "Ifm bs (linrqe p) = Ifm bs p \<and> qfree (linrqe p)" -using ferrack qelim_ci prep -unfolding linrqe_def by auto + using ferrack qelim_ci prep + unfolding linrqe_def by auto -definition ferrack_test :: "unit \<Rightarrow> fm" where - "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0))) - (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" +definition ferrack_test :: "unit \<Rightarrow> fm" +where + "ferrack_test u = + linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0))) + (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" ML_val \<open>@{code ferrack_test} ()\<close>