30439

1 
(* Title: HOL/Decision_Procs/Ferrack.thy

29789

2 
Author: Amine Chaieb


3 
*)


4 


5 
theory Ferrack

29818

6 
imports Complex_Main Dense_Linear_Order Efficient_Nat

29789

7 
uses ("ferrack_tac.ML")


8 
begin


9 


10 
section {* Quantifier elimination for @{text "\<real> (0, 1, +, <)"} *}


11 


12 
(*********************************************************************************)


13 
(* SOME GENERAL STUFF< HAS TO BE MOVED IN SOME LIB *)


14 
(*********************************************************************************)


15 


16 
consts alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list"


17 
primrec


18 
"alluopairs [] = []"


19 
"alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"


20 


21 
lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"


22 
by (induct xs, auto)


23 


24 
lemma alluopairs_set:


25 
"\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "


26 
by (induct xs, auto)


27 


28 
lemma alluopairs_ex:


29 
assumes Pc: "\<forall> x y. P x y = P y x"


30 
shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"


31 
proof


32 
assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"


33 
then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y" by blast


34 
from alluopairs_set[OF x y] P Pc show"\<exists>(x, y)\<in>set (alluopairs xs). P x y"


35 
by auto


36 
next


37 
assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"


38 
then obtain "x" and "y" where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+


39 
from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast


40 
with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast


41 
qed


42 


43 
lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n  1)"


44 
using Nat.gr0_conv_Suc


45 
by clarsimp


46 


47 
lemma filter_length: "length (List.filter P xs) < Suc (length xs)"


48 
apply (induct xs, auto) done


49 


50 
consts remdps:: "'a list \<Rightarrow> 'a list"


51 


52 
recdef remdps "measure size"


53 
"remdps [] = []"


54 
"remdps (x#xs) = (x#(remdps (List.filter (\<lambda> y. y \<noteq> x) xs)))"


55 
(hints simp add: filter_length[rule_format])


56 


57 
lemma remdps_set[simp]: "set (remdps xs) = set xs"


58 
by (induct xs rule: remdps.induct, auto)


59 


60 


61 


62 
(*********************************************************************************)


63 
(**** SHADOW SYNTAX AND SEMANTICS ****)


64 
(*********************************************************************************)


65 


66 
datatype num = C int  Bound nat  CN nat int num  Neg num  Add num num Sub num num


67 
 Mul int num


68 


69 
(* A size for num to make inductive proofs simpler*)


70 
consts num_size :: "num \<Rightarrow> nat"


71 
primrec


72 
"num_size (C c) = 1"


73 
"num_size (Bound n) = 1"


74 
"num_size (Neg a) = 1 + num_size a"


75 
"num_size (Add a b) = 1 + num_size a + num_size b"


76 
"num_size (Sub a b) = 3 + num_size a + num_size b"


77 
"num_size (Mul c a) = 1 + num_size a"


78 
"num_size (CN n c a) = 3 + num_size a "


79 


80 
(* Semantics of numeral terms (num) *)


81 
consts Inum :: "real list \<Rightarrow> num \<Rightarrow> real"


82 
primrec


83 
"Inum bs (C c) = (real c)"


84 
"Inum bs (Bound n) = bs!n"


85 
"Inum bs (CN n c a) = (real c) * (bs!n) + (Inum bs a)"


86 
"Inum bs (Neg a) = (Inum bs a)"


87 
"Inum bs (Add a b) = Inum bs a + Inum bs b"


88 
"Inum bs (Sub a b) = Inum bs a  Inum bs b"


89 
"Inum bs (Mul c a) = (real c) * Inum bs a"


90 
(* FORMULAE *)


91 
datatype fm =


92 
T F Lt num Le num Gt num Ge num Eq num NEq num


93 
NOT fm And fm fm Or fm fm Imp fm fm Iff fm fm E fm A fm


94 


95 


96 
(* A size for fm *)


97 
consts fmsize :: "fm \<Rightarrow> nat"


98 
recdef fmsize "measure size"


99 
"fmsize (NOT p) = 1 + fmsize p"


100 
"fmsize (And p q) = 1 + fmsize p + fmsize q"


101 
"fmsize (Or p q) = 1 + fmsize p + fmsize q"


102 
"fmsize (Imp p q) = 3 + fmsize p + fmsize q"


103 
"fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"


104 
"fmsize (E p) = 1 + fmsize p"


105 
"fmsize (A p) = 4+ fmsize p"


106 
"fmsize p = 1"


107 
(* several lemmas about fmsize *)


108 
lemma fmsize_pos: "fmsize p > 0"


109 
by (induct p rule: fmsize.induct) simp_all


110 


111 
(* Semantics of formulae (fm) *)


112 
consts Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool"


113 
primrec


114 
"Ifm bs T = True"


115 
"Ifm bs F = False"


116 
"Ifm bs (Lt a) = (Inum bs a < 0)"


117 
"Ifm bs (Gt a) = (Inum bs a > 0)"


118 
"Ifm bs (Le a) = (Inum bs a \<le> 0)"


119 
"Ifm bs (Ge a) = (Inum bs a \<ge> 0)"


120 
"Ifm bs (Eq a) = (Inum bs a = 0)"


121 
"Ifm bs (NEq a) = (Inum bs a \<noteq> 0)"


122 
"Ifm bs (NOT p) = (\<not> (Ifm bs p))"


123 
"Ifm bs (And p q) = (Ifm bs p \<and> Ifm bs q)"


124 
"Ifm bs (Or p q) = (Ifm bs p \<or> Ifm bs q)"


125 
"Ifm bs (Imp p q) = ((Ifm bs p) \<longrightarrow> (Ifm bs q))"


126 
"Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)"


127 
"Ifm bs (E p) = (\<exists> x. Ifm (x#bs) p)"


128 
"Ifm bs (A p) = (\<forall> x. Ifm (x#bs) p)"


129 


130 
lemma IfmLeSub: "\<lbrakk> Inum bs s = s' ; Inum bs t = t' \<rbrakk> \<Longrightarrow> Ifm bs (Le (Sub s t)) = (s' \<le> t')"


131 
apply simp


132 
done


133 


134 
lemma IfmLtSub: "\<lbrakk> Inum bs s = s' ; Inum bs t = t' \<rbrakk> \<Longrightarrow> Ifm bs (Lt (Sub s t)) = (s' < t')"


135 
apply simp


136 
done


137 
lemma IfmEqSub: "\<lbrakk> Inum bs s = s' ; Inum bs t = t' \<rbrakk> \<Longrightarrow> Ifm bs (Eq (Sub s t)) = (s' = t')"


138 
apply simp


139 
done


140 
lemma IfmNOT: " (Ifm bs p = P) \<Longrightarrow> (Ifm bs (NOT p) = (\<not>P))"


141 
apply simp


142 
done


143 
lemma IfmAnd: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (And p q) = (P \<and> Q))"


144 
apply simp


145 
done


146 
lemma IfmOr: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (Or p q) = (P \<or> Q))"


147 
apply simp


148 
done


149 
lemma IfmImp: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (Imp p q) = (P \<longrightarrow> Q))"


150 
apply simp


151 
done


152 
lemma IfmIff: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (Iff p q) = (P = Q))"


153 
apply simp


154 
done


155 


156 
lemma IfmE: " (!! x. Ifm (x#bs) p = P x) \<Longrightarrow> (Ifm bs (E p) = (\<exists>x. P x))"


157 
apply simp


158 
done


159 
lemma IfmA: " (!! x. Ifm (x#bs) p = P x) \<Longrightarrow> (Ifm bs (A p) = (\<forall>x. P x))"


160 
apply simp


161 
done


162 


163 
consts not:: "fm \<Rightarrow> fm"


164 
recdef not "measure size"


165 
"not (NOT p) = p"


166 
"not T = F"


167 
"not F = T"


168 
"not p = NOT p"


169 
lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)"


170 
by (cases p) auto


171 


172 
constdefs conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"


173 
"conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else


174 
if p = q then p else And p q)"


175 
lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)"


176 
by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all)


177 


178 
constdefs disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"


179 
"disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p


180 
else if p=q then p else Or p q)"


181 


182 
lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)"


183 
by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)


184 


185 
constdefs imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"


186 
"imp p q \<equiv> (if (p = F \<or> q=T \<or> p=q) then T else if p=T then q else if q=F then not p


187 
else Imp p q)"


188 
lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)"


189 
by (cases "p=F \<or> q=T",simp_all add: imp_def)


190 


191 
constdefs iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"


192 
"iff p q \<equiv> (if (p = q) then T else if (p = NOT q \<or> NOT p = q) then F else


193 
if p=F then not q else if q=F then not p else if p=T then q else if q=T then p else


194 
Iff p q)"


195 
lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)"


