src/HOL/Decision_Procs/Ferrack.thy
 author haftmann Thu Aug 19 16:08:59 2010 +0200 (2010-08-19) changeset 38558 32ad17fe2b9c parent 38549 d0385f2764d8 child 38786 e46e7a9cb622 permissions -rw-r--r--
tuned quotes
 hoelzl@30439 ` 1` ```(* Title: HOL/Decision_Procs/Ferrack.thy ``` haftmann@29789 ` 2` ``` Author: Amine Chaieb ``` haftmann@29789 ` 3` ```*) ``` haftmann@29789 ` 4` haftmann@29789 ` 5` ```theory Ferrack ``` chaieb@29818 ` 6` ```imports Complex_Main Dense_Linear_Order Efficient_Nat ``` haftmann@29789 ` 7` ```uses ("ferrack_tac.ML") ``` haftmann@29789 ` 8` ```begin ``` haftmann@29789 ` 9` haftmann@29789 ` 10` ```section {* Quantifier elimination for @{text "\ (0, 1, +, <)"} *} ``` haftmann@29789 ` 11` haftmann@29789 ` 12` ``` (*********************************************************************************) ``` haftmann@29789 ` 13` ``` (* SOME GENERAL STUFF< HAS TO BE MOVED IN SOME LIB *) ``` haftmann@29789 ` 14` ``` (*********************************************************************************) ``` haftmann@29789 ` 15` haftmann@36853 ` 16` ```primrec alluopairs:: "'a list \ ('a \ 'a) list" where ``` haftmann@29789 ` 17` ``` "alluopairs [] = []" ``` haftmann@36853 ` 18` ```| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)" ``` haftmann@29789 ` 19` haftmann@29789 ` 20` ```lemma alluopairs_set1: "set (alluopairs xs) \ {(x,y). x\ set xs \ y\ set xs}" ``` haftmann@29789 ` 21` ```by (induct xs, auto) ``` haftmann@29789 ` 22` haftmann@29789 ` 23` ```lemma alluopairs_set: ``` haftmann@29789 ` 24` ``` "\x\ set xs ; y \ set xs\ \ (x,y) \ set (alluopairs xs) \ (y,x) \ set (alluopairs xs) " ``` haftmann@29789 ` 25` ```by (induct xs, auto) ``` haftmann@29789 ` 26` haftmann@29789 ` 27` ```lemma alluopairs_ex: ``` haftmann@29789 ` 28` ``` assumes Pc: "\ x y. P x y = P y x" ``` haftmann@29789 ` 29` ``` shows "(\ x \ set xs. \ y \ set xs. P x y) = (\ (x,y) \ set (alluopairs xs). P x y)" ``` haftmann@29789 ` 30` ```proof ``` haftmann@29789 ` 31` ``` assume "\x\set xs. \y\set xs. P x y" ``` haftmann@29789 ` 32` ``` then obtain x y where x: "x \ set xs" and y:"y \ set xs" and P: "P x y" by blast ``` haftmann@29789 ` 33` ``` from alluopairs_set[OF x y] P Pc show"\(x, y)\set (alluopairs xs). P x y" ``` haftmann@29789 ` 34` ``` by auto ``` haftmann@29789 ` 35` ```next ``` haftmann@29789 ` 36` ``` assume "\(x, y)\set (alluopairs xs). P x y" ``` haftmann@29789 ` 37` ``` then obtain "x" and "y" where xy:"(x,y) \ set (alluopairs xs)" and P: "P x y" by blast+ ``` haftmann@29789 ` 38` ``` from xy have "x \ set xs \ y\ set xs" using alluopairs_set1 by blast ``` haftmann@29789 ` 39` ``` with P show "\x\set xs. \y\set xs. P x y" by blast ``` haftmann@29789 ` 40` ```qed ``` haftmann@29789 ` 41` haftmann@29789 ` 42` ```lemma nth_pos2: "0 < n \ (x#xs) ! n = xs ! (n - 1)" ``` haftmann@29789 ` 43` ```using Nat.gr0_conv_Suc ``` haftmann@29789 ` 44` ```by clarsimp ``` haftmann@29789 ` 45` haftmann@29789 ` 46` ```lemma filter_length: "length (List.filter P xs) < Suc (length xs)" ``` haftmann@29789 ` 47` ``` apply (induct xs, auto) done ``` haftmann@29789 ` 48` haftmann@29789 ` 49` haftmann@29789 ` 50` ``` (*********************************************************************************) ``` haftmann@29789 ` 51` ``` (**** SHADOW SYNTAX AND SEMANTICS ****) ``` haftmann@29789 ` 52` ``` (*********************************************************************************) ``` haftmann@29789 ` 53` haftmann@29789 ` 54` ```datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num ``` haftmann@29789 ` 55` ``` | Mul int num ``` haftmann@29789 ` 56` haftmann@29789 ` 57` ``` (* A size for num to make inductive proofs simpler*) ``` haftmann@36853 ` 58` ```primrec num_size :: "num \ nat" where ``` haftmann@29789 ` 59` ``` "num_size (C c) = 1" ``` haftmann@36853 ` 60` ```| "num_size (Bound n) = 1" ``` haftmann@36853 ` 61` ```| "num_size (Neg a) = 1 + num_size a" ``` haftmann@36853 ` 62` ```| "num_size (Add a b) = 1 + num_size a + num_size b" ``` haftmann@36853 ` 63` ```| "num_size (Sub a b) = 3 + num_size a + num_size b" ``` haftmann@36853 ` 64` ```| "num_size (Mul c a) = 1 + num_size a" ``` haftmann@36853 ` 65` ```| "num_size (CN n c a) = 3 + num_size a " ``` haftmann@29789 ` 66` haftmann@29789 ` 67` ``` (* Semantics of numeral terms (num) *) ``` haftmann@36853 ` 68` ```primrec Inum :: "real list \ num \ real" where ``` haftmann@29789 ` 69` ``` "Inum bs (C c) = (real c)" ``` haftmann@36853 ` 70` ```| "Inum bs (Bound n) = bs!n" ``` haftmann@36853 ` 71` ```| "Inum bs (CN n c a) = (real c) * (bs!n) + (Inum bs a)" ``` haftmann@36853 ` 72` ```| "Inum bs (Neg a) = -(Inum bs a)" ``` haftmann@36853 ` 73` ```| "Inum bs (Add a b) = Inum bs a + Inum bs b" ``` haftmann@36853 ` 74` ```| "Inum bs (Sub a b) = Inum bs a - Inum bs b" ``` haftmann@36853 ` 75` ```| "Inum bs (Mul c a) = (real c) * Inum bs a" ``` haftmann@29789 ` 76` ``` (* FORMULAE *) ``` haftmann@29789 ` 77` ```datatype fm = ``` haftmann@29789 ` 78` ``` T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| ``` haftmann@29789 ` 79` ``` NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm ``` haftmann@29789 ` 80` haftmann@29789 ` 81` haftmann@29789 ` 82` ``` (* A size for fm *) ``` haftmann@36853 ` 83` ```fun fmsize :: "fm \ nat" where ``` haftmann@29789 ` 84` ``` "fmsize (NOT p) = 1 + fmsize p" ``` haftmann@36853 ` 85` ```| "fmsize (And p q) = 1 + fmsize p + fmsize q" ``` haftmann@36853 ` 86` ```| "fmsize (Or p q) = 1 + fmsize p + fmsize q" ``` haftmann@36853 ` 87` ```| "fmsize (Imp p q) = 3 + fmsize p + fmsize q" ``` haftmann@36853 ` 88` ```| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)" ``` haftmann@36853 ` 89` ```| "fmsize (E p) = 1 + fmsize p" ``` haftmann@36853 ` 90` ```| "fmsize (A p) = 4+ fmsize p" ``` haftmann@36853 ` 91` ```| "fmsize p = 1" ``` haftmann@29789 ` 92` ``` (* several lemmas about fmsize *) ``` haftmann@29789 ` 93` ```lemma fmsize_pos: "fmsize p > 0" ``` haftmann@29789 ` 94` ```by (induct p rule: fmsize.induct) simp_all ``` haftmann@29789 ` 95` haftmann@29789 ` 96` ``` (* Semantics of formulae (fm) *) ``` haftmann@36853 ` 97` ```primrec Ifm ::"real list \ fm \ bool" where ``` haftmann@29789 ` 98` ``` "Ifm bs T = True" ``` haftmann@36853 ` 99` ```| "Ifm bs F = False" ``` haftmann@36853 ` 100` ```| "Ifm bs (Lt a) = (Inum bs a < 0)" ``` haftmann@36853 ` 101` ```| "Ifm bs (Gt a) = (Inum bs a > 0)" ``` haftmann@36853 ` 102` ```| "Ifm bs (Le a) = (Inum bs a \ 0)" ``` haftmann@36853 ` 103` ```| "Ifm bs (Ge a) = (Inum bs a \ 0)" ``` haftmann@36853 ` 104` ```| "Ifm bs (Eq a) = (Inum bs a = 0)" ``` haftmann@36853 ` 105` ```| "Ifm bs (NEq a) = (Inum bs a \ 0)" ``` haftmann@36853 ` 106` ```| "Ifm bs (NOT p) = (\ (Ifm bs p))" ``` haftmann@36853 ` 107` ```| "Ifm bs (And p q) = (Ifm bs p \ Ifm bs q)" ``` haftmann@36853 ` 108` ```| "Ifm bs (Or p q) = (Ifm bs p \ Ifm bs q)" ``` haftmann@36853 ` 109` ```| "Ifm bs (Imp p q) = ((Ifm bs p) \ (Ifm bs q))" ``` haftmann@36853 ` 110` ```| "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)" ``` haftmann@36853 ` 111` ```| "Ifm bs (E p) = (\ x. Ifm (x#bs) p)" ``` haftmann@36853 ` 112` ```| "Ifm bs (A p) = (\ x. Ifm (x#bs) p)" ``` haftmann@29789 ` 113` haftmann@29789 ` 114` ```lemma IfmLeSub: "\ Inum bs s = s' ; Inum bs t = t' \ \ Ifm bs (Le (Sub s t)) = (s' \ t')" ``` haftmann@29789 ` 115` ```apply simp ``` haftmann@29789 ` 116` ```done ``` haftmann@29789 ` 117` haftmann@29789 ` 118` ```lemma IfmLtSub: "\ Inum bs s = s' ; Inum bs t = t' \ \ Ifm bs (Lt (Sub s t)) = (s' < t')" ``` haftmann@29789 ` 119` ```apply simp ``` haftmann@29789 ` 120` ```done ``` haftmann@29789 ` 121` ```lemma IfmEqSub: "\ Inum bs s = s' ; Inum bs t = t' \ \ Ifm bs (Eq (Sub s t)) = (s' = t')" ``` haftmann@29789 ` 122` ```apply simp ``` haftmann@29789 ` 123` ```done ``` haftmann@29789 ` 124` ```lemma IfmNOT: " (Ifm bs p = P) \ (Ifm bs (NOT p) = (\P))" ``` haftmann@29789 ` 125` ```apply simp ``` haftmann@29789 ` 126` ```done ``` haftmann@29789 ` 127` ```lemma IfmAnd: " \ Ifm bs p = P ; Ifm bs q = Q\ \ (Ifm bs (And p q) = (P \ Q))" ``` haftmann@29789 ` 128` ```apply simp ``` haftmann@29789 ` 129` ```done ``` haftmann@29789 ` 130` ```lemma IfmOr: " \ Ifm bs p = P ; Ifm bs q = Q\ \ (Ifm bs (Or p q) = (P \ Q))" ``` haftmann@29789 ` 131` ```apply simp ``` haftmann@29789 ` 132` ```done ``` haftmann@29789 ` 133` ```lemma IfmImp: " \ Ifm bs p = P ; Ifm bs q = Q\ \ (Ifm bs (Imp p q) = (P \ Q))" ``` haftmann@29789 ` 134` ```apply simp ``` haftmann@29789 ` 135` ```done ``` haftmann@29789 ` 136` ```lemma IfmIff: " \ Ifm bs p = P ; Ifm bs q = Q\ \ (Ifm bs (Iff p q) = (P = Q))" ``` haftmann@29789 ` 137` ```apply simp ``` haftmann@29789 ` 138` ```done ``` haftmann@29789 ` 139` haftmann@29789 ` 140` ```lemma IfmE: " (!! x. Ifm (x#bs) p = P x) \ (Ifm bs (E p) = (\x. P x))" ``` haftmann@29789 ` 141` ```apply simp ``` haftmann@29789 ` 142` ```done ``` haftmann@29789 ` 143` ```lemma IfmA: " (!! x. Ifm (x#bs) p = P x) \ (Ifm bs (A p) = (\x. P x))" ``` haftmann@29789 ` 144` ```apply simp ``` haftmann@29789 ` 145` ```done ``` haftmann@29789 ` 146` haftmann@36853 ` 147` ```fun not:: "fm \ fm" where ``` haftmann@29789 ` 148` ``` "not (NOT p) = p" ``` haftmann@36853 ` 149` ```| "not T = F" ``` haftmann@36853 ` 150` ```| "not F = T" ``` haftmann@36853 ` 151` ```| "not p = NOT p" ``` haftmann@29789 ` 152` ```lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)" ``` haftmann@29789 ` 153` ```by (cases p) auto ``` haftmann@29789 ` 154` haftmann@35416 ` 155` ```definition conj :: "fm \ fm \ fm" where ``` haftmann@36853 ` 156` ``` "conj p q = (if (p = F \ q=F) then F else if p=T then q else if q=T then p else ``` haftmann@29789 ` 157` ``` if p = q then p else And p q)" ``` haftmann@29789 ` 158` ```lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)" ``` haftmann@29789 ` 159` ```by (cases "p=F \ q=F",simp_all add: conj_def) (cases p,simp_all) ``` haftmann@29789 ` 160` haftmann@35416 ` 161` ```definition disj :: "fm \ fm \ fm" where ``` haftmann@36853 ` 162` ``` "disj p q = (if (p = T \ q=T) then T else if p=F then q else if q=F then p ``` haftmann@29789 ` 163` ``` else if p=q then p else Or p q)" ``` haftmann@29789 ` 164` haftmann@29789 ` 165` ```lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)" ``` haftmann@29789 ` 166` ```by (cases "p=T \ q=T",simp_all add: disj_def) (cases p,simp_all) ``` haftmann@29789 ` 167` haftmann@35416 ` 168` ```definition imp :: "fm \ fm \ fm" where ``` haftmann@36853 ` 169` ``` "imp p q = (if (p = F \ q=T \ p=q) then T else if p=T then q else if q=F then not p ``` haftmann@29789 ` 170` ``` else Imp p q)" ``` haftmann@29789 ` 171` ```lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)" ``` haftmann@29789 ` 172` ```by (cases "p=F \ q=T",simp_all add: imp_def) ``` haftmann@29789 ` 173` haftmann@35416 ` 174` ```definition iff :: "fm \ fm \ fm" where ``` haftmann@36853 ` 175` ``` "iff p q = (if (p = q) then T else if (p = NOT q \ NOT p = q) then F else ``` haftmann@29789 ` 176` ``` 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 ``` haftmann@29789 ` 177` ``` Iff p q)" ``` haftmann@29789 ` 178` ```lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)" ``` haftmann@29789 ` 179` ``` by (unfold iff_def,cases "p=q", simp,cases "p=NOT q", simp) (cases "NOT p= q", auto) ``` haftmann@29789 ` 180` haftmann@29789 ` 181` ```lemma conj_simps: ``` haftmann@29789 ` 182` ``` "conj F Q = F" ``` haftmann@29789 ` 183` ``` "conj P F = F" ``` haftmann@29789 ` 184` ``` "conj T Q = Q" ``` haftmann@29789 ` 185` ``` "conj P T = P" ``` haftmann@29789 ` 186` ``` "conj P P = P" ``` haftmann@29789 ` 187` ``` "P \ T \ P \ F \ Q \ T \ Q \ F \ P \ Q \ conj P Q = And P Q" ``` haftmann@29789 ` 188` ``` by (simp_all add: conj_def) ``` haftmann@29789 ` 189` haftmann@29789 ` 190` ```lemma disj_simps: ``` haftmann@29789 ` 191` ``` "disj T Q = T" ``` haftmann@29789 ` 192` ``` "disj P T = T" ``` haftmann@29789 ` 193` ``` "disj F Q = Q" ``` haftmann@29789 ` 194` ``` "disj P F = P" ``` haftmann@29789 ` 195` ``` "disj P P = P" ``` haftmann@29789 ` 196` ``` "P \ T \ P \ F \ Q \ T \ Q \ F \ P \ Q \ disj P Q = Or P Q" ``` haftmann@29789 ` 197` ``` by (simp_all add: disj_def) ``` haftmann@29789 ` 198` ```lemma imp_simps: ``` haftmann@29789 ` 199` ``` "imp F Q = T" ``` haftmann@29789 ` 200` ``` "imp P T = T" ``` haftmann@29789 ` 201` ``` "imp T Q = Q" ``` haftmann@29789 ` 202` ``` "imp P F = not P" ``` haftmann@29789 ` 203` ``` "imp P P = T" ``` haftmann@29789 ` 204` ``` "P \ T \ P \ F \ P \ Q \ Q \ T \ Q \ F \ imp P Q = Imp P Q" ``` haftmann@29789 ` 205` ``` by (simp_all add: imp_def) ``` haftmann@29789 ` 206` ```lemma trivNOT: "p \ NOT p" "NOT p \ p" ``` haftmann@29789 ` 207` ```apply (induct p, auto) ``` haftmann@29789 ` 208` ```done ``` haftmann@29789 ` 209` haftmann@29789 ` 210` ```lemma iff_simps: ``` haftmann@29789 ` 211` ``` "iff p p = T" ``` haftmann@29789 ` 212` ``` "iff p (NOT p) = F" ``` haftmann@29789 ` 213` ``` "iff (NOT p) p = F" ``` haftmann@29789 ` 214` ``` "iff p F = not p" ``` haftmann@29789 ` 215` ``` "iff F p = not p" ``` haftmann@29789 ` 216` ``` "p \ NOT T \ iff T p = p" ``` haftmann@29789 ` 217` ``` "p\ NOT T \ iff p T = p" ``` haftmann@29789 ` 218` ``` "p\q \ p\ NOT q \ q\ NOT p \ p\ F \ q\ F \ p \ T \ q \ T \ iff p q = Iff p q" ``` haftmann@29789 ` 219` ``` using trivNOT ``` haftmann@29789 ` 220` ``` by (simp_all add: iff_def, cases p, auto) ``` haftmann@29789 ` 221` ``` (* Quantifier freeness *) ``` haftmann@36853 ` 222` ```fun qfree:: "fm \ bool" where ``` haftmann@29789 ` 223` ``` "qfree (E p) = False" ``` haftmann@36853 ` 224` ```| "qfree (A p) = False" ``` haftmann@36853 ` 225` ```| "qfree (NOT p) = qfree p" ``` haftmann@36853 ` 226` ```| "qfree (And p q) = (qfree p \ qfree q)" ``` haftmann@36853 ` 227` ```| "qfree (Or p q) = (qfree p \ qfree q)" ``` haftmann@36853 ` 228` ```| "qfree (Imp p q) = (qfree p \ qfree q)" ``` haftmann@36853 ` 229` ```| "qfree (Iff p q) = (qfree p \ qfree q)" ``` haftmann@36853 ` 230` ```| "qfree p = True" ``` haftmann@29789 ` 231` haftmann@29789 ` 232` ``` (* Boundedness and substitution *) ``` haftmann@36853 ` 233` ```primrec numbound0:: "num \ bool" (* a num is INDEPENDENT of Bound 0 *) where ``` haftmann@29789 ` 234` ``` "numbound0 (C c) = True" ``` haftmann@36853 ` 235` ```| "numbound0 (Bound n) = (n>0)" ``` haftmann@36853 ` 236` ```| "numbound0 (CN n c a) = (n\0 \ numbound0 a)" ``` haftmann@36853 ` 237` ```| "numbound0 (Neg a) = numbound0 a" ``` haftmann@36853 ` 238` ```| "numbound0 (Add a b) = (numbound0 a \ numbound0 b)" ``` haftmann@36853 ` 239` ```| "numbound0 (Sub a b) = (numbound0 a \ numbound0 b)" ``` haftmann@36853 ` 240` ```| "numbound0 (Mul i a) = numbound0 a" ``` haftmann@36853 ` 241` haftmann@29789 ` 242` ```lemma numbound0_I: ``` haftmann@29789 ` 243` ``` assumes nb: "numbound0 a" ``` haftmann@29789 ` 244` ``` shows "Inum (b#bs) a = Inum (b'#bs) a" ``` haftmann@29789 ` 245` ```using nb ``` haftmann@36853 ` 246` ```by (induct a) (simp_all add: nth_pos2) ``` haftmann@29789 ` 247` haftmann@36853 ` 248` ```primrec bound0:: "fm \ bool" (* A Formula is independent of Bound 0 *) where ``` haftmann@29789 ` 249` ``` "bound0 T = True" ``` haftmann@36853 ` 250` ```| "bound0 F = True" ``` haftmann@36853 ` 251` ```| "bound0 (Lt a) = numbound0 a" ``` haftmann@36853 ` 252` ```| "bound0 (Le a) = numbound0 a" ``` haftmann@36853 ` 253` ```| "bound0 (Gt a) = numbound0 a" ``` haftmann@36853 ` 254` ```| "bound0 (Ge a) = numbound0 a" ``` haftmann@36853 ` 255` ```| "bound0 (Eq a) = numbound0 a" ``` haftmann@36853 ` 256` ```| "bound0 (NEq a) = numbound0 a" ``` haftmann@36853 ` 257` ```| "bound0 (NOT p) = bound0 p" ``` haftmann@36853 ` 258` ```| "bound0 (And p q) = (bound0 p \ bound0 q)" ``` haftmann@36853 ` 259` ```| "bound0 (Or p q) = (bound0 p \ bound0 q)" ``` haftmann@36853 ` 260` ```| "bound0 (Imp p q) = ((bound0 p) \ (bound0 q))" ``` haftmann@36853 ` 261` ```| "bound0 (Iff p q) = (bound0 p \ bound0 q)" ``` haftmann@36853 ` 262` ```| "bound0 (E p) = False" ``` haftmann@36853 ` 263` ```| "bound0 (A p) = False" ``` haftmann@29789 ` 264` haftmann@29789 ` 265` ```lemma bound0_I: ``` haftmann@29789 ` 266` ``` assumes bp: "bound0 p" ``` haftmann@29789 ` 267` ``` shows "Ifm (b#bs) p = Ifm (b'#bs) p" ``` haftmann@29789 ` 268` ```using bp numbound0_I[where b="b" and bs="bs" and b'="b'"] ``` haftmann@36853 ` 269` ```by (induct p) (auto simp add: nth_pos2) ``` haftmann@29789 ` 270` haftmann@29789 ` 271` ```lemma not_qf[simp]: "qfree p \ qfree (not p)" ``` haftmann@29789 ` 272` ```by (cases p, auto) ``` haftmann@29789 ` 273` ```lemma not_bn[simp]: "bound0 p \ bound0 (not p)" ``` haftmann@29789 ` 274` ```by (cases p, auto) ``` haftmann@29789 ` 275` haftmann@29789 ` 276` haftmann@29789 ` 277` ```lemma conj_qf[simp]: "\qfree p ; qfree q\ \ qfree (conj p q)" ``` haftmann@29789 ` 278` ```using conj_def by auto ``` haftmann@29789 ` 279` ```lemma conj_nb[simp]: "\bound0 p ; bound0 q\ \ bound0 (conj p q)" ``` haftmann@29789 ` 280` ```using conj_def by auto ``` haftmann@29789 ` 281` haftmann@29789 ` 282` ```lemma disj_qf[simp]: "\qfree p ; qfree q\ \ qfree (disj p q)" ``` haftmann@29789 ` 283` ```using disj_def by auto ``` haftmann@29789 ` 284` ```lemma disj_nb[simp]: "\bound0 p ; bound0 q\ \ bound0 (disj p q)" ``` haftmann@29789 ` 285` ```using disj_def by auto ``` haftmann@29789 ` 286` haftmann@29789 ` 287` ```lemma imp_qf[simp]: "\qfree p ; qfree q\ \ qfree (imp p q)" ``` haftmann@29789 ` 288` ```using imp_def by (cases "p=F \ q=T",simp_all add: imp_def) ``` haftmann@29789 ` 289` ```lemma imp_nb[simp]: "\bound0 p ; bound0 q\ \ bound0 (imp p q)" ``` haftmann@29789 ` 290` ```using imp_def by (cases "p=F \ q=T \ p=q",simp_all add: imp_def) ``` haftmann@29789 ` 291` haftmann@29789 ` 292` ```lemma iff_qf[simp]: "\qfree p ; qfree q\ \ qfree (iff p q)" ``` haftmann@29789 ` 293` ``` by (unfold iff_def,cases "p=q", auto) ``` haftmann@29789 ` 294` ```lemma iff_nb[simp]: "\bound0 p ; bound0 q\ \ bound0 (iff p q)" ``` haftmann@29789 ` 295` ```using iff_def by (unfold iff_def,cases "p=q", auto) ``` haftmann@29789 ` 296` haftmann@36853 ` 297` ```fun decrnum:: "num \ num" where ``` haftmann@29789 ` 298` ``` "decrnum (Bound n) = Bound (n - 1)" ``` haftmann@36853 ` 299` ```| "decrnum (Neg a) = Neg (decrnum a)" ``` haftmann@36853 ` 300` ```| "decrnum (Add a b) = Add (decrnum a) (decrnum b)" ``` haftmann@36853 ` 301` ```| "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)" ``` haftmann@36853 ` 302` ```| "decrnum (Mul c a) = Mul c (decrnum a)" ``` haftmann@36853 ` 303` ```| "decrnum (CN n c a) = CN (n - 1) c (decrnum a)" ``` haftmann@36853 ` 304` ```| "decrnum a = a" ``` haftmann@29789 ` 305` haftmann@36853 ` 306` ```fun decr :: "fm \ fm" where ``` haftmann@29789 ` 307` ``` "decr (Lt a) = Lt (decrnum a)" ``` haftmann@36853 ` 308` ```| "decr (Le a) = Le (decrnum a)" ``` haftmann@36853 ` 309` ```| "decr (Gt a) = Gt (decrnum a)" ``` haftmann@36853 ` 310` ```| "decr (Ge a) = Ge (decrnum a)" ``` haftmann@36853 ` 311` ```| "decr (Eq a) = Eq (decrnum a)" ``` haftmann@36853 ` 312` ```| "decr (NEq a) = NEq (decrnum a)" ``` haftmann@36853 ` 313` ```| "decr (NOT p) = NOT (decr p)" ``` haftmann@36853 ` 314` ```| "decr (And p q) = conj (decr p) (decr q)" ``` haftmann@36853 ` 315` ```| "decr (Or p q) = disj (decr p) (decr q)" ``` haftmann@36853 ` 316` ```| "decr (Imp p q) = imp (decr p) (decr q)" ``` haftmann@36853 ` 317` ```| "decr (Iff p q) = iff (decr p) (decr q)" ``` haftmann@36853 ` 318` ```| "decr p = p" ``` haftmann@29789 ` 319` haftmann@29789 ` 320` ```lemma decrnum: assumes nb: "numbound0 t" ``` haftmann@29789 ` 321` ``` shows "Inum (x#bs) t = Inum bs (decrnum t)" ``` haftmann@29789 ` 322` ``` using nb by (induct t rule: decrnum.induct, simp_all add: nth_pos2) ``` haftmann@29789 ` 323` haftmann@29789 ` 324` ```lemma decr: assumes nb: "bound0 p" ``` haftmann@29789 ` 325` ``` shows "Ifm (x#bs) p = Ifm bs (decr p)" ``` haftmann@29789 ` 326` ``` using nb ``` haftmann@29789 ` 327` ``` by (induct p rule: decr.induct, simp_all add: nth_pos2 decrnum) ``` haftmann@29789 ` 328` haftmann@29789 ` 329` ```lemma decr_qf: "bound0 p \ qfree (decr p)" ``` haftmann@29789 ` 330` ```by (induct p, simp_all) ``` haftmann@29789 ` 331` haftmann@36853 ` 332` ```fun isatom :: "fm \ bool" (* test for atomicity *) where ``` haftmann@29789 ` 333` ``` "isatom T = True" ``` haftmann@36853 ` 334` ```| "isatom F = True" ``` haftmann@36853 ` 335` ```| "isatom (Lt a) = True" ``` haftmann@36853 ` 336` ```| "isatom (Le a) = True" ``` haftmann@36853 ` 337` ```| "isatom (Gt a) = True" ``` haftmann@36853 ` 338` ```| "isatom (Ge a) = True" ``` haftmann@36853 ` 339` ```| "isatom (Eq a) = True" ``` haftmann@36853 ` 340` ```| "isatom (NEq a) = True" ``` haftmann@36853 ` 341` ```| "isatom p = False" ``` haftmann@29789 ` 342` haftmann@29789 ` 343` ```lemma bound0_qf: "bound0 p \ qfree p" ``` haftmann@29789 ` 344` ```by (induct p, simp_all) ``` haftmann@29789 ` 345` haftmann@35416 ` 346` ```definition djf :: "('a \ fm) \ 'a \ fm \ fm" where ``` haftmann@36853 ` 347` ``` "djf f p q = (if q=T then T else if q=F then f p else ``` haftmann@29789 ` 348` ``` (let fp = f p in case fp of T \ T | F \ q | _ \ Or (f p) q))" ``` haftmann@35416 ` 349` ```definition evaldjf :: "('a \ fm) \ 'a list \ fm" where ``` haftmann@36853 ` 350` ``` "evaldjf f ps = foldr (djf f) ps F" ``` haftmann@29789 ` 351` haftmann@29789 ` 352` ```lemma djf_Or: "Ifm bs (djf f p q) = Ifm bs (Or (f p) q)" ``` haftmann@29789 ` 353` ```by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) ``` haftmann@29789 ` 354` ```(cases "f p", simp_all add: Let_def djf_def) ``` haftmann@29789 ` 355` haftmann@29789 ` 356` haftmann@29789 ` 357` ```lemma djf_simps: ``` haftmann@29789 ` 358` ``` "djf f p T = T" ``` haftmann@29789 ` 359` ``` "djf f p F = f p" ``` haftmann@29789 ` 360` ``` "q\T \ q\F \ djf f p q = (let fp = f p in case fp of T \ T | F \ q | _ \ Or (f p) q)" ``` haftmann@29789 ` 361` ``` by (simp_all add: djf_def) ``` haftmann@29789 ` 362` haftmann@29789 ` 363` ```lemma evaldjf_ex: "Ifm bs (evaldjf f ps) = (\ p \ set ps. Ifm bs (f p))" ``` haftmann@29789 ` 364` ``` by(induct ps, simp_all add: evaldjf_def djf_Or) ``` haftmann@29789 ` 365` haftmann@29789 ` 366` ```lemma evaldjf_bound0: ``` haftmann@29789 ` 367` ``` assumes nb: "\ x\ set xs. bound0 (f x)" ``` haftmann@29789 ` 368` ``` shows "bound0 (evaldjf f xs)" ``` haftmann@29789 ` 369` ``` using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) ``` haftmann@29789 ` 370` haftmann@29789 ` 371` ```lemma evaldjf_qf: ``` haftmann@29789 ` 372` ``` assumes nb: "\ x\ set xs. qfree (f x)" ``` haftmann@29789 ` 373` ``` shows "qfree (evaldjf f xs)" ``` haftmann@29789 ` 374` ``` using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) ``` haftmann@29789 ` 375` haftmann@36853 ` 376` ```fun disjuncts :: "fm \ fm list" where ``` haftmann@36853 ` 377` ``` "disjuncts (Or p q) = disjuncts p @ disjuncts q" ``` haftmann@36853 ` 378` ```| "disjuncts F = []" ``` haftmann@36853 ` 379` ```| "disjuncts p = [p]" ``` haftmann@29789 ` 380` haftmann@29789 ` 381` ```lemma disjuncts: "(\ q\ set (disjuncts p). Ifm bs q) = Ifm bs p" ``` haftmann@29789 ` 382` ```by(induct p rule: disjuncts.induct, auto) ``` haftmann@29789 ` 383` haftmann@29789 ` 384` ```lemma disjuncts_nb: "bound0 p \ \ q\ set (disjuncts p). bound0 q" ``` haftmann@29789 ` 385` ```proof- ``` haftmann@29789 ` 386` ``` assume nb: "bound0 p" ``` haftmann@29789 ` 387` ``` hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto) ``` haftmann@29789 ` 388` ``` thus ?thesis by (simp only: list_all_iff) ``` haftmann@29789 ` 389` ```qed ``` haftmann@29789 ` 390` haftmann@29789 ` 391` ```lemma disjuncts_qf: "qfree p \ \ q\ set (disjuncts p). qfree q" ``` haftmann@29789 ` 392` ```proof- ``` haftmann@29789 ` 393` ``` assume qf: "qfree p" ``` haftmann@29789 ` 394` ``` hence "list_all qfree (disjuncts p)" ``` haftmann@29789 ` 395` ``` by (induct p rule: disjuncts.induct, auto) ``` haftmann@29789 ` 396` ``` thus ?thesis by (simp only: list_all_iff) ``` haftmann@29789 ` 397` ```qed ``` haftmann@29789 ` 398` haftmann@35416 ` 399` ```definition DJ :: "(fm \ fm) \ fm \ fm" where ``` haftmann@36853 ` 400` ``` "DJ f p = evaldjf f (disjuncts p)" ``` haftmann@29789 ` 401` haftmann@29789 ` 402` ```lemma DJ: assumes fdj: "\ p q. Ifm bs (f (Or p q)) = Ifm bs (Or (f p) (f q))" ``` haftmann@29789 ` 403` ``` and fF: "f F = F" ``` haftmann@29789 ` 404` ``` shows "Ifm bs (DJ f p) = Ifm bs (f p)" ``` haftmann@29789 ` 405` ```proof- ``` haftmann@29789 ` 406` ``` have "Ifm bs (DJ f p) = (\ q \ set (disjuncts p). Ifm bs (f q))" ``` haftmann@29789 ` 407` ``` by (simp add: DJ_def evaldjf_ex) ``` haftmann@29789 ` 408` ``` also have "\ = Ifm bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto) ``` haftmann@29789 ` 409` ``` finally show ?thesis . ``` haftmann@29789 ` 410` ```qed ``` haftmann@29789 ` 411` haftmann@29789 ` 412` ```lemma DJ_qf: assumes ``` haftmann@29789 ` 413` ``` fqf: "\ p. qfree p \ qfree (f p)" ``` haftmann@29789 ` 414` ``` shows "\p. qfree p \ qfree (DJ f p) " ``` haftmann@29789 ` 415` ```proof(clarify) ``` haftmann@29789 ` 416` ``` fix p assume qf: "qfree p" ``` haftmann@29789 ` 417` ``` have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def) ``` haftmann@29789 ` 418` ``` from disjuncts_qf[OF qf] have "\ q\ set (disjuncts p). qfree q" . ``` haftmann@29789 ` 419` ``` with fqf have th':"\ q\ set (disjuncts p). qfree (f q)" by blast ``` haftmann@29789 ` 420` ``` ``` haftmann@29789 ` 421` ``` from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp ``` haftmann@29789 ` 422` ```qed ``` haftmann@29789 ` 423` haftmann@29789 ` 424` ```lemma DJ_qe: assumes qe: "\ bs p. qfree p \ qfree (qe p) \ (Ifm bs (qe p) = Ifm bs (E p))" ``` haftmann@29789 ` 425` ``` shows "\ bs p. qfree p \ qfree (DJ qe p) \ (Ifm bs ((DJ qe p)) = Ifm bs (E p))" ``` haftmann@29789 ` 426` ```proof(clarify) ``` haftmann@29789 ` 427` ``` fix p::fm and bs ``` haftmann@29789 ` 428` ``` assume qf: "qfree p" ``` haftmann@29789 ` 429` ``` from qe have qth: "\ p. qfree p \ qfree (qe p)" by blast ``` haftmann@29789 ` 430` ``` from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto ``` haftmann@29789 ` 431` ``` have "Ifm bs (DJ qe p) = (\ q\ set (disjuncts p). Ifm bs (qe q))" ``` haftmann@29789 ` 432` ``` by (simp add: DJ_def evaldjf_ex) ``` haftmann@29789 ` 433` ``` also have "\ = (\ q \ set(disjuncts p). Ifm bs (E q))" using qe disjuncts_qf[OF qf] by auto ``` haftmann@29789 ` 434` ``` also have "\ = Ifm bs (E p)" by (induct p rule: disjuncts.induct, auto) ``` haftmann@29789 ` 435` ``` finally show "qfree (DJ qe p) \ Ifm bs (DJ qe p) = Ifm bs (E p)" using qfth by blast ``` haftmann@29789 ` 436` ```qed ``` haftmann@29789 ` 437` ``` (* Simplification *) ``` haftmann@36853 ` 438` haftmann@36853 ` 439` ```fun maxcoeff:: "num \ int" where ``` haftmann@29789 ` 440` ``` "maxcoeff (C i) = abs i" ``` haftmann@36853 ` 441` ```| "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)" ``` haftmann@36853 ` 442` ```| "maxcoeff t = 1" ``` haftmann@29789 ` 443` haftmann@29789 ` 444` ```lemma maxcoeff_pos: "maxcoeff t \ 0" ``` haftmann@29789 ` 445` ``` by (induct t rule: maxcoeff.induct, auto) ``` haftmann@29789 ` 446` haftmann@36853 ` 447` ```fun numgcdh:: "num \ int \ int" where ``` huffman@31706 ` 448` ``` "numgcdh (C i) = (\g. gcd i g)" ``` haftmann@36853 ` 449` ```| "numgcdh (CN n c t) = (\g. gcd c (numgcdh t g))" ``` haftmann@36853 ` 450` ```| "numgcdh t = (\g. 1)" ``` haftmann@36853 ` 451` haftmann@36853 ` 452` ```definition numgcd :: "num \ int" where ``` haftmann@36853 ` 453` ``` "numgcd t = numgcdh t (maxcoeff t)" ``` haftmann@29789 ` 454` haftmann@36853 ` 455` ```fun reducecoeffh:: "num \ int \ num" where ``` haftmann@29789 ` 456` ``` "reducecoeffh (C i) = (\ g. C (i div g))" ``` haftmann@36853 ` 457` ```| "reducecoeffh (CN n c t) = (\ g. CN n (c div g) (reducecoeffh t g))" ``` haftmann@36853 ` 458` ```| "reducecoeffh t = (\g. t)" ``` haftmann@29789 ` 459` haftmann@36853 ` 460` ```definition reducecoeff :: "num \ num" where ``` haftmann@36853 ` 461` ``` "reducecoeff t = ``` haftmann@29789 ` 462` ``` (let g = numgcd t in ``` haftmann@29789 ` 463` ``` if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)" ``` haftmann@29789 ` 464` haftmann@36853 ` 465` ```fun dvdnumcoeff:: "num \ int \ bool" where ``` haftmann@29789 ` 466` ``` "dvdnumcoeff (C i) = (\ g. g dvd i)" ``` haftmann@36853 ` 467` ```| "dvdnumcoeff (CN n c t) = (\ g. g dvd c \ (dvdnumcoeff t g))" ``` haftmann@36853 ` 468` ```| "dvdnumcoeff t = (\g. False)" ``` haftmann@29789 ` 469` haftmann@29789 ` 470` ```lemma dvdnumcoeff_trans: ``` haftmann@29789 ` 471` ``` assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'" ``` haftmann@29789 ` 472` ``` shows "dvdnumcoeff t g" ``` haftmann@29789 ` 473` ``` using dgt' gdg ``` nipkow@30042 ` 474` ``` by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg]) ``` haftmann@29789 ` 475` nipkow@30042 ` 476` ```declare dvd_trans [trans add] ``` haftmann@29789 ` 477` haftmann@29789 ` 478` ```lemma natabs0: "(nat (abs x) = 0) = (x = 0)" ``` haftmann@29789 ` 479` ```by arith ``` haftmann@29789 ` 480` haftmann@29789 ` 481` ```lemma numgcd0: ``` haftmann@29789 ` 482` ``` assumes g0: "numgcd t = 0" ``` haftmann@29789 ` 483` ``` shows "Inum bs t = 0" ``` haftmann@29789 ` 484` ``` using g0[simplified numgcd_def] ``` haftmann@32642 ` 485` ``` by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos min_max.sup_absorb2) ``` haftmann@29789 ` 486` haftmann@29789 ` 487` ```lemma numgcdh_pos: assumes gp: "g \ 0" shows "numgcdh t g \ 0" ``` haftmann@29789 ` 488` ``` using gp ``` huffman@31706 ` 489` ``` by (induct t rule: numgcdh.induct, auto) ``` haftmann@29789 ` 490` haftmann@29789 ` 491` ```lemma numgcd_pos: "numgcd t \0" ``` haftmann@29789 ` 492` ``` by (simp add: numgcd_def numgcdh_pos maxcoeff_pos) ``` haftmann@29789 ` 493` haftmann@29789 ` 494` ```lemma reducecoeffh: ``` haftmann@29789 ` 495` ``` assumes gt: "dvdnumcoeff t g" and gp: "g > 0" ``` haftmann@29789 ` 496` ``` shows "real g *(Inum bs (reducecoeffh t g)) = Inum bs t" ``` haftmann@29789 ` 497` ``` using gt ``` haftmann@29789 ` 498` ```proof(induct t rule: reducecoeffh.induct) ``` haftmann@29789 ` 499` ``` case (1 i) hence gd: "g dvd i" by simp ``` haftmann@29789 ` 500` ``` from gp have gnz: "g \ 0" by simp ``` haftmann@29789 ` 501` ``` from prems show ?case by (simp add: real_of_int_div[OF gnz gd]) ``` haftmann@29789 ` 502` ```next ``` haftmann@29789 ` 503` ``` case (2 n c t) hence gd: "g dvd c" by simp ``` haftmann@29789 ` 504` ``` from gp have gnz: "g \ 0" by simp ``` haftmann@29789 ` 505` ``` from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) ``` haftmann@29789 ` 506` ```qed (auto simp add: numgcd_def gp) ``` haftmann@36853 ` 507` haftmann@36853 ` 508` ```fun ismaxcoeff:: "num \ int \ bool" where ``` haftmann@29789 ` 509` ``` "ismaxcoeff (C i) = (\ x. abs i \ x)" ``` haftmann@36853 ` 510` ```| "ismaxcoeff (CN n c t) = (\x. abs c \ x \ (ismaxcoeff t x))" ``` haftmann@36853 ` 511` ```| "ismaxcoeff t = (\x. True)" ``` haftmann@29789 ` 512` haftmann@29789 ` 513` ```lemma ismaxcoeff_mono: "ismaxcoeff t c \ c \ c' \ ismaxcoeff t c'" ``` haftmann@29789 ` 514` ```by (induct t rule: ismaxcoeff.induct, auto) ``` haftmann@29789 ` 515` haftmann@29789 ` 516` ```lemma maxcoeff_ismaxcoeff: "ismaxcoeff t (maxcoeff t)" ``` haftmann@29789 ` 517` ```proof (induct t rule: maxcoeff.induct) ``` haftmann@29789 ` 518` ``` case (2 n c t) ``` haftmann@29789 ` 519` ``` hence H:"ismaxcoeff t (maxcoeff t)" . ``` haftmann@29789 ` 520` ``` have thh: "maxcoeff t \ max (abs c) (maxcoeff t)" by (simp add: le_maxI2) ``` haftmann@29789 ` 521` ``` from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1) ``` haftmann@29789 ` 522` ```qed simp_all ``` haftmann@29789 ` 523` huffman@31706 ` 524` ```lemma zgcd_gt1: "gcd i j > (1::int) \ ((abs i > 1 \ abs j > 1) \ (abs i = 0 \ abs j > 1) \ (abs i > 1 \ abs j = 0))" ``` huffman@31706 ` 525` ``` apply (cases "abs i = 0", simp_all add: gcd_int_def) ``` haftmann@29789 ` 526` ``` apply (cases "abs j = 0", simp_all) ``` haftmann@29789 ` 527` ``` apply (cases "abs i = 1", simp_all) ``` haftmann@29789 ` 528` ``` apply (cases "abs j = 1", simp_all) ``` haftmann@29789 ` 529` ``` apply auto ``` haftmann@29789 ` 530` ``` done ``` haftmann@29789 ` 531` ```lemma numgcdh0:"numgcdh t m = 0 \ m =0" ``` huffman@31706 ` 532` ``` by (induct t rule: numgcdh.induct, auto) ``` haftmann@29789 ` 533` haftmann@29789 ` 534` ```lemma dvdnumcoeff_aux: ``` haftmann@29789 ` 535` ``` assumes "ismaxcoeff t m" and mp:"m \ 0" and "numgcdh t m > 1" ``` haftmann@29789 ` 536` ``` shows "dvdnumcoeff t (numgcdh t m)" ``` haftmann@29789 ` 537` ```using prems ``` haftmann@29789 ` 538` ```proof(induct t rule: numgcdh.induct) ``` haftmann@29789 ` 539` ``` case (2 n c t) ``` haftmann@29789 ` 540` ``` let ?g = "numgcdh t m" ``` huffman@31706 ` 541` ``` from prems have th:"gcd c ?g > 1" by simp ``` haftmann@29789 ` 542` ``` from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"] ``` haftmann@29789 ` 543` ``` have "(abs c > 1 \ ?g > 1) \ (abs c = 0 \ ?g > 1) \ (abs c > 1 \ ?g = 0)" by simp ``` haftmann@29789 ` 544` ``` moreover {assume "abs c > 1" and gp: "?g > 1" with prems ``` haftmann@29789 ` 545` ``` have th: "dvdnumcoeff t ?g" by simp ``` huffman@31706 ` 546` ``` have th': "gcd c ?g dvd ?g" by simp ``` huffman@31706 ` 547` ``` from dvdnumcoeff_trans[OF th' th] have ?case by simp } ``` haftmann@29789 ` 548` ``` moreover {assume "abs c = 0 \ ?g > 1" ``` haftmann@29789 ` 549` ``` with prems have th: "dvdnumcoeff t ?g" by simp ``` huffman@31706 ` 550` ``` have th': "gcd c ?g dvd ?g" by simp ``` huffman@31706 ` 551` ``` from dvdnumcoeff_trans[OF th' th] have ?case by simp ``` haftmann@29789 ` 552` ``` hence ?case by simp } ``` haftmann@29789 ` 553` ``` moreover {assume "abs c > 1" and g0:"?g = 0" ``` haftmann@29789 ` 554` ``` from numgcdh0[OF g0] have "m=0". with prems have ?case by simp } ``` haftmann@29789 ` 555` ``` ultimately show ?case by blast ``` huffman@31706 ` 556` ```qed auto ``` haftmann@29789 ` 557` haftmann@29789 ` 558` ```lemma dvdnumcoeff_aux2: ``` haftmann@29789 ` 559` ``` assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \ numgcd t > 0" ``` haftmann@29789 ` 560` ``` using prems ``` haftmann@29789 ` 561` ```proof (simp add: numgcd_def) ``` haftmann@29789 ` 562` ``` let ?mc = "maxcoeff t" ``` haftmann@29789 ` 563` ``` let ?g = "numgcdh t ?mc" ``` haftmann@29789 ` 564` ``` have th1: "ismaxcoeff t ?mc" by (rule maxcoeff_ismaxcoeff) ``` haftmann@29789 ` 565` ``` have th2: "?mc \ 0" by (rule maxcoeff_pos) ``` haftmann@29789 ` 566` ``` assume H: "numgcdh t ?mc > 1" ``` haftmann@29789 ` 567` ``` from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" . ``` haftmann@29789 ` 568` ```qed ``` haftmann@29789 ` 569` haftmann@29789 ` 570` ```lemma reducecoeff: "real (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t" ``` haftmann@29789 ` 571` ```proof- ``` haftmann@29789 ` 572` ``` let ?g = "numgcd t" ``` haftmann@29789 ` 573` ``` have "?g \ 0" by (simp add: numgcd_pos) ``` wenzelm@32960 ` 574` ``` hence "?g = 0 \ ?g = 1 \ ?g > 1" by auto ``` haftmann@29789 ` 575` ``` moreover {assume "?g = 0" hence ?thesis by (simp add: numgcd0)} ``` haftmann@29789 ` 576` ``` moreover {assume "?g = 1" hence ?thesis by (simp add: reducecoeff_def)} ``` haftmann@29789 ` 577` ``` moreover { assume g1:"?g > 1" ``` haftmann@29789 ` 578` ``` from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" and g0: "?g > 0" by blast+ ``` haftmann@29789 ` 579` ``` from reducecoeffh[OF th1 g0, where bs="bs"] g1 have ?thesis ``` haftmann@29789 ` 580` ``` by (simp add: reducecoeff_def Let_def)} ``` haftmann@29789 ` 581` ``` ultimately show ?thesis by blast ``` haftmann@29789 ` 582` ```qed ``` haftmann@29789 ` 583` haftmann@29789 ` 584` ```lemma reducecoeffh_numbound0: "numbound0 t \ numbound0 (reducecoeffh t g)" ``` haftmann@29789 ` 585` ```by (induct t rule: reducecoeffh.induct, auto) ``` haftmann@29789 ` 586` haftmann@29789 ` 587` ```lemma reducecoeff_numbound0: "numbound0 t \ numbound0 (reducecoeff t)" ``` haftmann@29789 ` 588` ```using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def) ``` haftmann@29789 ` 589` haftmann@29789 ` 590` ```consts ``` haftmann@29789 ` 591` ``` numadd:: "num \ num \ num" ``` haftmann@36853 ` 592` haftmann@29789 ` 593` ```recdef numadd "measure (\ (t,s). size t + size s)" ``` haftmann@29789 ` 594` ``` "numadd (CN n1 c1 r1,CN n2 c2 r2) = ``` haftmann@29789 ` 595` ``` (if n1=n2 then ``` haftmann@29789 ` 596` ``` (let c = c1 + c2 ``` haftmann@29789 ` 597` ``` in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2)))) ``` haftmann@29789 ` 598` ``` else if n1 \ n2 then (CN n1 c1 (numadd (r1,CN n2 c2 r2))) ``` haftmann@29789 ` 599` ``` else (CN n2 c2 (numadd (CN n1 c1 r1,r2))))" ``` haftmann@29789 ` 600` ``` "numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))" ``` haftmann@29789 ` 601` ``` "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))" ``` haftmann@29789 ` 602` ``` "numadd (C b1, C b2) = C (b1+b2)" ``` haftmann@29789 ` 603` ``` "numadd (a,b) = Add a b" ``` haftmann@29789 ` 604` haftmann@29789 ` 605` ```lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" ``` haftmann@29789 ` 606` ```apply (induct t s rule: numadd.induct, simp_all add: Let_def) ``` haftmann@29789 ` 607` ```apply (case_tac "c1+c2 = 0",case_tac "n1 \ n2", simp_all) ``` haftmann@29789 ` 608` ```apply (case_tac "n1 = n2", simp_all add: algebra_simps) ``` haftmann@29789 ` 609` ```by (simp only: left_distrib[symmetric],simp) ``` haftmann@29789 ` 610` haftmann@29789 ` 611` ```lemma numadd_nb[simp]: "\ numbound0 t ; numbound0 s\ \ numbound0 (numadd (t,s))" ``` haftmann@29789 ` 612` ```by (induct t s rule: numadd.induct, auto simp add: Let_def) ``` haftmann@29789 ` 613` haftmann@36853 ` 614` ```fun nummul:: "num \ int \ num" where ``` haftmann@29789 ` 615` ``` "nummul (C j) = (\ i. C (i*j))" ``` haftmann@36853 ` 616` ```| "nummul (CN n c a) = (\ i. CN n (i*c) (nummul a i))" ``` haftmann@36853 ` 617` ```| "nummul t = (\ i. Mul i t)" ``` haftmann@29789 ` 618` haftmann@29789 ` 619` ```lemma nummul[simp]: "\ i. Inum bs (nummul t i) = Inum bs (Mul i t)" ``` haftmann@29789 ` 620` ```by (induct t rule: nummul.induct, auto simp add: algebra_simps) ``` haftmann@29789 ` 621` haftmann@29789 ` 622` ```lemma nummul_nb[simp]: "\ i. numbound0 t \ numbound0 (nummul t i)" ``` haftmann@29789 ` 623` ```by (induct t rule: nummul.induct, auto ) ``` haftmann@29789 ` 624` haftmann@35416 ` 625` ```definition numneg :: "num \ num" where ``` haftmann@36853 ` 626` ``` "numneg t = nummul t (- 1)" ``` haftmann@29789 ` 627` haftmann@35416 ` 628` ```definition numsub :: "num \ num \ num" where ``` haftmann@36853 ` 629` ``` "numsub s t = (if s = t then C 0 else numadd (s,numneg t))" ``` haftmann@29789 ` 630` haftmann@29789 ` 631` ```lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)" ``` haftmann@29789 ` 632` ```using numneg_def by simp ``` haftmann@29789 ` 633` haftmann@29789 ` 634` ```lemma numneg_nb[simp]: "numbound0 t \ numbound0 (numneg t)" ``` haftmann@29789 ` 635` ```using numneg_def by simp ``` haftmann@29789 ` 636` haftmann@29789 ` 637` ```lemma numsub[simp]: "Inum bs (numsub a b) = Inum bs (Sub a b)" ``` haftmann@29789 ` 638` ```using numsub_def by simp ``` haftmann@29789 ` 639` haftmann@29789 ` 640` ```lemma numsub_nb[simp]: "\ numbound0 t ; numbound0 s\ \ numbound0 (numsub t s)" ``` haftmann@29789 ` 641` ```using numsub_def by simp ``` haftmann@29789 ` 642` haftmann@36853 ` 643` ```primrec simpnum:: "num \ num" where ``` haftmann@29789 ` 644` ``` "simpnum (C j) = C j" ``` haftmann@36853 ` 645` ```| "simpnum (Bound n) = CN n 1 (C 0)" ``` haftmann@36853 ` 646` ```| "simpnum (Neg t) = numneg (simpnum t)" ``` haftmann@36853 ` 647` ```| "simpnum (Add t s) = numadd (simpnum t,simpnum s)" ``` haftmann@36853 ` 648` ```| "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)" ``` haftmann@36853 ` 649` ```| "simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum t) i)" ``` haftmann@36853 ` 650` ```| "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0),simpnum t))" ``` haftmann@29789 ` 651` haftmann@29789 ` 652` ```lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t" ``` haftmann@36853 ` 653` ```by (induct t) simp_all ``` haftmann@29789 ` 654` haftmann@29789 ` 655` ```lemma simpnum_numbound0[simp]: ``` haftmann@29789 ` 656` ``` "numbound0 t \ numbound0 (simpnum t)" ``` haftmann@36853 ` 657` ```by (induct t) simp_all ``` haftmann@29789 ` 658` haftmann@36853 ` 659` ```fun nozerocoeff:: "num \ bool" where ``` haftmann@29789 ` 660` ``` "nozerocoeff (C c) = True" ``` haftmann@36853 ` 661` ```| "nozerocoeff (CN n c t) = (c\0 \ nozerocoeff t)" ``` haftmann@36853 ` 662` ```| "nozerocoeff t = True" ``` haftmann@29789 ` 663` haftmann@29789 ` 664` ```lemma numadd_nz : "nozerocoeff a \ nozerocoeff b \ nozerocoeff (numadd (a,b))" ``` haftmann@29789 ` 665` ```by (induct a b rule: numadd.induct,auto simp add: Let_def) ``` haftmann@29789 ` 666` haftmann@29789 ` 667` ```lemma nummul_nz : "\ i. i\0 \ nozerocoeff a \ nozerocoeff (nummul a i)" ``` haftmann@29789 ` 668` ```by (induct a rule: nummul.induct,auto simp add: Let_def numadd_nz) ``` haftmann@29789 ` 669` haftmann@29789 ` 670` ```lemma numneg_nz : "nozerocoeff a \ nozerocoeff (numneg a)" ``` haftmann@29789 ` 671` ```by (simp add: numneg_def nummul_nz) ``` haftmann@29789 ` 672` haftmann@29789 ` 673` ```lemma numsub_nz: "nozerocoeff a \ nozerocoeff b \ nozerocoeff (numsub a b)" ``` haftmann@29789 ` 674` ```by (simp add: numsub_def numneg_nz numadd_nz) ``` haftmann@29789 ` 675` haftmann@29789 ` 676` ```lemma simpnum_nz: "nozerocoeff (simpnum t)" ``` haftmann@36853 ` 677` ```by(induct t) (simp_all add: numadd_nz numneg_nz numsub_nz nummul_nz) ``` haftmann@29789 ` 678` haftmann@29789 ` 679` ```lemma maxcoeff_nz: "nozerocoeff t \ maxcoeff t = 0 \ t = C 0" ``` haftmann@29789 ` 680` ```proof (induct t rule: maxcoeff.induct) ``` haftmann@29789 ` 681` ``` case (2 n c t) ``` haftmann@29789 ` 682` ``` hence cnz: "c \0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ ``` haftmann@29789 ` 683` ``` have "max (abs c) (maxcoeff t) \ abs c" by (simp add: le_maxI1) ``` haftmann@29789 ` 684` ``` with cnz have "max (abs c) (maxcoeff t) > 0" by arith ``` haftmann@29789 ` 685` ``` with prems show ?case by simp ``` haftmann@29789 ` 686` ```qed auto ``` haftmann@29789 ` 687` haftmann@29789 ` 688` ```lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0" ``` haftmann@29789 ` 689` ```proof- ``` haftmann@29789 ` 690` ``` from g0 have th:"numgcdh t (maxcoeff t) = 0" by (simp add: numgcd_def) ``` haftmann@29789 ` 691` ``` from numgcdh0[OF th] have th:"maxcoeff t = 0" . ``` haftmann@29789 ` 692` ``` from maxcoeff_nz[OF nz th] show ?thesis . ``` haftmann@29789 ` 693` ```qed ``` haftmann@29789 ` 694` haftmann@35416 ` 695` ```definition simp_num_pair :: "(num \ int) \ num \ int" where ``` haftmann@36853 ` 696` ``` "simp_num_pair = (\ (t,n). (if n = 0 then (C 0, 0) else ``` haftmann@29789 ` 697` ``` (let t' = simpnum t ; g = numgcd t' in ``` huffman@31706 ` 698` ``` if g > 1 then (let g' = gcd n g in ``` haftmann@29789 ` 699` ``` if g' = 1 then (t',n) ``` haftmann@29789 ` 700` ``` else (reducecoeffh t' g', n div g')) ``` haftmann@29789 ` 701` ``` else (t',n))))" ``` haftmann@29789 ` 702` haftmann@29789 ` 703` ```lemma simp_num_pair_ci: ``` haftmann@29789 ` 704` ``` shows "((\ (t,n). Inum bs t / real n) (simp_num_pair (t,n))) = ((\ (t,n). Inum bs t / real n) (t,n))" ``` haftmann@29789 ` 705` ``` (is "?lhs = ?rhs") ``` haftmann@29789 ` 706` ```proof- ``` haftmann@29789 ` 707` ``` let ?t' = "simpnum t" ``` haftmann@29789 ` 708` ``` let ?g = "numgcd ?t'" ``` huffman@31706 ` 709` ``` let ?g' = "gcd n ?g" ``` haftmann@29789 ` 710` ``` {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)} ``` haftmann@29789 ` 711` ``` moreover ``` haftmann@29789 ` 712` ``` { assume nnz: "n \ 0" ``` haftmann@29789 ` 713` ``` {assume "\ ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)} ``` haftmann@29789 ` 714` ``` moreover ``` haftmann@29789 ` 715` ``` {assume g1:"?g>1" hence g0: "?g > 0" by simp ``` huffman@31706 ` 716` ``` from g1 nnz have gp0: "?g' \ 0" by simp ``` nipkow@31952 ` 717` ``` hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith ``` haftmann@29789 ` 718` ``` hence "?g'= 1 \ ?g' > 1" by arith ``` haftmann@29789 ` 719` ``` moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)} ``` haftmann@29789 ` 720` ``` moreover {assume g'1:"?g'>1" ``` wenzelm@32960 ` 721` ``` from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" .. ``` wenzelm@32960 ` 722` ``` let ?tt = "reducecoeffh ?t' ?g'" ``` wenzelm@32960 ` 723` ``` let ?t = "Inum bs ?tt" ``` wenzelm@32960 ` 724` ``` have gpdg: "?g' dvd ?g" by simp ``` wenzelm@32960 ` 725` ``` have gpdd: "?g' dvd n" by simp ``` wenzelm@32960 ` 726` ``` have gpdgp: "?g' dvd ?g'" by simp ``` wenzelm@32960 ` 727` ``` from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] ``` wenzelm@32960 ` 728` ``` have th2:"real ?g' * ?t = Inum bs ?t'" by simp ``` wenzelm@32960 ` 729` ``` from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) ``` wenzelm@32960 ` 730` ``` also have "\ = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp ``` wenzelm@32960 ` 731` ``` also have "\ = (Inum bs ?t' / real n)" ``` wenzelm@32960 ` 732` ``` using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp ``` wenzelm@32960 ` 733` ``` finally have "?lhs = Inum bs t / real n" by (simp add: simpnum_ci) ``` wenzelm@32960 ` 734` ``` then have ?thesis using prems by (simp add: simp_num_pair_def)} ``` haftmann@29789 ` 735` ``` ultimately have ?thesis by blast} ``` haftmann@29789 ` 736` ``` ultimately have ?thesis by blast} ``` haftmann@29789 ` 737` ``` ultimately show ?thesis by blast ``` haftmann@29789 ` 738` ```qed ``` haftmann@29789 ` 739` haftmann@29789 ` 740` ```lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')" ``` haftmann@29789 ` 741` ``` shows "numbound0 t' \ n' >0" ``` haftmann@29789 ` 742` ```proof- ``` haftmann@29789 ` 743` ``` let ?t' = "simpnum t" ``` haftmann@29789 ` 744` ``` let ?g = "numgcd ?t'" ``` huffman@31706 ` 745` ``` let ?g' = "gcd n ?g" ``` haftmann@29789 ` 746` ``` {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)} ``` haftmann@29789 ` 747` ``` moreover ``` haftmann@29789 ` 748` ``` { assume nnz: "n \ 0" ``` haftmann@29789 ` 749` ``` {assume "\ ?g > 1" hence ?thesis using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)} ``` haftmann@29789 ` 750` ``` moreover ``` haftmann@29789 ` 751` ``` {assume g1:"?g>1" hence g0: "?g > 0" by simp ``` huffman@31706 ` 752` ``` from g1 nnz have gp0: "?g' \ 0" by simp ``` nipkow@31952 ` 753` ``` hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith ``` haftmann@29789 ` 754` ``` hence "?g'= 1 \ ?g' > 1" by arith ``` haftmann@29789 ` 755` ``` moreover {assume "?g'=1" hence ?thesis using prems ``` wenzelm@32960 ` 756` ``` by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)} ``` haftmann@29789 ` 757` ``` moreover {assume g'1:"?g'>1" ``` wenzelm@32960 ` 758` ``` have gpdg: "?g' dvd ?g" by simp ``` wenzelm@32960 ` 759` ``` have gpdd: "?g' dvd n" by simp ``` wenzelm@32960 ` 760` ``` have gpdgp: "?g' dvd ?g'" by simp ``` wenzelm@32960 ` 761` ``` from zdvd_imp_le[OF gpdd np] have g'n: "?g' \ n" . ``` wenzelm@32960 ` 762` ``` from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]] ``` wenzelm@32960 ` 763` ``` have "n div ?g' >0" by simp ``` wenzelm@32960 ` 764` ``` hence ?thesis using prems ``` wenzelm@32960 ` 765` ``` by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0)} ``` haftmann@29789 ` 766` ``` ultimately have ?thesis by blast} ``` haftmann@29789 ` 767` ``` ultimately have ?thesis by blast} ``` haftmann@29789 ` 768` ``` ultimately show ?thesis by blast ``` haftmann@29789 ` 769` ```qed ``` haftmann@29789 ` 770` haftmann@36853 ` 771` ```fun simpfm :: "fm \ fm" where ``` haftmann@29789 ` 772` ``` "simpfm (And p q) = conj (simpfm p) (simpfm q)" ``` haftmann@36853 ` 773` ```| "simpfm (Or p q) = disj (simpfm p) (simpfm q)" ``` haftmann@36853 ` 774` ```| "simpfm (Imp p q) = imp (simpfm p) (simpfm q)" ``` haftmann@36853 ` 775` ```| "simpfm (Iff p q) = iff (simpfm p) (simpfm q)" ``` haftmann@36853 ` 776` ```| "simpfm (NOT p) = not (simpfm p)" ``` haftmann@36853 ` 777` ```| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \ if (v < 0) then T else F ``` haftmann@29789 ` 778` ``` | _ \ Lt a')" ``` haftmann@36853 ` 779` ```| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ Le a')" ``` haftmann@36853 ` 780` ```| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \ if (v > 0) then T else F | _ \ Gt a')" ``` haftmann@36853 ` 781` ```| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ Ge a')" ``` haftmann@36853 ` 782` ```| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \ if (v = 0) then T else F | _ \ Eq a')" ``` haftmann@36853 ` 783` ```| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ NEq a')" ``` haftmann@36853 ` 784` ```| "simpfm p = p" ``` haftmann@29789 ` 785` ```lemma simpfm: "Ifm bs (simpfm p) = Ifm bs p" ``` haftmann@29789 ` 786` ```proof(induct p rule: simpfm.induct) ``` haftmann@29789 ` 787` ``` case (6 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp ``` haftmann@29789 ` 788` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` haftmann@29789 ` 789` ``` moreover {assume "\ (\ v. ?sa = C v)" hence ?case using sa ``` haftmann@29789 ` 790` ``` by (cases ?sa, simp_all add: Let_def)} ``` haftmann@29789 ` 791` ``` ultimately show ?case by blast ``` haftmann@29789 ` 792` ```next ``` haftmann@29789 ` 793` ``` case (7 a) let ?sa = "simpnum a" ``` haftmann@29789 ` 794` ``` from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp ``` haftmann@29789 ` 795` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` haftmann@29789 ` 796` ``` moreover {assume "\ (\ v. ?sa = C v)" hence ?case using sa ``` haftmann@29789 ` 797` ``` by (cases ?sa, simp_all add: Let_def)} ``` haftmann@29789 ` 798` ``` ultimately show ?case by blast ``` haftmann@29789 ` 799` ```next ``` haftmann@29789 ` 800` ``` case (8 a) let ?sa = "simpnum a" ``` haftmann@29789 ` 801` ``` from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp ``` haftmann@29789 ` 802` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` haftmann@29789 ` 803` ``` moreover {assume "\ (\ v. ?sa = C v)" hence ?case using sa ``` haftmann@29789 ` 804` ``` by (cases ?sa, simp_all add: Let_def)} ``` haftmann@29789 ` 805` ``` ultimately show ?case by blast ``` haftmann@29789 ` 806` ```next ``` haftmann@29789 ` 807` ``` case (9 a) let ?sa = "simpnum a" ``` haftmann@29789 ` 808` ``` from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp ``` haftmann@29789 ` 809` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` haftmann@29789 ` 810` ``` moreover {assume "\ (\ v. ?sa = C v)" hence ?case using sa ``` haftmann@29789 ` 811` ``` by (cases ?sa, simp_all add: Let_def)} ``` haftmann@29789 ` 812` ``` ultimately show ?case by blast ``` haftmann@29789 ` 813` ```next ``` haftmann@29789 ` 814` ``` case (10 a) let ?sa = "simpnum a" ``` haftmann@29789 ` 815` ``` from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp ``` haftmann@29789 ` 816` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` haftmann@29789 ` 817` ``` moreover {assume "\ (\ v. ?sa = C v)" hence ?case using sa ``` haftmann@29789 ` 818` ``` by (cases ?sa, simp_all add: Let_def)} ``` haftmann@29789 ` 819` ``` ultimately show ?case by blast ``` haftmann@29789 ` 820` ```next ``` haftmann@29789 ` 821` ``` case (11 a) let ?sa = "simpnum a" ``` haftmann@29789 ` 822` ``` from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp ``` haftmann@29789 ` 823` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` haftmann@29789 ` 824` ``` moreover {assume "\ (\ v. ?sa = C v)" hence ?case using sa ``` haftmann@29789 ` 825` ``` by (cases ?sa, simp_all add: Let_def)} ``` haftmann@29789 ` 826` ``` ultimately show ?case by blast ``` haftmann@29789 ` 827` ```qed (induct p rule: simpfm.induct, simp_all add: conj disj imp iff not) ``` haftmann@29789 ` 828` haftmann@29789 ` 829` haftmann@29789 ` 830` ```lemma simpfm_bound0: "bound0 p \ bound0 (simpfm p)" ``` haftmann@29789 ` 831` ```proof(induct p rule: simpfm.induct) ``` haftmann@29789 ` 832` ``` case (6 a) hence nb: "numbound0 a" by simp ``` haftmann@29789 ` 833` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` haftmann@29789 ` 834` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def) ``` haftmann@29789 ` 835` ```next ``` haftmann@29789 ` 836` ``` case (7 a) hence nb: "numbound0 a" by simp ``` haftmann@29789 ` 837` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` haftmann@29789 ` 838` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def) ``` haftmann@29789 ` 839` ```next ``` haftmann@29789 ` 840` ``` case (8 a) hence nb: "numbound0 a" by simp ``` haftmann@29789 ` 841` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` haftmann@29789 ` 842` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def) ``` haftmann@29789 ` 843` ```next ``` haftmann@29789 ` 844` ``` case (9 a) hence nb: "numbound0 a" by simp ``` haftmann@29789 ` 845` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` haftmann@29789 ` 846` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def) ``` haftmann@29789 ` 847` ```next ``` haftmann@29789 ` 848` ``` case (10 a) hence nb: "numbound0 a" by simp ``` haftmann@29789 ` 849` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` haftmann@29789 ` 850` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def) ``` haftmann@29789 ` 851` ```next ``` haftmann@29789 ` 852` ``` case (11 a) hence nb: "numbound0 a" by simp ``` haftmann@29789 ` 853` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` haftmann@29789 ` 854` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def) ``` haftmann@29789 ` 855` ```qed(auto simp add: disj_def imp_def iff_def conj_def not_bn) ``` haftmann@29789 ` 856` haftmann@29789 ` 857` ```lemma simpfm_qf: "qfree p \ qfree (simpfm p)" ``` haftmann@29789 ` 858` ```by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def) ``` haftmann@29789 ` 859` ``` (case_tac "simpnum a",auto)+ ``` haftmann@29789 ` 860` haftmann@29789 ` 861` ```consts prep :: "fm \ fm" ``` haftmann@29789 ` 862` ```recdef prep "measure fmsize" ``` haftmann@29789 ` 863` ``` "prep (E T) = T" ``` haftmann@29789 ` 864` ``` "prep (E F) = F" ``` haftmann@29789 ` 865` ``` "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))" ``` haftmann@29789 ` 866` ``` "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))" ``` haftmann@29789 ` 867` ``` "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" ``` haftmann@29789 ` 868` ``` "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))" ``` haftmann@29789 ` 869` ``` "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))" ``` haftmann@29789 ` 870` ``` "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))" ``` haftmann@29789 ` 871` ``` "prep (E p) = E (prep p)" ``` haftmann@29789 ` 872` ``` "prep (A (And p q)) = conj (prep (A p)) (prep (A q))" ``` haftmann@29789 ` 873` ``` "prep (A p) = prep (NOT (E (NOT p)))" ``` haftmann@29789 ` 874` ``` "prep (NOT (NOT p)) = prep p" ``` haftmann@29789 ` 875` ``` "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))" ``` haftmann@29789 ` 876` ``` "prep (NOT (A p)) = prep (E (NOT p))" ``` haftmann@29789 ` 877` ``` "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))" ``` haftmann@29789 ` 878` ``` "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))" ``` haftmann@29789 ` 879` ``` "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))" ``` haftmann@29789 ` 880` ``` "prep (NOT p) = not (prep p)" ``` haftmann@29789 ` 881` ``` "prep (Or p q) = disj (prep p) (prep q)" ``` haftmann@29789 ` 882` ``` "prep (And p q) = conj (prep p) (prep q)" ``` haftmann@29789 ` 883` ``` "prep (Imp p q) = prep (Or (NOT p) q)" ``` haftmann@29789 ` 884` ``` "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))" ``` haftmann@29789 ` 885` ``` "prep p = p" ``` haftmann@29789 ` 886` ```(hints simp add: fmsize_pos) ``` haftmann@29789 ` 887` ```lemma prep: "\ bs. Ifm bs (prep p) = Ifm bs p" ``` haftmann@29789 ` 888` ```by (induct p rule: prep.induct, auto) ``` haftmann@29789 ` 889` haftmann@29789 ` 890` ``` (* Generic quantifier elimination *) ``` haftmann@36853 ` 891` ```function (sequential) qelim :: "fm \ (fm \ fm) \ fm" where ``` haftmann@29789 ` 892` ``` "qelim (E p) = (\ qe. DJ qe (qelim p qe))" ``` haftmann@36853 ` 893` ```| "qelim (A p) = (\ qe. not (qe ((qelim (NOT p) qe))))" ``` haftmann@36853 ` 894` ```| "qelim (NOT p) = (\ qe. not (qelim p qe))" ``` haftmann@36853 ` 895` ```| "qelim (And p q) = (\ qe. conj (qelim p qe) (qelim q qe))" ``` haftmann@36853 ` 896` ```| "qelim (Or p q) = (\ qe. disj (qelim p qe) (qelim q qe))" ``` haftmann@36853 ` 897` ```| "qelim (Imp p q) = (\ qe. imp (qelim p qe) (qelim q qe))" ``` haftmann@36853 ` 898` ```| "qelim (Iff p q) = (\ qe. iff (qelim p qe) (qelim q qe))" ``` haftmann@36853 ` 899` ```| "qelim p = (\ y. simpfm p)" ``` haftmann@36853 ` 900` ```by pat_completeness auto ``` haftmann@36853 ` 901` ```termination qelim by (relation "measure fmsize") simp_all ``` haftmann@29789 ` 902` haftmann@29789 ` 903` ```lemma qelim_ci: ``` haftmann@29789 ` 904` ``` assumes qe_inv: "\ bs p. qfree p \ qfree (qe p) \ (Ifm bs (qe p) = Ifm bs (E p))" ``` haftmann@29789 ` 905` ``` shows "\ bs. qfree (qelim p qe) \ (Ifm bs (qelim p qe) = Ifm bs p)" ``` haftmann@29789 ` 906` ```using qe_inv DJ_qe[OF qe_inv] ``` haftmann@29789 ` 907` ```by(induct p rule: qelim.induct) ``` haftmann@29789 ` 908` ```(auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf ``` haftmann@29789 ` 909` ``` simpfm simpfm_qf simp del: simpfm.simps) ``` haftmann@29789 ` 910` haftmann@36853 ` 911` ```fun minusinf:: "fm \ fm" (* Virtual substitution of -\*) where ``` haftmann@29789 ` 912` ``` "minusinf (And p q) = conj (minusinf p) (minusinf q)" ``` haftmann@36853 ` 913` ```| "minusinf (Or p q) = disj (minusinf p) (minusinf q)" ``` haftmann@36853 ` 914` ```| "minusinf (Eq (CN 0 c e)) = F" ``` haftmann@36853 ` 915` ```| "minusinf (NEq (CN 0 c e)) = T" ``` haftmann@36853 ` 916` ```| "minusinf (Lt (CN 0 c e)) = T" ``` haftmann@36853 ` 917` ```| "minusinf (Le (CN 0 c e)) = T" ``` haftmann@36853 ` 918` ```| "minusinf (Gt (CN 0 c e)) = F" ``` haftmann@36853 ` 919` ```| "minusinf (Ge (CN 0 c e)) = F" ``` haftmann@36853 ` 920` ```| "minusinf p = p" ``` haftmann@29789 ` 921` haftmann@36853 ` 922` ```fun plusinf:: "fm \ fm" (* Virtual substitution of +\*) where ``` haftmann@29789 ` 923` ``` "plusinf (And p q) = conj (plusinf p) (plusinf q)" ``` haftmann@36853 ` 924` ```| "plusinf (Or p q) = disj (plusinf p) (plusinf q)" ``` haftmann@36853 ` 925` ```| "plusinf (Eq (CN 0 c e)) = F" ``` haftmann@36853 ` 926` ```| "plusinf (NEq (CN 0 c e)) = T" ``` haftmann@36853 ` 927` ```| "plusinf (Lt (CN 0 c e)) = F" ``` haftmann@36853 ` 928` ```| "plusinf (Le (CN 0 c e)) = F" ``` haftmann@36853 ` 929` ```| "plusinf (Gt (CN 0 c e)) = T" ``` haftmann@36853 ` 930` ```| "plusinf (Ge (CN 0 c e)) = T" ``` haftmann@36853 ` 931` ```| "plusinf p = p" ``` haftmann@29789 ` 932` haftmann@36853 ` 933` ```fun isrlfm :: "fm \ bool" (* Linearity test for fm *) where ``` haftmann@29789 ` 934` ``` "isrlfm (And p q) = (isrlfm p \ isrlfm q)" ``` haftmann@36853 ` 935` ```| "isrlfm (Or p q) = (isrlfm p \ isrlfm q)" ``` haftmann@36853 ` 936` ```| "isrlfm (Eq (CN 0 c e)) = (c>0 \ numbound0 e)" ``` haftmann@36853 ` 937` ```| "isrlfm (NEq (CN 0 c e)) = (c>0 \ numbound0 e)" ``` haftmann@36853 ` 938` ```| "isrlfm (Lt (CN 0 c e)) = (c>0 \ numbound0 e)" ``` haftmann@36853 ` 939` ```| "isrlfm (Le (CN 0 c e)) = (c>0 \ numbound0 e)" ``` haftmann@36853 ` 940` ```| "isrlfm (Gt (CN 0 c e)) = (c>0 \ numbound0 e)" ``` haftmann@36853 ` 941` ```| "isrlfm (Ge (CN 0 c e)) = (c>0 \ numbound0 e)" ``` haftmann@36853 ` 942` ```| "isrlfm p = (isatom p \ (bound0 p))" ``` haftmann@29789 ` 943` haftmann@29789 ` 944` ``` (* splits the bounded from the unbounded part*) ``` haftmann@36853 ` 945` ```function (sequential) rsplit0 :: "num \ int \ num" where ``` haftmann@29789 ` 946` ``` "rsplit0 (Bound 0) = (1,C 0)" ``` haftmann@36853 ` 947` ```| "rsplit0 (Add a b) = (let (ca,ta) = rsplit0 a ; (cb,tb) = rsplit0 b ``` haftmann@29789 ` 948` ``` in (ca+cb, Add ta tb))" ``` haftmann@36853 ` 949` ```| "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))" ``` haftmann@36853 ` 950` ```| "rsplit0 (Neg a) = (let (c,t) = rsplit0 a in (-c,Neg t))" ``` haftmann@36853 ` 951` ```| "rsplit0 (Mul c a) = (let (ca,ta) = rsplit0 a in (c*ca,Mul c ta))" ``` haftmann@36853 ` 952` ```| "rsplit0 (CN 0 c a) = (let (ca,ta) = rsplit0 a in (c+ca,ta))" ``` haftmann@36853 ` 953` ```| "rsplit0 (CN n c a) = (let (ca,ta) = rsplit0 a in (ca,CN n c ta))" ``` haftmann@36853 ` 954` ```| "rsplit0 t = (0,t)" ``` haftmann@36853 ` 955` ```by pat_completeness auto ``` haftmann@36853 ` 956` ```termination rsplit0 by (relation "measure num_size") simp_all ``` haftmann@36853 ` 957` haftmann@29789 ` 958` ```lemma rsplit0: ``` haftmann@29789 ` 959` ``` shows "Inum bs ((split (CN 0)) (rsplit0 t)) = Inum bs t \ numbound0 (snd (rsplit0 t))" ``` haftmann@29789 ` 960` ```proof (induct t rule: rsplit0.induct) ``` haftmann@29789 ` 961` ``` case (2 a b) ``` haftmann@29789 ` 962` ``` let ?sa = "rsplit0 a" let ?sb = "rsplit0 b" ``` haftmann@29789 ` 963` ``` let ?ca = "fst ?sa" let ?cb = "fst ?sb" ``` haftmann@29789 ` 964` ``` let ?ta = "snd ?sa" let ?tb = "snd ?sb" ``` haftmann@29789 ` 965` ``` from prems have nb: "numbound0 (snd(rsplit0 (Add a b)))" ``` haftmann@36853 ` 966` ``` by (cases "rsplit0 a") (auto simp add: Let_def split_def) ``` haftmann@29789 ` 967` ``` have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) = ``` haftmann@29789 ` 968` ``` Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)" ``` haftmann@29789 ` 969` ``` by (simp add: Let_def split_def algebra_simps) ``` haftmann@36853 ` 970` ``` also have "\ = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a") auto ``` haftmann@29789 ` 971` ``` finally show ?case using nb by simp ``` haftmann@36853 ` 972` ```qed (auto simp add: Let_def split_def algebra_simps , simp add: right_distrib[symmetric]) ``` haftmann@29789 ` 973` haftmann@29789 ` 974` ``` (* Linearize a formula*) ``` haftmann@29789 ` 975` ```definition ``` haftmann@29789 ` 976` ``` lt :: "int \ num \ fm" ``` haftmann@29789 ` 977` ```where ``` haftmann@29789 ` 978` ``` "lt c t = (if c = 0 then (Lt t) else if c > 0 then (Lt (CN 0 c t)) ``` haftmann@29789 ` 979` ``` else (Gt (CN 0 (-c) (Neg t))))" ``` haftmann@29789 ` 980` haftmann@29789 ` 981` ```definition ``` haftmann@29789 ` 982` ``` le :: "int \ num \ fm" ``` haftmann@29789 ` 983` ```where ``` haftmann@29789 ` 984` ``` "le c t = (if c = 0 then (Le t) else if c > 0 then (Le (CN 0 c t)) ``` haftmann@29789 ` 985` ``` else (Ge (CN 0 (-c) (Neg t))))" ``` haftmann@29789 ` 986` haftmann@29789 ` 987` ```definition ``` haftmann@29789 ` 988` ``` gt :: "int \ num \ fm" ``` haftmann@29789 ` 989` ```where ``` haftmann@29789 ` 990` ``` "gt c t = (if c = 0 then (Gt t) else if c > 0 then (Gt (CN 0 c t)) ``` haftmann@29789 ` 991` ``` else (Lt (CN 0 (-c) (Neg t))))" ``` haftmann@29789 ` 992` haftmann@29789 ` 993` ```definition ``` haftmann@29789 ` 994` ``` ge :: "int \ num \ fm" ``` haftmann@29789 ` 995` ```where ``` haftmann@29789 ` 996` ``` "ge c t = (if c = 0 then (Ge t) else if c > 0 then (Ge (CN 0 c t)) ``` haftmann@29789 ` 997` ``` else (Le (CN 0 (-c) (Neg t))))" ``` haftmann@29789 ` 998` haftmann@29789 ` 999` ```definition ``` haftmann@29789 ` 1000` ``` eq :: "int \ num \ fm" ``` haftmann@29789 ` 1001` ```where ``` haftmann@29789 ` 1002` ``` "eq c t = (if c = 0 then (Eq t) else if c > 0 then (Eq (CN 0 c t)) ``` haftmann@29789 ` 1003` ``` else (Eq (CN 0 (-c) (Neg t))))" ``` haftmann@29789 ` 1004` haftmann@29789 ` 1005` ```definition ``` haftmann@29789 ` 1006` ``` neq :: "int \ num \ fm" ``` haftmann@29789 ` 1007` ```where ``` haftmann@29789 ` 1008` ``` "neq c t = (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t)) ``` haftmann@29789 ` 1009` ``` else (NEq (CN 0 (-c) (Neg t))))" ``` haftmann@29789 ` 1010` haftmann@29789 ` 1011` ```lemma lt: "numnoabs t \ Ifm bs (split lt (rsplit0 t)) = Ifm bs (Lt t) \ isrlfm (split lt (rsplit0 t))" ``` haftmann@29789 ` 1012` ```using rsplit0[where bs = "bs" and t="t"] ``` haftmann@29789 ` 1013` ```by (auto simp add: lt_def split_def,cases "snd(rsplit0 t)",auto,case_tac "nat",auto) ``` haftmann@29789 ` 1014` haftmann@29789 ` 1015` ```lemma le: "numnoabs t \ Ifm bs (split le (rsplit0 t)) = Ifm bs (Le t) \ isrlfm (split le (rsplit0 t))" ``` haftmann@29789 ` 1016` ```using rsplit0[where bs = "bs" and t="t"] ``` haftmann@29789 ` 1017` ```by (auto simp add: le_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto) ``` haftmann@29789 ` 1018` haftmann@29789 ` 1019` ```lemma gt: "numnoabs t \ Ifm bs (split gt (rsplit0 t)) = Ifm bs (Gt t) \ isrlfm (split gt (rsplit0 t))" ``` haftmann@29789 ` 1020` ```using rsplit0[where bs = "bs" and t="t"] ``` haftmann@29789 ` 1021` ```by (auto simp add: gt_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto) ``` haftmann@29789 ` 1022` haftmann@29789 ` 1023` ```lemma ge: "numnoabs t \ Ifm bs (split ge (rsplit0 t)) = Ifm bs (Ge t) \ isrlfm (split ge (rsplit0 t))" ``` haftmann@29789 ` 1024` ```using rsplit0[where bs = "bs" and t="t"] ``` haftmann@29789 ` 1025` ```by (auto simp add: ge_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto) ``` haftmann@29789 ` 1026` haftmann@29789 ` 1027` ```lemma eq: "numnoabs t \ Ifm bs (split eq (rsplit0 t)) = Ifm bs (Eq t) \ isrlfm (split eq (rsplit0 t))" ``` haftmann@29789 ` 1028` ```using rsplit0[where bs = "bs" and t="t"] ``` haftmann@29789 ` 1029` ```by (auto simp add: eq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto) ``` haftmann@29789 ` 1030` haftmann@29789 ` 1031` ```lemma neq: "numnoabs t \ Ifm bs (split neq (rsplit0 t)) = Ifm bs (NEq t) \ isrlfm (split neq (rsplit0 t))" ``` haftmann@29789 ` 1032` ```using rsplit0[where bs = "bs" and t="t"] ``` haftmann@29789 ` 1033` ```by (auto simp add: neq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto) ``` haftmann@29789 ` 1034` haftmann@29789 ` 1035` ```lemma conj_lin: "isrlfm p \ isrlfm q \ isrlfm (conj p q)" ``` haftmann@29789 ` 1036` ```by (auto simp add: conj_def) ``` haftmann@29789 ` 1037` ```lemma disj_lin: "isrlfm p \ isrlfm q \ isrlfm (disj p q)" ``` haftmann@29789 ` 1038` ```by (auto simp add: disj_def) ``` haftmann@29789 ` 1039` haftmann@29789 ` 1040` ```consts rlfm :: "fm \ fm" ``` haftmann@29789 ` 1041` ```recdef rlfm "measure fmsize" ``` haftmann@29789 ` 1042` ``` "rlfm (And p q) = conj (rlfm p) (rlfm q)" ``` haftmann@29789 ` 1043` ``` "rlfm (Or p q) = disj (rlfm p) (rlfm q)" ``` haftmann@29789 ` 1044` ``` "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)" ``` haftmann@29789 ` 1045` ``` "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))" ``` haftmann@29789 ` 1046` ``` "rlfm (Lt a) = split lt (rsplit0 a)" ``` haftmann@29789 ` 1047` ``` "rlfm (Le a) = split le (rsplit0 a)" ``` haftmann@29789 ` 1048` ``` "rlfm (Gt a) = split gt (rsplit0 a)" ``` haftmann@29789 ` 1049` ``` "rlfm (Ge a) = split ge (rsplit0 a)" ``` haftmann@29789 ` 1050` ``` "rlfm (Eq a) = split eq (rsplit0 a)" ``` haftmann@29789 ` 1051` ``` "rlfm (NEq a) = split neq (rsplit0 a)" ``` haftmann@29789 ` 1052` ``` "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))" ``` haftmann@29789 ` 1053` ``` "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))" ``` haftmann@29789 ` 1054` ``` "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))" ``` haftmann@29789 ` 1055` ``` "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))" ``` haftmann@29789 ` 1056` ``` "rlfm (NOT (NOT p)) = rlfm p" ``` haftmann@29789 ` 1057` ``` "rlfm (NOT T) = F" ``` haftmann@29789 ` 1058` ``` "rlfm (NOT F) = T" ``` haftmann@29789 ` 1059` ``` "rlfm (NOT (Lt a)) = rlfm (Ge a)" ``` haftmann@29789 ` 1060` ``` "rlfm (NOT (Le a)) = rlfm (Gt a)" ``` haftmann@29789 ` 1061` ``` "rlfm (NOT (Gt a)) = rlfm (Le a)" ``` haftmann@29789 ` 1062` ``` "rlfm (NOT (Ge a)) = rlfm (Lt a)" ``` haftmann@29789 ` 1063` ``` "rlfm (NOT (Eq a)) = rlfm (NEq a)" ``` haftmann@29789 ` 1064` ``` "rlfm (NOT (NEq a)) = rlfm (Eq a)" ``` haftmann@29789 ` 1065` ``` "rlfm p = p" (hints simp add: fmsize_pos) ``` haftmann@29789 ` 1066` haftmann@29789 ` 1067` ```lemma rlfm_I: ``` haftmann@29789 ` 1068` ``` assumes qfp: "qfree p" ``` haftmann@29789 ` 1069` ``` shows "(Ifm bs (rlfm p) = Ifm bs p) \ isrlfm (rlfm p)" ``` haftmann@29789 ` 1070` ``` using qfp ``` haftmann@29789 ` 1071` ```by (induct p rule: rlfm.induct, auto simp add: lt le gt ge eq neq conj disj conj_lin disj_lin) ``` haftmann@29789 ` 1072` haftmann@29789 ` 1073` ``` (* Operations needed for Ferrante and Rackoff *) ``` haftmann@29789 ` 1074` ```lemma rminusinf_inf: ``` haftmann@29789 ` 1075` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1076` ``` shows "\ z. \ x < z. Ifm (x#bs) (minusinf p) = Ifm (x#bs) p" (is "\ z. \ x. ?P z x p") ``` haftmann@29789 ` 1077` ```using lp ``` haftmann@29789 ` 1078` ```proof (induct p rule: minusinf.induct) ``` haftmann@29789 ` 1079` ``` case (1 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto ``` haftmann@29789 ` 1080` ```next ``` haftmann@29789 ` 1081` ``` case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto ``` haftmann@29789 ` 1082` ```next ``` haftmann@29789 ` 1083` ``` case (3 c e) ``` haftmann@29789 ` 1084` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1085` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1086` ``` fix a ``` haftmann@29789 ` 1087` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1088` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1089` ``` {fix x ``` haftmann@29789 ` 1090` ``` assume xz: "x < ?z" ``` haftmann@29789 ` 1091` ``` hence "(real c * x < - ?e)" ``` haftmann@29789 ` 1092` ``` by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) ``` haftmann@29789 ` 1093` ``` hence "real c * x + ?e < 0" by arith ``` haftmann@29789 ` 1094` ``` hence "real c * x + ?e \ 0" by simp ``` haftmann@29789 ` 1095` ``` with xz have "?P ?z x (Eq (CN 0 c e))" ``` haftmann@29789 ` 1096` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1097` ``` hence "\ x < ?z. ?P ?z x (Eq (CN 0 c e))" by simp ``` haftmann@29789 ` 1098` ``` thus ?case by blast ``` haftmann@29789 ` 1099` ```next ``` haftmann@29789 ` 1100` ``` case (4 c e) ``` haftmann@29789 ` 1101` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1102` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1103` ``` fix a ``` haftmann@29789 ` 1104` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1105` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1106` ``` {fix x ``` haftmann@29789 ` 1107` ``` assume xz: "x < ?z" ``` haftmann@29789 ` 1108` ``` hence "(real c * x < - ?e)" ``` haftmann@29789 ` 1109` ``` by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) ``` haftmann@29789 ` 1110` ``` hence "real c * x + ?e < 0" by arith ``` haftmann@29789 ` 1111` ``` hence "real c * x + ?e \ 0" by simp ``` haftmann@29789 ` 1112` ``` with xz have "?P ?z x (NEq (CN 0 c e))" ``` haftmann@29789 ` 1113` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1114` ``` hence "\ x < ?z. ?P ?z x (NEq (CN 0 c e))" by simp ``` haftmann@29789 ` 1115` ``` thus ?case by blast ``` haftmann@29789 ` 1116` ```next ``` haftmann@29789 ` 1117` ``` case (5 c e) ``` haftmann@29789 ` 1118` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1119` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1120` ``` fix a ``` haftmann@29789 ` 1121` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1122` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1123` ``` {fix x ``` haftmann@29789 ` 1124` ``` assume xz: "x < ?z" ``` haftmann@29789 ` 1125` ``` hence "(real c * x < - ?e)" ``` haftmann@29789 ` 1126` ``` by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) ``` haftmann@29789 ` 1127` ``` hence "real c * x + ?e < 0" by arith ``` haftmann@29789 ` 1128` ``` with xz have "?P ?z x (Lt (CN 0 c e))" ``` haftmann@29789 ` 1129` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1130` ``` hence "\ x < ?z. ?P ?z x (Lt (CN 0 c e))" by simp ``` haftmann@29789 ` 1131` ``` thus ?case by blast ``` haftmann@29789 ` 1132` ```next ``` haftmann@29789 ` 1133` ``` case (6 c e) ``` haftmann@29789 ` 1134` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1135` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1136` ``` fix a ``` haftmann@29789 ` 1137` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1138` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1139` ``` {fix x ``` haftmann@29789 ` 1140` ``` assume xz: "x < ?z" ``` haftmann@29789 ` 1141` ``` hence "(real c * x < - ?e)" ``` haftmann@29789 ` 1142` ``` by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) ``` haftmann@29789 ` 1143` ``` hence "real c * x + ?e < 0" by arith ``` haftmann@29789 ` 1144` ``` with xz have "?P ?z x (Le (CN 0 c e))" ``` haftmann@29789 ` 1145` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1146` ``` hence "\ x < ?z. ?P ?z x (Le (CN 0 c e))" by simp ``` haftmann@29789 ` 1147` ``` thus ?case by blast ``` haftmann@29789 ` 1148` ```next ``` haftmann@29789 ` 1149` ``` case (7 c e) ``` haftmann@29789 ` 1150` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1151` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1152` ``` fix a ``` haftmann@29789 ` 1153` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1154` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1155` ``` {fix x ``` haftmann@29789 ` 1156` ``` assume xz: "x < ?z" ``` haftmann@29789 ` 1157` ``` hence "(real c * x < - ?e)" ``` haftmann@29789 ` 1158` ``` by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) ``` haftmann@29789 ` 1159` ``` hence "real c * x + ?e < 0" by arith ``` haftmann@29789 ` 1160` ``` with xz have "?P ?z x (Gt (CN 0 c e))" ``` haftmann@29789 ` 1161` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1162` ``` hence "\ x < ?z. ?P ?z x (Gt (CN 0 c e))" by simp ``` haftmann@29789 ` 1163` ``` thus ?case by blast ``` haftmann@29789 ` 1164` ```next ``` haftmann@29789 ` 1165` ``` case (8 c e) ``` haftmann@29789 ` 1166` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1167` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1168` ``` fix a ``` haftmann@29789 ` 1169` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1170` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1171` ``` {fix x ``` haftmann@29789 ` 1172` ``` assume xz: "x < ?z" ``` haftmann@29789 ` 1173` ``` hence "(real c * x < - ?e)" ``` haftmann@29789 ` 1174` ``` by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) ``` haftmann@29789 ` 1175` ``` hence "real c * x + ?e < 0" by arith ``` haftmann@29789 ` 1176` ``` with xz have "?P ?z x (Ge (CN 0 c e))" ``` haftmann@29789 ` 1177` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1178` ``` hence "\ x < ?z. ?P ?z x (Ge (CN 0 c e))" by simp ``` haftmann@29789 ` 1179` ``` thus ?case by blast ``` haftmann@29789 ` 1180` ```qed simp_all ``` haftmann@29789 ` 1181` haftmann@29789 ` 1182` ```lemma rplusinf_inf: ``` haftmann@29789 ` 1183` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1184` ``` shows "\ z. \ x > z. Ifm (x#bs) (plusinf p) = Ifm (x#bs) p" (is "\ z. \ x. ?P z x p") ``` haftmann@29789 ` 1185` ```using lp ``` haftmann@29789 ` 1186` ```proof (induct p rule: isrlfm.induct) ``` haftmann@29789 ` 1187` ``` case (1 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto ``` haftmann@29789 ` 1188` ```next ``` haftmann@29789 ` 1189` ``` case (2 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto ``` haftmann@29789 ` 1190` ```next ``` haftmann@29789 ` 1191` ``` case (3 c e) ``` haftmann@29789 ` 1192` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1193` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1194` ``` fix a ``` haftmann@29789 ` 1195` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1196` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1197` ``` {fix x ``` haftmann@29789 ` 1198` ``` assume xz: "x > ?z" ``` haftmann@29789 ` 1199` ``` with mult_strict_right_mono [OF xz cp] cp ``` haftmann@29789 ` 1200` ``` have "(real c * x > - ?e)" by (simp add: mult_ac) ``` haftmann@29789 ` 1201` ``` hence "real c * x + ?e > 0" by arith ``` haftmann@29789 ` 1202` ``` hence "real c * x + ?e \ 0" by simp ``` haftmann@29789 ` 1203` ``` with xz have "?P ?z x (Eq (CN 0 c e))" ``` haftmann@29789 ` 1204` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1205` ``` hence "\ x > ?z. ?P ?z x (Eq (CN 0 c e))" by simp ``` haftmann@29789 ` 1206` ``` thus ?case by blast ``` haftmann@29789 ` 1207` ```next ``` haftmann@29789 ` 1208` ``` case (4 c e) ``` haftmann@29789 ` 1209` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1210` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1211` ``` fix a ``` haftmann@29789 ` 1212` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1213` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1214` ``` {fix x ``` haftmann@29789 ` 1215` ``` assume xz: "x > ?z" ``` haftmann@29789 ` 1216` ``` with mult_strict_right_mono [OF xz cp] cp ``` haftmann@29789 ` 1217` ``` have "(real c * x > - ?e)" by (simp add: mult_ac) ``` haftmann@29789 ` 1218` ``` hence "real c * x + ?e > 0" by arith ``` haftmann@29789 ` 1219` ``` hence "real c * x + ?e \ 0" by simp ``` haftmann@29789 ` 1220` ``` with xz have "?P ?z x (NEq (CN 0 c e))" ``` haftmann@29789 ` 1221` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1222` ``` hence "\ x > ?z. ?P ?z x (NEq (CN 0 c e))" by simp ``` haftmann@29789 ` 1223` ``` thus ?case by blast ``` haftmann@29789 ` 1224` ```next ``` haftmann@29789 ` 1225` ``` case (5 c e) ``` haftmann@29789 ` 1226` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1227` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1228` ``` fix a ``` haftmann@29789 ` 1229` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1230` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1231` ``` {fix x ``` haftmann@29789 ` 1232` ``` assume xz: "x > ?z" ``` haftmann@29789 ` 1233` ``` with mult_strict_right_mono [OF xz cp] cp ``` haftmann@29789 ` 1234` ``` have "(real c * x > - ?e)" by (simp add: mult_ac) ``` haftmann@29789 ` 1235` ``` hence "real c * x + ?e > 0" by arith ``` haftmann@29789 ` 1236` ``` with xz have "?P ?z x (Lt (CN 0 c e))" ``` haftmann@29789 ` 1237` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1238` ``` hence "\ x > ?z. ?P ?z x (Lt (CN 0 c e))" by simp ``` haftmann@29789 ` 1239` ``` thus ?case by blast ``` haftmann@29789 ` 1240` ```next ``` haftmann@29789 ` 1241` ``` case (6 c e) ``` haftmann@29789 ` 1242` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1243` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1244` ``` fix a ``` haftmann@29789 ` 1245` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1246` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1247` ``` {fix x ``` haftmann@29789 ` 1248` ``` assume xz: "x > ?z" ``` haftmann@29789 ` 1249` ``` with mult_strict_right_mono [OF xz cp] cp ``` haftmann@29789 ` 1250` ``` have "(real c * x > - ?e)" by (simp add: mult_ac) ``` haftmann@29789 ` 1251` ``` hence "real c * x + ?e > 0" by arith ``` haftmann@29789 ` 1252` ``` with xz have "?P ?z x (Le (CN 0 c e))" ``` haftmann@29789 ` 1253` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1254` ``` hence "\ x > ?z. ?P ?z x (Le (CN 0 c e))" by simp ``` haftmann@29789 ` 1255` ``` thus ?case by blast ``` haftmann@29789 ` 1256` ```next ``` haftmann@29789 ` 1257` ``` case (7 c e) ``` haftmann@29789 ` 1258` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1259` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1260` ``` fix a ``` haftmann@29789 ` 1261` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1262` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1263` ``` {fix x ``` haftmann@29789 ` 1264` ``` assume xz: "x > ?z" ``` haftmann@29789 ` 1265` ``` with mult_strict_right_mono [OF xz cp] cp ``` haftmann@29789 ` 1266` ``` have "(real c * x > - ?e)" by (simp add: mult_ac) ``` haftmann@29789 ` 1267` ``` hence "real c * x + ?e > 0" by arith ``` haftmann@29789 ` 1268` ``` with xz have "?P ?z x (Gt (CN 0 c e))" ``` haftmann@29789 ` 1269` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1270` ``` hence "\ x > ?z. ?P ?z x (Gt (CN 0 c e))" by simp ``` haftmann@29789 ` 1271` ``` thus ?case by blast ``` haftmann@29789 ` 1272` ```next ``` haftmann@29789 ` 1273` ``` case (8 c e) ``` haftmann@29789 ` 1274` ``` from prems have nb: "numbound0 e" by simp ``` haftmann@29789 ` 1275` ``` from prems have cp: "real c > 0" by simp ``` haftmann@29789 ` 1276` ``` fix a ``` haftmann@29789 ` 1277` ``` let ?e="Inum (a#bs) e" ``` haftmann@29789 ` 1278` ``` let ?z = "(- ?e) / real c" ``` haftmann@29789 ` 1279` ``` {fix x ``` haftmann@29789 ` 1280` ``` assume xz: "x > ?z" ``` haftmann@29789 ` 1281` ``` with mult_strict_right_mono [OF xz cp] cp ``` haftmann@29789 ` 1282` ``` have "(real c * x > - ?e)" by (simp add: mult_ac) ``` haftmann@29789 ` 1283` ``` hence "real c * x + ?e > 0" by arith ``` haftmann@29789 ` 1284` ``` with xz have "?P ?z x (Ge (CN 0 c e))" ``` haftmann@29789 ` 1285` ``` using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp } ``` haftmann@29789 ` 1286` ``` hence "\ x > ?z. ?P ?z x (Ge (CN 0 c e))" by simp ``` haftmann@29789 ` 1287` ``` thus ?case by blast ``` haftmann@29789 ` 1288` ```qed simp_all ``` haftmann@29789 ` 1289` haftmann@29789 ` 1290` ```lemma rminusinf_bound0: ``` haftmann@29789 ` 1291` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1292` ``` shows "bound0 (minusinf p)" ``` haftmann@29789 ` 1293` ``` using lp ``` haftmann@29789 ` 1294` ``` by (induct p rule: minusinf.induct) simp_all ``` haftmann@29789 ` 1295` haftmann@29789 ` 1296` ```lemma rplusinf_bound0: ``` haftmann@29789 ` 1297` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1298` ``` shows "bound0 (plusinf p)" ``` haftmann@29789 ` 1299` ``` using lp ``` haftmann@29789 ` 1300` ``` by (induct p rule: plusinf.induct) simp_all ``` haftmann@29789 ` 1301` haftmann@29789 ` 1302` ```lemma rminusinf_ex: ``` haftmann@29789 ` 1303` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1304` ``` and ex: "Ifm (a#bs) (minusinf p)" ``` haftmann@29789 ` 1305` ``` shows "\ x. Ifm (x#bs) p" ``` haftmann@29789 ` 1306` ```proof- ``` haftmann@29789 ` 1307` ``` from bound0_I [OF rminusinf_bound0[OF lp], where b="a" and bs ="bs"] ex ``` haftmann@29789 ` 1308` ``` have th: "\ x. Ifm (x#bs) (minusinf p)" by auto ``` haftmann@29789 ` 1309` ``` from rminusinf_inf[OF lp, where bs="bs"] ``` haftmann@29789 ` 1310` ``` obtain z where z_def: "\x x. Ifm (x#bs) p" ``` haftmann@29789 ` 1320` ```proof- ``` haftmann@29789 ` 1321` ``` from bound0_I [OF rplusinf_bound0[OF lp], where b="a" and bs ="bs"] ex ``` haftmann@29789 ` 1322` ``` have th: "\ x. Ifm (x#bs) (plusinf p)" by auto ``` haftmann@29789 ` 1323` ``` from rplusinf_inf[OF lp, where bs="bs"] ``` haftmann@29789 ` 1324` ``` obtain z where z_def: "\x>z. Ifm (x # bs) (plusinf p) = Ifm (x # bs) p" by blast ``` haftmann@29789 ` 1325` ``` from th have "Ifm ((z + 1)#bs) (plusinf p)" by simp ``` haftmann@29789 ` 1326` ``` moreover have "z + 1 > z" by simp ``` haftmann@29789 ` 1327` ``` ultimately show ?thesis using z_def by auto ``` haftmann@29789 ` 1328` ```qed ``` haftmann@29789 ` 1329` haftmann@29789 ` 1330` ```consts ``` haftmann@29789 ` 1331` ``` uset:: "fm \ (num \ int) list" ``` haftmann@29789 ` 1332` ``` usubst :: "fm \ (num \ int) \ fm " ``` haftmann@29789 ` 1333` ```recdef uset "measure size" ``` haftmann@29789 ` 1334` ``` "uset (And p q) = (uset p @ uset q)" ``` haftmann@29789 ` 1335` ``` "uset (Or p q) = (uset p @ uset q)" ``` haftmann@29789 ` 1336` ``` "uset (Eq (CN 0 c e)) = [(Neg e,c)]" ``` haftmann@29789 ` 1337` ``` "uset (NEq (CN 0 c e)) = [(Neg e,c)]" ``` haftmann@29789 ` 1338` ``` "uset (Lt (CN 0 c e)) = [(Neg e,c)]" ``` haftmann@29789 ` 1339` ``` "uset (Le (CN 0 c e)) = [(Neg e,c)]" ``` haftmann@29789 ` 1340` ``` "uset (Gt (CN 0 c e)) = [(Neg e,c)]" ``` haftmann@29789 ` 1341` ``` "uset (Ge (CN 0 c e)) = [(Neg e,c)]" ``` haftmann@29789 ` 1342` ``` "uset p = []" ``` haftmann@29789 ` 1343` ```recdef usubst "measure size" ``` haftmann@29789 ` 1344` ``` "usubst (And p q) = (\ (t,n). And (usubst p (t,n)) (usubst q (t,n)))" ``` haftmann@29789 ` 1345` ``` "usubst (Or p q) = (\ (t,n). Or (usubst p (t,n)) (usubst q (t,n)))" ``` haftmann@29789 ` 1346` ``` "usubst (Eq (CN 0 c e)) = (\ (t,n). Eq (Add (Mul c t) (Mul n e)))" ``` haftmann@29789 ` 1347` ``` "usubst (NEq (CN 0 c e)) = (\ (t,n). NEq (Add (Mul c t) (Mul n e)))" ``` haftmann@29789 ` 1348` ``` "usubst (Lt (CN 0 c e)) = (\ (t,n). Lt (Add (Mul c t) (Mul n e)))" ``` haftmann@29789 ` 1349` ``` "usubst (Le (CN 0 c e)) = (\ (t,n). Le (Add (Mul c t) (Mul n e)))" ``` haftmann@29789 ` 1350` ``` "usubst (Gt (CN 0 c e)) = (\ (t,n). Gt (Add (Mul c t) (Mul n e)))" ``` haftmann@29789 ` 1351` ``` "usubst (Ge (CN 0 c e)) = (\ (t,n). Ge (Add (Mul c t) (Mul n e)))" ``` haftmann@29789 ` 1352` ``` "usubst p = (\ (t,n). p)" ``` haftmann@29789 ` 1353` haftmann@29789 ` 1354` ```lemma usubst_I: assumes lp: "isrlfm p" ``` haftmann@29789 ` 1355` ``` and np: "real n > 0" and nbt: "numbound0 t" ``` haftmann@29789 ` 1356` ``` shows "(Ifm (x#bs) (usubst p (t,n)) = Ifm (((Inum (x#bs) t)/(real n))#bs) p) \ bound0 (usubst p (t,n))" (is "(?I x (usubst p (t,n)) = ?I ?u p) \ ?B p" is "(_ = ?I (?t/?n) p) \ _" is "(_ = ?I (?N x t /_) p) \ _") ``` haftmann@29789 ` 1357` ``` using lp ``` haftmann@29789 ` 1358` ```proof(induct p rule: usubst.induct) ``` haftmann@29789 ` 1359` ``` case (5 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ ``` haftmann@29789 ` 1360` ``` have "?I ?u (Lt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) < 0)" ``` haftmann@29789 ` 1361` ``` using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp ``` haftmann@29789 ` 1362` ``` also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)" ``` haftmann@29789 ` 1363` ``` by (simp only: pos_less_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" ``` haftmann@29789 ` 1364` ``` and b="0", simplified divide_zero_left]) (simp only: algebra_simps) ``` haftmann@29789 ` 1365` ``` also have "\ = (real c *?t + ?n* (?N x e) < 0)" ``` haftmann@29789 ` 1366` ``` using np by simp ``` haftmann@29789 ` 1367` ``` finally show ?case using nbt nb by (simp add: algebra_simps) ``` haftmann@29789 ` 1368` ```next ``` haftmann@29789 ` 1369` ``` case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ ``` haftmann@29789 ` 1370` ``` have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \ 0)" ``` haftmann@29789 ` 1371` ``` using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp ``` haftmann@29789 ` 1372` ``` also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) \ 0)" ``` haftmann@29789 ` 1373` ``` by (simp only: pos_le_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" ``` haftmann@29789 ` 1374` ``` and b="0", simplified divide_zero_left]) (simp only: algebra_simps) ``` haftmann@29789 ` 1375` ``` also have "\ = (real c *?t + ?n* (?N x e) \ 0)" ``` haftmann@29789 ` 1376` ``` using np by simp ``` haftmann@29789 ` 1377` ``` finally show ?case using nbt nb by (simp add: algebra_simps) ``` haftmann@29789 ` 1378` ```next ``` haftmann@29789 ` 1379` ``` case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ ``` haftmann@29789 ` 1380` ``` have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)" ``` haftmann@29789 ` 1381` ``` using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp ``` haftmann@29789 ` 1382` ``` also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)" ``` haftmann@29789 ` 1383` ``` by (simp only: pos_divide_less_eq[OF np, where a="real c *(?t/?n) + (?N x e)" ``` haftmann@29789 ` 1384` ``` and b="0", simplified divide_zero_left]) (simp only: algebra_simps) ``` haftmann@29789 ` 1385` ``` also have "\ = (real c *?t + ?n* (?N x e) > 0)" ``` haftmann@29789 ` 1386` ``` using np by simp ``` haftmann@29789 ` 1387` ``` finally show ?case using nbt nb by (simp add: algebra_simps) ``` haftmann@29789 ` 1388` ```next ``` haftmann@29789 ` 1389` ``` case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ ``` haftmann@29789 ` 1390` ``` have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \ 0)" ``` haftmann@29789 ` 1391` ``` using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp ``` haftmann@29789 ` 1392` ``` also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) \ 0)" ``` haftmann@29789 ` 1393` ``` by (simp only: pos_divide_le_eq[OF np, where a="real c *(?t/?n) + (?N x e)" ``` haftmann@29789 ` 1394` ``` and b="0", simplified divide_zero_left]) (simp only: algebra_simps) ``` haftmann@29789 ` 1395` ``` also have "\ = (real c *?t + ?n* (?N x e) \ 0)" ``` haftmann@29789 ` 1396` ``` using np by simp ``` haftmann@29789 ` 1397` ``` finally show ?case using nbt nb by (simp add: algebra_simps) ``` haftmann@29789 ` 1398` ```next ``` haftmann@29789 ` 1399` ``` case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ ``` haftmann@29789 ` 1400` ``` from np have np: "real n \ 0" by simp ``` haftmann@29789 ` 1401` ``` have "?I ?u (Eq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) = 0)" ``` haftmann@29789 ` 1402` ``` using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp ``` haftmann@29789 ` 1403` ``` also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) = 0)" ``` haftmann@29789 ` 1404` ``` by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" ``` haftmann@29789 ` 1405` ``` and b="0", simplified divide_zero_left]) (simp only: algebra_simps) ``` haftmann@29789 ` 1406` ``` also have "\ = (real c *?t + ?n* (?N x e) = 0)" ``` haftmann@29789 ` 1407` ``` using np by simp ``` haftmann@29789 ` 1408` ``` finally show ?case using nbt nb by (simp add: algebra_simps) ``` haftmann@29789 ` 1409` ```next ``` haftmann@29789 ` 1410` ``` case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ ``` haftmann@29789 ` 1411` ``` from np have np: "real n \ 0" by simp ``` haftmann@29789 ` 1412` ``` have "?I ?u (NEq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \ 0)" ``` haftmann@29789 ` 1413` ``` using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp ``` haftmann@29789 ` 1414` ``` also have "\ = (?n*(real c *(?t/?n)) + ?n*(?N x e) \ 0)" ``` haftmann@29789 ` 1415` ``` by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" ``` haftmann@29789 ` 1416` ``` and b="0", simplified divide_zero_left]) (simp only: algebra_simps) ``` haftmann@29789 ` 1417` ``` also have "\ = (real c *?t + ?n* (?N x e) \ 0)" ``` haftmann@29789 ` 1418` ``` using np by simp ``` haftmann@29789 ` 1419` ``` finally show ?case using nbt nb by (simp add: algebra_simps) ``` haftmann@29789 ` 1420` ```qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2) ``` haftmann@29789 ` 1421` haftmann@29789 ` 1422` ```lemma uset_l: ``` haftmann@29789 ` 1423` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1424` ``` shows "\ (t,k) \ set (uset p). numbound0 t \ k >0" ``` haftmann@29789 ` 1425` ```using lp ``` haftmann@29789 ` 1426` ```by(induct p rule: uset.induct,auto) ``` haftmann@29789 ` 1427` haftmann@29789 ` 1428` ```lemma rminusinf_uset: ``` haftmann@29789 ` 1429` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1430` ``` and nmi: "\ (Ifm (a#bs) (minusinf p))" (is "\ (Ifm (a#bs) (?M p))") ``` haftmann@29789 ` 1431` ``` and ex: "Ifm (x#bs) p" (is "?I x p") ``` haftmann@29789 ` 1432` ``` shows "\ (s,m) \ set (uset p). x \ Inum (a#bs) s / real m" (is "\ (s,m) \ ?U p. x \ ?N a s / real m") ``` haftmann@29789 ` 1433` ```proof- ``` haftmann@29789 ` 1434` ``` have "\ (s,m) \ set (uset p). real m * x \ Inum (a#bs) s " (is "\ (s,m) \ ?U p. real m *x \ ?N a s") ``` haftmann@29789 ` 1435` ``` using lp nmi ex ``` haftmann@29789 ` 1436` ``` by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2) ``` haftmann@29789 ` 1437` ``` then obtain s m where smU: "(s,m) \ set (uset p)" and mx: "real m * x \ ?N a s" by blast ``` haftmann@29789 ` 1438` ``` from uset_l[OF lp] smU have mp: "real m > 0" by auto ``` haftmann@29789 ` 1439` ``` from pos_divide_le_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \ ?N a s / real m" ``` haftmann@29789 ` 1440` ``` by (auto simp add: mult_commute) ``` haftmann@29789 ` 1441` ``` thus ?thesis using smU by auto ``` haftmann@29789 ` 1442` ```qed ``` haftmann@29789 ` 1443` haftmann@29789 ` 1444` ```lemma rplusinf_uset: ``` haftmann@29789 ` 1445` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1446` ``` and nmi: "\ (Ifm (a#bs) (plusinf p))" (is "\ (Ifm (a#bs) (?M p))") ``` haftmann@29789 ` 1447` ``` and ex: "Ifm (x#bs) p" (is "?I x p") ``` haftmann@29789 ` 1448` ``` shows "\ (s,m) \ set (uset p). x \ Inum (a#bs) s / real m" (is "\ (s,m) \ ?U p. x \ ?N a s / real m") ``` haftmann@29789 ` 1449` ```proof- ``` haftmann@29789 ` 1450` ``` have "\ (s,m) \ set (uset p). real m * x \ Inum (a#bs) s " (is "\ (s,m) \ ?U p. real m *x \ ?N a s") ``` haftmann@29789 ` 1451` ``` using lp nmi ex ``` haftmann@29789 ` 1452` ``` by (induct p rule: minusinf.induct, auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"] nth_pos2) ``` haftmann@29789 ` 1453` ``` then obtain s m where smU: "(s,m) \ set (uset p)" and mx: "real m * x \ ?N a s" by blast ``` haftmann@29789 ` 1454` ``` from uset_l[OF lp] smU have mp: "real m > 0" by auto ``` haftmann@29789 ` 1455` ``` from pos_le_divide_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \ ?N a s / real m" ``` haftmann@29789 ` 1456` ``` by (auto simp add: mult_commute) ``` haftmann@29789 ` 1457` ``` thus ?thesis using smU by auto ``` haftmann@29789 ` 1458` ```qed ``` haftmann@29789 ` 1459` haftmann@29789 ` 1460` ```lemma lin_dense: ``` haftmann@29789 ` 1461` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1462` ``` and noS: "\ t. l < t \ t< u \ t \ (\ (t,n). Inum (x#bs) t / real n) ` set (uset p)" ``` haftmann@29789 ` 1463` ``` (is "\ t. _ \ _ \ t \ (\ (t,n). ?N x t / real n ) ` (?U p)") ``` haftmann@29789 ` 1464` ``` and lx: "l < x" and xu:"x < u" and px:" Ifm (x#bs) p" ``` haftmann@29789 ` 1465` ``` and ly: "l < y" and yu: "y < u" ``` haftmann@29789 ` 1466` ``` shows "Ifm (y#bs) p" ``` haftmann@29789 ` 1467` ```using lp px noS ``` haftmann@29789 ` 1468` ```proof (induct p rule: isrlfm.induct) ``` haftmann@29789 ` 1469` ``` case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ ``` haftmann@29789 ` 1470` ``` from prems have "x * real c + ?N x e < 0" by (simp add: algebra_simps) ``` haftmann@29789 ` 1471` ``` hence pxc: "x < (- ?N x e) / real c" ``` haftmann@29789 ` 1472` ``` by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"]) ``` haftmann@29789 ` 1473` ``` from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto ``` haftmann@29789 ` 1474` ``` with ly yu have yne: "y \ - ?N x e / real c" by auto ``` haftmann@29789 ` 1475` ``` hence "y < (- ?N x e) / real c \ y > (-?N x e) / real c" by auto ``` haftmann@29789 ` 1476` ``` moreover {assume y: "y < (-?N x e)/ real c" ``` haftmann@29789 ` 1477` ``` hence "y * real c < - ?N x e" ``` wenzelm@32960 ` 1478` ``` by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) ``` haftmann@29789 ` 1479` ``` hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) ``` haftmann@29789 ` 1480` ``` hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} ``` haftmann@29789 ` 1481` ``` moreover {assume y: "y > (- ?N x e) / real c" ``` haftmann@29789 ` 1482` ``` with yu have eu: "u > (- ?N x e) / real c" by auto ``` haftmann@29789 ` 1483` ``` with noSc ly yu have "(- ?N x e) / real c \ l" by (cases "(- ?N x e) / real c > l", auto) ``` haftmann@29789 ` 1484` ``` with lx pxc have "False" by auto ``` haftmann@29789 ` 1485` ``` hence ?case by simp } ``` haftmann@29789 ` 1486` ``` ultimately show ?case by blast ``` haftmann@29789 ` 1487` ```next ``` haftmann@29789 ` 1488` ``` case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp + ``` haftmann@29789 ` 1489` ``` from prems have "x * real c + ?N x e \ 0" by (simp add: algebra_simps) ``` haftmann@29789 ` 1490` ``` hence pxc: "x \ (- ?N x e) / real c" ``` haftmann@29789 ` 1491` ``` by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) ``` haftmann@29789 ` 1492` ``` from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto ``` haftmann@29789 ` 1493` ``` with ly yu have yne: "y \ - ?N x e / real c" by auto ``` haftmann@29789 ` 1494` ``` hence "y < (- ?N x e) / real c \ y > (-?N x e) / real c" by auto ``` haftmann@29789 ` 1495` ``` moreover {assume y: "y < (-?N x e)/ real c" ``` haftmann@29789 ` 1496` ``` hence "y * real c < - ?N x e" ``` wenzelm@32960 ` 1497` ``` by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) ``` haftmann@29789 ` 1498` ``` hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) ``` haftmann@29789 ` 1499` ``` hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} ``` haftmann@29789 ` 1500` ``` moreover {assume y: "y > (- ?N x e) / real c" ``` haftmann@29789 ` 1501` ``` with yu have eu: "u > (- ?N x e) / real c" by auto ``` haftmann@29789 ` 1502` ``` with noSc ly yu have "(- ?N x e) / real c \ l" by (cases "(- ?N x e) / real c > l", auto) ``` haftmann@29789 ` 1503` ``` with lx pxc have "False" by auto ``` haftmann@29789 ` 1504` ``` hence ?case by simp } ``` haftmann@29789 ` 1505` ``` ultimately show ?case by blast ``` haftmann@29789 ` 1506` ```next ``` haftmann@29789 ` 1507` ``` case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ ``` haftmann@29789 ` 1508` ``` from prems have "x * real c + ?N x e > 0" by (simp add: algebra_simps) ``` haftmann@29789 ` 1509` ``` hence pxc: "x > (- ?N x e) / real c" ``` haftmann@29789 ` 1510` ``` by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"]) ``` haftmann@29789 ` 1511` ``` from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto ``` haftmann@29789 ` 1512` ``` with ly yu have yne: "y \ - ?N x e / real c" by auto ``` haftmann@29789 ` 1513` ``` hence "y < (- ?N x e) / real c \ y > (-?N x e) / real c" by auto ``` haftmann@29789 ` 1514` ``` moreover {assume y: "y > (-?N x e)/ real c" ``` haftmann@29789 ` 1515` ``` hence "y * real c > - ?N x e" ``` wenzelm@32960 ` 1516` ``` by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) ``` haftmann@29789 ` 1517` ``` hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) ``` haftmann@29789 ` 1518` ``` hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} ``` haftmann@29789 ` 1519` ``` moreover {assume y: "y < (- ?N x e) / real c" ``` haftmann@29789 ` 1520` ``` with ly have eu: "l < (- ?N x e) / real c" by auto ``` haftmann@29789 ` 1521` ``` with noSc ly yu have "(- ?N x e) / real c \ u" by (cases "(- ?N x e) / real c > l", auto) ``` haftmann@29789 ` 1522` ``` with xu pxc have "False" by auto ``` haftmann@29789 ` 1523` ``` hence ?case by simp } ``` haftmann@29789 ` 1524` ``` ultimately show ?case by blast ``` haftmann@29789 ` 1525` ```next ``` haftmann@29789 ` 1526` ``` case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ ``` haftmann@29789 ` 1527` ``` from prems have "x * real c + ?N x e \ 0" by (simp add: algebra_simps) ``` haftmann@29789 ` 1528` ``` hence pxc: "x \ (- ?N x e) / real c" ``` haftmann@29789 ` 1529` ``` by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) ``` haftmann@29789 ` 1530` ``` from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto ``` haftmann@29789 ` 1531` ``` with ly yu have yne: "y \ - ?N x e / real c" by auto ``` haftmann@29789 ` 1532` ``` hence "y < (- ?N x e) / real c \ y > (-?N x e) / real c" by auto ``` haftmann@29789 ` 1533` ``` moreover {assume y: "y > (-?N x e)/ real c" ``` haftmann@29789 ` 1534` ``` hence "y * real c > - ?N x e" ``` wenzelm@32960 ` 1535` ``` by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) ``` haftmann@29789 ` 1536` ``` hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) ``` haftmann@29789 ` 1537` ``` hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} ``` haftmann@29789 ` 1538` ``` moreover {assume y: "y < (- ?N x e) / real c" ``` haftmann@29789 ` 1539` ``` with ly have eu: "l < (- ?N x e) / real c" by auto ``` haftmann@29789 ` 1540` ``` with noSc ly yu have "(- ?N x e) / real c \ u" by (cases "(- ?N x e) / real c > l", auto) ``` haftmann@29789 ` 1541` ``` with xu pxc have "False" by auto ``` haftmann@29789 ` 1542` ``` hence ?case by simp } ``` haftmann@29789 ` 1543` ``` ultimately show ?case by blast ``` haftmann@29789 ` 1544` ```next ``` haftmann@29789 ` 1545` ``` case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ ``` haftmann@29789 ` 1546` ``` from cp have cnz: "real c \ 0" by simp ``` haftmann@29789 ` 1547` ``` from prems have "x * real c + ?N x e = 0" by (simp add: algebra_simps) ``` haftmann@29789 ` 1548` ``` hence pxc: "x = (- ?N x e) / real c" ``` haftmann@29789 ` 1549` ``` by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"]) ``` haftmann@29789 ` 1550` ``` from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto ``` haftmann@29789 ` 1551` ``` with lx xu have yne: "x \ - ?N x e / real c" by auto ``` haftmann@29789 ` 1552` ``` with pxc show ?case by simp ``` haftmann@29789 ` 1553` ```next ``` haftmann@29789 ` 1554` ``` case (4 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ ``` haftmann@29789 ` 1555` ``` from cp have cnz: "real c \ 0" by simp ``` haftmann@29789 ` 1556` ``` from prems have noSc:"\ t. l < t \ t < u \ t \ (- ?N x e) / real c" by auto ``` haftmann@29789 ` 1557` ``` with ly yu have yne: "y \ - ?N x e / real c" by auto ``` haftmann@29789 ` 1558` ``` hence "y* real c \ -?N x e" ``` haftmann@29789 ` 1559` ``` by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp ``` haftmann@29789 ` 1560` ``` hence "y* real c + ?N x e \ 0" by (simp add: algebra_simps) ``` haftmann@29789 ` 1561` ``` thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] ``` haftmann@29789 ` 1562` ``` by (simp add: algebra_simps) ``` haftmann@29789 ` 1563` ```qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"]) ``` haftmann@29789 ` 1564` haftmann@29789 ` 1565` ```lemma finite_set_intervals: ``` haftmann@29789 ` 1566` ``` assumes px: "P (x::real)" ``` haftmann@29789 ` 1567` ``` and lx: "l \ x" and xu: "x \ u" ``` haftmann@29789 ` 1568` ``` and linS: "l\ S" and uinS: "u \ S" ``` haftmann@29789 ` 1569` ``` and fS:"finite S" and lS: "\ x\ S. l \ x" and Su: "\ x\ S. x \ u" ``` haftmann@29789 ` 1570` ``` shows "\ a \ S. \ b \ S. (\ y. a < y \ y < b \ y \ S) \ a \ x \ x \ b \ P x" ``` haftmann@29789 ` 1571` ```proof- ``` haftmann@29789 ` 1572` ``` let ?Mx = "{y. y\ S \ y \ x}" ``` haftmann@29789 ` 1573` ``` let ?xM = "{y. y\ S \ x \ y}" ``` haftmann@29789 ` 1574` ``` let ?a = "Max ?Mx" ``` haftmann@29789 ` 1575` ``` let ?b = "Min ?xM" ``` haftmann@29789 ` 1576` ``` have MxS: "?Mx \ S" by blast ``` haftmann@29789 ` 1577` ``` hence fMx: "finite ?Mx" using fS finite_subset by auto ``` haftmann@29789 ` 1578` ``` from lx linS have linMx: "l \ ?Mx" by blast ``` haftmann@29789 ` 1579` ``` hence Mxne: "?Mx \ {}" by blast ``` haftmann@29789 ` 1580` ``` have xMS: "?xM \ S" by blast ``` haftmann@29789 ` 1581` ``` hence fxM: "finite ?xM" using fS finite_subset by auto ``` haftmann@29789 ` 1582` ``` from xu uinS have linxM: "u \ ?xM" by blast ``` haftmann@29789 ` 1583` ``` hence xMne: "?xM \ {}" by blast ``` haftmann@29789 ` 1584` ``` have ax:"?a \ x" using Mxne fMx by auto ``` haftmann@29789 ` 1585` ``` have xb:"x \ ?b" using xMne fxM by auto ``` haftmann@29789 ` 1586` ``` have "?a \ ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \ S" using MxS by blast ``` haftmann@29789 ` 1587` ``` have "?b \ ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \ S" using xMS by blast ``` haftmann@29789 ` 1588` ``` have noy:"\ y. ?a < y \ y < ?b \ y \ S" ``` haftmann@29789 ` 1589` ``` proof(clarsimp) ``` haftmann@29789 ` 1590` ``` fix y ``` haftmann@29789 ` 1591` ``` assume ay: "?a < y" and yb: "y < ?b" and yS: "y \ S" ``` haftmann@29789 ` 1592` ``` from yS have "y\ ?Mx \ y\ ?xM" by auto ``` haftmann@29789 ` 1593` ``` moreover {assume "y \ ?Mx" hence "y \ ?a" using Mxne fMx by auto with ay have "False" by simp} ``` haftmann@29789 ` 1594` ``` moreover {assume "y \ ?xM" hence "y \ ?b" using xMne fxM by auto with yb have "False" by simp} ``` haftmann@29789 ` 1595` ``` ultimately show "False" by blast ``` haftmann@29789 ` 1596` ``` qed ``` haftmann@29789 ` 1597` ``` from ainS binS noy ax xb px show ?thesis by blast ``` haftmann@29789 ` 1598` ```qed ``` haftmann@29789 ` 1599` haftmann@29789 ` 1600` ```lemma finite_set_intervals2: ``` haftmann@29789 ` 1601` ``` assumes px: "P (x::real)" ``` haftmann@29789 ` 1602` ``` and lx: "l \ x" and xu: "x \ u" ``` haftmann@29789 ` 1603` ``` and linS: "l\ S" and uinS: "u \ S" ``` haftmann@29789 ` 1604` ``` and fS:"finite S" and lS: "\ x\ S. l \ x" and Su: "\ x\ S. x \ u" ``` haftmann@29789 ` 1605` ``` shows "(\ s\ S. P s) \ (\ a \ S. \ b \ S. (\ y. a < y \ y < b \ y \ S) \ a < x \ x < b \ P x)" ``` haftmann@29789 ` 1606` ```proof- ``` haftmann@29789 ` 1607` ``` from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] ``` haftmann@29789 ` 1608` ``` obtain a and b where ``` haftmann@29789 ` 1609` ``` as: "a\ S" and bs: "b\ S" and noS:"\y. a < y \ y < b \ y \ S" and axb: "a \ x \ x \ b \ P x" by auto ``` haftmann@29789 ` 1610` ``` from axb have "x= a \ x= b \ (a < x \ x < b)" by auto ``` haftmann@29789 ` 1611` ``` thus ?thesis using px as bs noS by blast ``` haftmann@29789 ` 1612` ```qed ``` haftmann@29789 ` 1613` haftmann@29789 ` 1614` ```lemma rinf_uset: ``` haftmann@29789 ` 1615` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1616` ``` and nmi: "\ (Ifm (x#bs) (minusinf p))" (is "\ (Ifm (x#bs) (?M p))") ``` haftmann@29789 ` 1617` ``` and npi: "\ (Ifm (x#bs) (plusinf p))" (is "\ (Ifm (x#bs) (?P p))") ``` haftmann@29789 ` 1618` ``` and ex: "\ x. Ifm (x#bs) p" (is "\ x. ?I x p") ``` haftmann@29789 ` 1619` ``` shows "\ (l,n) \ set (uset p). \ (s,m) \ set (uset p). ?I ((Inum (x#bs) l / real n + Inum (x#bs) s / real m) / 2) p" ``` haftmann@29789 ` 1620` ```proof- ``` haftmann@29789 ` 1621` ``` let ?N = "\ x t. Inum (x#bs) t" ``` haftmann@29789 ` 1622` ``` let ?U = "set (uset p)" ``` haftmann@29789 ` 1623` ``` from ex obtain a where pa: "?I a p" by blast ``` haftmann@29789 ` 1624` ``` from bound0_I[OF rminusinf_bound0[OF lp], where bs="bs" and b="x" and b'="a"] nmi ``` haftmann@29789 ` 1625` ``` have nmi': "\ (?I a (?M p))" by simp ``` haftmann@29789 ` 1626` ``` from bound0_I[OF rplusinf_bound0[OF lp], where bs="bs" and b="x" and b'="a"] npi ``` haftmann@29789 ` 1627` ``` have npi': "\ (?I a (?P p))" by simp ``` haftmann@29789 ` 1628` ``` have "\ (l,n) \ set (uset p). \ (s,m) \ set (uset p). ?I ((?N a l/real n + ?N a s /real m) / 2) p" ``` haftmann@29789 ` 1629` ``` proof- ``` haftmann@29789 ` 1630` ``` let ?M = "(\ (t,c). ?N a t / real c) ` ?U" ``` haftmann@29789 ` 1631` ``` have fM: "finite ?M" by auto ``` haftmann@29789 ` 1632` ``` from rminusinf_uset[OF lp nmi pa] rplusinf_uset[OF lp npi pa] ``` haftmann@29789 ` 1633` ``` have "\ (l,n) \ set (uset p). \ (s,m) \ set (uset p). a \ ?N x l / real n \ a \ ?N x s / real m" by blast ``` haftmann@29789 ` 1634` ``` then obtain "t" "n" "s" "m" where ``` haftmann@29789 ` 1635` ``` tnU: "(t,n) \ ?U" and smU: "(s,m) \ ?U" ``` haftmann@29789 ` 1636` ``` and xs1: "a \ ?N x s / real m" and tx1: "a \ ?N x t / real n" by blast ``` haftmann@29789 ` 1637` ``` from uset_l[OF lp] tnU smU numbound0_I[where bs="bs" and b="x" and b'="a"] xs1 tx1 have xs: "a \ ?N a s / real m" and tx: "a \ ?N a t / real n" by auto ``` haftmann@29789 ` 1638` ``` from tnU have Mne: "?M \ {}" by auto ``` haftmann@29789 ` 1639` ``` hence Une: "?U \ {}" by simp ``` haftmann@29789 ` 1640` ``` let ?l = "Min ?M" ``` haftmann@29789 ` 1641` ``` let ?u = "Max ?M" ``` haftmann@29789 ` 1642` ``` have linM: "?l \ ?M" using fM Mne by simp ``` haftmann@29789 ` 1643` ``` have uinM: "?u \ ?M" using fM Mne by simp ``` haftmann@29789 ` 1644` ``` have tnM: "?N a t / real n \ ?M" using tnU by auto ``` haftmann@29789 ` 1645` ``` have smM: "?N a s / real m \ ?M" using smU by auto ``` haftmann@29789 ` 1646` ``` have lM: "\ t\ ?M. ?l \ t" using Mne fM by auto ``` haftmann@29789 ` 1647` ``` have Mu: "\ t\ ?M. t \ ?u" using Mne fM by auto ``` haftmann@29789 ` 1648` ``` have "?l \ ?N a t / real n" using tnM Mne by simp hence lx: "?l \ a" using tx by simp ``` haftmann@29789 ` 1649` ``` have "?N a s / real m \ ?u" using smM Mne by simp hence xu: "a \ ?u" using xs by simp ``` haftmann@29789 ` 1650` ``` from finite_set_intervals2[where P="\ x. ?I x p",OF pa lx xu linM uinM fM lM Mu] ``` haftmann@29789 ` 1651` ``` have "(\ s\ ?M. ?I s p) \ ``` haftmann@29789 ` 1652` ``` (\ t1\ ?M. \ t2 \ ?M. (\ y. t1 < y \ y < t2 \ y \ ?M) \ t1 < a \ a < t2 \ ?I a p)" . ``` haftmann@29789 ` 1653` ``` moreover { fix u assume um: "u\ ?M" and pu: "?I u p" ``` haftmann@29789 ` 1654` ``` hence "\ (tu,nu) \ ?U. u = ?N a tu / real nu" by auto ``` haftmann@29789 ` 1655` ``` then obtain "tu" "nu" where tuU: "(tu,nu) \ ?U" and tuu:"u= ?N a tu / real nu" by blast ``` haftmann@29789 ` 1656` ``` have "(u + u) / 2 = u" by auto with pu tuu ``` haftmann@29789 ` 1657` ``` have "?I (((?N a tu / real nu) + (?N a tu / real nu)) / 2) p" by simp ``` haftmann@29789 ` 1658` ``` with tuU have ?thesis by blast} ``` haftmann@29789 ` 1659` ``` moreover{ ``` haftmann@29789 ` 1660` ``` assume "\ t1\ ?M. \ t2 \ ?M. (\ y. t1 < y \ y < t2 \ y \ ?M) \ t1 < a \ a < t2 \ ?I a p" ``` haftmann@29789 ` 1661` ``` then obtain t1 and t2 where t1M: "t1 \ ?M" and t2M: "t2\ ?M" ``` wenzelm@32960 ` 1662` ``` and noM: "\ y. t1 < y \ y < t2 \ y \ ?M" and t1x: "t1 < a" and xt2: "a < t2" and px: "?I a p" ``` wenzelm@32960 ` 1663` ``` by blast ``` haftmann@29789 ` 1664` ``` from t1M have "\ (t1u,t1n) \ ?U. t1 = ?N a t1u / real t1n" by auto ``` haftmann@29789 ` 1665` ``` then obtain "t1u" "t1n" where t1uU: "(t1u,t1n) \ ?U" and t1u: "t1 = ?N a t1u / real t1n" by blast ``` haftmann@29789 ` 1666` ``` from t2M have "\ (t2u,t2n) \ ?U. t2 = ?N a t2u / real t2n" by auto ``` haftmann@29789 ` 1667` ``` then obtain "t2u" "t2n" where t2uU: "(t2u,t2n) \ ?U" and t2u: "t2 = ?N a t2u / real t2n" by blast ``` haftmann@29789 ` 1668` ``` from t1x xt2 have t1t2: "t1 < t2" by simp ``` haftmann@29789 ` 1669` ``` let ?u = "(t1 + t2) / 2" ``` haftmann@29789 ` 1670` ``` from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2" by auto ``` haftmann@29789 ` 1671` ``` from lin_dense[OF lp noM t1x xt2 px t1lu ut2] have "?I ?u p" . ``` haftmann@29789 ` 1672` ``` with t1uU t2uU t1u t2u have ?thesis by blast} ``` haftmann@29789 ` 1673` ``` ultimately show ?thesis by blast ``` haftmann@29789 ` 1674` ``` qed ``` haftmann@29789 ` 1675` ``` then obtain "l" "n" "s" "m" where lnU: "(l,n) \ ?U" and smU:"(s,m) \ ?U" ``` haftmann@29789 ` 1676` ``` and pu: "?I ((?N a l / real n + ?N a s / real m) / 2) p" by blast ``` haftmann@29789 ` 1677` ``` from lnU smU uset_l[OF lp] have nbl: "numbound0 l" and nbs: "numbound0 s" by auto ``` haftmann@29789 ` 1678` ``` from numbound0_I[OF nbl, where bs="bs" and b="a" and b'="x"] ``` haftmann@29789 ` 1679` ``` numbound0_I[OF nbs, where bs="bs" and b="a" and b'="x"] pu ``` haftmann@29789 ` 1680` ``` have "?I ((?N x l / real n + ?N x s / real m) / 2) p" by simp ``` haftmann@29789 ` 1681` ``` with lnU smU ``` haftmann@29789 ` 1682` ``` show ?thesis by auto ``` haftmann@29789 ` 1683` ```qed ``` haftmann@29789 ` 1684` ``` (* The Ferrante - Rackoff Theorem *) ``` haftmann@29789 ` 1685` haftmann@29789 ` 1686` ```theorem fr_eq: ``` haftmann@29789 ` 1687` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1688` ``` shows "(\ x. Ifm (x#bs) p) = ((Ifm (x#bs) (minusinf p)) \ (Ifm (x#bs) (plusinf p)) \ (\ (t,n) \ set (uset p). \ (s,m) \ set (uset p). Ifm ((((Inum (x#bs) t)/ real n + (Inum (x#bs) s) / real m) /2)#bs) p))" ``` haftmann@29789 ` 1689` ``` (is "(\ x. ?I x p) = (?M \ ?P \ ?F)" is "?E = ?D") ``` haftmann@29789 ` 1690` ```proof ``` haftmann@29789 ` 1691` ``` assume px: "\ x. ?I x p" ``` haftmann@29789 ` 1692` ``` have "?M \ ?P \ (\ ?M \ \ ?P)" by blast ``` haftmann@29789 ` 1693` ``` moreover {assume "?M \ ?P" hence "?D" by blast} ``` haftmann@29789 ` 1694` ``` moreover {assume nmi: "\ ?M" and npi: "\ ?P" ``` haftmann@29789 ` 1695` ``` from rinf_uset[OF lp nmi npi] have "?F" using px by blast hence "?D" by blast} ``` haftmann@29789 ` 1696` ``` ultimately show "?D" by blast ``` haftmann@29789 ` 1697` ```next ``` haftmann@29789 ` 1698` ``` assume "?D" ``` haftmann@29789 ` 1699` ``` moreover {assume m:"?M" from rminusinf_ex[OF lp m] have "?E" .} ``` haftmann@29789 ` 1700` ``` moreover {assume p: "?P" from rplusinf_ex[OF lp p] have "?E" . } ``` haftmann@29789 ` 1701` ``` moreover {assume f:"?F" hence "?E" by blast} ``` haftmann@29789 ` 1702` ``` ultimately show "?E" by blast ``` haftmann@29789 ` 1703` ```qed ``` haftmann@29789 ` 1704` haftmann@29789 ` 1705` haftmann@29789 ` 1706` ```lemma fr_equsubst: ``` haftmann@29789 ` 1707` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1708` ``` shows "(\ x. Ifm (x#bs) p) = ((Ifm (x#bs) (minusinf p)) \ (Ifm (x#bs) (plusinf p)) \ (\ (t,k) \ set (uset p). \ (s,l) \ set (uset p). Ifm (x#bs) (usubst p (Add(Mul l t) (Mul k s) , 2*k*l))))" ``` haftmann@29789 ` 1709` ``` (is "(\ x. ?I x p) = (?M \ ?P \ ?F)" is "?E = ?D") ``` haftmann@29789 ` 1710` ```proof ``` haftmann@29789 ` 1711` ``` assume px: "\ x. ?I x p" ``` haftmann@29789 ` 1712` ``` have "?M \ ?P \ (\ ?M \ \ ?P)" by blast ``` haftmann@29789 ` 1713` ``` moreover {assume "?M \ ?P" hence "?D" by blast} ``` haftmann@29789 ` 1714` ``` moreover {assume nmi: "\ ?M" and npi: "\ ?P" ``` haftmann@29789 ` 1715` ``` let ?f ="\ (t,n). Inum (x#bs) t / real n" ``` haftmann@29789 ` 1716` ``` let ?N = "\ t. Inum (x#bs) t" ``` haftmann@29789 ` 1717` ``` {fix t n s m assume "(t,n)\ set (uset p)" and "(s,m) \ set (uset p)" ``` haftmann@29789 ` 1718` ``` with uset_l[OF lp] have tnb: "numbound0 t" and np:"real n > 0" and snb: "numbound0 s" and mp:"real m > 0" ``` wenzelm@32960 ` 1719` ``` by auto ``` haftmann@29789 ` 1720` ``` let ?st = "Add (Mul m t) (Mul n s)" ``` haftmann@29789 ` 1721` ``` from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" ``` wenzelm@32960 ` 1722` ``` by (simp add: mult_commute) ``` haftmann@29789 ` 1723` ``` from tnb snb have st_nb: "numbound0 ?st" by simp ``` haftmann@29789 ` 1724` ``` have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" ``` wenzelm@32960 ` 1725` ``` using mnp mp np by (simp add: algebra_simps add_divide_distrib) ``` haftmann@29789 ` 1726` ``` from usubst_I[OF lp mnp st_nb, where x="x" and bs="bs"] ``` haftmann@29789 ` 1727` ``` 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])} ``` haftmann@29789 ` 1728` ``` with rinf_uset[OF lp nmi npi px] have "?F" by blast hence "?D" by blast} ``` haftmann@29789 ` 1729` ``` ultimately show "?D" by blast ``` haftmann@29789 ` 1730` ```next ``` haftmann@29789 ` 1731` ``` assume "?D" ``` haftmann@29789 ` 1732` ``` moreover {assume m:"?M" from rminusinf_ex[OF lp m] have "?E" .} ``` haftmann@29789 ` 1733` ``` moreover {assume p: "?P" from rplusinf_ex[OF lp p] have "?E" . } ``` haftmann@29789 ` 1734` ``` moreover {fix t k s l assume "(t,k) \ set (uset p)" and "(s,l) \ set (uset p)" ``` haftmann@29789 ` 1735` ``` and px:"?I x (usubst p (Add (Mul l t) (Mul k s), 2*k*l))" ``` haftmann@29789 ` 1736` ``` 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 ``` haftmann@29789 ` 1737` ``` let ?st = "Add (Mul l t) (Mul k s)" ``` haftmann@29789 ` 1738` ``` from mult_pos_pos[OF np mp] have mnp: "real (2*k*l) > 0" ``` haftmann@29789 ` 1739` ``` by (simp add: mult_commute) ``` haftmann@29789 ` 1740` ``` from tnb snb have st_nb: "numbound0 ?st" by simp ``` haftmann@29789 ` 1741` ``` from usubst_I[OF lp mnp st_nb, where bs="bs"] px have "?E" by auto} ``` haftmann@29789 ` 1742` ``` ultimately show "?E" by blast ``` haftmann@29789 ` 1743` ```qed ``` haftmann@29789 ` 1744` haftmann@29789 ` 1745` haftmann@29789 ` 1746` ``` (* Implement the right hand side of Ferrante and Rackoff's Theorem. *) ``` haftmann@35416 ` 1747` ```definition ferrack :: "fm \ fm" where ``` haftmann@36853 ` 1748` ``` "ferrack p = (let p' = rlfm (simpfm p); mp = minusinf p'; pp = plusinf p' ``` haftmann@29789 ` 1749` ``` in if (mp = T \ pp = T) then T else ``` haftmann@36853 ` 1750` ``` (let U = remdups(map simp_num_pair ``` haftmann@29789 ` 1751` ``` (map (\ ((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2*n*m)) ``` haftmann@29789 ` 1752` ``` (alluopairs (uset p')))) ``` haftmann@29789 ` 1753` ``` in decr (disj mp (disj pp (evaldjf (simpfm o (usubst p')) U)))))" ``` haftmann@29789 ` 1754` haftmann@29789 ` 1755` ```lemma uset_cong_aux: ``` haftmann@29789 ` 1756` ``` assumes Ul: "\ (t,n) \ set U. numbound0 t \ n >0" ``` haftmann@29789 ` 1757` ``` shows "((\ (t,n). Inum (x#bs) t /real n) ` (set (map (\ ((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2*n*m)) (alluopairs U)))) = ((\ ((t,n),(s,m)). (Inum (x#bs) t /real n + Inum (x#bs) s /real m)/2) ` (set U \ set U))" ``` haftmann@29789 ` 1758` ``` (is "?lhs = ?rhs") ``` haftmann@29789 ` 1759` ```proof(auto) ``` haftmann@29789 ` 1760` ``` fix t n s m ``` haftmann@29789 ` 1761` ``` assume "((t,n),(s,m)) \ set (alluopairs U)" ``` haftmann@29789 ` 1762` ``` hence th: "((t,n),(s,m)) \ (set U \ set U)" ``` haftmann@29789 ` 1763` ``` using alluopairs_set1[where xs="U"] by blast ``` haftmann@29789 ` 1764` ``` let ?N = "\ t. Inum (x#bs) t" ``` haftmann@29789 ` 1765` ``` let ?st= "Add (Mul m t) (Mul n s)" ``` haftmann@29789 ` 1766` ``` from Ul th have mnz: "m \ 0" by auto ``` haftmann@29789 ` 1767` ``` from Ul th have nnz: "n \ 0" by auto ``` haftmann@29789 ` 1768` ``` have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" ``` haftmann@29789 ` 1769` ``` using mnz nnz by (simp add: algebra_simps add_divide_distrib) ``` haftmann@29789 ` 1770` ``` ``` haftmann@29789 ` 1771` ``` thus "(real m * Inum (x # bs) t + real n * Inum (x # bs) s) / ``` haftmann@29789 ` 1772` ``` (2 * real n * real m) ``` haftmann@29789 ` 1773` ``` \ (\((t, n), s, m). ``` haftmann@29789 ` 1774` ``` (Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) ` ``` haftmann@29789 ` 1775` ``` (set U \ set U)"using mnz nnz th ``` haftmann@29789 ` 1776` ``` apply (auto simp add: th add_divide_distrib algebra_simps split_def image_def) ``` haftmann@29789 ` 1777` ``` by (rule_tac x="(s,m)" in bexI,simp_all) ``` haftmann@29789 ` 1778` ``` (rule_tac x="(t,n)" in bexI,simp_all) ``` haftmann@29789 ` 1779` ```next ``` haftmann@29789 ` 1780` ``` fix t n s m ``` haftmann@29789 ` 1781` ``` assume tnU: "(t,n) \ set U" and smU:"(s,m) \ set U" ``` haftmann@29789 ` 1782` ``` let ?N = "\ t. Inum (x#bs) t" ``` haftmann@29789 ` 1783` ``` let ?st= "Add (Mul m t) (Mul n s)" ``` haftmann@29789 ` 1784` ``` from Ul smU have mnz: "m \ 0" by auto ``` haftmann@29789 ` 1785` ``` from Ul tnU have nnz: "n \ 0" by auto ``` haftmann@29789 ` 1786` ``` have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" ``` haftmann@29789 ` 1787` ``` using mnz nnz by (simp add: algebra_simps add_divide_distrib) ``` haftmann@29789 ` 1788` ``` let ?P = "\ (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" ``` haftmann@29789 ` 1789` ``` have Pc:"\ a b. ?P a b = ?P b a" ``` haftmann@29789 ` 1790` ``` by auto ``` haftmann@29789 ` 1791` ``` from Ul alluopairs_set1 have Up:"\ ((t,n),(s,m)) \ set (alluopairs U). n \ 0 \ m \ 0" by blast ``` haftmann@29789 ` 1792` ``` from alluopairs_ex[OF Pc, where xs="U"] tnU smU ``` haftmann@29789 ` 1793` ``` have th':"\ ((t',n'),(s',m')) \ set (alluopairs U). ?P (t',n') (s',m')" ``` haftmann@29789 ` 1794` ``` by blast ``` haftmann@29789 ` 1795` ``` then obtain t' n' s' m' where ts'_U: "((t',n'),(s',m')) \ set (alluopairs U)" ``` haftmann@29789 ` 1796` ``` and Pts': "?P (t',n') (s',m')" by blast ``` haftmann@29789 ` 1797` ``` from ts'_U Up have mnz': "m' \ 0" and nnz': "n'\ 0" by auto ``` haftmann@29789 ` 1798` ``` let ?st' = "Add (Mul m' t') (Mul n' s')" ``` haftmann@29789 ` 1799` ``` have st': "(?N t' / real n' + ?N s' / real m')/2 = ?N ?st' / real (2*n'*m')" ``` haftmann@29789 ` 1800` ``` using mnz' nnz' by (simp add: algebra_simps add_divide_distrib) ``` haftmann@29789 ` 1801` ``` from Pts' have ``` haftmann@29789 ` 1802` ``` "(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 ``` haftmann@29789 ` 1803` ``` also have "\ = ((\(t, n). Inum (x # bs) t / real n) ((\((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t',n'),(s',m'))))" by (simp add: st') ``` haftmann@29789 ` 1804` ``` finally show "(Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2 ``` haftmann@29789 ` 1805` ``` \ (\(t, n). Inum (x # bs) t / real n) ` ``` haftmann@29789 ` 1806` ``` (\((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ` ``` haftmann@29789 ` 1807` ``` set (alluopairs U)" ``` haftmann@29789 ` 1808` ``` using ts'_U by blast ``` haftmann@29789 ` 1809` ```qed ``` haftmann@29789 ` 1810` haftmann@29789 ` 1811` ```lemma uset_cong: ``` haftmann@29789 ` 1812` ``` assumes lp: "isrlfm p" ``` haftmann@29789 ` 1813` ``` and UU': "((\ (t,n). Inum (x#bs) t /real n) ` U') = ((\ ((t,n),(s,m)). (Inum (x#bs) t /real n + Inum (x#bs) s /real m)/2) ` (U \ U))" (is "?f ` U' = ?g ` (U\U)") ``` haftmann@29789 ` 1814` ``` and U: "\ (t,n) \ U. numbound0 t \ n > 0" ``` haftmann@29789 ` 1815` ``` and U': "\ (t,n) \ U'. numbound0 t \ n > 0" ``` haftmann@29789 ` 1816` ``` shows "(\ (t,n) \ U. \ (s,m) \ U. Ifm (x#bs) (usubst p (Add (Mul m t) (Mul n s),2*n*m))) = (\ (t,n) \ U'. Ifm (x#bs) (usubst p (t,n)))" ``` haftmann@29789 ` 1817` ``` (is "?lhs = ?rhs") ``` haftmann@29789 ` 1818` ```proof ``` haftmann@29789 ` 1819` ``` assume ?lhs ``` haftmann@29789 ` 1820` ``` then obtain t n s m where tnU: "(t,n) \ U" and smU:"(s,m) \ U" and ``` haftmann@29789 ` 1821` ``` Pst: "Ifm (x#bs) (usubst p (Add (Mul m t) (Mul n s),2*n*m))" by blast ``` haftmann@29789 ` 1822` ``` let ?N = "\ t. Inum (x#bs) t" ``` haftmann@29789 ` 1823` ``` from tnU smU U have tnb: "numbound0 t" and np: "n > 0" ``` haftmann@29789 ` 1824` ``` and snb: "numbound0 s" and mp:"m > 0" by auto ``` haftmann@29789 ` 1825` ``` let ?st= "Add (Mul m t) (Mul n s)" ``` haftmann@29789 ` 1826` ``` from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" ``` haftmann@29789 ` 1827` ``` by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult) ``` haftmann@29789 ` 1828` ``` from tnb snb have stnb: "numbound0 ?st" by simp ``` haftmann@29789 ` 1829` ``` have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" ``` haftmann@29789 ` 1830` ``` using mp np by (simp add: algebra_simps add_divide_distrib) ``` haftmann@29789 ` 1831` ``` from tnU smU UU' have "?g ((t,n),(s,m)) \ ?f ` U'" by blast ``` haftmann@29789 ` 1832` ``` hence "\ (t',n') \ U'. ?g ((t,n),(s,m)) = ?f (t',n')" ``` haftmann@29789 ` 1833` ``` by auto (rule_tac x="(a,b)" in bexI, auto) ``` haftmann@29789 ` 1834` ``` then obtain t' n' where tnU': "(t',n') \ U'" and th: "?g ((t,n),(s,m)) = ?f (t',n')" by blast ``` haftmann@29789 ` 1835` ``` from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto ``` haftmann@29789 ` 1836` ``` from usubst_I[OF lp mnp stnb, where bs="bs" and x="x"] Pst ``` haftmann@29789 ` 1837` ``` have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" by simp ``` haftmann@29789 ` 1838` ``` 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]] ``` haftmann@29789 ` 1839` ``` have "Ifm (x # bs) (usubst p (t', n')) " by (simp only: st) ``` haftmann@29789 ` 1840` ``` then show ?rhs using tnU' by auto ``` haftmann@29789 ` 1841` ```next ``` haftmann@29789 ` 1842` ``` assume ?rhs ``` haftmann@29789 ` 1843` ``` then obtain t' n' where tnU': "(t',n') \ U'" and Pt': "Ifm (x # bs) (usubst p (t', n'))" ``` haftmann@29789 ` 1844` ``` by blast ``` haftmann@29789 ` 1845` ``` from tnU' UU' have "?f (t',n') \ ?g ` (U\U)" by blast ``` haftmann@29789 ` 1846` ``` hence "\ ((t,n),(s,m)) \ (U\U). ?f (t',n') = ?g ((t,n),(s,m))" ``` haftmann@29789 ` 1847` ``` by auto (rule_tac x="(a,b)" in bexI, auto) ``` haftmann@29789 ` 1848` ``` then obtain t n s m where tnU: "(t,n) \ U" and smU:"(s,m) \ U" and ``` haftmann@29789 ` 1849` ``` th: "?f (t',n') = ?g((t,n),(s,m)) "by blast ``` haftmann@29789 ` 1850` ``` let ?N = "\ t. Inum (x#bs) t" ``` haftmann@29789 ` 1851` ``` from tnU smU U have tnb: "numbound0 t" and np: "n > 0" ``` haftmann@29789 ` 1852` ``` and snb: "numbound0 s" and mp:"m > 0" by auto ``` haftmann@29789 ` 1853` ``` let ?st= "Add (Mul m t) (Mul n s)" ``` haftmann@29789 ` 1854` ``` from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" ``` haftmann@29789 ` 1855` ``` by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult) ``` haftmann@29789 ` 1856` ``` from tnb snb have stnb: "numbound0 ?st" by simp ``` haftmann@29789 ` 1857` ``` have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)" ``` haftmann@29789 ` 1858` ``` using mp np by (simp add: algebra_simps add_divide_distrib) ``` haftmann@29789 ` 1859` ``` from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto ``` haftmann@29789 ` 1860` ``` from usubst_I[OF lp np' tnb', where bs="bs" and x="x",simplified th[simplified split_def fst_conv snd_conv] st] Pt' ``` haftmann@29789 ` 1861` ``` have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" by simp ``` haftmann@29789 ` 1862` ``` with usubst_I[OF lp mnp stnb, where x="x" and bs="bs"] tnU smU show ?lhs by blast ``` haftmann@29789 ` 1863` ```qed ``` haftmann@29789 ` 1864` haftmann@29789 ` 1865` ```lemma ferrack: ``` haftmann@29789 ` 1866` ``` assumes qf: "qfree p" ``` haftmann@29789 ` 1867` ``` shows "qfree (ferrack p) \ ((Ifm bs (ferrack p)) = (\ x. Ifm (x#bs) p))" ``` haftmann@29789 ` 1868` ``` (is "_ \ (?rhs = ?lhs)") ``` haftmann@29789 ` 1869` ```proof- ``` haftmann@29789 ` 1870` ``` let ?I = "\ x p. Ifm (x#bs) p" ``` haftmann@29789 ` 1871` ``` fix x ``` haftmann@29789 ` 1872` ``` let ?N = "\ t. Inum (x#bs) t" ``` haftmann@29789 ` 1873` ``` let ?q = "rlfm (simpfm p)" ``` haftmann@29789 ` 1874` ``` let ?U = "uset ?q" ``` haftmann@29789 ` 1875` ``` let ?Up = "alluopairs ?U" ``` haftmann@29789 ` 1876` ``` let ?g = "\ ((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2*n*m)" ``` haftmann@29789 ` 1877` ``` let ?S = "map ?g ?Up" ``` haftmann@29789 ` 1878` ``` let ?SS = "map simp_num_pair ?S" ``` haftmann@36853 ` 1879` ``` let ?Y = "remdups ?SS" ``` haftmann@29789 ` 1880` ``` let ?f= "(\ (t,n). ?N t / real n)" ``` haftmann@29789 ` 1881` ``` let ?h = "\ ((t,n),(s,m)). (?N t/real n + ?N s/ real m) /2" ``` haftmann@29789 ` 1882` ``` let ?F = "\ p. \ a \ set (uset p). \ b \ set (uset p). ?I x (usubst p (?g(a,b)))" ``` haftmann@29789 ` 1883` ``` let ?ep = "evaldjf (simpfm o (usubst ?q)) ?Y" ``` haftmann@29789 ` 1884` ``` from rlfm_I[OF simpfm_qf[OF qf]] have lq: "isrlfm ?q" by blast ``` haftmann@29789 ` 1885` ``` from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \ (set ?U \ set ?U)" by simp ``` haftmann@29789 ` 1886` ``` from uset_l[OF lq] have U_l: "\ (t,n) \ set ?U. numbound0 t \ n > 0" . ``` haftmann@29789 ` 1887` ``` from U_l UpU ``` haftmann@29789 ` 1888` ``` have "\ ((t,n),(s,m)) \ set ?Up. numbound0 t \ n> 0 \ numbound0 s \ m > 0" by auto ``` haftmann@29789 ` 1889` ``` hence Snb: "\ (t,n) \ set ?S. numbound0 t \ n > 0 " ``` haftmann@29789 ` 1890` ``` by (auto simp add: mult_pos_pos) ``` haftmann@29789 ` 1891` ``` have Y_l: "\ (t,n) \ set ?Y. numbound0 t \ n > 0" ``` haftmann@29789 ` 1892` ``` proof- ``` haftmann@29789 ` 1893` ``` { fix t n assume tnY: "(t,n) \ set ?Y" ``` haftmann@29789 ` 1894` ``` hence "(t,n) \ set ?SS" by simp ``` haftmann@29789 ` 1895` ``` hence "\ (t',n') \ set ?S. simp_num_pair (t',n') = (t,n)" ``` hoelzl@33639 ` 1896` ``` by (auto simp add: split_def simp del: map_map) ``` hoelzl@33639 ` 1897` ``` (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all) ``` haftmann@29789 ` 1898` ``` then obtain t' n' where tn'S: "(t',n') \ set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast ``` haftmann@29789 ` 1899` ``` from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto ``` haftmann@29789 ` 1900` ``` from simp_num_pair_l[OF tnb np tns] ``` haftmann@29789 ` 1901` ``` have "numbound0 t \ n > 0" . } ``` haftmann@29789 ` 1902` ``` thus ?thesis by blast ``` haftmann@29789 ` 1903` ``` qed ``` haftmann@29789 ` 1904` haftmann@29789 ` 1905` ``` have YU: "(?f ` set ?Y) = (?h ` (set ?U \ set ?U))" ``` haftmann@29789 ` 1906` ``` proof- ``` haftmann@29789 ` 1907` ``` from simp_num_pair_ci[where bs="x#bs"] have ``` haftmann@29789 ` 1908` ``` "\x. (?f o simp_num_pair) x = ?f x" by auto ``` haftmann@29789 ` 1909` ``` hence th: "?f o simp_num_pair = ?f" using ext by blast ``` haftmann@29789 ` 1910` ``` have "(?f ` set ?Y) = ((?f o simp_num_pair) ` set ?S)" by (simp add: image_compose) ``` haftmann@29789 ` 1911` ``` also have "\ = (?f ` set ?S)" by (simp add: th) ``` haftmann@29789 ` 1912` ``` also have "\ = ((?f o ?g) ` set ?Up)" ``` haftmann@29789 ` 1913` ``` by (simp only: set_map o_def image_compose[symmetric]) ``` haftmann@29789 ` 1914` ``` also have "\ = (?h ` (set ?U \ set ?U))" ``` haftmann@29789 ` 1915` ``` using uset_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_compose[symmetric]] by blast ``` haftmann@29789 ` 1916` ``` finally show ?thesis . ``` haftmann@29789 ` 1917` ``` qed ``` haftmann@29789 ` 1918` ``` have "\ (t,n) \ set ?Y. bound0 (simpfm (usubst ?q (t,n)))" ``` haftmann@29789 ` 1919` ``` proof- ``` haftmann@29789 ` 1920` ``` { fix t n assume tnY: "(t,n) \ set ?Y" ``` haftmann@29789 ` 1921` ``` with Y_l have tnb: "numbound0 t" and np: "real n > 0" by auto ``` haftmann@29789 ` 1922` ``` from usubst_I[OF lq np tnb] ``` haftmann@29789 ` 1923` ``` have "bound0 (usubst ?q (t,n))" by simp hence "bound0 (simpfm (usubst ?q (t,n)))" ``` haftmann@29789 ` 1924` ``` using simpfm_bound0 by simp} ``` haftmann@29789 ` 1925` ``` thus ?thesis by blast ``` haftmann@29789 ` 1926` ``` qed ``` haftmann@29789 ` 1927` ``` hence ep_nb: "bound0 ?ep" using evaldjf_bound0[where xs="?Y" and f="simpfm o (usubst ?q)"] by auto ``` haftmann@29789 ` 1928` ``` let ?mp = "minusinf ?q" ``` haftmann@29789 ` 1929` ``` let ?pp = "plusinf ?q" ``` haftmann@29789 ` 1930` ``` let ?M = "?I x ?mp" ``` haftmann@29789 ` 1931` ``` let ?P = "?I x ?pp" ``` haftmann@29789 ` 1932` ``` let ?res = "disj ?mp (disj ?pp ?ep)" ``` haftmann@29789 ` 1933` ``` from rminusinf_bound0[OF lq] rplusinf_bound0[OF lq] ep_nb ``` haftmann@29789 ` 1934` ``` have nbth: "bound0 ?res" by auto ``` haftmann@29789 ` 1935` haftmann@29789 ` 1936` ``` from conjunct1[OF rlfm_I[OF simpfm_qf[OF qf]]] simpfm ``` haftmann@29789 ` 1937` haftmann@29789 ` 1938` ``` have th: "?lhs = (\ x. ?I x ?q)" by auto ``` haftmann@29789 ` 1939` ``` from th fr_equsubst[OF lq, where bs="bs" and x="x"] have lhfr: "?lhs = (?M \ ?P \ ?F ?q)" ``` haftmann@29789 ` 1940` ``` by (simp only: split_def fst_conv snd_conv) ``` haftmann@29789 ` 1941` ``` also have "\ = (?M \ ?P \ (\ (t,n) \ set ?Y. ?I x (simpfm (usubst ?q (t,n)))))" ``` haftmann@29789 ` 1942` ``` using uset_cong[OF lq YU U_l Y_l] by (simp only: split_def fst_conv snd_conv simpfm) ``` haftmann@29789 ` 1943` ``` also have "\ = (Ifm (x#bs) ?res)" ``` haftmann@29789 ` 1944` ``` using evaldjf_ex[where ps="?Y" and bs = "x#bs" and f="simpfm o (usubst ?q)",symmetric] ``` haftmann@29789 ` 1945` ``` by (simp add: split_def pair_collapse) ``` haftmann@29789 ` 1946` ``` finally have lheq: "?lhs = (Ifm bs (decr ?res))" using decr[OF nbth] by blast ``` haftmann@29789 ` 1947` ``` hence lr: "?lhs = ?rhs" apply (unfold ferrack_def Let_def) ``` haftmann@29789 ` 1948` ``` by (cases "?mp = T \ ?pp = T", auto) (simp add: disj_def)+ ``` haftmann@29789 ` 1949` ``` from decr_qf[OF nbth] have "qfree (ferrack p)" by (auto simp add: Let_def ferrack_def) ``` haftmann@29789 ` 1950` ``` with lr show ?thesis by blast ``` haftmann@29789 ` 1951` ```qed ``` haftmann@29789 ` 1952` haftmann@29789 ` 1953` ```definition linrqe:: "fm \ fm" where ``` haftmann@29789 ` 1954` ``` "linrqe p = qelim (prep p) ferrack" ``` haftmann@29789 ` 1955` haftmann@29789 ` 1956` ```theorem linrqe: "Ifm bs (linrqe p) = Ifm bs p \ qfree (linrqe p)" ``` haftmann@29789 ` 1957` ```using ferrack qelim_ci prep ``` haftmann@29789 ` 1958` ```unfolding linrqe_def by auto ``` haftmann@29789 ` 1959` haftmann@29789 ` 1960` ```definition ferrack_test :: "unit \ fm" where ``` haftmann@29789 ` 1961` ``` "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0))) ``` haftmann@29789 ` 1962` ``` (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" ``` haftmann@29789 ` 1963` haftmann@29789 ` 1964` ```ML {* @{code ferrack_test} () *} ``` haftmann@29789 ` 1965` haftmann@29789 ` 1966` ```oracle linr_oracle = {* ``` haftmann@29789 ` 1967` ```let ``` haftmann@29789 ` 1968` haftmann@36853 ` 1969` ```fun num_of_term vs (Free vT) = @{code Bound} (find_index (fn vT' => vT = vT') vs) ``` haftmann@29789 ` 1970` ``` | num_of_term vs @{term "real (0::int)"} = @{code C} 0 ``` haftmann@29789 ` 1971` ``` | num_of_term vs @{term "real (1::int)"} = @{code C} 1 ``` haftmann@29789 ` 1972` ``` | num_of_term vs @{term "0::real"} = @{code C} 0 ``` haftmann@29789 ` 1973` ``` | num_of_term vs @{term "1::real"} = @{code C} 1 ``` haftmann@29789 ` 1974` ``` | num_of_term vs (Bound i) = @{code Bound} i ``` haftmann@29789 ` 1975` ``` | num_of_term vs (@{term "uminus :: real \ real"} \$ t') = @{code Neg} (num_of_term vs t') ``` haftmann@36853 ` 1976` ``` | num_of_term vs (@{term "op + :: real \ real \ real"} \$ t1 \$ t2) = ``` haftmann@36853 ` 1977` ``` @{code Add} (num_of_term vs t1, num_of_term vs t2) ``` haftmann@36853 ` 1978` ``` | num_of_term vs (@{term "op - :: real \ real \ real"} \$ t1 \$ t2) = ``` haftmann@36853 ` 1979` ``` @{code Sub} (num_of_term vs t1, num_of_term vs t2) ``` haftmann@36853 ` 1980` ``` | num_of_term vs (@{term "op * :: real \ real \ real"} \$ t1 \$ t2) = (case num_of_term vs t1 ``` haftmann@29789 ` 1981` ``` of @{code C} i => @{code Mul} (i, num_of_term vs t2) ``` haftmann@36853 ` 1982` ``` | _ => error "num_of_term: unsupported multiplication") ``` haftmann@36853 ` 1983` ``` | num_of_term vs (@{term "real :: int \ real"} \$ (@{term "number_of :: int \ int"} \$ t')) = ``` haftmann@36853 ` 1984` ``` @{code C} (HOLogic.dest_numeral t') ``` haftmann@36853 ` 1985` ``` | num_of_term vs (@{term "number_of :: int \ real"} \$ t') = ``` haftmann@36853 ` 1986` ``` @{code C} (HOLogic.dest_numeral t') ``` haftmann@36853 ` 1987` ``` | num_of_term vs t = error ("num_of_term: unknown term"); ``` haftmann@29789 ` 1988` haftmann@29789 ` 1989` ```fun fm_of_term vs @{term True} = @{code T} ``` haftmann@29789 ` 1990` ``` | fm_of_term vs @{term False} = @{code F} ``` haftmann@36853 ` 1991` ``` | fm_of_term vs (@{term "op < :: real \ real \ bool"} \$ t1 \$ t2) = ``` haftmann@36853 ` 1992` ``` @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) ``` haftmann@36853 ` 1993` ``` | fm_of_term vs (@{term "op \ :: real \ real \ bool"} \$ t1 \$ t2) = ``` haftmann@36853 ` 1994` ``` @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) ``` haftmann@36853 ` 1995` ``` | fm_of_term vs (@{term "op = :: real \ real \ bool"} \$ t1 \$ t2) = ``` haftmann@36853 ` 1996` ``` @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) ``` haftmann@36853 ` 1997` ``` | fm_of_term vs (@{term "op \ :: bool \ bool \ bool"} \$ t1 \$ t2) = ``` haftmann@36853 ` 1998` ``` @{code Iff} (fm_of_term vs t1, fm_of_term vs t2) ``` haftmann@29789 ` 1999` ``` | fm_of_term vs (@{term "op &"} \$ t1 \$ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2) ``` haftmann@29789 ` 2000` ``` | fm_of_term vs (@{term "op |"} \$ t1 \$ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2) ``` haftmann@29789 ` 2001` ``` | fm_of_term vs (@{term "op -->"} \$ t1 \$ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2) ``` haftmann@29789 ` 2002` ``` | fm_of_term vs (@{term "Not"} \$ t') = @{code NOT} (fm_of_term vs t') ``` haftmann@38558 ` 2003` ``` | fm_of_term vs (Const (@{const_name Ex}, _) \$ Abs (xn, xT, p)) = ``` haftmann@36853 ` 2004` ``` @{code E} (fm_of_term (("", dummyT) :: vs) p) ``` haftmann@38558 ` 2005` ``` | fm_of_term vs (Const (@{const_name All}, _) \$ Abs (xn, xT, p)) = ``` haftmann@36853 ` 2006` ``` @{code A} (fm_of_term (("", dummyT) :: vs) p) ``` haftmann@29789 ` 2007` ``` | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); ``` haftmann@29789 ` 2008` haftmann@29789 ` 2009` ```fun term_of_num vs (@{code C} i) = @{term "real :: int \ real"} \$ HOLogic.mk_number HOLogic.intT i ``` haftmann@36853 ` 2010` ``` | term_of_num vs (@{code Bound} n) = Free (nth vs n) ``` haftmann@29789 ` 2011` ``` | term_of_num vs (@{code Neg} t') = @{term "uminus :: real \ real"} \$ term_of_num vs t' ``` haftmann@29789 ` 2012` ``` | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: real \ real \ real"} \$ ``` haftmann@29789 ` 2013` ``` term_of_num vs t1 \$ term_of_num vs t2 ``` haftmann@29789 ` 2014` ``` | term_of_num vs (@{code Sub} (t1, t2)) = @{term "op - :: real \ real \ real"} \$ ``` haftmann@29789 ` 2015` ``` term_of_num vs t1 \$ term_of_num vs t2 ``` haftmann@29789 ` 2016` ``` | term_of_num vs (@{code Mul} (i, t2)) = @{term "op * :: real \ real \ real"} \$ ``` haftmann@29789 ` 2017` ``` term_of_num vs (@{code C} i) \$ term_of_num vs t2 ``` haftmann@29789 ` 2018` ``` | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t)); ``` haftmann@29789 ` 2019` haftmann@29789 ` 2020` ```fun term_of_fm vs @{code T} = HOLogic.true_const ``` haftmann@29789 ` 2021` ``` | term_of_fm vs @{code F} = HOLogic.false_const ``` haftmann@29789 ` 2022` ``` | term_of_fm vs (@{code Lt} t) = @{term "op < :: real \ real \ bool"} \$ ``` haftmann@29789 ` 2023` ``` term_of_num vs t \$ @{term "0::real"} ``` haftmann@29789 ` 2024` ``` | term_of_fm vs (@{code Le} t) = @{term "op \ :: real \ real \ bool"} \$ ``` haftmann@29789 ` 2025` ``` term_of_num vs t \$ @{term "0::real"} ``` haftmann@29789 ` 2026` ``` | term_of_fm vs (@{code Gt} t) = @{term "op < :: real \ real \ bool"} \$ ``` haftmann@29789 ` 2027` ``` @{term "0::real"} \$ term_of_num vs t ``` haftmann@29789 ` 2028` ``` | term_of_fm vs (@{code Ge} t) = @{term "op \ :: real \ real \ bool"} \$ ``` haftmann@29789 ` 2029` ``` @{term "0::real"} \$ term_of_num vs t ``` haftmann@29789 ` 2030` ``` | term_of_fm vs (@{code Eq} t) = @{term "op = :: real \ real \ bool"} \$ ``` haftmann@29789 ` 2031` ``` term_of_num vs t \$ @{term "0::real"} ``` haftmann@29789 ` 2032` ``` | term_of_fm vs (@{code NEq} t) = term_of_fm vs (@{code NOT} (@{code Eq} t)) ``` haftmann@29789 ` 2033` ``` | term_of_fm vs (@{code NOT} t') = HOLogic.Not \$ term_of_fm vs t' ``` haftmann@29789 ` 2034` ``` | term_of_fm vs (@{code And} (t1, t2)) = HOLogic.conj \$ term_of_fm vs t1 \$ term_of_fm vs t2 ``` haftmann@29789 ` 2035` ``` | term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj \$ term_of_fm vs t1 \$ term_of_fm vs t2 ``` haftmann@29789 ` 2036` ``` | term_of_fm vs (@{code Imp} (t1, t2)) = HOLogic.imp \$ term_of_fm vs t1 \$ term_of_fm vs t2 ``` haftmann@29789 ` 2037` ``` | term_of_fm vs (@{code Iff} (t1, t2)) = @{term "op \ :: bool \ bool \ bool"} \$ ``` haftmann@36853 ` 2038` ``` term_of_fm vs t1 \$ term_of_fm vs t2; ``` haftmann@29789 ` 2039` haftmann@36853 ` 2040` ```in fn (ctxt, t) => ``` haftmann@29789 ` 2041` ``` let ``` haftmann@36853 ` 2042` ``` val vs = Term.add_frees t []; ``` haftmann@36853 ` 2043` ``` val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t; ``` haftmann@36853 ` 2044` ``` in (Thm.cterm_of (ProofContext.theory_of ctxt) o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end ``` haftmann@29789 ` 2045` ```end; ``` haftmann@29789 ` 2046` ```*} ``` haftmann@29789 ` 2047` haftmann@29789 ` 2048` ```use "ferrack_tac.ML" ``` haftmann@29789 ` 2049` ```setup Ferrack_Tac.setup ``` haftmann@29789 ` 2050` haftmann@29789 ` 2051` ```lemma ``` haftmann@29789 ` 2052` ``` fixes x :: real ``` haftmann@29789 ` 2053` ``` shows "2 * x \ 2 * x \ 2 * x \ 2 * x + 1" ``` haftmann@29789 ` 2054` ```apply rferrack ``` haftmann@29789 ` 2055` ```done ``` haftmann@29789 ` 2056` haftmann@29789 ` 2057` ```lemma ``` haftmann@29789 ` 2058` ``` fixes x :: real ``` haftmann@29789 ` 2059` ``` shows "\y \ x. x = y + 1" ``` haftmann@29789 ` 2060` ```apply rferrack ``` haftmann@29789 ` 2061` ```done ``` haftmann@29789 ` 2062` haftmann@29789 ` 2063` ```lemma ``` haftmann@29789 ` 2064` ``` fixes x :: real ``` haftmann@29789 ` 2065` ``` shows "\ (\z. x + z = x + z + 1)" ``` haftmann@29789 ` 2066` ```apply rferrack ``` haftmann@29789 ` 2067` ```done ``` haftmann@29789 ` 2068` haftmann@29789 ` 2069` ```end ```