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