196 
by (unfold iff_def,cases "p=q", simp,cases "p=NOT q", simp) (cases "NOT p= q", auto)


197 


198 
lemma conj_simps:


199 
"conj F Q = F"


200 
"conj P F = F"


201 
"conj T Q = Q"


202 
"conj P T = P"


203 
"conj P P = P"


204 
"P \<noteq> T \<Longrightarrow> P \<noteq> F \<Longrightarrow> Q \<noteq> T \<Longrightarrow> Q \<noteq> F \<Longrightarrow> P \<noteq> Q \<Longrightarrow> conj P Q = And P Q"


205 
by (simp_all add: conj_def)


206 


207 
lemma disj_simps:


208 
"disj T Q = T"


209 
"disj P T = T"


210 
"disj F Q = Q"


211 
"disj P F = P"


212 
"disj P P = P"


213 
"P \<noteq> T \<Longrightarrow> P \<noteq> F \<Longrightarrow> Q \<noteq> T \<Longrightarrow> Q \<noteq> F \<Longrightarrow> P \<noteq> Q \<Longrightarrow> disj P Q = Or P Q"


214 
by (simp_all add: disj_def)


215 
lemma imp_simps:


216 
"imp F Q = T"


217 
"imp P T = T"


218 
"imp T Q = Q"


219 
"imp P F = not P"


220 
"imp P P = T"


221 
"P \<noteq> T \<Longrightarrow> P \<noteq> F \<Longrightarrow> P \<noteq> Q \<Longrightarrow> Q \<noteq> T \<Longrightarrow> Q \<noteq> F \<Longrightarrow> imp P Q = Imp P Q"


222 
by (simp_all add: imp_def)


223 
lemma trivNOT: "p \<noteq> NOT p" "NOT p \<noteq> p"


224 
apply (induct p, auto)


225 
done


226 


227 
lemma iff_simps:


228 
"iff p p = T"


229 
"iff p (NOT p) = F"


230 
"iff (NOT p) p = F"


231 
"iff p F = not p"


232 
"iff F p = not p"


233 
"p \<noteq> NOT T \<Longrightarrow> iff T p = p"


234 
"p\<noteq> NOT T \<Longrightarrow> iff p T = p"


235 
"p\<noteq>q \<Longrightarrow> p\<noteq> NOT q \<Longrightarrow> q\<noteq> NOT p \<Longrightarrow> p\<noteq> F \<Longrightarrow> q\<noteq> F \<Longrightarrow> p \<noteq> T \<Longrightarrow> q \<noteq> T \<Longrightarrow> iff p q = Iff p q"


236 
using trivNOT


237 
by (simp_all add: iff_def, cases p, auto)


238 
(* Quantifier freeness *)


239 
consts qfree:: "fm \<Rightarrow> bool"


240 
recdef qfree "measure size"


241 
"qfree (E p) = False"


242 
"qfree (A p) = False"


243 
"qfree (NOT p) = qfree p"


244 
"qfree (And p q) = (qfree p \<and> qfree q)"


245 
"qfree (Or p q) = (qfree p \<and> qfree q)"


246 
"qfree (Imp p q) = (qfree p \<and> qfree q)"


247 
"qfree (Iff p q) = (qfree p \<and> qfree q)"


248 
"qfree p = True"


249 


250 
(* Boundedness and substitution *)


251 
consts


252 
numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)


253 
bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)


254 
primrec


255 
"numbound0 (C c) = True"


256 
"numbound0 (Bound n) = (n>0)"


257 
"numbound0 (CN n c a) = (n\<noteq>0 \<and> numbound0 a)"


258 
"numbound0 (Neg a) = numbound0 a"


259 
"numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"


260 
"numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"


261 
"numbound0 (Mul i a) = numbound0 a"


262 
lemma numbound0_I:


263 
assumes nb: "numbound0 a"


264 
shows "Inum (b#bs) a = Inum (b'#bs) a"


265 
using nb


266 
by (induct a rule: numbound0.induct,auto simp add: nth_pos2)


267 


268 
primrec


269 
"bound0 T = True"


270 
"bound0 F = True"


271 
"bound0 (Lt a) = numbound0 a"


272 
"bound0 (Le a) = numbound0 a"


273 
"bound0 (Gt a) = numbound0 a"


274 
"bound0 (Ge a) = numbound0 a"


275 
"bound0 (Eq a) = numbound0 a"


276 
"bound0 (NEq a) = numbound0 a"


277 
"bound0 (NOT p) = bound0 p"


278 
"bound0 (And p q) = (bound0 p \<and> bound0 q)"


279 
"bound0 (Or p q) = (bound0 p \<and> bound0 q)"


280 
"bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"


281 
"bound0 (Iff p q) = (bound0 p \<and> bound0 q)"


282 
"bound0 (E p) = False"


283 
"bound0 (A p) = False"


284 


285 
lemma bound0_I:


286 
assumes bp: "bound0 p"


287 
shows "Ifm (b#bs) p = Ifm (b'#bs) p"


288 
using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]


289 
by (induct p rule: bound0.induct) (auto simp add: nth_pos2)


290 


291 
lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"


292 
by (cases p, auto)


293 
lemma not_bn[simp]: "bound0 p \<Longrightarrow> bound0 (not p)"


294 
by (cases p, auto)


295 


296 


297 
lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)"


298 
using conj_def by auto


299 
lemma conj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)"


300 
using conj_def by auto


301 


302 
lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"


303 
using disj_def by auto


304 
lemma disj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"


305 
using disj_def by auto


306 


307 
lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"


308 
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def)


309 
lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"


310 
using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def)


311 


312 
lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"


313 
by (unfold iff_def,cases "p=q", auto)


314 
lemma iff_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"


315 
using iff_def by (unfold iff_def,cases "p=q", auto)


316 


317 
consts


318 
decrnum:: "num \<Rightarrow> num"


319 
decr :: "fm \<Rightarrow> fm"


320 


321 
recdef decrnum "measure size"


322 
"decrnum (Bound n) = Bound (n  1)"


323 
"decrnum (Neg a) = Neg (decrnum a)"


324 
"decrnum (Add a b) = Add (decrnum a) (decrnum b)"


325 
"decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"


326 
"decrnum (Mul c a) = Mul c (decrnum a)"


327 
"decrnum (CN n c a) = CN (n  1) c (decrnum a)"


328 
"decrnum a = a"


329 


330 
recdef decr "measure size"


331 
"decr (Lt a) = Lt (decrnum a)"


332 
"decr (Le a) = Le (decrnum a)"


333 
"decr (Gt a) = Gt (decrnum a)"


334 
"decr (Ge a) = Ge (decrnum a)"


335 
"decr (Eq a) = Eq (decrnum a)"


336 
"decr (NEq a) = NEq (decrnum a)"


337 
"decr (NOT p) = NOT (decr p)"


338 
"decr (And p q) = conj (decr p) (decr q)"


339 
"decr (Or p q) = disj (decr p) (decr q)"


340 
"decr (Imp p q) = imp (decr p) (decr q)"


341 
"decr (Iff p q) = iff (decr p) (decr q)"


342 
"decr p = p"


343 


344 
lemma decrnum: assumes nb: "numbound0 t"


345 
shows "Inum (x#bs) t = Inum bs (decrnum t)"


346 
using nb by (induct t rule: decrnum.induct, simp_all add: nth_pos2)


347 


348 
lemma decr: assumes nb: "bound0 p"


349 
shows "Ifm (x#bs) p = Ifm bs (decr p)"


350 
using nb


351 
by (induct p rule: decr.induct, simp_all add: nth_pos2 decrnum)


352 


353 
lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"


354 
by (induct p, simp_all)


355 


356 
consts


357 
isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)


358 
recdef isatom "measure size"


359 
"isatom T = True"


360 
"isatom F = True"


361 
"isatom (Lt a) = True"


362 
"isatom (Le a) = True"


363 
"isatom (Gt a) = True"


364 
"isatom (Ge a) = True"


365 
"isatom (Eq a) = True"


366 
"isatom (NEq a) = True"


367 
"isatom p = False"


368 


369 
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"


370 
by (induct p, simp_all)


371 


372 
constdefs djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"


373 
"djf f p q \<equiv> (if q=T then T else if q=F then f p else


374 
(let fp = f p in case fp of T \<Rightarrow> T  F \<Rightarrow> q  _ \<Rightarrow> Or (f p) q))"


375 
constdefs evaldjf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"


376 
"evaldjf f ps \<equiv> foldr (djf f) ps F"


377 


378 
lemma djf_Or: "Ifm bs (djf f p q) = Ifm bs (Or (f p) q)"


379 
by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def)


380 
(cases "f p", simp_all add: Let_def djf_def)


381 


382 


383 
lemma djf_simps:


384 
"djf f p T = T"


385 
"djf f p F = f p"


386 
"q\<noteq>T \<Longrightarrow> q\<noteq>F \<Longrightarrow> djf f p q = (let fp = f p in case fp of T \<Rightarrow> T  F \<Rightarrow> q  _ \<Rightarrow> Or (f p) q)"


387 
by (simp_all add: djf_def)


388 


389 
lemma evaldjf_ex: "Ifm bs (evaldjf f ps) = (\<exists> p \<in> set ps. Ifm bs (f p))"


390 
by(induct ps, simp_all add: evaldjf_def djf_Or)


391 


392 
lemma evaldjf_bound0:


393 
assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"


394 
shows "bound0 (evaldjf f xs)"


395 
using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)


396 


397 
lemma evaldjf_qf:


398 
assumes nb: "\<forall> x\<in> set xs. qfree (f x)"


399 
shows "qfree (evaldjf f xs)"


400 
using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)


401 


402 
consts disjuncts :: "fm \<Rightarrow> fm list"


403 
recdef disjuncts "measure size"


404 
"disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"


405 
"disjuncts F = []"


406 
"disjuncts p = [p]"


407 


408 
lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bs q) = Ifm bs p"


409 
by(induct p rule: disjuncts.induct, auto)


410 


411 
lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 q"


412 
proof


413 
assume nb: "bound0 p"


414 
hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto)


415 
thus ?thesis by (simp only: list_all_iff)


416 
qed


417 


418 
lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q"


419 
proof


420 
assume qf: "qfree p"


421 
hence "list_all qfree (disjuncts p)"


422 
by (induct p rule: disjuncts.induct, auto)


423 
thus ?thesis by (simp only: list_all_iff)


424 
qed


425 


426 
constdefs DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"


427 
"DJ f p \<equiv> evaldjf f (disjuncts p)"


428 


429 
lemma DJ: assumes fdj: "\<forall> p q. Ifm bs (f (Or p q)) = Ifm bs (Or (f p) (f q))"


430 
and fF: "f F = F"


431 
shows "Ifm bs (DJ f p) = Ifm bs (f p)"


432 
proof


433 
have "Ifm bs (DJ f p) = (\<exists> q \<in> set (disjuncts p). Ifm bs (f q))"


434 
by (simp add: DJ_def evaldjf_ex)


435 
also have "\<dots> = Ifm bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto)


436 
finally show ?thesis .


437 
qed


438 


439 
lemma DJ_qf: assumes


440 
fqf: "\<forall> p. qfree p \<longrightarrow> qfree (f p)"


441 
shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "


442 
proof(clarify)


443 
fix p assume qf: "qfree p"


444 
have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def)


445 
from disjuncts_qf[OF qf] have "\<forall> q\<in> set (disjuncts p). qfree q" .


446 
with fqf have th':"\<forall> q\<in> set (disjuncts p). qfree (f q)" by blast


447 


448 
from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp


449 
qed


450 


451 
lemma DJ_qe: assumes qe: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"


452 
shows "\<forall> bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bs ((DJ qe p)) = Ifm bs (E p))"


453 
proof(clarify)


454 
fix p::fm and bs


455 
assume qf: "qfree p"


456 
from qe have qth: "\<forall> p. qfree p \<longrightarrow> qfree (qe p)" by blast


457 
from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto


458 
have "Ifm bs (DJ qe p) = (\<exists> q\<in> set (disjuncts p). Ifm bs (qe q))"


459 
by (simp add: DJ_def evaldjf_ex)


460 
also have "\<dots> = (\<exists> q \<in> set(disjuncts p). Ifm bs (E q))" using qe disjuncts_qf[OF qf] by auto


461 
also have "\<dots> = Ifm bs (E p)" by (induct p rule: disjuncts.induct, auto)


462 
finally show "qfree (DJ qe p) \<and> Ifm bs (DJ qe p) = Ifm bs (E p)" using qfth by blast


463 
qed


464 
(* Simplification *)


465 
consts


466 
numgcd :: "num \<Rightarrow> int"


467 
numgcdh:: "num \<Rightarrow> int \<Rightarrow> int"


468 
reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num"


469 
reducecoeff :: "num \<Rightarrow> num"


470 
dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"


471 
consts maxcoeff:: "num \<Rightarrow> int"


472 
recdef maxcoeff "measure size"


473 
"maxcoeff (C i) = abs i"


474 
"maxcoeff (CN n c t) = max (abs c) (maxcoeff t)"


475 
"maxcoeff t = 1"


476 


477 
lemma maxcoeff_pos: "maxcoeff t \<ge> 0"


478 
by (induct t rule: maxcoeff.induct, auto)


479 


480 
recdef numgcdh "measure size"


481 
"numgcdh (C i) = (\<lambda>g. zgcd i g)"


482 
"numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"


483 
"numgcdh t = (\<lambda>g. 1)"


484 
defs numgcd_def [code]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"


485 


486 
recdef reducecoeffh "measure size"


487 
"reducecoeffh (C i) = (\<lambda> g. C (i div g))"


488 
"reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))"


489 
"reducecoeffh t = (\<lambda>g. t)"


490 


491 
defs reducecoeff_def: "reducecoeff t \<equiv>


492 
(let g = numgcd t in


493 
if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)"


494 


495 
recdef dvdnumcoeff "measure size"


496 
"dvdnumcoeff (C i) = (\<lambda> g. g dvd i)"


497 
"dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"


498 
"dvdnumcoeff t = (\<lambda>g. False)"


499 


500 
lemma dvdnumcoeff_trans:


501 
assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'"


502 
shows "dvdnumcoeff t g"


503 
using dgt' gdg

30042

504 
by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg])

29789

505 

30042

506 
declare dvd_trans [trans add]

29789

507 


508 
lemma natabs0: "(nat (abs x) = 0) = (x = 0)"


509 
by arith


510 


511 
lemma numgcd0:


512 
assumes g0: "numgcd t = 0"


513 
shows "Inum bs t = 0"


514 
using g0[simplified numgcd_def]


515 
by (induct t rule: numgcdh.induct, auto simp add: zgcd_def gcd_zero natabs0 max_def maxcoeff_pos)


516 


517 
lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"


518 
using gp


519 
by (induct t rule: numgcdh.induct, auto simp add: zgcd_def)


520 


521 
lemma numgcd_pos: "numgcd t \<ge>0"


522 
by (simp add: numgcd_def numgcdh_pos maxcoeff_pos)


523 


524 
lemma reducecoeffh:


525 
assumes gt: "dvdnumcoeff t g" and gp: "g > 0"


526 
shows "real g *(Inum bs (reducecoeffh t g)) = Inum bs t"


527 
using gt


528 
proof(induct t rule: reducecoeffh.induct)


529 
case (1 i) hence gd: "g dvd i" by simp


530 
from gp have gnz: "g \<noteq> 0" by simp


531 
from prems show ?case by (simp add: real_of_int_div[OF gnz gd])


532 
next


533 
case (2 n c t) hence gd: "g dvd c" by simp


534 
from gp have gnz: "g \<noteq> 0" by simp


535 
from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)


536 
qed (auto simp add: numgcd_def gp)


537 
consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"


538 
recdef ismaxcoeff "measure size"


539 
"ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)"


540 
"ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"


541 
"ismaxcoeff t = (\<lambda>x. True)"


542 


543 
lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'"


544 
by (induct t rule: ismaxcoeff.induct, auto)


545 


546 
lemma maxcoeff_ismaxcoeff: "ismaxcoeff t (maxcoeff t)"


547 
proof (induct t rule: maxcoeff.induct)


548 
case (2 n c t)


549 
hence H:"ismaxcoeff t (maxcoeff t)" .


550 
have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by (simp add: le_maxI2)


551 
from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1)


552 
qed simp_all


553 


554 
lemma zgcd_gt1: "zgcd i j > 1 \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"


555 
apply (cases "abs i = 0", simp_all add: zgcd_def)


556 
apply (cases "abs j = 0", simp_all)


557 
apply (cases "abs i = 1", simp_all)


558 
apply (cases "abs j = 1", simp_all)


559 
apply auto


560 
done


561 
lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow> m =0"


562 
by (induct t rule: numgcdh.induct, auto simp add:zgcd0)


563 


564 
lemma dvdnumcoeff_aux:


565 
assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"


566 
shows "dvdnumcoeff t (numgcdh t m)"


567 
using prems


568 
proof(induct t rule: numgcdh.induct)


569 
case (2 n c t)


570 
let ?g = "numgcdh t m"


571 
from prems have th:"zgcd c ?g > 1" by simp


572 
from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]


573 
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp


574 
moreover {assume "abs c > 1" and gp: "?g > 1" with prems


575 
have th: "dvdnumcoeff t ?g" by simp


576 
have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)


577 
from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}


578 
moreover {assume "abs c = 0 \<and> ?g > 1"


579 
with prems have th: "dvdnumcoeff t ?g" by simp


580 
have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)


581 
from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)


582 
hence ?case by simp }


583 
moreover {assume "abs c > 1" and g0:"?g = 0"


584 
from numgcdh0[OF g0] have "m=0". with prems have ?case by simp }


585 
ultimately show ?case by blast


586 
qed(auto simp add: zgcd_zdvd1)


587 


588 
lemma dvdnumcoeff_aux2:


589 
assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"


590 
using prems


591 
proof (simp add: numgcd_def)


592 
let ?mc = "maxcoeff t"


593 
let ?g = "numgcdh t ?mc"


594 
have th1: "ismaxcoeff t ?mc" by (rule maxcoeff_ismaxcoeff)


595 
have th2: "?mc \<ge> 0" by (rule maxcoeff_pos)


596 
assume H: "numgcdh t ?mc > 1"


597 
from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" .


598 
qed


599 


600 
lemma reducecoeff: "real (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t"


601 
proof


602 
let ?g = "numgcd t"


603 
have "?g \<ge> 0" by (simp add: numgcd_pos)


604 
hence "?g = 0 \<or> ?g = 1 \<or> ?g > 1" by auto


605 
moreover {assume "?g = 0" hence ?thesis by (simp add: numgcd0)}


606 
moreover {assume "?g = 1" hence ?thesis by (simp add: reducecoeff_def)}


607 
moreover { assume g1:"?g > 1"


608 
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" and g0: "?g > 0" by blast+


609 
from reducecoeffh[OF th1 g0, where bs="bs"] g1 have ?thesis


610 
by (simp add: reducecoeff_def Let_def)}


611 
ultimately show ?thesis by blast


612 
qed


613 


614 
lemma reducecoeffh_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeffh t g)"


615 
by (induct t rule: reducecoeffh.induct, auto)


616 


617 
lemma reducecoeff_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeff t)"


618 
using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)


619 


620 
consts


621 
simpnum:: "num \<Rightarrow> num"


622 
numadd:: "num \<times> num \<Rightarrow> num"


623 
nummul:: "num \<Rightarrow> int \<Rightarrow> num"


624 
recdef numadd "measure (\<lambda> (t,s). size t + size s)"


625 
"numadd (CN n1 c1 r1,CN n2 c2 r2) =


626 
(if n1=n2 then


627 
(let c = c1 + c2


628 
in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2))))


629 
else if n1 \<le> n2 then (CN n1 c1 (numadd (r1,CN n2 c2 r2)))


630 
else (CN n2 c2 (numadd (CN n1 c1 r1,r2))))"


631 
"numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))"


632 
"numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))"


633 
"numadd (C b1, C b2) = C (b1+b2)"


634 
"numadd (a,b) = Add a b"


635 


636 
lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"


637 
apply (induct t s rule: numadd.induct, simp_all add: Let_def)


638 
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)


639 
apply (case_tac "n1 = n2", simp_all add: algebra_simps)


640 
by (simp only: left_distrib[symmetric],simp)


641 


642 
lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"


643 
by (induct t s rule: numadd.induct, auto simp add: Let_def)


644 


645 
recdef nummul "measure size"


646 
"nummul (C j) = (\<lambda> i. C (i*j))"


647 
"nummul (CN n c a) = (\<lambda> i. CN n (i*c) (nummul a i))"


648 
"nummul t = (\<lambda> i. Mul i t)"


649 


650 
lemma nummul[simp]: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)"


651 
by (induct t rule: nummul.induct, auto simp add: algebra_simps)


652 


653 
lemma nummul_nb[simp]: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"


654 
by (induct t rule: nummul.induct, auto )


655 


656 
constdefs numneg :: "num \<Rightarrow> num"


657 
"numneg t \<equiv> nummul t ( 1)"


658 


659 
constdefs numsub :: "num \<Rightarrow> num \<Rightarrow> num"


660 
"numsub s t \<equiv> (if s = t then C 0 else numadd (s,numneg t))"


661 


662 
lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)"


663 
using numneg_def by simp


664 


665 
lemma numneg_nb[simp]: "numbound0 t \<Longrightarrow> numbound0 (numneg t)"


666 
using numneg_def by simp


667 


668 
lemma numsub[simp]: "Inum bs (numsub a b) = Inum bs (Sub a b)"


669 
using numsub_def by simp


670 


671 
lemma numsub_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numsub t s)"


672 
using numsub_def by simp


673 


674 
recdef simpnum "measure size"


675 
"simpnum (C j) = C j"


676 
"simpnum (Bound n) = CN n 1 (C 0)"


677 
"simpnum (Neg t) = numneg (simpnum t)"


678 
"simpnum (Add t s) = numadd (simpnum t,simpnum s)"


679 
"simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"


680 
"simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum t) i)"


681 
"simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0),simpnum t))"


682 


683 
lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t"


684 
by (induct t rule: simpnum.induct, auto simp add: numneg numadd numsub nummul)


685 


686 
lemma simpnum_numbound0[simp]:


687 
"numbound0 t \<Longrightarrow> numbound0 (simpnum t)"


688 
by (induct t rule: simpnum.induct, auto)


689 


690 
consts nozerocoeff:: "num \<Rightarrow> bool"


691 
recdef nozerocoeff "measure size"


692 
"nozerocoeff (C c) = True"


693 
"nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff t)"


694 
"nozerocoeff t = True"


695 


696 
lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd (a,b))"


697 
by (induct a b rule: numadd.induct,auto simp add: Let_def)


698 


699 
lemma nummul_nz : "\<And> i. i\<noteq>0 \<Longrightarrow> nozerocoeff a \<Longrightarrow> nozerocoeff (nummul a i)"


700 
by (induct a rule: nummul.induct,auto simp add: Let_def numadd_nz)


701 


702 
lemma numneg_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff (numneg a)"


703 
by (simp add: numneg_def nummul_nz)


704 


705 
lemma numsub_nz: "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numsub a b)"


706 
by (simp add: numsub_def numneg_nz numadd_nz)


707 


708 
lemma simpnum_nz: "nozerocoeff (simpnum t)"


709 
by(induct t rule: simpnum.induct, auto simp add: numadd_nz numneg_nz numsub_nz nummul_nz)


710 


711 
lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"


712 
proof (induct t rule: maxcoeff.induct)


713 
case (2 n c t)


714 
hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+


715 
have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1)


716 
with cnz have "max (abs c) (maxcoeff t) > 0" by arith


717 
with prems show ?case by simp


718 
qed auto


719 


720 
lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0"


721 
proof


722 
from g0 have th:"numgcdh t (maxcoeff t) = 0" by (simp add: numgcd_def)


723 
from numgcdh0[OF th] have th:"maxcoeff t = 0" .


724 
from maxcoeff_nz[OF nz th] show ?thesis .


725 
qed


726 


727 
constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> int"


728 
"simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else


729 
(let t' = simpnum t ; g = numgcd t' in


730 
if g > 1 then (let g' = zgcd n g in


731 
if g' = 1 then (t',n)


732 
else (reducecoeffh t' g', n div g'))


733 
else (t',n))))"


734 


735 
lemma simp_num_pair_ci:


736 
shows "((\<lambda> (t,n). Inum bs t / real n) (simp_num_pair (t,n))) = ((\<lambda> (t,n). Inum bs t / real n) (t,n))"


737 
(is "?lhs = ?rhs")


738 
proof


739 
let ?t' = "simpnum t"


740 
let ?g = "numgcd ?t'"


741 
let ?g' = "zgcd n ?g"


742 
{assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}


743 
moreover


744 
{ assume nnz: "n \<noteq> 0"


745 
{assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}


746 
moreover


747 
{assume g1:"?g>1" hence g0: "?g > 0" by simp


748 
from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp


749 
hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith


750 
hence "?g'= 1 \<or> ?g' > 1" by arith


751 
moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}


752 
moreover {assume g'1:"?g'>1"


753 
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..


754 
let ?tt = "reducecoeffh ?t' ?g'"


755 
let ?t = "Inum bs ?tt"


756 
have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)


757 
have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1)


758 
have gpdgp: "?g' dvd ?g'" by simp


759 
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]


760 
have th2:"real ?g' * ?t = Inum bs ?t'" by simp


761 
from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)


762 
also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp


763 
also have "\<dots> = (Inum bs ?t' / real n)"


764 
using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp


765 
finally have "?lhs = Inum bs t / real n" by (simp add: simpnum_ci)


766 
then have ?thesis using prems by (simp add: simp_num_pair_def)}


767 
ultimately have ?thesis by blast}


768 
ultimately have ?thesis by blast}


769 
ultimately show ?thesis by blast


770 
qed


771 


772 
lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')"


773 
shows "numbound0 t' \<and> n' >0"


774 
proof


775 
let ?t' = "simpnum t"


776 
let ?g = "numgcd ?t'"


777 
let ?g' = "zgcd n ?g"


778 
{assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}


779 
moreover


780 
{ assume nnz: "n \<noteq> 0"


781 
{assume "\<not> ?g > 1" hence ?thesis using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}


782 
moreover


783 
{assume g1:"?g>1" hence g0: "?g > 0" by simp


784 
from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp


785 
hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith


786 
hence "?g'= 1 \<or> ?g' > 1" by arith


787 
moreover {assume "?g'=1" hence ?thesis using prems


788 
by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}


789 
moreover {assume g'1:"?g'>1"


790 
have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)


791 
have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1)


792 
have gpdgp: "?g' dvd ?g'" by simp


793 
from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .


794 
from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]


795 
have "n div ?g' >0" by simp


796 
hence ?thesis using prems


797 
by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0)}


798 
ultimately have ?thesis by blast}


799 
ultimately have ?thesis by blast}


800 
ultimately show ?thesis by blast


801 
qed


802 


803 
consts simpfm :: "fm \<Rightarrow> fm"


804 
recdef simpfm "measure fmsize"


805 
"simpfm (And p q) = conj (simpfm p) (simpfm q)"


806 
"simpfm (Or p q) = disj (simpfm p) (simpfm q)"


807 
"simpfm (Imp p q) = imp (simpfm p) (simpfm q)"


808 
"simpfm (Iff p q) = iff (simpfm p) (simpfm q)"


809 
"simpfm (NOT p) = not (simpfm p)"


810 
"simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F


811 
 _ \<Rightarrow> Lt a')"


812 
"simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0) then T else F  _ \<Rightarrow> Le a')"


813 
"simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0) then T else F  _ \<Rightarrow> Gt a')"


814 
"simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0) then T else F  _ \<Rightarrow> Ge a')"


815 
"simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0) then T else F  _ \<Rightarrow> Eq a')"


816 
"simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0) then T else F  _ \<Rightarrow> NEq a')"


817 
"simpfm p = p"


818 
lemma simpfm: "Ifm bs (simpfm p) = Ifm bs p"


819 
proof(induct p rule: simpfm.induct)


820 
case (6 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp


821 
{fix v assume "?sa = C v" hence ?case using sa by simp }


822 
moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa


823 
by (cases ?sa, simp_all add: Let_def)}


824 
ultimately show ?case by blast


825 
next


826 
case (7 a) let ?sa = "simpnum a"


827 
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp


828 
{fix v assume "?sa = C v" hence ?case using sa by simp }


829 
moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa


830 
by (cases ?sa, simp_all add: Let_def)}


831 
ultimately show ?case by blast


832 
next


833 
case (8 a) let ?sa = "simpnum a"


834 
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp


835 
{fix v assume "?sa = C v" hence ?case using sa by simp }


836 
moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa


837 
by (cases ?sa, simp_all add: Let_def)}


838 
ultimately show ?case by blast


839 
next


840 
case (9 a) let ?sa = "simpnum a"


841 
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp


842 
{fix v assume "?sa = C v" hence ?case using sa by simp }


843 
moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa


844 
by (cases ?sa, simp_all add: Let_def)}


845 
ultimately show ?case by blast


846 
next


847 
case (10 a) let ?sa = "simpnum a"


848 
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp


849 
{fix v assume "?sa = C v" hence ?case using sa by simp }


850 
moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa


851 
by (cases ?sa, simp_all add: Let_def)}


852 
ultimately show ?case by blast


853 
next


854 
case (11 a) let ?sa = "simpnum a"


855 
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp


856 
{fix v assume "?sa = C v" hence ?case using sa by simp }


857 
moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa


858 
by (cases ?sa, simp_all add: Let_def)}


859 
ultimately show ?case by blast


860 
qed (induct p rule: simpfm.induct, simp_all add: conj disj imp iff not)


861 


862 


863 
lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"


864 
proof(induct p rule: simpfm.induct)


865 
case (6 a) hence nb: "numbound0 a" by simp


866 
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])


867 
thus ?case by (cases "simpnum a", auto simp add: Let_def)


868 
next


869 
case (7 a) hence nb: "numbound0 a" by simp


870 
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])


871 
thus ?case by (cases "simpnum a", auto simp add: Let_def)


872 
next


873 
case (8 a) hence nb: "numbound0 a" by simp


874 
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])


875 
thus ?case by (cases "simpnum a", auto simp add: Let_def)


876 
next


877 
case (9 a) hence nb: "numbound0 a" by simp


878 
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])


879 
thus ?case by (cases "simpnum a", auto simp add: Let_def)


880 
next


881 
case (10 a) hence nb: "numbound0 a" by simp


882 
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])


883 
thus ?case by (cases "simpnum a", auto simp add: Let_def)


884 
next


885 
case (11 a) hence nb: "numbound0 a" by simp


886 
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])


887 
thus ?case by (cases "simpnum a", auto simp add: Let_def)


888 
qed(auto simp add: disj_def imp_def iff_def conj_def not_bn)


889 


890 
lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"


891 
by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)


892 
(case_tac "simpnum a",auto)+


893 


894 
consts prep :: "fm \<Rightarrow> fm"


895 
recdef prep "measure fmsize"


896 
"prep (E T) = T"


897 
"prep (E F) = F"


898 
"prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"


899 
"prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"


900 
"prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"


901 
"prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"


902 
"prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"


903 
"prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"


904 
"prep (E p) = E (prep p)"


905 
"prep (A (And p q)) = conj (prep (A p)) (prep (A q))"


906 
"prep (A p) = prep (NOT (E (NOT p)))"


907 
"prep (NOT (NOT p)) = prep p"


908 
"prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"


909 
"prep (NOT (A p)) = prep (E (NOT p))"


910 
"prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"


911 
"prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"


912 
"prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"


913 
"prep (NOT p) = not (prep p)"


914 
"prep (Or p q) = disj (prep p) (prep q)"


915 
"prep (And p q) = conj (prep p) (prep q)"


916 
"prep (Imp p q) = prep (Or (NOT p) q)"


917 
"prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"


918 
"prep p = p"


919 
(hints simp add: fmsize_pos)


920 
lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"


921 
by (induct p rule: prep.induct, auto)


922 


923 
(* Generic quantifier elimination *)


924 
consts qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"


925 
recdef qelim "measure fmsize"


926 
"qelim (E p) = (\<lambda> qe. DJ qe (qelim p qe))"


927 
"qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"


928 
"qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"


929 
"qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))"


930 
"qelim (Or p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))"


931 
"qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))"


932 
"qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"


933 
"qelim p = (\<lambda> y. simpfm p)"


934 


935 
lemma qelim_ci:


936 
assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"


937 
shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm bs (qelim p qe) = Ifm bs p)"


938 
using qe_inv DJ_qe[OF qe_inv]


939 
by(induct p rule: qelim.induct)


940 
(auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf


941 
simpfm simpfm_qf simp del: simpfm.simps)


942 


943 
consts


944 
plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)


945 
minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of \<infinity>*)


946 
recdef minusinf "measure size"


947 
"minusinf (And p q) = conj (minusinf p) (minusinf q)"


948 
"minusinf (Or p q) = disj (minusinf p) (minusinf q)"


949 
"minusinf (Eq (CN 0 c e)) = F"


950 
"minusinf (NEq (CN 0 c e)) = T"


951 
"minusinf (Lt (CN 0 c e)) = T"


952 
"minusinf (Le (CN 0 c e)) = T"


953 
"minusinf (Gt (CN 0 c e)) = F"


954 
"minusinf (Ge (CN 0 c e)) = F"


955 
"minusinf p = p"


956 


957 
recdef plusinf "measure size"


958 
"plusinf (And p q) = conj (plusinf p) (plusinf q)"


959 
"plusinf (Or p q) = disj (plusinf p) (plusinf q)"


960 
"plusinf (Eq (CN 0 c e)) = F"


961 
"plusinf (NEq (CN 0 c e)) = T"


962 
"plusinf (Lt (CN 0 c e)) = F"


963 
"plusinf (Le (CN 0 c e)) = F"


964 
"plusinf (Gt (CN 0 c e)) = T"


965 
"plusinf (Ge (CN 0 c e)) = T"


966 
"plusinf p = p"


967 


968 
consts


969 
isrlfm :: "fm \<Rightarrow> bool" (* Linearity test for fm *)


970 
recdef isrlfm "measure size"


971 
"isrlfm (And p q) = (isrlfm p \<and> isrlfm q)"


972 
"isrlfm (Or p q) = (isrlfm p \<and> isrlfm q)"


973 
"isrlfm (Eq (CN 0 c e)) = (c>0 \<and> numbound0 e)"


974 
"isrlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"


975 
"isrlfm (Lt (CN 0 c e)) = (c>0 \<and> numbound0 e)"


976 
"isrlfm (Le (CN 0 c e)) = (c>0 \<and> numbound0 e)"


977 
"isrlfm (Gt (CN 0 c e)) = (c>0 \<and> numbound0 e)"


978 
"isrlfm (Ge (CN 0 c e)) = (c>0 \<and> numbound0 e)"


979 
"isrlfm p = (isatom p \<and> (bound0 p))"


980 


981 
(* splits the bounded from the unbounded part*)


982 
consts rsplit0 :: "num \<Rightarrow> int \<times> num"


983 
recdef rsplit0 "measure num_size"


984 
"rsplit0 (Bound 0) = (1,C 0)"


985 
"rsplit0 (Add a b) = (let (ca,ta) = rsplit0 a ; (cb,tb) = rsplit0 b


986 
in (ca+cb, Add ta tb))"


987 
"rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))"


988 
"rsplit0 (Neg a) = (let (c,t) = rsplit0 a in (c,Neg t))"


989 
"rsplit0 (Mul c a) = (let (ca,ta) = rsplit0 a in (c*ca,Mul c ta))"


990 
"rsplit0 (CN 0 c a) = (let (ca,ta) = rsplit0 a in (c+ca,ta))"


991 
"rsplit0 (CN n c a) = (let (ca,ta) = rsplit0 a in (ca,CN n c ta))"


992 
"rsplit0 t = (0,t)"


993 
lemma rsplit0:


994 
shows "Inum bs ((split (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))"


995 
proof (induct t rule: rsplit0.induct)


996 
case (2 a b)


997 
let ?sa = "rsplit0 a" let ?sb = "rsplit0 b"


998 
let ?ca = "fst ?sa" let ?cb = "fst ?sb"


999 
let ?ta = "snd ?sa" let ?tb = "snd ?sb"


1000 
from prems have nb: "numbound0 (snd(rsplit0 (Add a b)))"


1001 
by(cases "rsplit0 a",auto simp add: Let_def split_def)


1002 
have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) =


1003 
Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)"


1004 
by (simp add: Let_def split_def algebra_simps)


1005 
also have "\<dots> = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a", simp_all)


1006 
finally show ?case using nb by simp


1007 
qed(auto simp add: Let_def split_def algebra_simps , simp add: right_distrib[symmetric])


1008 


1009 
(* Linearize a formula*)


1010 
definition


1011 
lt :: "int \<Rightarrow> num \<Rightarrow> fm"


1012 
where


1013 
"lt c t = (if c = 0 then (Lt t) else if c > 0 then (Lt (CN 0 c t))


1014 
else (Gt (CN 0 (c) (Neg t))))"


1015 


1016 
definition


1017 
le :: "int \<Rightarrow> num \<Rightarrow> fm"


1018 
where


1019 
"le c t = (if c = 0 then (Le t) else if c > 0 then (Le (CN 0 c t))


1020 
else (Ge (CN 0 (c) (Neg t))))"


1021 


1022 
definition


1023 
gt :: "int \<Rightarrow> num \<Rightarrow> fm"


1024 
where


1025 
"gt c t = (if c = 0 then (Gt t) else if c > 0 then (Gt (CN 0 c t))


1026 
else (Lt (CN 0 (c) (Neg t))))"


1027 


1028 
definition


1029 
ge :: "int \<Rightarrow> num \<Rightarrow> fm"


1030 
where


1031 
"ge c t = (if c = 0 then (Ge t) else if c > 0 then (Ge (CN 0 c t))


1032 
else (Le (CN 0 (c) (Neg t))))"


1033 


1034 
definition


1035 
eq :: "int \<Rightarrow> num \<Rightarrow> fm"


1036 
where


1037 
"eq c t = (if c = 0 then (Eq t) else if c > 0 then (Eq (CN 0 c t))


1038 
else (Eq (CN 0 (c) (Neg t))))"


1039 


1040 
definition


1041 
neq :: "int \<Rightarrow> num \<Rightarrow> fm"


1042 
where


1043 
"neq c t = (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t))


1044 
else (NEq (CN 0 (c) (Neg t))))"


1045 


1046 
lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (split lt (rsplit0 t)) = Ifm bs (Lt t) \<and> isrlfm (split lt (rsplit0 t))"


1047 
using rsplit0[where bs = "bs" and t="t"]


1048 
by (auto simp add: lt_def split_def,cases "snd(rsplit0 t)",auto,case_tac "nat",auto)


1049 


1050 
lemma le: "numnoabs t \<Longrightarrow> Ifm bs (split le (rsplit0 t)) = Ifm bs (Le t) \<and> isrlfm (split le (rsplit0 t))"


1051 
using rsplit0[where bs = "bs" and t="t"]


1052 
by (auto simp add: le_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)


1053 


1054 
lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (split gt (rsplit0 t)) = Ifm bs (Gt t) \<and> isrlfm (split gt (rsplit0 t))"


1055 
using rsplit0[where bs = "bs" and t="t"]


1056 
by (auto simp add: gt_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)


1057 


1058 
lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (split ge (rsplit0 t)) = Ifm bs (Ge t) \<and> isrlfm (split ge (rsplit0 t))"


1059 
using rsplit0[where bs = "bs" and t="t"]


1060 
by (auto simp add: ge_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)


1061 


1062 
lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (split eq (rsplit0 t)) = Ifm bs (Eq t) \<and> isrlfm (split eq (rsplit0 t))"


1063 
using rsplit0[where bs = "bs" and t="t"]


1064 
by (auto simp add: eq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)


1065 


1066 
lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (split neq (rsplit0 t)) = Ifm bs (NEq t) \<and> isrlfm (split neq (rsplit0 t))"


1067 
using rsplit0[where bs = "bs" and t="t"]


1068 
by (auto simp add: neq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)


1069 


1070 
lemma conj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)"


1071 
by (auto simp add: conj_def)


1072 
lemma disj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (disj p q)"


1073 
by (auto simp add: disj_def)


1074 


1075 
consts rlfm :: "fm \<Rightarrow> fm"


1076 
recdef rlfm "measure fmsize"


1077 
"rlfm (And p q) = conj (rlfm p) (rlfm q)"


1078 
"rlfm (Or p q) = disj (rlfm p) (rlfm q)"


1079 
"rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"


1080 
"rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))"


1081 
"rlfm (Lt a) = split lt (rsplit0 a)"


1082 
"rlfm (Le a) = split le (rsplit0 a)"


1083 
"rlfm (Gt a) = split gt (rsplit0 a)"


1084 
"rlfm (Ge a) = split ge (rsplit0 a)"


1085 
"rlfm (Eq a) = split eq (rsplit0 a)"


1086 
"rlfm (NEq a) = split neq (rsplit0 a)"


1087 
"rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"


1088 
"rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"


1089 
"rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"


1090 
"rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"


1091 
"rlfm (NOT (NOT p)) = rlfm p"


1092 
"rlfm (NOT T) = F"


1093 
"rlfm (NOT F) = T"


1094 
"rlfm (NOT (Lt a)) = rlfm (Ge a)"


1095 
"rlfm (NOT (Le a)) = rlfm (Gt a)"


1096 
"rlfm (NOT (Gt a)) = rlfm (Le a)"


1097 
"rlfm (NOT (Ge a)) = rlfm (Lt a)"


1098 
"rlfm (NOT (Eq a)) = rlfm (NEq a)"


1099 
"rlfm (NOT (NEq a)) = rlfm (Eq a)"


1100 
"rlfm p = p" (hints simp add: fmsize_pos)


1101 


1102 
lemma rlfm_I:


1103 
assumes qfp: "qfree p"


1104 
shows "(Ifm bs (rlfm p) = Ifm bs p) \<and> isrlfm (rlfm p)"


1105 
using qfp


1106 
by (induct p rule: rlfm.induct, auto simp add: lt le gt ge eq neq conj disj conj_lin disj_lin)


1107 


1108 
(* Operations needed for Ferrante and Rackoff *)


1109 
lemma rminusinf_inf:


1110 
assumes lp: "isrlfm p"


1111 
shows "\<exists> z. \<forall> x < z. Ifm (x#bs) (minusinf p) = Ifm (x#bs) p" (is "\<exists> z. \<forall> x. ?P z x p")


1112 
using lp


1113 
proof (induct p rule: minusinf.induct)


1114 
case (1 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto


1115 
next


1116 
case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto


1117 
next


1118 
case (3 c e)


1119 
from prems have nb: "numbound0 e" by simp


1120 
from prems have cp: "real c > 0" by simp


1121 
fix a


1122 
let ?e="Inum (a#bs) e"


1123 
let ?z = "( ?e) / real c"


1124 
{fix x


1125 
assume xz: "x < ?z"


1126 
hence "(real c * x <  ?e)"


1127 
by (simp only: pos_less_divide_eq[OF cp, where a="x" and b=" ?e"] mult_ac)


1128 
hence "real c * x + ?e < 0" by arith


1129 
hence "real c * x + ?e \<noteq> 0" by simp


1130 
with xz have "?P ?z x (Eq (CN 0 c e))"


1131 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1132 
hence "\<forall> x < ?z. ?P ?z x (Eq (CN 0 c e))" by simp


1133 
thus ?case by blast


1134 
next


1135 
case (4 c e)


1136 
from prems have nb: "numbound0 e" by simp


1137 
from prems have cp: "real c > 0" by simp


1138 
fix a


1139 
let ?e="Inum (a#bs) e"


1140 
let ?z = "( ?e) / real c"


1141 
{fix x


1142 
assume xz: "x < ?z"


1143 
hence "(real c * x <  ?e)"


1144 
by (simp only: pos_less_divide_eq[OF cp, where a="x" and b=" ?e"] mult_ac)


1145 
hence "real c * x + ?e < 0" by arith


1146 
hence "real c * x + ?e \<noteq> 0" by simp


1147 
with xz have "?P ?z x (NEq (CN 0 c e))"


1148 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1149 
hence "\<forall> x < ?z. ?P ?z x (NEq (CN 0 c e))" by simp


1150 
thus ?case by blast


1151 
next


1152 
case (5 c e)


1153 
from prems have nb: "numbound0 e" by simp


1154 
from prems have cp: "real c > 0" by simp


1155 
fix a


1156 
let ?e="Inum (a#bs) e"


1157 
let ?z = "( ?e) / real c"


1158 
{fix x


1159 
assume xz: "x < ?z"


1160 
hence "(real c * x <  ?e)"


1161 
by (simp only: pos_less_divide_eq[OF cp, where a="x" and b=" ?e"] mult_ac)


1162 
hence "real c * x + ?e < 0" by arith


1163 
with xz have "?P ?z x (Lt (CN 0 c e))"


1164 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1165 
hence "\<forall> x < ?z. ?P ?z x (Lt (CN 0 c e))" by simp


1166 
thus ?case by blast


1167 
next


1168 
case (6 c e)


1169 
from prems have nb: "numbound0 e" by simp


1170 
from prems have cp: "real c > 0" by simp


1171 
fix a


1172 
let ?e="Inum (a#bs) e"


1173 
let ?z = "( ?e) / real c"


1174 
{fix x


1175 
assume xz: "x < ?z"


1176 
hence "(real c * x <  ?e)"


1177 
by (simp only: pos_less_divide_eq[OF cp, where a="x" and b=" ?e"] mult_ac)


1178 
hence "real c * x + ?e < 0" by arith


1179 
with xz have "?P ?z x (Le (CN 0 c e))"


1180 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1181 
hence "\<forall> x < ?z. ?P ?z x (Le (CN 0 c e))" by simp


1182 
thus ?case by blast


1183 
next


1184 
case (7 c e)


1185 
from prems have nb: "numbound0 e" by simp


1186 
from prems have cp: "real c > 0" by simp


1187 
fix a


1188 
let ?e="Inum (a#bs) e"


1189 
let ?z = "( ?e) / real c"


1190 
{fix x


1191 
assume xz: "x < ?z"


1192 
hence "(real c * x <  ?e)"


1193 
by (simp only: pos_less_divide_eq[OF cp, where a="x" and b=" ?e"] mult_ac)


1194 
hence "real c * x + ?e < 0" by arith


1195 
with xz have "?P ?z x (Gt (CN 0 c e))"


1196 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1197 
hence "\<forall> x < ?z. ?P ?z x (Gt (CN 0 c e))" by simp


1198 
thus ?case by blast


1199 
next


1200 
case (8 c e)


1201 
from prems have nb: "numbound0 e" by simp


1202 
from prems have cp: "real c > 0" by simp


1203 
fix a


1204 
let ?e="Inum (a#bs) e"


1205 
let ?z = "( ?e) / real c"


1206 
{fix x


1207 
assume xz: "x < ?z"


1208 
hence "(real c * x <  ?e)"


1209 
by (simp only: pos_less_divide_eq[OF cp, where a="x" and b=" ?e"] mult_ac)


1210 
hence "real c * x + ?e < 0" by arith


1211 
with xz have "?P ?z x (Ge (CN 0 c e))"


1212 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1213 
hence "\<forall> x < ?z. ?P ?z x (Ge (CN 0 c e))" by simp


1214 
thus ?case by blast


1215 
qed simp_all


1216 


1217 
lemma rplusinf_inf:


1218 
assumes lp: "isrlfm p"


1219 
shows "\<exists> z. \<forall> x > z. Ifm (x#bs) (plusinf p) = Ifm (x#bs) p" (is "\<exists> z. \<forall> x. ?P z x p")


1220 
using lp


1221 
proof (induct p rule: isrlfm.induct)


1222 
case (1 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto


1223 
next


1224 
case (2 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto


1225 
next


1226 
case (3 c e)


1227 
from prems have nb: "numbound0 e" by simp


1228 
from prems have cp: "real c > 0" by simp


1229 
fix a


1230 
let ?e="Inum (a#bs) e"


1231 
let ?z = "( ?e) / real c"


1232 
{fix x


1233 
assume xz: "x > ?z"


1234 
with mult_strict_right_mono [OF xz cp] cp


1235 
have "(real c * x >  ?e)" by (simp add: mult_ac)


1236 
hence "real c * x + ?e > 0" by arith


1237 
hence "real c * x + ?e \<noteq> 0" by simp


1238 
with xz have "?P ?z x (Eq (CN 0 c e))"


1239 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1240 
hence "\<forall> x > ?z. ?P ?z x (Eq (CN 0 c e))" by simp


1241 
thus ?case by blast


1242 
next


1243 
case (4 c e)


1244 
from prems have nb: "numbound0 e" by simp


1245 
from prems have cp: "real c > 0" by simp


1246 
fix a


1247 
let ?e="Inum (a#bs) e"


1248 
let ?z = "( ?e) / real c"


1249 
{fix x


1250 
assume xz: "x > ?z"


1251 
with mult_strict_right_mono [OF xz cp] cp


1252 
have "(real c * x >  ?e)" by (simp add: mult_ac)


1253 
hence "real c * x + ?e > 0" by arith


1254 
hence "real c * x + ?e \<noteq> 0" by simp


1255 
with xz have "?P ?z x (NEq (CN 0 c e))"


1256 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1257 
hence "\<forall> x > ?z. ?P ?z x (NEq (CN 0 c e))" by simp


1258 
thus ?case by blast


1259 
next


1260 
case (5 c e)


1261 
from prems have nb: "numbound0 e" by simp


1262 
from prems have cp: "real c > 0" by simp


1263 
fix a


1264 
let ?e="Inum (a#bs) e"


1265 
let ?z = "( ?e) / real c"


1266 
{fix x


1267 
assume xz: "x > ?z"


1268 
with mult_strict_right_mono [OF xz cp] cp


1269 
have "(real c * x >  ?e)" by (simp add: mult_ac)


1270 
hence "real c * x + ?e > 0" by arith


1271 
with xz have "?P ?z x (Lt (CN 0 c e))"


1272 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1273 
hence "\<forall> x > ?z. ?P ?z x (Lt (CN 0 c e))" by simp


1274 
thus ?case by blast


1275 
next


1276 
case (6 c e)


1277 
from prems have nb: "numbound0 e" by simp


1278 
from prems have cp: "real c > 0" by simp


1279 
fix a


1280 
let ?e="Inum (a#bs) e"


1281 
let ?z = "( ?e) / real c"


1282 
{fix x


1283 
assume xz: "x > ?z"


1284 
with mult_strict_right_mono [OF xz cp] cp


1285 
have "(real c * x >  ?e)" by (simp add: mult_ac)


1286 
hence "real c * x + ?e > 0" by arith


1287 
with xz have "?P ?z x (Le (CN 0 c e))"


1288 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1289 
hence "\<forall> x > ?z. ?P ?z x (Le (CN 0 c e))" by simp


1290 
thus ?case by blast


1291 
next


1292 
case (7 c e)


1293 
from prems have nb: "numbound0 e" by simp


1294 
from prems have cp: "real c > 0" by simp


1295 
fix a


1296 
let ?e="Inum (a#bs) e"


1297 
let ?z = "( ?e) / real c"


1298 
{fix x


1299 
assume xz: "x > ?z"


1300 
with mult_strict_right_mono [OF xz cp] cp


1301 
have "(real c * x >  ?e)" by (simp add: mult_ac)


1302 
hence "real c * x + ?e > 0" by arith


1303 
with xz have "?P ?z x (Gt (CN 0 c e))"


1304 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1305 
hence "\<forall> x > ?z. ?P ?z x (Gt (CN 0 c e))" by simp


1306 
thus ?case by blast


1307 
next


1308 
case (8 c e)


1309 
from prems have nb: "numbound0 e" by simp


1310 
from prems have cp: "real c > 0" by simp


1311 
fix a


1312 
let ?e="Inum (a#bs) e"


1313 
let ?z = "( ?e) / real c"


1314 
{fix x


1315 
assume xz: "x > ?z"


1316 
with mult_strict_right_mono [OF xz cp] cp


1317 
have "(real c * x >  ?e)" by (simp add: mult_ac)


1318 
hence "real c * x + ?e > 0" by arith


1319 
with xz have "?P ?z x (Ge (CN 0 c e))"


1320 
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }


1321 
hence "\<forall> x > ?z. ?P ?z x (Ge (CN 0 c e))" by simp


1322 
thus ?case by blast


1323 
qed simp_all


1324 


1325 
lemma rminusinf_bound0:


1326 
assumes lp: "isrlfm p"


1327 
shows "bound0 (minusinf p)"


1328 
using lp


1329 
by (induct p rule: minusinf.induct) simp_all


1330 


1331 
lemma rplusinf_bound0:


1332 
assumes lp: "isrlfm p"


1333 
shows "bound0 (plusinf p)"


1334 
using lp


1335 
by (induct p rule: plusinf.induct) simp_all


1336 


1337 
lemma rminusinf_ex:


1338 
assumes lp: "isrlfm p"


1339 
and ex: "Ifm (a#bs) (minusinf p)"


1340 
shows "\<exists> x. Ifm (x#bs) p"


1341 
proof


1342 
from bound0_I [OF rminusinf_bound0[OF lp], where b="a" and bs ="bs"] ex


1343 
have th: "\<forall> x. Ifm (x#bs) (minusinf p)" by auto


1344 
from rminusinf_inf[OF lp, where bs="bs"]


1345 
obtain z where z_def: "\<forall>x<z. Ifm (x # bs) (minusinf p) = Ifm (x # bs) p" by blast


1346 
from th have "Ifm ((z  1)#bs) (minusinf p)" by simp


1347 
moreover have "z  1 < z" by simp


1348 
ultimately show ?thesis using z_def by auto


1349 
qed


1350 


1351 
lemma rplusinf_ex:


1352 
assumes lp: "isrlfm p"


1353 
and ex: "Ifm (a#bs) (plusinf p)"


1354 
shows "\<exists> x. Ifm (x#bs) p"


1355 
proof


1356 
from bound0_I [OF rplusinf_bound0[OF lp], where b="a" and bs ="bs"] ex


1357 
have th: "\<forall> x. Ifm (x#bs) (plusinf p)" by auto


1358 
from rplusinf_inf[OF lp, where bs="bs"]


1359 
obtain z where z_def: "\<forall>x>z. Ifm (x # bs) (plusinf p) = Ifm (x # bs) p" by blast


1360 
from th have "Ifm ((z + 1)#bs) (plusinf p)" by simp


1361 
moreover have "z + 1 > z" by simp


1362 
ultimately show ?thesis using z_def by auto


1363 
qed


1364 


1365 
consts


1366 
uset:: "fm \<Rightarrow> (num \<times> int) list"


1367 
usubst :: "fm \<Rightarrow> (num \<times> int) \<Rightarrow> fm "


1368 
recdef uset "measure size"


1369 
"uset (And p q) = (uset p @ uset q)"


1370 
"uset (Or p q) = (uset p @ uset q)"


1371 
"uset (Eq (CN 0 c e)) = [(Neg e,c)]"


1372 
"uset (NEq (CN 0 c e)) = [(Neg e,c)]"


1373 
"uset (Lt (CN 0 c e)) = [(Neg e,c)]"


1374 
"uset (Le (CN 0 c e)) = [(Neg e,c)]"


1375 
"uset (Gt (CN 0 c e)) = [(Neg e,c)]"


1376 
"uset (Ge (CN 0 c e)) = [(Neg e,c)]"


1377 
"uset p = []"


1378 
recdef usubst "measure size"


1379 
"usubst (And p q) = (\<lambda> (t,n). And (usubst p (t,n)) (usubst q (t,n)))"


1380 
"usubst (Or p q) = (\<lambda> (t,n). Or (usubst p (t,n)) (usubst q (t,n)))"


1381 
"usubst (Eq (CN 0 c e)) = (\<lambda> (t,n). Eq (Add (Mul c t) (Mul n e)))"


1382 
"usubst (NEq (CN 0 c e)) = (\<lambda> (t,n). NEq (Add (Mul c t) (Mul n e)))"


1383 
"usubst (Lt (CN 0 c e)) = (\<lambda> (t,n). Lt (Add (Mul c t) (Mul n e)))"


1384 
"usubst (Le (CN 0 c e)) = (\<lambda> (t,n). Le (Add (Mul c t) (Mul n e)))"


1385 
"usubst (Gt (CN 0 c e)) = (\<lambda> (t,n). Gt (Add (Mul c t) (Mul n e)))"


1386 
"usubst (Ge (CN 0 c e)) = (\<lambda> (t,n). Ge (Add (Mul c t) (Mul n e)))"


1387 
"usubst p = (\<lambda> (t,n). p)"


1388 


1389 
lemma usubst_I: assumes lp: "isrlfm p"


1390 
and np: "real n > 0" and nbt: "numbound0 t"


1391 
shows "(Ifm (x#bs) (usubst p (t,n)) = Ifm (((Inum (x#bs) t)/(real n))#bs) p) \<and> bound0 (usubst p (t,n))" (is "(?I x (usubst p (t,n)) = ?I ?u p) \<and> ?B p" is "(_ = ?I (?t/?n) p) \<and> _" is "(_ = ?I (?N x t /_) p) \<and> _")


1392 
using lp


1393 
proof(induct p rule: usubst.induct)


1394 
case (5 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+


1395 
have "?I ?u (Lt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) < 0)"


1396 
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp


1397 
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)"


1398 
by (simp only: pos_less_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)"


1399 
and b="0", simplified divide_zero_left]) (simp only: algebra_simps)


1400 
also have "\<dots> = (real c *?t + ?n* (?N x e) < 0)"


1401 
using np by simp


1402 
finally show ?case using nbt nb by (simp add: algebra_simps)


1403 
next


1404 
case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+


1405 
have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)"


1406 
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp


1407 
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)"


1408 
by (simp only: pos_le_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)"


1409 
and b="0", simplified divide_zero_left]) (simp only: algebra_simps)


1410 
also have "\<dots> = (real c *?t + ?n* (?N x e) \<le> 0)"


1411 
using np by simp


1412 
finally show ?case using nbt nb by (simp add: algebra_simps)


1413 
next


1414 
case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+


1415 
have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)"


1416 
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp


1417 
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)"


1418 
by (simp only: pos_divide_less_eq[OF np, where a="real c *(?t/?n) + (?N x e)"


1419 
and b="0", simplified divide_zero_left]) (simp only: algebra_simps)


1420 
also have "\<dots> = (real c *?t + ?n* (?N x e) > 0)"


1421 
using np by simp


1422 
finally show ?case using nbt nb by (simp add: algebra_simps)


1423 
next


1424 
case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+


1425 
have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)"


1426 
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp


1427 
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)"


1428 
by (simp only: pos_divide_le_eq[OF np, where a="real c *(?t/?n) + (?N x e)"


1429 
and b="0", simplified divide_zero_left]) (simp only: algebra_simps)


1430 
also have "\<dots> = (real c *?t + ?n* (?N x e) \<ge> 0)"


1431 
using np by simp


1432 
finally show ?case using nbt nb by (simp add: algebra_simps)


1433 
next


1434 
case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+


1435 
from np have np: "real n \<noteq> 0" by simp


1436 
have "?I ?u (Eq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) = 0)"


1437 
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp


1438 
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) = 0)"


1439 
by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)"


1440 
and b="0", simplified divide_zero_left]) (simp only: algebra_simps)


1441 
also have "\<dots> = (real c *?t + ?n* (?N x e) = 0)"


1442 
using np by simp


1443 
finally show ?case using nbt nb by (simp add: algebra_simps)


1444 
next


1445 
case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+


1446 
from np have np: "real n \<noteq> 0" by simp


1447 
have "?I ?u (NEq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<noteq> 0)"


1448 
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp


1449 
also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)"


1450 
by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)"


1451 
and b="0", simplified divide_zero_left]) (simp only: algebra_simps)


1452 
also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"


1453 
using np by simp


1454 
finally show ?case using nbt nb by (simp add: algebra_simps)
