src/HOL/Decision_Procs/MIR.thy
 author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51474 1e9e68247ad1 parent 51369 960b0ca9ae5d child 53168 d998de7f0efc permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
 hoelzl@30439 ` 1` ```(* Title: HOL/Decision_Procs/MIR.thy ``` chaieb@23264 ` 2` ``` Author: Amine Chaieb ``` chaieb@23264 ` 3` ```*) ``` chaieb@23264 ` 4` chaieb@23264 ` 5` ```theory MIR ``` nipkow@41849 ` 6` ```imports Complex_Main Dense_Linear_Order DP_Library ``` haftmann@51143 ` 7` ``` "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef" ``` haftmann@27368 ` 8` ```begin ``` chaieb@23264 ` 9` haftmann@27456 ` 10` ```section {* Quantifier elimination for @{text "\ (0, 1, +, floor, <)"} *} ``` haftmann@27456 ` 11` chaieb@23264 ` 12` ```declare real_of_int_floor_cancel [simp del] ``` chaieb@23264 ` 13` wenzelm@51369 ` 14` ```lemma myle: ``` wenzelm@51369 ` 15` ``` fixes a b :: "'a::{ordered_ab_group_add}" ``` nipkow@41849 ` 16` ``` shows "(a \ b) = (0 \ b - a)" ``` wenzelm@51369 ` 17` ``` by (metis add_0_left add_le_cancel_right diff_add_cancel) ``` wenzelm@51369 ` 18` wenzelm@51369 ` 19` ```lemma myless: ``` wenzelm@51369 ` 20` ``` fixes a b :: "'a::{ordered_ab_group_add}" ``` nipkow@41849 ` 21` ``` shows "(a < b) = (0 < b - a)" ``` wenzelm@51369 ` 22` ``` by (metis le_iff_diff_le_0 less_le_not_le myle) ``` chaieb@23264 ` 23` chaieb@23264 ` 24` ``` (* Maybe should be added to the library \ *) ``` chaieb@23264 ` 25` ```lemma floor_int_eq: "(real n\ x \ x < real (n+1)) = (floor x = n)" ``` chaieb@23264 ` 26` ```proof( auto) ``` chaieb@23264 ` 27` ``` assume lb: "real n \ x" ``` chaieb@23264 ` 28` ``` and ub: "x < real n + 1" ``` chaieb@23264 ` 29` ``` have "real (floor x) \ x" by simp ``` chaieb@23264 ` 30` ``` hence "real (floor x) < real (n + 1) " using ub by arith ``` chaieb@23264 ` 31` ``` hence "floor x < n+1" by simp ``` huffman@30097 ` 32` ``` moreover from lb have "n \ floor x" using floor_mono[where x="real n" and y="x"] ``` chaieb@23264 ` 33` ``` by simp ultimately show "floor x = n" by simp ``` chaieb@23264 ` 34` ```qed ``` chaieb@23264 ` 35` chaieb@23264 ` 36` ```(* Periodicity of dvd *) ``` chaieb@23264 ` 37` ```lemma dvd_period: ``` chaieb@23264 ` 38` ``` assumes advdd: "(a::int) dvd d" ``` chaieb@23264 ` 39` ``` shows "(a dvd (x + t)) = (a dvd ((x+ c*d) + t))" ``` chaieb@23264 ` 40` ``` using advdd ``` chaieb@23264 ` 41` ```proof- ``` wenzelm@51369 ` 42` ``` { fix x k ``` chaieb@23316 ` 43` ``` from inf_period(3)[OF advdd, rule_format, where x=x and k="-k"] ``` chaieb@23316 ` 44` ``` have " ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))" by simp} ``` chaieb@23316 ` 45` ``` hence "\x.\k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))" by simp ``` chaieb@23264 ` 46` ``` then show ?thesis by simp ``` chaieb@23264 ` 47` ```qed ``` chaieb@23264 ` 48` wenzelm@32960 ` 49` ```(* The Divisibility relation between reals *) ``` wenzelm@51369 ` 50` ```definition rdvd:: "real \ real \ bool" (infixl "rdvd" 50) ``` wenzelm@51369 ` 51` ``` where "x rdvd y \ (\k\int. y = x * real k)" ``` chaieb@23264 ` 52` chaieb@23264 ` 53` ```lemma int_rdvd_real: ``` wenzelm@51369 ` 54` ``` "real (i::int) rdvd x = (i dvd (floor x) \ real (floor x) = x)" (is "?l = ?r") ``` chaieb@23264 ` 55` ```proof ``` chaieb@23264 ` 56` ``` assume "?l" ``` chaieb@23264 ` 57` ``` hence th: "\ k. x=real (i*k)" by (simp add: rdvd_def) ``` chaieb@23264 ` 58` ``` hence th': "real (floor x) = x" by (auto simp del: real_of_int_mult) ``` chaieb@23264 ` 59` ``` with th have "\ k. real (floor x) = real (i*k)" by simp ``` chaieb@23264 ` 60` ``` hence "\ k. floor x = i*k" by (simp only: real_of_int_inject) ``` chaieb@23264 ` 61` ``` thus ?r using th' by (simp add: dvd_def) ``` chaieb@23264 ` 62` ```next ``` chaieb@23264 ` 63` ``` assume "?r" hence "(i\int) dvd \x\real\" .. ``` chaieb@23264 ` 64` ``` hence "\ k. real (floor x) = real (i*k)" ``` chaieb@23264 ` 65` ``` by (simp only: real_of_int_inject) (simp add: dvd_def) ``` wenzelm@41807 ` 66` ``` thus ?l using `?r` by (simp add: rdvd_def) ``` chaieb@23264 ` 67` ```qed ``` chaieb@23264 ` 68` chaieb@23264 ` 69` ```lemma int_rdvd_iff: "(real (i::int) rdvd real t) = (i dvd t)" ``` wenzelm@51369 ` 70` ``` by (auto simp add: rdvd_def dvd_def) (rule_tac x="k" in exI, simp only: real_of_int_mult[symmetric]) ``` wenzelm@51369 ` 71` wenzelm@51369 ` 72` wenzelm@51369 ` 73` ```lemma rdvd_abs1: "(abs (real d) rdvd t) = (real (d ::int) rdvd t)" ``` chaieb@23264 ` 74` ```proof ``` chaieb@23264 ` 75` ``` assume d: "real d rdvd t" ``` wenzelm@51369 ` 76` ``` from d int_rdvd_real have d2: "d dvd (floor t)" and ti: "real (floor t) = t" ``` wenzelm@51369 ` 77` ``` by auto ``` chaieb@23264 ` 78` nipkow@30042 ` 79` ``` from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd (floor t)" by blast ``` chaieb@23264 ` 80` ``` with ti int_rdvd_real[symmetric] have "real (abs d) rdvd t" by blast ``` chaieb@23264 ` 81` ``` thus "abs (real d) rdvd t" by simp ``` chaieb@23264 ` 82` ```next ``` chaieb@23264 ` 83` ``` assume "abs (real d) rdvd t" hence "real (abs d) rdvd t" by simp ``` wenzelm@51369 ` 84` ``` with int_rdvd_real[where i="abs d" and x="t"] have d2: "abs d dvd floor t" and ti: "real (floor t) =t" ``` wenzelm@51369 ` 85` ``` by auto ``` nipkow@30042 ` 86` ``` from iffD1[OF abs_dvd_iff] d2 have "d dvd floor t" by blast ``` chaieb@23264 ` 87` ``` with ti int_rdvd_real[symmetric] show "real d rdvd t" by blast ``` chaieb@23264 ` 88` ```qed ``` chaieb@23264 ` 89` chaieb@23264 ` 90` ```lemma rdvd_minus: "(real (d::int) rdvd t) = (real d rdvd -t)" ``` chaieb@23264 ` 91` ``` apply (auto simp add: rdvd_def) ``` chaieb@23264 ` 92` ``` apply (rule_tac x="-k" in exI, simp) ``` chaieb@23264 ` 93` ``` apply (rule_tac x="-k" in exI, simp) ``` wenzelm@51369 ` 94` ``` done ``` chaieb@23264 ` 95` chaieb@23264 ` 96` ```lemma rdvd_left_0_eq: "(0 rdvd t) = (t=0)" ``` wenzelm@51369 ` 97` ``` by (auto simp add: rdvd_def) ``` chaieb@23264 ` 98` chaieb@23264 ` 99` ```lemma rdvd_mult: ``` chaieb@23264 ` 100` ``` assumes knz: "k\0" ``` chaieb@23264 ` 101` ``` shows "(real (n::int) * real (k::int) rdvd x * real k) = (real n rdvd x)" ``` wenzelm@51369 ` 102` ``` using knz by (simp add: rdvd_def) ``` chaieb@23264 ` 103` chaieb@23264 ` 104` ``` (*********************************************************************************) ``` chaieb@23264 ` 105` ``` (**** SHADOW SYNTAX AND SEMANTICS ****) ``` chaieb@23264 ` 106` ``` (*********************************************************************************) ``` chaieb@23264 ` 107` chaieb@23264 ` 108` ```datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num ``` chaieb@23264 ` 109` ``` | Mul int num | Floor num| CF int num num ``` chaieb@23264 ` 110` chaieb@23264 ` 111` ``` (* A size for num to make inductive proofs simpler*) ``` haftmann@25765 ` 112` ```primrec num_size :: "num \ nat" where ``` chaieb@23264 ` 113` ``` "num_size (C c) = 1" ``` chaieb@23264 ` 114` ```| "num_size (Bound n) = 1" ``` chaieb@23264 ` 115` ```| "num_size (Neg a) = 1 + num_size a" ``` chaieb@23264 ` 116` ```| "num_size (Add a b) = 1 + num_size a + num_size b" ``` chaieb@23264 ` 117` ```| "num_size (Sub a b) = 3 + num_size a + num_size b" ``` chaieb@23264 ` 118` ```| "num_size (CN n c a) = 4 + num_size a " ``` chaieb@23264 ` 119` ```| "num_size (CF c a b) = 4 + num_size a + num_size b" ``` chaieb@23264 ` 120` ```| "num_size (Mul c a) = 1 + num_size a" ``` chaieb@23264 ` 121` ```| "num_size (Floor a) = 1 + num_size a" ``` chaieb@23264 ` 122` chaieb@23264 ` 123` ``` (* Semantics of numeral terms (num) *) ``` haftmann@25765 ` 124` ```primrec Inum :: "real list \ num \ real" where ``` chaieb@23264 ` 125` ``` "Inum bs (C c) = (real c)" ``` chaieb@23264 ` 126` ```| "Inum bs (Bound n) = bs!n" ``` chaieb@23264 ` 127` ```| "Inum bs (CN n c a) = (real c) * (bs!n) + (Inum bs a)" ``` chaieb@23264 ` 128` ```| "Inum bs (Neg a) = -(Inum bs a)" ``` chaieb@23264 ` 129` ```| "Inum bs (Add a b) = Inum bs a + Inum bs b" ``` chaieb@23264 ` 130` ```| "Inum bs (Sub a b) = Inum bs a - Inum bs b" ``` chaieb@23264 ` 131` ```| "Inum bs (Mul c a) = (real c) * Inum bs a" ``` chaieb@23264 ` 132` ```| "Inum bs (Floor a) = real (floor (Inum bs a))" ``` chaieb@23264 ` 133` ```| "Inum bs (CF c a b) = real c * real (floor (Inum bs a)) + Inum bs b" ``` chaieb@23264 ` 134` ```definition "isint t bs \ real (floor (Inum bs t)) = Inum bs t" ``` chaieb@23264 ` 135` chaieb@23264 ` 136` ```lemma isint_iff: "isint n bs = (real (floor (Inum bs n)) = Inum bs n)" ``` wenzelm@51369 ` 137` ``` by (simp add: isint_def) ``` chaieb@23264 ` 138` chaieb@23264 ` 139` ```lemma isint_Floor: "isint (Floor n) bs" ``` chaieb@23264 ` 140` ``` by (simp add: isint_iff) ``` chaieb@23264 ` 141` chaieb@23264 ` 142` ```lemma isint_Mul: "isint e bs \ isint (Mul c e) bs" ``` chaieb@23264 ` 143` ```proof- ``` chaieb@23264 ` 144` ``` let ?e = "Inum bs e" ``` chaieb@23264 ` 145` ``` let ?fe = "floor ?e" ``` chaieb@23264 ` 146` ``` assume be: "isint e bs" hence efe:"real ?fe = ?e" by (simp add: isint_iff) ``` chaieb@23264 ` 147` ``` have "real ((floor (Inum bs (Mul c e)))) = real (floor (real (c * ?fe)))" using efe by simp ``` chaieb@23264 ` 148` ``` also have "\ = real (c* ?fe)" by (simp only: floor_real_of_int) ``` chaieb@23264 ` 149` ``` also have "\ = real c * ?e" using efe by simp ``` chaieb@23264 ` 150` ``` finally show ?thesis using isint_iff by simp ``` chaieb@23264 ` 151` ```qed ``` chaieb@23264 ` 152` chaieb@23264 ` 153` ```lemma isint_neg: "isint e bs \ isint (Neg e) bs" ``` chaieb@23264 ` 154` ```proof- ``` chaieb@23264 ` 155` ``` let ?I = "\ t. Inum bs t" ``` chaieb@23264 ` 156` ``` assume ie: "isint e bs" ``` chaieb@23264 ` 157` ``` hence th: "real (floor (?I e)) = ?I e" by (simp add: isint_def) ``` chaieb@23264 ` 158` ``` have "real (floor (?I (Neg e))) = real (floor (- (real (floor (?I e)))))" by (simp add: th) ``` wenzelm@51369 ` 159` ``` also have "\ = - real (floor (?I e))" by simp ``` chaieb@23264 ` 160` ``` finally show "isint (Neg e) bs" by (simp add: isint_def th) ``` chaieb@23264 ` 161` ```qed ``` chaieb@23264 ` 162` chaieb@23264 ` 163` ```lemma isint_sub: ``` chaieb@23264 ` 164` ``` assumes ie: "isint e bs" shows "isint (Sub (C c) e) bs" ``` chaieb@23264 ` 165` ```proof- ``` chaieb@23264 ` 166` ``` let ?I = "\ t. Inum bs t" ``` chaieb@23264 ` 167` ``` from ie have th: "real (floor (?I e)) = ?I e" by (simp add: isint_def) ``` chaieb@23264 ` 168` ``` have "real (floor (?I (Sub (C c) e))) = real (floor ((real (c -floor (?I e)))))" by (simp add: th) ``` wenzelm@51369 ` 169` ``` also have "\ = real (c- floor (?I e))" by simp ``` chaieb@23264 ` 170` ``` finally show "isint (Sub (C c) e) bs" by (simp add: isint_def th) ``` chaieb@23264 ` 171` ```qed ``` chaieb@23264 ` 172` wenzelm@51369 ` 173` ```lemma isint_add: ``` wenzelm@51369 ` 174` ``` assumes ai: "isint a bs" and bi: "isint b bs" ``` wenzelm@51369 ` 175` ``` shows "isint (Add a b) bs" ``` chaieb@23264 ` 176` ```proof- ``` chaieb@23264 ` 177` ``` let ?a = "Inum bs a" ``` chaieb@23264 ` 178` ``` let ?b = "Inum bs b" ``` wenzelm@51369 ` 179` ``` from ai bi isint_iff have "real (floor (?a + ?b)) = real (floor (real (floor ?a) + real (floor ?b)))" ``` wenzelm@51369 ` 180` ``` by simp ``` chaieb@23264 ` 181` ``` also have "\ = real (floor ?a) + real (floor ?b)" by simp ``` chaieb@23264 ` 182` ``` also have "\ = ?a + ?b" using ai bi isint_iff by simp ``` chaieb@23264 ` 183` ``` finally show "isint (Add a b) bs" by (simp add: isint_iff) ``` chaieb@23264 ` 184` ```qed ``` chaieb@23264 ` 185` chaieb@23264 ` 186` ```lemma isint_c: "isint (C j) bs" ``` chaieb@23264 ` 187` ``` by (simp add: isint_iff) ``` chaieb@23264 ` 188` chaieb@23264 ` 189` chaieb@23264 ` 190` ``` (* FORMULAE *) ``` chaieb@23264 ` 191` ```datatype fm = ``` chaieb@23264 ` 192` ``` T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num| ``` chaieb@23264 ` 193` ``` NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm ``` chaieb@23264 ` 194` chaieb@23264 ` 195` chaieb@23264 ` 196` ``` (* A size for fm *) ``` chaieb@23264 ` 197` ```fun fmsize :: "fm \ nat" where ``` chaieb@23264 ` 198` ``` "fmsize (NOT p) = 1 + fmsize p" ``` chaieb@23264 ` 199` ```| "fmsize (And p q) = 1 + fmsize p + fmsize q" ``` chaieb@23264 ` 200` ```| "fmsize (Or p q) = 1 + fmsize p + fmsize q" ``` chaieb@23264 ` 201` ```| "fmsize (Imp p q) = 3 + fmsize p + fmsize q" ``` chaieb@23264 ` 202` ```| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)" ``` chaieb@23264 ` 203` ```| "fmsize (E p) = 1 + fmsize p" ``` chaieb@23264 ` 204` ```| "fmsize (A p) = 4+ fmsize p" ``` chaieb@23264 ` 205` ```| "fmsize (Dvd i t) = 2" ``` chaieb@23264 ` 206` ```| "fmsize (NDvd i t) = 2" ``` chaieb@23264 ` 207` ```| "fmsize p = 1" ``` chaieb@23264 ` 208` ``` (* several lemmas about fmsize *) ``` wenzelm@32960 ` 209` ```lemma fmsize_pos: "fmsize p > 0" ``` wenzelm@51369 ` 210` ``` by (induct p rule: fmsize.induct) simp_all ``` chaieb@23264 ` 211` chaieb@23264 ` 212` ``` (* Semantics of formulae (fm) *) ``` haftmann@25765 ` 213` ```primrec Ifm ::"real list \ fm \ bool" where ``` chaieb@23264 ` 214` ``` "Ifm bs T = True" ``` chaieb@23264 ` 215` ```| "Ifm bs F = False" ``` chaieb@23264 ` 216` ```| "Ifm bs (Lt a) = (Inum bs a < 0)" ``` chaieb@23264 ` 217` ```| "Ifm bs (Gt a) = (Inum bs a > 0)" ``` chaieb@23264 ` 218` ```| "Ifm bs (Le a) = (Inum bs a \ 0)" ``` chaieb@23264 ` 219` ```| "Ifm bs (Ge a) = (Inum bs a \ 0)" ``` chaieb@23264 ` 220` ```| "Ifm bs (Eq a) = (Inum bs a = 0)" ``` chaieb@23264 ` 221` ```| "Ifm bs (NEq a) = (Inum bs a \ 0)" ``` chaieb@23264 ` 222` ```| "Ifm bs (Dvd i b) = (real i rdvd Inum bs b)" ``` chaieb@23264 ` 223` ```| "Ifm bs (NDvd i b) = (\(real i rdvd Inum bs b))" ``` chaieb@23264 ` 224` ```| "Ifm bs (NOT p) = (\ (Ifm bs p))" ``` chaieb@23264 ` 225` ```| "Ifm bs (And p q) = (Ifm bs p \ Ifm bs q)" ``` chaieb@23264 ` 226` ```| "Ifm bs (Or p q) = (Ifm bs p \ Ifm bs q)" ``` chaieb@23264 ` 227` ```| "Ifm bs (Imp p q) = ((Ifm bs p) \ (Ifm bs q))" ``` chaieb@23264 ` 228` ```| "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)" ``` chaieb@23264 ` 229` ```| "Ifm bs (E p) = (\ x. Ifm (x#bs) p)" ``` chaieb@23264 ` 230` ```| "Ifm bs (A p) = (\ x. Ifm (x#bs) p)" ``` chaieb@23264 ` 231` chaieb@23264 ` 232` ```consts prep :: "fm \ fm" ``` chaieb@23264 ` 233` ```recdef prep "measure fmsize" ``` chaieb@23264 ` 234` ``` "prep (E T) = T" ``` chaieb@23264 ` 235` ``` "prep (E F) = F" ``` chaieb@23264 ` 236` ``` "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))" ``` chaieb@23264 ` 237` ``` "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))" ``` chaieb@23264 ` 238` ``` "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" ``` chaieb@23264 ` 239` ``` "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))" ``` chaieb@23264 ` 240` ``` "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))" ``` chaieb@23264 ` 241` ``` "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))" ``` chaieb@23264 ` 242` ``` "prep (E p) = E (prep p)" ``` chaieb@23264 ` 243` ``` "prep (A (And p q)) = And (prep (A p)) (prep (A q))" ``` chaieb@23264 ` 244` ``` "prep (A p) = prep (NOT (E (NOT p)))" ``` chaieb@23264 ` 245` ``` "prep (NOT (NOT p)) = prep p" ``` chaieb@23264 ` 246` ``` "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))" ``` chaieb@23264 ` 247` ``` "prep (NOT (A p)) = prep (E (NOT p))" ``` chaieb@23264 ` 248` ``` "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))" ``` chaieb@23264 ` 249` ``` "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))" ``` chaieb@23264 ` 250` ``` "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))" ``` chaieb@23264 ` 251` ``` "prep (NOT p) = NOT (prep p)" ``` chaieb@23264 ` 252` ``` "prep (Or p q) = Or (prep p) (prep q)" ``` chaieb@23264 ` 253` ``` "prep (And p q) = And (prep p) (prep q)" ``` chaieb@23264 ` 254` ``` "prep (Imp p q) = prep (Or (NOT p) q)" ``` chaieb@23264 ` 255` ``` "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))" ``` chaieb@23264 ` 256` ``` "prep p = p" ``` nipkow@25162 ` 257` ```(hints simp add: fmsize_pos) ``` chaieb@23264 ` 258` ```lemma prep: "\ bs. Ifm bs (prep p) = Ifm bs p" ``` wenzelm@51369 ` 259` ``` by (induct p rule: prep.induct) auto ``` chaieb@23264 ` 260` chaieb@23264 ` 261` chaieb@23264 ` 262` ``` (* Quantifier freeness *) ``` haftmann@25765 ` 263` ```fun qfree:: "fm \ bool" where ``` chaieb@23264 ` 264` ``` "qfree (E p) = False" ``` haftmann@25765 ` 265` ``` | "qfree (A p) = False" ``` haftmann@25765 ` 266` ``` | "qfree (NOT p) = qfree p" ``` haftmann@25765 ` 267` ``` | "qfree (And p q) = (qfree p \ qfree q)" ``` haftmann@25765 ` 268` ``` | "qfree (Or p q) = (qfree p \ qfree q)" ``` haftmann@25765 ` 269` ``` | "qfree (Imp p q) = (qfree p \ qfree q)" ``` haftmann@25765 ` 270` ``` | "qfree (Iff p q) = (qfree p \ qfree q)" ``` haftmann@25765 ` 271` ``` | "qfree p = True" ``` chaieb@23264 ` 272` chaieb@23264 ` 273` ``` (* Boundedness and substitution *) ``` haftmann@25765 ` 274` ```primrec numbound0 :: "num \ bool" (* a num is INDEPENDENT of Bound 0 *) where ``` chaieb@23264 ` 275` ``` "numbound0 (C c) = True" ``` haftmann@25765 ` 276` ``` | "numbound0 (Bound n) = (n>0)" ``` haftmann@25765 ` 277` ``` | "numbound0 (CN n i a) = (n > 0 \ numbound0 a)" ``` haftmann@25765 ` 278` ``` | "numbound0 (Neg a) = numbound0 a" ``` haftmann@25765 ` 279` ``` | "numbound0 (Add a b) = (numbound0 a \ numbound0 b)" ``` haftmann@25765 ` 280` ``` | "numbound0 (Sub a b) = (numbound0 a \ numbound0 b)" ``` haftmann@25765 ` 281` ``` | "numbound0 (Mul i a) = numbound0 a" ``` haftmann@25765 ` 282` ``` | "numbound0 (Floor a) = numbound0 a" ``` haftmann@25765 ` 283` ``` | "numbound0 (CF c a b) = (numbound0 a \ numbound0 b)" ``` haftmann@25765 ` 284` chaieb@23264 ` 285` ```lemma numbound0_I: ``` chaieb@23264 ` 286` ``` assumes nb: "numbound0 a" ``` chaieb@23264 ` 287` ``` shows "Inum (b#bs) a = Inum (b'#bs) a" ``` nipkow@41849 ` 288` ``` using nb by (induct a) auto ``` chaieb@23264 ` 289` chaieb@23264 ` 290` ```lemma numbound0_gen: ``` chaieb@23264 ` 291` ``` assumes nb: "numbound0 t" and ti: "isint t (x#bs)" ``` chaieb@23264 ` 292` ``` shows "\ y. isint t (y#bs)" ``` wenzelm@51369 ` 293` ``` using nb ti ``` chaieb@23264 ` 294` ```proof(clarify) ``` chaieb@23264 ` 295` ``` fix y ``` chaieb@23264 ` 296` ``` from numbound0_I[OF nb, where bs="bs" and b="y" and b'="x"] ti[simplified isint_def] ``` chaieb@23264 ` 297` ``` show "isint t (y#bs)" ``` chaieb@23264 ` 298` ``` by (simp add: isint_def) ``` chaieb@23264 ` 299` ```qed ``` chaieb@23264 ` 300` haftmann@25765 ` 301` ```primrec bound0:: "fm \ bool" (* A Formula is independent of Bound 0 *) where ``` chaieb@23264 ` 302` ``` "bound0 T = True" ``` haftmann@25765 ` 303` ``` | "bound0 F = True" ``` haftmann@25765 ` 304` ``` | "bound0 (Lt a) = numbound0 a" ``` haftmann@25765 ` 305` ``` | "bound0 (Le a) = numbound0 a" ``` haftmann@25765 ` 306` ``` | "bound0 (Gt a) = numbound0 a" ``` haftmann@25765 ` 307` ``` | "bound0 (Ge a) = numbound0 a" ``` haftmann@25765 ` 308` ``` | "bound0 (Eq a) = numbound0 a" ``` haftmann@25765 ` 309` ``` | "bound0 (NEq a) = numbound0 a" ``` haftmann@25765 ` 310` ``` | "bound0 (Dvd i a) = numbound0 a" ``` haftmann@25765 ` 311` ``` | "bound0 (NDvd i a) = numbound0 a" ``` haftmann@25765 ` 312` ``` | "bound0 (NOT p) = bound0 p" ``` haftmann@25765 ` 313` ``` | "bound0 (And p q) = (bound0 p \ bound0 q)" ``` haftmann@25765 ` 314` ``` | "bound0 (Or p q) = (bound0 p \ bound0 q)" ``` haftmann@25765 ` 315` ``` | "bound0 (Imp p q) = ((bound0 p) \ (bound0 q))" ``` haftmann@25765 ` 316` ``` | "bound0 (Iff p q) = (bound0 p \ bound0 q)" ``` haftmann@25765 ` 317` ``` | "bound0 (E p) = False" ``` haftmann@25765 ` 318` ``` | "bound0 (A p) = False" ``` chaieb@23264 ` 319` chaieb@23264 ` 320` ```lemma bound0_I: ``` chaieb@23264 ` 321` ``` assumes bp: "bound0 p" ``` chaieb@23264 ` 322` ``` shows "Ifm (b#bs) p = Ifm (b'#bs) p" ``` wenzelm@51369 ` 323` ``` using bp numbound0_I [where b="b" and bs="bs" and b'="b'"] ``` nipkow@41849 ` 324` ``` by (induct p) auto ``` haftmann@25765 ` 325` haftmann@25765 ` 326` ```primrec numsubst0:: "num \ num \ num" (* substitute a num into a num for Bound 0 *) where ``` chaieb@23264 ` 327` ``` "numsubst0 t (C c) = (C c)" ``` haftmann@25765 ` 328` ``` | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)" ``` haftmann@25765 ` 329` ``` | "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))" ``` haftmann@25765 ` 330` ``` | "numsubst0 t (CF i a b) = CF i (numsubst0 t a) (numsubst0 t b)" ``` haftmann@25765 ` 331` ``` | "numsubst0 t (Neg a) = Neg (numsubst0 t a)" ``` haftmann@25765 ` 332` ``` | "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)" ``` haftmann@25765 ` 333` ``` | "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" ``` haftmann@25765 ` 334` ``` | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)" ``` haftmann@25765 ` 335` ``` | "numsubst0 t (Floor a) = Floor (numsubst0 t a)" ``` chaieb@23264 ` 336` chaieb@23264 ` 337` ```lemma numsubst0_I: ``` chaieb@23264 ` 338` ``` shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t" ``` nipkow@41849 ` 339` ``` by (induct t) simp_all ``` chaieb@23264 ` 340` haftmann@25765 ` 341` ```primrec subst0:: "num \ fm \ fm" (* substitue a num into a formula for Bound 0 *) where ``` chaieb@23264 ` 342` ``` "subst0 t T = T" ``` haftmann@25765 ` 343` ``` | "subst0 t F = F" ``` haftmann@25765 ` 344` ``` | "subst0 t (Lt a) = Lt (numsubst0 t a)" ``` haftmann@25765 ` 345` ``` | "subst0 t (Le a) = Le (numsubst0 t a)" ``` haftmann@25765 ` 346` ``` | "subst0 t (Gt a) = Gt (numsubst0 t a)" ``` haftmann@25765 ` 347` ``` | "subst0 t (Ge a) = Ge (numsubst0 t a)" ``` haftmann@25765 ` 348` ``` | "subst0 t (Eq a) = Eq (numsubst0 t a)" ``` haftmann@25765 ` 349` ``` | "subst0 t (NEq a) = NEq (numsubst0 t a)" ``` haftmann@25765 ` 350` ``` | "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)" ``` haftmann@25765 ` 351` ``` | "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)" ``` haftmann@25765 ` 352` ``` | "subst0 t (NOT p) = NOT (subst0 t p)" ``` haftmann@25765 ` 353` ``` | "subst0 t (And p q) = And (subst0 t p) (subst0 t q)" ``` haftmann@25765 ` 354` ``` | "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)" ``` haftmann@25765 ` 355` ``` | "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)" ``` haftmann@25765 ` 356` ``` | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)" ``` chaieb@23264 ` 357` chaieb@23264 ` 358` ```lemma subst0_I: assumes qfp: "qfree p" ``` chaieb@23264 ` 359` ``` shows "Ifm (b#bs) (subst0 a p) = Ifm ((Inum (b#bs) a)#bs) p" ``` chaieb@23264 ` 360` ``` using qfp numsubst0_I[where b="b" and bs="bs" and a="a"] ``` nipkow@41849 ` 361` ``` by (induct p) simp_all ``` chaieb@23264 ` 362` krauss@41839 ` 363` ```fun decrnum:: "num \ num" where ``` chaieb@23264 ` 364` ``` "decrnum (Bound n) = Bound (n - 1)" ``` krauss@41839 ` 365` ```| "decrnum (Neg a) = Neg (decrnum a)" ``` krauss@41839 ` 366` ```| "decrnum (Add a b) = Add (decrnum a) (decrnum b)" ``` krauss@41839 ` 367` ```| "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)" ``` krauss@41839 ` 368` ```| "decrnum (Mul c a) = Mul c (decrnum a)" ``` krauss@41839 ` 369` ```| "decrnum (Floor a) = Floor (decrnum a)" ``` krauss@41839 ` 370` ```| "decrnum (CN n c a) = CN (n - 1) c (decrnum a)" ``` krauss@41839 ` 371` ```| "decrnum (CF c a b) = CF c (decrnum a) (decrnum b)" ``` krauss@41839 ` 372` ```| "decrnum a = a" ``` krauss@41839 ` 373` krauss@41839 ` 374` ```fun decr :: "fm \ fm" where ``` chaieb@23264 ` 375` ``` "decr (Lt a) = Lt (decrnum a)" ``` krauss@41839 ` 376` ```| "decr (Le a) = Le (decrnum a)" ``` krauss@41839 ` 377` ```| "decr (Gt a) = Gt (decrnum a)" ``` krauss@41839 ` 378` ```| "decr (Ge a) = Ge (decrnum a)" ``` krauss@41839 ` 379` ```| "decr (Eq a) = Eq (decrnum a)" ``` krauss@41839 ` 380` ```| "decr (NEq a) = NEq (decrnum a)" ``` krauss@41839 ` 381` ```| "decr (Dvd i a) = Dvd i (decrnum a)" ``` krauss@41839 ` 382` ```| "decr (NDvd i a) = NDvd i (decrnum a)" ``` krauss@41839 ` 383` ```| "decr (NOT p) = NOT (decr p)" ``` krauss@41839 ` 384` ```| "decr (And p q) = And (decr p) (decr q)" ``` krauss@41839 ` 385` ```| "decr (Or p q) = Or (decr p) (decr q)" ``` krauss@41839 ` 386` ```| "decr (Imp p q) = Imp (decr p) (decr q)" ``` krauss@41839 ` 387` ```| "decr (Iff p q) = Iff (decr p) (decr q)" ``` krauss@41839 ` 388` ```| "decr p = p" ``` chaieb@23264 ` 389` chaieb@23264 ` 390` ```lemma decrnum: assumes nb: "numbound0 t" ``` chaieb@23264 ` 391` ``` shows "Inum (x#bs) t = Inum bs (decrnum t)" ``` wenzelm@51369 ` 392` ``` using nb by (induct t rule: decrnum.induct) simp_all ``` chaieb@23264 ` 393` chaieb@23264 ` 394` ```lemma decr: assumes nb: "bound0 p" ``` chaieb@23264 ` 395` ``` shows "Ifm (x#bs) p = Ifm bs (decr p)" ``` wenzelm@51369 ` 396` ``` using nb by (induct p rule: decr.induct) (simp_all add: decrnum) ``` chaieb@23264 ` 397` chaieb@23264 ` 398` ```lemma decr_qf: "bound0 p \ qfree (decr p)" ``` wenzelm@51369 ` 399` ``` by (induct p) simp_all ``` chaieb@23264 ` 400` krauss@41839 ` 401` ```fun isatom :: "fm \ bool" (* test for atomicity *) where ``` chaieb@23264 ` 402` ``` "isatom T = True" ``` krauss@41839 ` 403` ```| "isatom F = True" ``` krauss@41839 ` 404` ```| "isatom (Lt a) = True" ``` krauss@41839 ` 405` ```| "isatom (Le a) = True" ``` krauss@41839 ` 406` ```| "isatom (Gt a) = True" ``` krauss@41839 ` 407` ```| "isatom (Ge a) = True" ``` krauss@41839 ` 408` ```| "isatom (Eq a) = True" ``` krauss@41839 ` 409` ```| "isatom (NEq a) = True" ``` krauss@41839 ` 410` ```| "isatom (Dvd i b) = True" ``` krauss@41839 ` 411` ```| "isatom (NDvd i b) = True" ``` krauss@41839 ` 412` ```| "isatom p = False" ``` chaieb@23264 ` 413` wenzelm@51369 ` 414` ```lemma numsubst0_numbound0: ``` wenzelm@51369 ` 415` ``` assumes nb: "numbound0 t" ``` chaieb@23264 ` 416` ``` shows "numbound0 (numsubst0 t a)" ``` wenzelm@51369 ` 417` ``` using nb by (induct a) auto ``` wenzelm@51369 ` 418` wenzelm@51369 ` 419` ```lemma subst0_bound0: ``` wenzelm@51369 ` 420` ``` assumes qf: "qfree p" and nb: "numbound0 t" ``` chaieb@23264 ` 421` ``` shows "bound0 (subst0 t p)" ``` wenzelm@51369 ` 422` ``` using qf numsubst0_numbound0[OF nb] by (induct p) auto ``` chaieb@23264 ` 423` chaieb@23264 ` 424` ```lemma bound0_qf: "bound0 p \ qfree p" ``` wenzelm@51369 ` 425` ``` by (induct p) simp_all ``` chaieb@23264 ` 426` chaieb@23264 ` 427` haftmann@25765 ` 428` ```definition djf:: "('a \ fm) \ 'a \ fm \ fm" where ``` haftmann@25765 ` 429` ``` "djf f p q = (if q=T then T else if q=F then f p else ``` chaieb@23264 ` 430` ``` (let fp = f p in case fp of T \ T | F \ q | _ \ Or fp q))" ``` haftmann@25765 ` 431` haftmann@25765 ` 432` ```definition evaldjf:: "('a \ fm) \ 'a list \ fm" where ``` haftmann@25765 ` 433` ``` "evaldjf f ps = foldr (djf f) ps F" ``` chaieb@23264 ` 434` chaieb@23264 ` 435` ```lemma djf_Or: "Ifm bs (djf f p q) = Ifm bs (Or (f p) q)" ``` wenzelm@51369 ` 436` ``` by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) ``` wenzelm@51369 ` 437` ``` (cases "f p", simp_all add: Let_def djf_def) ``` chaieb@23264 ` 438` chaieb@23264 ` 439` ```lemma evaldjf_ex: "Ifm bs (evaldjf f ps) = (\ p \ set ps. Ifm bs (f p))" ``` wenzelm@51369 ` 440` ``` by (induct ps) (simp_all add: evaldjf_def djf_Or) ``` chaieb@23264 ` 441` chaieb@23264 ` 442` ```lemma evaldjf_bound0: ``` chaieb@23264 ` 443` ``` assumes nb: "\ x\ set xs. bound0 (f x)" ``` chaieb@23264 ` 444` ``` shows "bound0 (evaldjf f xs)" ``` wenzelm@51369 ` 445` ``` using nb ``` wenzelm@51369 ` 446` ``` apply (induct xs) ``` wenzelm@51369 ` 447` ``` apply (auto simp add: evaldjf_def djf_def Let_def) ``` wenzelm@51369 ` 448` ``` apply (case_tac "f a") ``` wenzelm@51369 ` 449` ``` apply auto ``` wenzelm@51369 ` 450` ``` done ``` chaieb@23264 ` 451` chaieb@23264 ` 452` ```lemma evaldjf_qf: ``` chaieb@23264 ` 453` ``` assumes nb: "\ x\ set xs. qfree (f x)" ``` chaieb@23264 ` 454` ``` shows "qfree (evaldjf f xs)" ``` wenzelm@51369 ` 455` ``` using nb ``` wenzelm@51369 ` 456` ``` apply (induct xs) ``` wenzelm@51369 ` 457` ``` apply (auto simp add: evaldjf_def djf_def Let_def) ``` wenzelm@51369 ` 458` ``` apply (case_tac "f a") ``` wenzelm@51369 ` 459` ``` apply auto ``` wenzelm@51369 ` 460` ``` done ``` chaieb@23264 ` 461` krauss@41839 ` 462` ```fun disjuncts :: "fm \ fm list" where ``` chaieb@23264 ` 463` ``` "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)" ``` krauss@41839 ` 464` ```| "disjuncts F = []" ``` krauss@41839 ` 465` ```| "disjuncts p = [p]" ``` krauss@41839 ` 466` krauss@41839 ` 467` ```fun conjuncts :: "fm \ fm list" where ``` chaieb@23264 ` 468` ``` "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)" ``` krauss@41839 ` 469` ```| "conjuncts T = []" ``` krauss@41839 ` 470` ```| "conjuncts p = [p]" ``` krauss@41839 ` 471` chaieb@23264 ` 472` ```lemma conjuncts: "(\ q\ set (conjuncts p). Ifm bs q) = Ifm bs p" ``` wenzelm@51369 ` 473` ``` by (induct p rule: conjuncts.induct) auto ``` chaieb@23264 ` 474` chaieb@23264 ` 475` ```lemma disjuncts_qf: "qfree p \ \ q\ set (disjuncts p). qfree q" ``` wenzelm@51369 ` 476` ```proof - ``` chaieb@23264 ` 477` ``` assume qf: "qfree p" ``` chaieb@23264 ` 478` ``` hence "list_all qfree (disjuncts p)" ``` chaieb@23264 ` 479` ``` by (induct p rule: disjuncts.induct, auto) ``` chaieb@23264 ` 480` ``` thus ?thesis by (simp only: list_all_iff) ``` chaieb@23264 ` 481` ```qed ``` wenzelm@51369 ` 482` chaieb@23264 ` 483` ```lemma conjuncts_qf: "qfree p \ \ q\ set (conjuncts p). qfree q" ``` chaieb@23264 ` 484` ```proof- ``` chaieb@23264 ` 485` ``` assume qf: "qfree p" ``` chaieb@23264 ` 486` ``` hence "list_all qfree (conjuncts p)" ``` chaieb@23264 ` 487` ``` by (induct p rule: conjuncts.induct, auto) ``` chaieb@23264 ` 488` ``` thus ?thesis by (simp only: list_all_iff) ``` chaieb@23264 ` 489` ```qed ``` chaieb@23264 ` 490` haftmann@35416 ` 491` ```definition DJ :: "(fm \ fm) \ fm \ fm" where ``` chaieb@23264 ` 492` ``` "DJ f p \ evaldjf f (disjuncts p)" ``` chaieb@23264 ` 493` chaieb@23264 ` 494` ```lemma DJ: assumes fdj: "\ p q. f (Or p q) = Or (f p) (f q)" ``` chaieb@23264 ` 495` ``` and fF: "f F = F" ``` chaieb@23264 ` 496` ``` shows "Ifm bs (DJ f p) = Ifm bs (f p)" ``` wenzelm@51369 ` 497` ```proof - ``` chaieb@23264 ` 498` ``` have "Ifm bs (DJ f p) = (\ q \ set (disjuncts p). Ifm bs (f q))" ``` chaieb@23264 ` 499` ``` by (simp add: DJ_def evaldjf_ex) ``` chaieb@23264 ` 500` ``` also have "\ = Ifm bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto) ``` chaieb@23264 ` 501` ``` finally show ?thesis . ``` chaieb@23264 ` 502` ```qed ``` chaieb@23264 ` 503` chaieb@23264 ` 504` ```lemma DJ_qf: assumes ``` chaieb@23264 ` 505` ``` fqf: "\ p. qfree p \ qfree (f p)" ``` chaieb@23264 ` 506` ``` shows "\p. qfree p \ qfree (DJ f p) " ``` chaieb@23264 ` 507` ```proof(clarify) ``` chaieb@23264 ` 508` ``` fix p assume qf: "qfree p" ``` chaieb@23264 ` 509` ``` have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def) ``` chaieb@23264 ` 510` ``` from disjuncts_qf[OF qf] have "\ q\ set (disjuncts p). qfree q" . ``` chaieb@23264 ` 511` ``` with fqf have th':"\ q\ set (disjuncts p). qfree (f q)" by blast ``` chaieb@23264 ` 512` ``` ``` chaieb@23264 ` 513` ``` from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp ``` chaieb@23264 ` 514` ```qed ``` chaieb@23264 ` 515` chaieb@23264 ` 516` ```lemma DJ_qe: assumes qe: "\ bs p. qfree p \ qfree (qe p) \ (Ifm bs (qe p) = Ifm bs (E p))" ``` chaieb@23264 ` 517` ``` shows "\ bs p. qfree p \ qfree (DJ qe p) \ (Ifm bs ((DJ qe p)) = Ifm bs (E p))" ``` chaieb@23264 ` 518` ```proof(clarify) ``` chaieb@23264 ` 519` ``` fix p::fm and bs ``` chaieb@23264 ` 520` ``` assume qf: "qfree p" ``` chaieb@23264 ` 521` ``` from qe have qth: "\ p. qfree p \ qfree (qe p)" by blast ``` chaieb@23264 ` 522` ``` from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto ``` chaieb@23264 ` 523` ``` have "Ifm bs (DJ qe p) = (\ q\ set (disjuncts p). Ifm bs (qe q))" ``` chaieb@23264 ` 524` ``` by (simp add: DJ_def evaldjf_ex) ``` chaieb@23264 ` 525` ``` also have "\ = (\ q \ set(disjuncts p). Ifm bs (E q))" using qe disjuncts_qf[OF qf] by auto ``` chaieb@23264 ` 526` ``` also have "\ = Ifm bs (E p)" by (induct p rule: disjuncts.induct, auto) ``` chaieb@23264 ` 527` ``` finally show "qfree (DJ qe p) \ Ifm bs (DJ qe p) = Ifm bs (E p)" using qfth by blast ``` chaieb@23264 ` 528` ```qed ``` chaieb@23264 ` 529` ``` (* Simplification *) ``` chaieb@23264 ` 530` chaieb@23264 ` 531` ``` (* Algebraic simplifications for nums *) ``` krauss@41839 ` 532` ```fun bnds:: "num \ nat list" where ``` chaieb@23264 ` 533` ``` "bnds (Bound n) = [n]" ``` krauss@41839 ` 534` ```| "bnds (CN n c a) = n#(bnds a)" ``` krauss@41839 ` 535` ```| "bnds (Neg a) = bnds a" ``` krauss@41839 ` 536` ```| "bnds (Add a b) = (bnds a)@(bnds b)" ``` krauss@41839 ` 537` ```| "bnds (Sub a b) = (bnds a)@(bnds b)" ``` krauss@41839 ` 538` ```| "bnds (Mul i a) = bnds a" ``` krauss@41839 ` 539` ```| "bnds (Floor a) = bnds a" ``` krauss@41839 ` 540` ```| "bnds (CF c a b) = (bnds a)@(bnds b)" ``` krauss@41839 ` 541` ```| "bnds a = []" ``` krauss@41839 ` 542` ```fun lex_ns:: "nat list \ nat list \ bool" where ``` krauss@41839 ` 543` ``` "lex_ns [] ms = True" ``` krauss@41839 ` 544` ```| "lex_ns ns [] = False" ``` krauss@41839 ` 545` ```| "lex_ns (n#ns) (m#ms) = (n ((n = m) \ lex_ns ns ms)) " ``` haftmann@35416 ` 546` ```definition lex_bnd :: "num \ num \ bool" where ``` krauss@41839 ` 547` ``` "lex_bnd t s \ lex_ns (bnds t) (bnds s)" ``` krauss@41839 ` 548` krauss@41839 ` 549` ```fun maxcoeff:: "num \ int" where ``` chaieb@23264 ` 550` ``` "maxcoeff (C i) = abs i" ``` krauss@41839 ` 551` ```| "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)" ``` krauss@41839 ` 552` ```| "maxcoeff (CF c t s) = max (abs c) (maxcoeff s)" ``` krauss@41839 ` 553` ```| "maxcoeff t = 1" ``` chaieb@23264 ` 554` chaieb@23264 ` 555` ```lemma maxcoeff_pos: "maxcoeff t \ 0" ``` wenzelm@51369 ` 556` ``` by (induct t rule: maxcoeff.induct) auto ``` chaieb@23264 ` 557` krauss@41839 ` 558` ```fun numgcdh:: "num \ int \ int" where ``` huffman@31706 ` 559` ``` "numgcdh (C i) = (\g. gcd i g)" ``` krauss@41839 ` 560` ```| "numgcdh (CN n c t) = (\g. gcd c (numgcdh t g))" ``` krauss@41839 ` 561` ```| "numgcdh (CF c s t) = (\g. gcd c (numgcdh t g))" ``` krauss@41839 ` 562` ```| "numgcdh t = (\g. 1)" ``` haftmann@23858 ` 563` wenzelm@51369 ` 564` ```definition numgcd :: "num \ int" ``` wenzelm@51369 ` 565` ``` where "numgcd t = numgcdh t (maxcoeff t)" ``` chaieb@23264 ` 566` krauss@41839 ` 567` ```fun reducecoeffh:: "num \ int \ num" where ``` chaieb@23264 ` 568` ``` "reducecoeffh (C i) = (\ g. C (i div g))" ``` krauss@41839 ` 569` ```| "reducecoeffh (CN n c t) = (\ g. CN n (c div g) (reducecoeffh t g))" ``` krauss@41839 ` 570` ```| "reducecoeffh (CF c s t) = (\ g. CF (c div g) s (reducecoeffh t g))" ``` krauss@41839 ` 571` ```| "reducecoeffh t = (\g. t)" ``` chaieb@23264 ` 572` wenzelm@51369 ` 573` ```definition reducecoeff :: "num \ num" ``` haftmann@23858 ` 574` ```where ``` wenzelm@51369 ` 575` ``` "reducecoeff t = ``` wenzelm@51369 ` 576` ``` (let g = numgcd t in ``` wenzelm@51369 ` 577` ``` if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)" ``` chaieb@23264 ` 578` krauss@41839 ` 579` ```fun dvdnumcoeff:: "num \ int \ bool" where ``` chaieb@23264 ` 580` ``` "dvdnumcoeff (C i) = (\ g. g dvd i)" ``` krauss@41839 ` 581` ```| "dvdnumcoeff (CN n c t) = (\ g. g dvd c \ (dvdnumcoeff t g))" ``` krauss@41839 ` 582` ```| "dvdnumcoeff (CF c s t) = (\ g. g dvd c \ (dvdnumcoeff t g))" ``` krauss@41839 ` 583` ```| "dvdnumcoeff t = (\g. False)" ``` chaieb@23264 ` 584` chaieb@23264 ` 585` ```lemma dvdnumcoeff_trans: ``` chaieb@23264 ` 586` ``` assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'" ``` chaieb@23264 ` 587` ``` shows "dvdnumcoeff t g" ``` chaieb@23264 ` 588` ``` using dgt' gdg ``` wenzelm@51369 ` 589` ``` by (induct t rule: dvdnumcoeff.induct) (simp_all add: gdg dvd_trans[OF gdg]) ``` nipkow@30042 ` 590` nipkow@30042 ` 591` ```declare dvd_trans [trans add] ``` chaieb@23264 ` 592` chaieb@23264 ` 593` ```lemma numgcd0: ``` chaieb@23264 ` 594` ``` assumes g0: "numgcd t = 0" ``` chaieb@23264 ` 595` ``` shows "Inum bs t = 0" ``` chaieb@23264 ` 596` ```proof- ``` chaieb@23264 ` 597` ``` have "\x. numgcdh t x= 0 \ Inum bs t = 0" ``` huffman@31706 ` 598` ``` by (induct t rule: numgcdh.induct, auto) ``` chaieb@23264 ` 599` ``` thus ?thesis using g0[simplified numgcd_def] by blast ``` chaieb@23264 ` 600` ```qed ``` chaieb@23264 ` 601` chaieb@23264 ` 602` ```lemma numgcdh_pos: assumes gp: "g \ 0" shows "numgcdh t g \ 0" ``` wenzelm@51369 ` 603` ``` using gp by (induct t rule: numgcdh.induct) auto ``` chaieb@23264 ` 604` chaieb@23264 ` 605` ```lemma numgcd_pos: "numgcd t \0" ``` chaieb@23264 ` 606` ``` by (simp add: numgcd_def numgcdh_pos maxcoeff_pos) ``` chaieb@23264 ` 607` chaieb@23264 ` 608` ```lemma reducecoeffh: ``` chaieb@23264 ` 609` ``` assumes gt: "dvdnumcoeff t g" and gp: "g > 0" ``` chaieb@23264 ` 610` ``` shows "real g *(Inum bs (reducecoeffh t g)) = Inum bs t" ``` chaieb@23264 ` 611` ``` using gt ``` chaieb@23264 ` 612` ```proof(induct t rule: reducecoeffh.induct) ``` chaieb@23264 ` 613` ``` case (1 i) hence gd: "g dvd i" by simp ``` bulwahn@46670 ` 614` ``` from assms 1 show ?case by (simp add: real_of_int_div[OF gd]) ``` chaieb@23264 ` 615` ```next ``` chaieb@23264 ` 616` ``` case (2 n c t) hence gd: "g dvd c" by simp ``` bulwahn@46670 ` 617` ``` from assms 2 show ?case by (simp add: real_of_int_div[OF gd] algebra_simps) ``` chaieb@23264 ` 618` ```next ``` chaieb@23264 ` 619` ``` case (3 c s t) hence gd: "g dvd c" by simp ``` bulwahn@46670 ` 620` ``` from assms 3 show ?case by (simp add: real_of_int_div[OF gd] algebra_simps) ``` chaieb@23264 ` 621` ```qed (auto simp add: numgcd_def gp) ``` wenzelm@41807 ` 622` krauss@41839 ` 623` ```fun ismaxcoeff:: "num \ int \ bool" where ``` chaieb@23264 ` 624` ``` "ismaxcoeff (C i) = (\ x. abs i \ x)" ``` krauss@41839 ` 625` ```| "ismaxcoeff (CN n c t) = (\x. abs c \ x \ (ismaxcoeff t x))" ``` krauss@41839 ` 626` ```| "ismaxcoeff (CF c s t) = (\x. abs c \ x \ (ismaxcoeff t x))" ``` krauss@41839 ` 627` ```| "ismaxcoeff t = (\x. True)" ``` chaieb@23264 ` 628` chaieb@23264 ` 629` ```lemma ismaxcoeff_mono: "ismaxcoeff t c \ c \ c' \ ismaxcoeff t c'" ``` wenzelm@51369 ` 630` ``` by (induct t rule: ismaxcoeff.induct) auto ``` chaieb@23264 ` 631` chaieb@23264 ` 632` ```lemma maxcoeff_ismaxcoeff: "ismaxcoeff t (maxcoeff t)" ``` chaieb@23264 ` 633` ```proof (induct t rule: maxcoeff.induct) ``` chaieb@23264 ` 634` ``` case (2 n c t) ``` chaieb@23264 ` 635` ``` hence H:"ismaxcoeff t (maxcoeff t)" . ``` wenzelm@41807 ` 636` ``` have thh: "maxcoeff t \ max (abs c) (maxcoeff t)" by simp ``` wenzelm@51369 ` 637` ``` from ismaxcoeff_mono[OF H thh] show ?case by simp ``` chaieb@23264 ` 638` ```next ``` chaieb@23264 ` 639` ``` case (3 c t s) ``` chaieb@23264 ` 640` ``` hence H1:"ismaxcoeff s (maxcoeff s)" by auto ``` chaieb@23264 ` 641` ``` have thh1: "maxcoeff s \ max \c\ (maxcoeff s)" by (simp add: max_def) ``` wenzelm@51369 ` 642` ``` from ismaxcoeff_mono[OF H1 thh1] show ?case by simp ``` chaieb@23264 ` 643` ```qed simp_all ``` chaieb@23264 ` 644` huffman@31706 ` 645` ```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 ` 646` ``` apply (unfold gcd_int_def) ``` chaieb@23264 ` 647` ``` apply (cases "i = 0", simp_all) ``` chaieb@23264 ` 648` ``` apply (cases "j = 0", simp_all) ``` chaieb@23264 ` 649` ``` apply (cases "abs i = 1", simp_all) ``` chaieb@23264 ` 650` ``` apply (cases "abs j = 1", simp_all) ``` chaieb@23264 ` 651` ``` apply auto ``` chaieb@23264 ` 652` ``` done ``` wenzelm@51369 ` 653` chaieb@23264 ` 654` ```lemma numgcdh0:"numgcdh t m = 0 \ m =0" ``` wenzelm@41807 ` 655` ``` by (induct t rule: numgcdh.induct) auto ``` chaieb@23264 ` 656` chaieb@23264 ` 657` ```lemma dvdnumcoeff_aux: ``` chaieb@23264 ` 658` ``` assumes "ismaxcoeff t m" and mp:"m \ 0" and "numgcdh t m > 1" ``` chaieb@23264 ` 659` ``` shows "dvdnumcoeff t (numgcdh t m)" ``` wenzelm@41807 ` 660` ```using assms ``` chaieb@23264 ` 661` ```proof(induct t rule: numgcdh.induct) ``` chaieb@23264 ` 662` ``` case (2 n c t) ``` chaieb@23264 ` 663` ``` let ?g = "numgcdh t m" ``` wenzelm@41807 ` 664` ``` from 2 have th:"gcd c ?g > 1" by simp ``` haftmann@27556 ` 665` ``` from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"] ``` chaieb@23264 ` 666` ``` have "(abs c > 1 \ ?g > 1) \ (abs c = 0 \ ?g > 1) \ (abs c > 1 \ ?g = 0)" by simp ``` wenzelm@41807 ` 667` ``` moreover {assume "abs c > 1" and gp: "?g > 1" with 2 ``` chaieb@23264 ` 668` ``` have th: "dvdnumcoeff t ?g" by simp ``` huffman@31706 ` 669` ``` have th': "gcd c ?g dvd ?g" by simp ``` huffman@31706 ` 670` ``` from dvdnumcoeff_trans[OF th' th] have ?case by simp } ``` chaieb@23264 ` 671` ``` moreover {assume "abs c = 0 \ ?g > 1" ``` wenzelm@41807 ` 672` ``` with 2 have th: "dvdnumcoeff t ?g" by simp ``` huffman@31706 ` 673` ``` have th': "gcd c ?g dvd ?g" by simp ``` huffman@31706 ` 674` ``` from dvdnumcoeff_trans[OF th' th] have ?case by simp ``` chaieb@23264 ` 675` ``` hence ?case by simp } ``` chaieb@23264 ` 676` ``` moreover {assume "abs c > 1" and g0:"?g = 0" ``` wenzelm@41807 ` 677` ``` from numgcdh0[OF g0] have "m=0". with 2 g0 have ?case by simp } ``` chaieb@23264 ` 678` ``` ultimately show ?case by blast ``` chaieb@23264 ` 679` ```next ``` chaieb@23264 ` 680` ``` case (3 c s t) ``` chaieb@23264 ` 681` ``` let ?g = "numgcdh t m" ``` wenzelm@41807 ` 682` ``` from 3 have th:"gcd c ?g > 1" by simp ``` haftmann@27556 ` 683` ``` from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"] ``` chaieb@23264 ` 684` ``` have "(abs c > 1 \ ?g > 1) \ (abs c = 0 \ ?g > 1) \ (abs c > 1 \ ?g = 0)" by simp ``` wenzelm@41807 ` 685` ``` moreover {assume "abs c > 1" and gp: "?g > 1" with 3 ``` chaieb@23264 ` 686` ``` have th: "dvdnumcoeff t ?g" by simp ``` huffman@31706 ` 687` ``` have th': "gcd c ?g dvd ?g" by simp ``` huffman@31706 ` 688` ``` from dvdnumcoeff_trans[OF th' th] have ?case by simp } ``` chaieb@23264 ` 689` ``` moreover {assume "abs c = 0 \ ?g > 1" ``` wenzelm@41807 ` 690` ``` with 3 have th: "dvdnumcoeff t ?g" by simp ``` huffman@31706 ` 691` ``` have th': "gcd c ?g dvd ?g" by simp ``` huffman@31706 ` 692` ``` from dvdnumcoeff_trans[OF th' th] have ?case by simp ``` chaieb@23264 ` 693` ``` hence ?case by simp } ``` chaieb@23264 ` 694` ``` moreover {assume "abs c > 1" and g0:"?g = 0" ``` wenzelm@41807 ` 695` ``` from numgcdh0[OF g0] have "m=0". with 3 g0 have ?case by simp } ``` chaieb@23264 ` 696` ``` ultimately show ?case by blast ``` huffman@31706 ` 697` ```qed auto ``` chaieb@23264 ` 698` chaieb@23264 ` 699` ```lemma dvdnumcoeff_aux2: ``` chaieb@23264 ` 700` ``` assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \ numgcd t > 0" ``` wenzelm@41807 ` 701` ``` using assms ``` chaieb@23264 ` 702` ```proof (simp add: numgcd_def) ``` chaieb@23264 ` 703` ``` let ?mc = "maxcoeff t" ``` chaieb@23264 ` 704` ``` let ?g = "numgcdh t ?mc" ``` chaieb@23264 ` 705` ``` have th1: "ismaxcoeff t ?mc" by (rule maxcoeff_ismaxcoeff) ``` chaieb@23264 ` 706` ``` have th2: "?mc \ 0" by (rule maxcoeff_pos) ``` chaieb@23264 ` 707` ``` assume H: "numgcdh t ?mc > 1" ``` wenzelm@41807 ` 708` ``` from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" . ``` chaieb@23264 ` 709` ```qed ``` chaieb@23264 ` 710` chaieb@23264 ` 711` ```lemma reducecoeff: "real (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t" ``` chaieb@23264 ` 712` ```proof- ``` chaieb@23264 ` 713` ``` let ?g = "numgcd t" ``` chaieb@23264 ` 714` ``` have "?g \ 0" by (simp add: numgcd_pos) ``` wenzelm@32960 ` 715` ``` hence "?g = 0 \ ?g = 1 \ ?g > 1" by auto ``` chaieb@23264 ` 716` ``` moreover {assume "?g = 0" hence ?thesis by (simp add: numgcd0)} ``` chaieb@23264 ` 717` ``` moreover {assume "?g = 1" hence ?thesis by (simp add: reducecoeff_def)} ``` chaieb@23264 ` 718` ``` moreover { assume g1:"?g > 1" ``` chaieb@23264 ` 719` ``` from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" and g0: "?g > 0" by blast+ ``` chaieb@23264 ` 720` ``` from reducecoeffh[OF th1 g0, where bs="bs"] g1 have ?thesis ``` chaieb@23264 ` 721` ``` by (simp add: reducecoeff_def Let_def)} ``` chaieb@23264 ` 722` ``` ultimately show ?thesis by blast ``` chaieb@23264 ` 723` ```qed ``` chaieb@23264 ` 724` chaieb@23264 ` 725` ```lemma reducecoeffh_numbound0: "numbound0 t \ numbound0 (reducecoeffh t g)" ``` wenzelm@51369 ` 726` ``` by (induct t rule: reducecoeffh.induct) auto ``` chaieb@23264 ` 727` chaieb@23264 ` 728` ```lemma reducecoeff_numbound0: "numbound0 t \ numbound0 (reducecoeff t)" ``` wenzelm@51369 ` 729` ``` using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def) ``` wenzelm@51369 ` 730` wenzelm@51369 ` 731` ```consts numadd:: "num \ num \ num" ``` chaieb@23264 ` 732` ```recdef numadd "measure (\ (t,s). size t + size s)" ``` chaieb@23264 ` 733` ``` "numadd (CN n1 c1 r1,CN n2 c2 r2) = ``` chaieb@23264 ` 734` ``` (if n1=n2 then ``` chaieb@23264 ` 735` ``` (let c = c1 + c2 ``` chaieb@23264 ` 736` ``` in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2)))) ``` chaieb@23264 ` 737` ``` else if n1 \ n2 then CN n1 c1 (numadd (r1,CN n2 c2 r2)) ``` chaieb@23264 ` 738` ``` else (CN n2 c2 (numadd (CN n1 c1 r1,r2))))" ``` chaieb@23264 ` 739` ``` "numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))" ``` chaieb@23264 ` 740` ``` "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))" ``` chaieb@23264 ` 741` ``` "numadd (CF c1 t1 r1,CF c2 t2 r2) = ``` chaieb@23264 ` 742` ``` (if t1 = t2 then ``` chaieb@23264 ` 743` ``` (let c=c1+c2; s= numadd(r1,r2) in (if c=0 then s else CF c t1 s)) ``` chaieb@23264 ` 744` ``` else if lex_bnd t1 t2 then CF c1 t1 (numadd(r1,CF c2 t2 r2)) ``` chaieb@23264 ` 745` ``` else CF c2 t2 (numadd(CF c1 t1 r1,r2)))" ``` chaieb@23264 ` 746` ``` "numadd (CF c1 t1 r1,C c) = CF c1 t1 (numadd (r1, C c))" ``` chaieb@23264 ` 747` ``` "numadd (C c,CF c1 t1 r1) = CF c1 t1 (numadd (r1, C c))" ``` chaieb@23264 ` 748` ``` "numadd (C b1, C b2) = C (b1+b2)" ``` chaieb@23264 ` 749` ``` "numadd (a,b) = Add a b" ``` chaieb@23264 ` 750` chaieb@23264 ` 751` ```lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" ``` chaieb@23264 ` 752` ```apply (induct t s rule: numadd.induct, simp_all add: Let_def) ``` nipkow@23477 ` 753` ``` apply (case_tac "c1+c2 = 0",case_tac "n1 \ n2", simp_all) ``` nipkow@29667 ` 754` ``` apply (case_tac "n1 = n2", simp_all add: algebra_simps) ``` webertj@49962 ` 755` ``` apply (simp only: distrib_right[symmetric]) ``` nipkow@23477 ` 756` ``` apply simp ``` chaieb@23264 ` 757` ```apply (case_tac "lex_bnd t1 t2", simp_all) ``` nipkow@23477 ` 758` ``` apply (case_tac "c1+c2 = 0") ``` wenzelm@51369 ` 759` ``` apply (case_tac "t1 = t2") ``` wenzelm@51369 ` 760` ``` apply (simp_all add: algebra_simps distrib_right[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add distrib_right) ``` wenzelm@51369 ` 761` ``` done ``` chaieb@23264 ` 762` chaieb@23264 ` 763` ```lemma numadd_nb[simp]: "\ numbound0 t ; numbound0 s\ \ numbound0 (numadd (t,s))" ``` wenzelm@51369 ` 764` ``` by (induct t s rule: numadd.induct) (auto simp add: Let_def) ``` chaieb@23264 ` 765` krauss@41839 ` 766` ```fun nummul:: "num \ int \ num" where ``` chaieb@23264 ` 767` ``` "nummul (C j) = (\ i. C (i*j))" ``` krauss@41839 ` 768` ```| "nummul (CN n c t) = (\ i. CN n (c*i) (nummul t i))" ``` krauss@41839 ` 769` ```| "nummul (CF c t s) = (\ i. CF (c*i) t (nummul s i))" ``` krauss@41839 ` 770` ```| "nummul (Mul c t) = (\ i. nummul t (i*c))" ``` krauss@41839 ` 771` ```| "nummul t = (\ i. Mul i t)" ``` chaieb@23264 ` 772` chaieb@23264 ` 773` ```lemma nummul[simp]: "\ i. Inum bs (nummul t i) = Inum bs (Mul i t)" ``` wenzelm@51369 ` 774` ``` by (induct t rule: nummul.induct) (auto simp add: algebra_simps) ``` chaieb@23264 ` 775` chaieb@23264 ` 776` ```lemma nummul_nb[simp]: "\ i. numbound0 t \ numbound0 (nummul t i)" ``` wenzelm@51369 ` 777` ``` by (induct t rule: nummul.induct) auto ``` wenzelm@51369 ` 778` wenzelm@51369 ` 779` ```definition numneg :: "num \ num" ``` wenzelm@51369 ` 780` ``` where "numneg t \ nummul t (- 1)" ``` wenzelm@51369 ` 781` wenzelm@51369 ` 782` ```definition numsub :: "num \ num \ num" ``` wenzelm@51369 ` 783` ``` where "numsub s t \ (if s = t then C 0 else numadd (s,numneg t))" ``` chaieb@23264 ` 784` chaieb@23264 ` 785` ```lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)" ``` wenzelm@51369 ` 786` ``` using numneg_def nummul by simp ``` chaieb@23264 ` 787` chaieb@23264 ` 788` ```lemma numneg_nb[simp]: "numbound0 t \ numbound0 (numneg t)" ``` wenzelm@51369 ` 789` ``` using numneg_def by simp ``` chaieb@23264 ` 790` chaieb@23264 ` 791` ```lemma numsub[simp]: "Inum bs (numsub a b) = Inum bs (Sub a b)" ``` wenzelm@51369 ` 792` ``` using numsub_def by simp ``` chaieb@23264 ` 793` chaieb@23264 ` 794` ```lemma numsub_nb[simp]: "\ numbound0 t ; numbound0 s\ \ numbound0 (numsub t s)" ``` wenzelm@51369 ` 795` ``` using numsub_def by simp ``` chaieb@23264 ` 796` chaieb@23264 ` 797` ```lemma isint_CF: assumes si: "isint s bs" shows "isint (CF c t s) bs" ``` chaieb@23264 ` 798` ```proof- ``` chaieb@23264 ` 799` ``` have cti: "isint (Mul c (Floor t)) bs" by (simp add: isint_Mul isint_Floor) ``` chaieb@23264 ` 800` ``` ``` chaieb@23264 ` 801` ``` have "?thesis = isint (Add (Mul c (Floor t)) s) bs" by (simp add: isint_def) ``` chaieb@23264 ` 802` ``` also have "\" by (simp add: isint_add cti si) ``` chaieb@23264 ` 803` ``` finally show ?thesis . ``` chaieb@23264 ` 804` ```qed ``` chaieb@23264 ` 805` krauss@41839 ` 806` ```fun split_int:: "num \ num \ num" where ``` chaieb@23264 ` 807` ``` "split_int (C c) = (C 0, C c)" ``` krauss@41839 ` 808` ```| "split_int (CN n c b) = ``` chaieb@23264 ` 809` ``` (let (bv,bi) = split_int b ``` chaieb@23264 ` 810` ``` in (CN n c bv, bi))" ``` krauss@41839 ` 811` ```| "split_int (CF c a b) = ``` chaieb@23264 ` 812` ``` (let (bv,bi) = split_int b ``` chaieb@23264 ` 813` ``` in (bv, CF c a bi))" ``` krauss@41839 ` 814` ```| "split_int a = (a,C 0)" ``` chaieb@23264 ` 815` wenzelm@41807 ` 816` ```lemma split_int: "\tv ti. split_int t = (tv,ti) \ (Inum bs (Add tv ti) = Inum bs t) \ isint ti bs" ``` chaieb@23264 ` 817` ```proof (induct t rule: split_int.induct) ``` chaieb@23264 ` 818` ``` case (2 c n b tv ti) ``` chaieb@23264 ` 819` ``` let ?bv = "fst (split_int b)" ``` chaieb@23264 ` 820` ``` let ?bi = "snd (split_int b)" ``` chaieb@23264 ` 821` ``` have "split_int b = (?bv,?bi)" by simp ``` wenzelm@41807 ` 822` ``` with 2(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ ``` wenzelm@41807 ` 823` ``` from 2(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def) ``` wenzelm@41807 ` 824` ``` from 2(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def) ``` chaieb@23264 ` 825` ```next ``` chaieb@23264 ` 826` ``` case (3 c a b tv ti) ``` chaieb@23264 ` 827` ``` let ?bv = "fst (split_int b)" ``` chaieb@23264 ` 828` ``` let ?bi = "snd (split_int b)" ``` chaieb@23264 ` 829` ``` have "split_int b = (?bv,?bi)" by simp ``` wenzelm@41807 ` 830` ``` with 3(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ ``` wenzelm@41807 ` 831` ``` from 3(2) have tibi: "ti = CF c a ?bi" ``` wenzelm@41807 ` 832` ``` by (simp add: Let_def split_def) ``` wenzelm@41807 ` 833` ``` from 3(2) b[symmetric] bii show ?case ``` wenzelm@41807 ` 834` ``` by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF) ``` nipkow@29667 ` 835` ```qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def algebra_simps) ``` chaieb@23264 ` 836` chaieb@23264 ` 837` ```lemma split_int_nb: "numbound0 t \ numbound0 (fst (split_int t)) \ numbound0 (snd (split_int t)) " ``` wenzelm@41807 ` 838` ``` by (induct t rule: split_int.induct) (auto simp add: Let_def split_def) ``` wenzelm@41807 ` 839` wenzelm@41807 ` 840` ```definition numfloor:: "num \ num" ``` haftmann@23858 ` 841` ```where ``` wenzelm@41807 ` 842` ``` "numfloor t = (let (tv,ti) = split_int t in ``` chaieb@23264 ` 843` ``` (case tv of C i \ numadd (tv,ti) ``` chaieb@23264 ` 844` ``` | _ \ numadd(CF 1 tv (C 0),ti)))" ``` chaieb@23264 ` 845` chaieb@23264 ` 846` ```lemma numfloor[simp]: "Inum bs (numfloor t) = Inum bs (Floor t)" (is "?n t = ?N (Floor t)") ``` chaieb@23264 ` 847` ```proof- ``` chaieb@23264 ` 848` ``` let ?tv = "fst (split_int t)" ``` chaieb@23264 ` 849` ``` let ?ti = "snd (split_int t)" ``` chaieb@23264 ` 850` ``` have tvti:"split_int t = (?tv,?ti)" by simp ``` chaieb@23264 ` 851` ``` {assume H: "\ v. ?tv \ C v" ``` chaieb@23264 ` 852` ``` hence th1: "?n t = ?N (Add (Floor ?tv) ?ti)" ``` wenzelm@51369 ` 853` ``` by (cases ?tv) (auto simp add: numfloor_def Let_def split_def) ``` chaieb@23264 ` 854` ``` from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+ ``` chaieb@23264 ` 855` ``` hence "?N (Floor t) = real (floor (?N (Add ?tv ?ti)))" by simp ``` chaieb@23264 ` 856` ``` also have "\ = real (floor (?N ?tv) + (floor (?N ?ti)))" ``` chaieb@23264 ` 857` ``` by (simp,subst tii[simplified isint_iff, symmetric]) simp ``` chaieb@23264 ` 858` ``` also have "\ = ?N (Add (Floor ?tv) ?ti)" by (simp add: tii[simplified isint_iff]) ``` chaieb@23264 ` 859` ``` finally have ?thesis using th1 by simp} ``` chaieb@23264 ` 860` ``` moreover {fix v assume H:"?tv = C v" ``` chaieb@23264 ` 861` ``` from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+ ``` chaieb@23264 ` 862` ``` hence "?N (Floor t) = real (floor (?N (Add ?tv ?ti)))" by simp ``` chaieb@23264 ` 863` ``` also have "\ = real (floor (?N ?tv) + (floor (?N ?ti)))" ``` chaieb@23264 ` 864` ``` by (simp,subst tii[simplified isint_iff, symmetric]) simp ``` chaieb@23264 ` 865` ``` also have "\ = ?N (Add (Floor ?tv) ?ti)" by (simp add: tii[simplified isint_iff]) ``` wenzelm@51369 ` 866` ``` finally have ?thesis by (simp add: H numfloor_def Let_def split_def) } ``` chaieb@23264 ` 867` ``` ultimately show ?thesis by auto ``` chaieb@23264 ` 868` ```qed ``` chaieb@23264 ` 869` chaieb@23264 ` 870` ```lemma numfloor_nb[simp]: "numbound0 t \ numbound0 (numfloor t)" ``` chaieb@23264 ` 871` ``` using split_int_nb[where t="t"] ``` wenzelm@51369 ` 872` ``` by (cases "fst (split_int t)") (auto simp add: numfloor_def Let_def split_def) ``` chaieb@23264 ` 873` krauss@41839 ` 874` ```function simpnum:: "num \ num" where ``` chaieb@23264 ` 875` ``` "simpnum (C j) = C j" ``` krauss@41839 ` 876` ```| "simpnum (Bound n) = CN n 1 (C 0)" ``` krauss@41839 ` 877` ```| "simpnum (Neg t) = numneg (simpnum t)" ``` krauss@41839 ` 878` ```| "simpnum (Add t s) = numadd (simpnum t,simpnum s)" ``` krauss@41839 ` 879` ```| "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)" ``` krauss@41839 ` 880` ```| "simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum t) i)" ``` krauss@41839 ` 881` ```| "simpnum (Floor t) = numfloor (simpnum t)" ``` krauss@41839 ` 882` ```| "simpnum (CN n c t) = (if c=0 then simpnum t else CN n c (simpnum t))" ``` krauss@41839 ` 883` ```| "simpnum (CF c t s) = simpnum(Add (Mul c (Floor t)) s)" ``` krauss@41839 ` 884` ```by pat_completeness auto ``` krauss@41839 ` 885` ```termination by (relation "measure num_size") auto ``` chaieb@23264 ` 886` chaieb@23264 ` 887` ```lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t" ``` wenzelm@51369 ` 888` ``` by (induct t rule: simpnum.induct) auto ``` wenzelm@51369 ` 889` wenzelm@51369 ` 890` ```lemma simpnum_numbound0[simp]: "numbound0 t \ numbound0 (simpnum t)" ``` wenzelm@51369 ` 891` ``` by (induct t rule: simpnum.induct) auto ``` chaieb@23264 ` 892` krauss@41839 ` 893` ```fun nozerocoeff:: "num \ bool" where ``` chaieb@23264 ` 894` ``` "nozerocoeff (C c) = True" ``` krauss@41839 ` 895` ```| "nozerocoeff (CN n c t) = (c\0 \ nozerocoeff t)" ``` krauss@41839 ` 896` ```| "nozerocoeff (CF c s t) = (c \ 0 \ nozerocoeff t)" ``` krauss@41839 ` 897` ```| "nozerocoeff (Mul c t) = (c\0 \ nozerocoeff t)" ``` krauss@41839 ` 898` ```| "nozerocoeff t = True" ``` chaieb@23264 ` 899` chaieb@23264 ` 900` ```lemma numadd_nz : "nozerocoeff a \ nozerocoeff b \ nozerocoeff (numadd (a,b))" ``` wenzelm@51369 ` 901` ``` by (induct a b rule: numadd.induct) (auto simp add: Let_def) ``` chaieb@23264 ` 902` chaieb@23264 ` 903` ```lemma nummul_nz : "\ i. i\0 \ nozerocoeff a \ nozerocoeff (nummul a i)" ``` wenzelm@51369 ` 904` ``` by (induct a rule: nummul.induct) (auto simp add: Let_def numadd_nz) ``` chaieb@23264 ` 905` chaieb@23264 ` 906` ```lemma numneg_nz : "nozerocoeff a \ nozerocoeff (numneg a)" ``` wenzelm@51369 ` 907` ``` by (simp add: numneg_def nummul_nz) ``` chaieb@23264 ` 908` chaieb@23264 ` 909` ```lemma numsub_nz: "nozerocoeff a \ nozerocoeff b \ nozerocoeff (numsub a b)" ``` wenzelm@51369 ` 910` ``` by (simp add: numsub_def numneg_nz numadd_nz) ``` chaieb@23264 ` 911` chaieb@23264 ` 912` ```lemma split_int_nz: "nozerocoeff t \ nozerocoeff (fst (split_int t)) \ nozerocoeff (snd (split_int t))" ``` wenzelm@51369 ` 913` ``` by (induct t rule: split_int.induct) (auto simp add: Let_def split_def) ``` chaieb@23264 ` 914` chaieb@23264 ` 915` ```lemma numfloor_nz: "nozerocoeff t \ nozerocoeff (numfloor t)" ``` wenzelm@51369 ` 916` ``` by (simp add: numfloor_def Let_def split_def) ``` wenzelm@51369 ` 917` ``` (cases "fst (split_int t)", simp_all add: split_int_nz numadd_nz) ``` chaieb@23264 ` 918` chaieb@23264 ` 919` ```lemma simpnum_nz: "nozerocoeff (simpnum t)" ``` wenzelm@51369 ` 920` ``` by (induct t rule: simpnum.induct) ``` wenzelm@51369 ` 921` ``` (auto simp add: numadd_nz numneg_nz numsub_nz nummul_nz numfloor_nz) ``` chaieb@23264 ` 922` chaieb@23264 ` 923` ```lemma maxcoeff_nz: "nozerocoeff t \ maxcoeff t = 0 \ t = C 0" ``` chaieb@23264 ` 924` ```proof (induct t rule: maxcoeff.induct) ``` chaieb@23264 ` 925` ``` case (2 n c t) ``` chaieb@23264 ` 926` ``` hence cnz: "c \0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ ``` wenzelm@51369 ` 927` ``` have "max (abs c) (maxcoeff t) \ abs c" by simp ``` chaieb@23264 ` 928` ``` with cnz have "max (abs c) (maxcoeff t) > 0" by arith ``` wenzelm@41807 ` 929` ``` with 2 show ?case by simp ``` chaieb@23264 ` 930` ```next ``` chaieb@23264 ` 931` ``` case (3 c s t) ``` chaieb@23264 ` 932` ``` hence cnz: "c \0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ ``` wenzelm@51369 ` 933` ``` have "max (abs c) (maxcoeff t) \ abs c" by simp ``` chaieb@23264 ` 934` ``` with cnz have "max (abs c) (maxcoeff t) > 0" by arith ``` wenzelm@41807 ` 935` ``` with 3 show ?case by simp ``` chaieb@23264 ` 936` ```qed auto ``` chaieb@23264 ` 937` chaieb@23264 ` 938` ```lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0" ``` chaieb@23264 ` 939` ```proof- ``` chaieb@23264 ` 940` ``` from g0 have th:"numgcdh t (maxcoeff t) = 0" by (simp add: numgcd_def) ``` chaieb@23264 ` 941` ``` from numgcdh0[OF th] have th:"maxcoeff t = 0" . ``` chaieb@23264 ` 942` ``` from maxcoeff_nz[OF nz th] show ?thesis . ``` chaieb@23264 ` 943` ```qed ``` chaieb@23264 ` 944` haftmann@35416 ` 945` ```definition simp_num_pair :: "(num \ int) \ num \ int" where ``` chaieb@23264 ` 946` ``` "simp_num_pair \ (\ (t,n). (if n = 0 then (C 0, 0) else ``` chaieb@23264 ` 947` ``` (let t' = simpnum t ; g = numgcd t' in ``` huffman@31706 ` 948` ``` if g > 1 then (let g' = gcd n g in ``` chaieb@23264 ` 949` ``` if g' = 1 then (t',n) ``` chaieb@23264 ` 950` ``` else (reducecoeffh t' g', n div g')) ``` chaieb@23264 ` 951` ``` else (t',n))))" ``` chaieb@23264 ` 952` chaieb@23264 ` 953` ```lemma simp_num_pair_ci: ``` chaieb@23264 ` 954` ``` shows "((\ (t,n). Inum bs t / real n) (simp_num_pair (t,n))) = ((\ (t,n). Inum bs t / real n) (t,n))" ``` chaieb@23264 ` 955` ``` (is "?lhs = ?rhs") ``` chaieb@23264 ` 956` ```proof- ``` chaieb@23264 ` 957` ``` let ?t' = "simpnum t" ``` chaieb@23264 ` 958` ``` let ?g = "numgcd ?t'" ``` huffman@31706 ` 959` ``` let ?g' = "gcd n ?g" ``` chaieb@23264 ` 960` ``` {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)} ``` chaieb@23264 ` 961` ``` moreover ``` chaieb@23264 ` 962` ``` { assume nnz: "n \ 0" ``` chaieb@23264 ` 963` ``` {assume "\ ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def)} ``` chaieb@23264 ` 964` ``` moreover ``` chaieb@23264 ` 965` ``` {assume g1:"?g>1" hence g0: "?g > 0" by simp ``` huffman@31706 ` 966` ``` from g1 nnz have gp0: "?g' \ 0" by simp ``` nipkow@31952 ` 967` ``` hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith ``` chaieb@23264 ` 968` ``` hence "?g'= 1 \ ?g' > 1" by arith ``` chaieb@23264 ` 969` ``` moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def)} ``` chaieb@23264 ` 970` ``` moreover {assume g'1:"?g'>1" ``` wenzelm@32960 ` 971` ``` from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" .. ``` wenzelm@32960 ` 972` ``` let ?tt = "reducecoeffh ?t' ?g'" ``` wenzelm@32960 ` 973` ``` let ?t = "Inum bs ?tt" ``` wenzelm@32960 ` 974` ``` have gpdg: "?g' dvd ?g" by simp ``` wenzelm@32960 ` 975` ``` have gpdd: "?g' dvd n" by simp ``` wenzelm@32960 ` 976` ``` have gpdgp: "?g' dvd ?g'" by simp ``` wenzelm@32960 ` 977` ``` from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] ``` wenzelm@32960 ` 978` ``` have th2:"real ?g' * ?t = Inum bs ?t'" by simp ``` wenzelm@41807 ` 979` ``` from nnz g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) ``` wenzelm@32960 ` 980` ``` also have "\ = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp ``` wenzelm@32960 ` 981` ``` also have "\ = (Inum bs ?t' / real n)" ``` bulwahn@46670 ` 982` ``` using real_of_int_div[OF gpdd] th2 gp0 by simp ``` wenzelm@32960 ` 983` ``` finally have "?lhs = Inum bs t / real n" by simp ``` wenzelm@41807 ` 984` ``` then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) } ``` wenzelm@41807 ` 985` ``` ultimately have ?thesis by blast } ``` wenzelm@41807 ` 986` ``` ultimately have ?thesis by blast } ``` chaieb@23264 ` 987` ``` ultimately show ?thesis by blast ``` chaieb@23264 ` 988` ```qed ``` chaieb@23264 ` 989` wenzelm@41807 ` 990` ```lemma simp_num_pair_l: ``` wenzelm@41807 ` 991` ``` assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')" ``` chaieb@23264 ` 992` ``` shows "numbound0 t' \ n' >0" ``` chaieb@23264 ` 993` ```proof- ``` wenzelm@41807 ` 994` ``` let ?t' = "simpnum t" ``` chaieb@23264 ` 995` ``` let ?g = "numgcd ?t'" ``` huffman@31706 ` 996` ``` let ?g' = "gcd n ?g" ``` wenzelm@41807 ` 997` ``` { assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) } ``` chaieb@23264 ` 998` ``` moreover ``` chaieb@23264 ` 999` ``` { assume nnz: "n \ 0" ``` wenzelm@41807 ` 1000` ``` {assume "\ ?g > 1" hence ?thesis using assms by (auto simp add: Let_def simp_num_pair_def) } ``` chaieb@23264 ` 1001` ``` moreover ``` chaieb@23264 ` 1002` ``` {assume g1:"?g>1" hence g0: "?g > 0" by simp ``` huffman@31706 ` 1003` ``` from g1 nnz have gp0: "?g' \ 0" by simp ``` nipkow@31952 ` 1004` ``` hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith ``` chaieb@23264 ` 1005` ``` hence "?g'= 1 \ ?g' > 1" by arith ``` wenzelm@41807 ` 1006` ``` moreover {assume "?g'=1" hence ?thesis using assms g1 g0 ``` wenzelm@41807 ` 1007` ``` by (auto simp add: Let_def simp_num_pair_def) } ``` chaieb@23264 ` 1008` ``` moreover {assume g'1:"?g'>1" ``` wenzelm@32960 ` 1009` ``` have gpdg: "?g' dvd ?g" by simp ``` wenzelm@32960 ` 1010` ``` have gpdd: "?g' dvd n" by simp ``` wenzelm@32960 ` 1011` ``` have gpdgp: "?g' dvd ?g'" by simp ``` wenzelm@32960 ` 1012` ``` from zdvd_imp_le[OF gpdd np] have g'n: "?g' \ n" . ``` huffman@47142 ` 1013` ``` from zdiv_mono1[OF g'n g'p, simplified div_self[OF gp0]] ``` wenzelm@32960 ` 1014` ``` have "n div ?g' >0" by simp ``` wenzelm@41807 ` 1015` ``` hence ?thesis using assms g1 g'1 ``` wenzelm@32960 ` 1016` ``` by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)} ``` wenzelm@41807 ` 1017` ``` ultimately have ?thesis by blast } ``` wenzelm@41807 ` 1018` ``` ultimately have ?thesis by blast } ``` chaieb@23264 ` 1019` ``` ultimately show ?thesis by blast ``` chaieb@23264 ` 1020` ```qed ``` chaieb@23264 ` 1021` krauss@41839 ` 1022` ```fun not:: "fm \ fm" where ``` chaieb@23264 ` 1023` ``` "not (NOT p) = p" ``` krauss@41839 ` 1024` ```| "not T = F" ``` krauss@41839 ` 1025` ```| "not F = T" ``` krauss@41839 ` 1026` ```| "not (Lt t) = Ge t" ``` krauss@41839 ` 1027` ```| "not (Le t) = Gt t" ``` krauss@41839 ` 1028` ```| "not (Gt t) = Le t" ``` krauss@41839 ` 1029` ```| "not (Ge t) = Lt t" ``` krauss@41839 ` 1030` ```| "not (Eq t) = NEq t" ``` krauss@41839 ` 1031` ```| "not (NEq t) = Eq t" ``` krauss@41839 ` 1032` ```| "not (Dvd i t) = NDvd i t" ``` krauss@41839 ` 1033` ```| "not (NDvd i t) = Dvd i t" ``` krauss@41839 ` 1034` ```| "not (And p q) = Or (not p) (not q)" ``` krauss@41839 ` 1035` ```| "not (Or p q) = And (not p) (not q)" ``` krauss@41839 ` 1036` ```| "not p = NOT p" ``` chaieb@23264 ` 1037` ```lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)" ``` wenzelm@41807 ` 1038` ``` by (induct p) auto ``` chaieb@23264 ` 1039` ```lemma not_qf[simp]: "qfree p \ qfree (not p)" ``` wenzelm@41807 ` 1040` ``` by (induct p) auto ``` chaieb@23264 ` 1041` ```lemma not_nb[simp]: "bound0 p \ bound0 (not p)" ``` wenzelm@41807 ` 1042` ``` by (induct p) auto ``` chaieb@23264 ` 1043` haftmann@35416 ` 1044` ```definition conj :: "fm \ fm \ fm" where ``` chaieb@23264 ` 1045` ``` "conj p q \ (if (p = F \ q=F) then F else if p=T then q else if q=T then p else ``` chaieb@23264 ` 1046` ``` if p = q then p else And p q)" ``` chaieb@23264 ` 1047` ```lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)" ``` wenzelm@41807 ` 1048` ``` by (cases "p=F \ q=F", simp_all add: conj_def) (cases p, simp_all) ``` chaieb@23264 ` 1049` chaieb@23264 ` 1050` ```lemma conj_qf[simp]: "\qfree p ; qfree q\ \ qfree (conj p q)" ``` wenzelm@41807 ` 1051` ``` using conj_def by auto ``` chaieb@23264 ` 1052` ```lemma conj_nb[simp]: "\bound0 p ; bound0 q\ \ bound0 (conj p q)" ``` wenzelm@41807 ` 1053` ``` using conj_def by auto ``` chaieb@23264 ` 1054` haftmann@35416 ` 1055` ```definition disj :: "fm \ fm \ fm" where ``` chaieb@23264 ` 1056` ``` "disj p q \ (if (p = T \ q=T) then T else if p=F then q else if q=F then p ``` chaieb@23264 ` 1057` ``` else if p=q then p else Or p q)" ``` chaieb@23264 ` 1058` chaieb@23264 ` 1059` ```lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)" ``` wenzelm@41807 ` 1060` ``` by (cases "p=T \ q=T",simp_all add: disj_def) (cases p,simp_all) ``` chaieb@23264 ` 1061` ```lemma disj_qf[simp]: "\qfree p ; qfree q\ \ qfree (disj p q)" ``` wenzelm@41807 ` 1062` ``` using disj_def by auto ``` chaieb@23264 ` 1063` ```lemma disj_nb[simp]: "\bound0 p ; bound0 q\ \ bound0 (disj p q)" ``` wenzelm@41807 ` 1064` ``` using disj_def by auto ``` chaieb@23264 ` 1065` haftmann@35416 ` 1066` ```definition imp :: "fm \ fm \ fm" where ``` chaieb@23264 ` 1067` ``` "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 ``` chaieb@23264 ` 1068` ``` else Imp p q)" ``` chaieb@23264 ` 1069` ```lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)" ``` wenzelm@41807 ` 1070` ``` by (cases "p=F \ q=T",simp_all add: imp_def) ``` chaieb@23264 ` 1071` ```lemma imp_qf[simp]: "\qfree p ; qfree q\ \ qfree (imp p q)" ``` wenzelm@41807 ` 1072` ``` using imp_def by (cases "p=F \ q=T",simp_all add: imp_def) ``` chaieb@23264 ` 1073` haftmann@35416 ` 1074` ```definition iff :: "fm \ fm \ fm" where ``` chaieb@23264 ` 1075` ``` "iff p q \ (if (p = q) then T else if (p = not q \ not p = q) then F else ``` chaieb@23264 ` 1076` ``` 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 ``` chaieb@23264 ` 1077` ``` Iff p q)" ``` chaieb@23264 ` 1078` ```lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)" ``` wenzelm@51369 ` 1079` ``` by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp) ``` chaieb@23264 ` 1080` ```(cases "not p= q", auto simp add:not) ``` chaieb@23264 ` 1081` ```lemma iff_qf[simp]: "\qfree p ; qfree q\ \ qfree (iff p q)" ``` chaieb@23264 ` 1082` ``` by (unfold iff_def,cases "p=q", auto) ``` chaieb@23264 ` 1083` krauss@41839 ` 1084` ```fun check_int:: "num \ bool" where ``` chaieb@23264 ` 1085` ``` "check_int (C i) = True" ``` krauss@41839 ` 1086` ```| "check_int (Floor t) = True" ``` krauss@41839 ` 1087` ```| "check_int (Mul i t) = check_int t" ``` krauss@41839 ` 1088` ```| "check_int (Add t s) = (check_int t \ check_int s)" ``` krauss@41839 ` 1089` ```| "check_int (Neg t) = check_int t" ``` krauss@41839 ` 1090` ```| "check_int (CF c t s) = check_int s" ``` krauss@41839 ` 1091` ```| "check_int t = False" ``` chaieb@23264 ` 1092` ```lemma check_int: "check_int t \ isint t bs" ``` wenzelm@51369 ` 1093` ``` by (induct t) (auto simp add: isint_add isint_Floor isint_Mul isint_neg isint_c isint_CF) ``` chaieb@23264 ` 1094` chaieb@23264 ` 1095` ```lemma rdvd_left1_int: "real \t\ = t \ 1 rdvd t" ``` chaieb@23264 ` 1096` ``` by (simp add: rdvd_def,rule_tac x="\t\" in exI) simp ``` chaieb@23264 ` 1097` chaieb@23264 ` 1098` ```lemma rdvd_reduce: ``` chaieb@23264 ` 1099` ``` assumes gd:"g dvd d" and gc:"g dvd c" and gp: "g > 0" ``` chaieb@23264 ` 1100` ``` shows "real (d::int) rdvd real (c::int)*t = (real (d div g) rdvd real (c div g)*t)" ``` chaieb@23264 ` 1101` ```proof ``` chaieb@23264 ` 1102` ``` assume d: "real d rdvd real c * t" ``` chaieb@23264 ` 1103` ``` from d rdvd_def obtain k where k_def: "real c * t = real d* real (k::int)" by auto ``` chaieb@23264 ` 1104` ``` from gd dvd_def obtain kd where kd_def: "d = g * kd" by auto ``` chaieb@23264 ` 1105` ``` from gc dvd_def obtain kc where kc_def: "c = g * kc" by auto ``` chaieb@23264 ` 1106` ``` from k_def kd_def kc_def have "real g * real kc * t = real g * real kd * real k" by simp ``` chaieb@23264 ` 1107` ``` hence "real kc * t = real kd * real k" using gp by simp ``` chaieb@23264 ` 1108` ``` hence th:"real kd rdvd real kc * t" using rdvd_def by blast ``` chaieb@23264 ` 1109` ``` from kd_def gp have th':"kd = d div g" by simp ``` chaieb@23264 ` 1110` ``` from kc_def gp have "kc = c div g" by simp ``` chaieb@23264 ` 1111` ``` with th th' show "real (d div g) rdvd real (c div g) * t" by simp ``` chaieb@23264 ` 1112` ```next ``` chaieb@23264 ` 1113` ``` assume d: "real (d div g) rdvd real (c div g) * t" ``` chaieb@23264 ` 1114` ``` from gp have gnz: "g \ 0" by simp ``` bulwahn@46670 ` 1115` ``` thus "real d rdvd real c * t" using d rdvd_mult[OF gnz, where n="d div g" and x="real (c div g) * t"] real_of_int_div[OF gd] real_of_int_div[OF gc] by simp ``` chaieb@23264 ` 1116` ```qed ``` chaieb@23264 ` 1117` haftmann@35416 ` 1118` ```definition simpdvd :: "int \ num \ (int \ num)" where ``` chaieb@23264 ` 1119` ``` "simpdvd d t \ ``` chaieb@23264 ` 1120` ``` (let g = numgcd t in ``` huffman@31706 ` 1121` ``` if g > 1 then (let g' = gcd d g in ``` chaieb@23264 ` 1122` ``` if g' = 1 then (d, t) ``` chaieb@23264 ` 1123` ``` else (d div g',reducecoeffh t g')) ``` chaieb@23264 ` 1124` ``` else (d, t))" ``` chaieb@23264 ` 1125` ```lemma simpdvd: ``` chaieb@23264 ` 1126` ``` assumes tnz: "nozerocoeff t" and dnz: "d \ 0" ``` chaieb@23264 ` 1127` ``` shows "Ifm bs (Dvd (fst (simpdvd d t)) (snd (simpdvd d t))) = Ifm bs (Dvd d t)" ``` chaieb@23264 ` 1128` ```proof- ``` chaieb@23264 ` 1129` ``` let ?g = "numgcd t" ``` huffman@31706 ` 1130` ``` let ?g' = "gcd d ?g" ``` chaieb@23264 ` 1131` ``` {assume "\ ?g > 1" hence ?thesis by (simp add: Let_def simpdvd_def)} ``` chaieb@23264 ` 1132` ``` moreover ``` chaieb@23264 ` 1133` ``` {assume g1:"?g>1" hence g0: "?g > 0" by simp ``` huffman@31706 ` 1134` ``` from g1 dnz have gp0: "?g' \ 0" by simp ``` nipkow@31952 ` 1135` ``` hence g'p: "?g' > 0" using gcd_ge_0_int[where x="d" and y="numgcd t"] by arith ``` chaieb@23264 ` 1136` ``` hence "?g'= 1 \ ?g' > 1" by arith ``` chaieb@23264 ` 1137` ``` moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simpdvd_def)} ``` chaieb@23264 ` 1138` ``` moreover {assume g'1:"?g'>1" ``` chaieb@23264 ` 1139` ``` from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" .. ``` chaieb@23264 ` 1140` ``` let ?tt = "reducecoeffh t ?g'" ``` chaieb@23264 ` 1141` ``` let ?t = "Inum bs ?tt" ``` huffman@31706 ` 1142` ``` have gpdg: "?g' dvd ?g" by simp ``` huffman@31706 ` 1143` ``` have gpdd: "?g' dvd d" by simp ``` chaieb@23264 ` 1144` ``` have gpdgp: "?g' dvd ?g'" by simp ``` chaieb@23264 ` 1145` ``` from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] ``` chaieb@23264 ` 1146` ``` have th2:"real ?g' * ?t = Inum bs t" by simp ``` wenzelm@41807 ` 1147` ``` from assms g1 g0 g'1 ``` wenzelm@41807 ` 1148` ``` have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)" ``` wenzelm@32960 ` 1149` ``` by (simp add: simpdvd_def Let_def) ``` chaieb@23264 ` 1150` ``` also have "\ = (real d rdvd (Inum bs t))" ``` huffman@47142 ` 1151` ``` using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified div_self[OF gp0]] ``` wenzelm@32960 ` 1152` ``` th2[symmetric] by simp ``` chaieb@23264 ` 1153` ``` finally have ?thesis by simp } ``` chaieb@23264 ` 1154` ``` ultimately have ?thesis by blast ``` chaieb@23264 ` 1155` ``` } ``` chaieb@23264 ` 1156` ``` ultimately show ?thesis by blast ``` chaieb@23264 ` 1157` ```qed ``` chaieb@23264 ` 1158` krauss@41839 ` 1159` ```function (sequential) simpfm :: "fm \ fm" where ``` chaieb@23264 ` 1160` ``` "simpfm (And p q) = conj (simpfm p) (simpfm q)" ``` krauss@41839 ` 1161` ```| "simpfm (Or p q) = disj (simpfm p) (simpfm q)" ``` krauss@41839 ` 1162` ```| "simpfm (Imp p q) = imp (simpfm p) (simpfm q)" ``` krauss@41839 ` 1163` ```| "simpfm (Iff p q) = iff (simpfm p) (simpfm q)" ``` krauss@41839 ` 1164` ```| "simpfm (NOT p) = not (simpfm p)" ``` krauss@41839 ` 1165` ```| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \ if (v < 0) then T else F ``` chaieb@23264 ` 1166` ``` | _ \ Lt (reducecoeff a'))" ``` krauss@41839 ` 1167` ```| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ Le (reducecoeff a'))" ``` krauss@41839 ` 1168` ```| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \ if (v > 0) then T else F | _ \ Gt (reducecoeff a'))" ``` krauss@41839 ` 1169` ```| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ Ge (reducecoeff a'))" ``` krauss@41839 ` 1170` ```| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \ if (v = 0) then T else F | _ \ Eq (reducecoeff a'))" ``` krauss@41839 ` 1171` ```| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ NEq (reducecoeff a'))" ``` krauss@41839 ` 1172` ```| "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a) ``` chaieb@23264 ` 1173` ``` else if (abs i = 1) \ check_int a then T ``` chaieb@23264 ` 1174` ``` else let a' = simpnum a in case a' of C v \ if (i dvd v) then T else F | _ \ (let (d,t) = simpdvd i a' in Dvd d t))" ``` krauss@41839 ` 1175` ```| "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a) ``` chaieb@23264 ` 1176` ``` else if (abs i = 1) \ check_int a then F ``` chaieb@23264 ` 1177` ``` else let a' = simpnum a in case a' of C v \ if (\(i dvd v)) then T else F | _ \ (let (d,t) = simpdvd i a' in NDvd d t))" ``` krauss@41839 ` 1178` ```| "simpfm p = p" ``` krauss@41839 ` 1179` ```by pat_completeness auto ``` krauss@41839 ` 1180` ```termination by (relation "measure fmsize") auto ``` chaieb@23264 ` 1181` chaieb@23264 ` 1182` ```lemma simpfm[simp]: "Ifm bs (simpfm p) = Ifm bs p" ``` chaieb@23264 ` 1183` ```proof(induct p rule: simpfm.induct) ``` chaieb@23264 ` 1184` ``` case (6 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp ``` chaieb@23264 ` 1185` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` chaieb@23264 ` 1186` ``` moreover {assume H:"\ (\ v. ?sa = C v)" ``` chaieb@23264 ` 1187` ``` let ?g = "numgcd ?sa" ``` chaieb@23264 ` 1188` ``` let ?rsa = "reducecoeff ?sa" ``` chaieb@23264 ` 1189` ``` let ?r = "Inum bs ?rsa" ``` chaieb@23264 ` 1190` ``` have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) ``` chaieb@23264 ` 1191` ``` {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} ``` chaieb@23264 ` 1192` ``` with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) ``` chaieb@23264 ` 1193` ``` hence gp: "real ?g > 0" by simp ``` chaieb@23264 ` 1194` ``` have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff) ``` chaieb@23264 ` 1195` ``` with sa have "Inum bs a < 0 = (real ?g * ?r < real ?g * 0)" by simp ``` chaieb@23264 ` 1196` ``` also have "\ = (?r < 0)" using gp ``` chaieb@23264 ` 1197` ``` by (simp only: mult_less_cancel_left) simp ``` chaieb@23264 ` 1198` ``` finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} ``` chaieb@23264 ` 1199` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1200` ```next ``` chaieb@23264 ` 1201` ``` case (7 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp ``` chaieb@23264 ` 1202` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` chaieb@23264 ` 1203` ``` moreover {assume H:"\ (\ v. ?sa = C v)" ``` chaieb@23264 ` 1204` ``` let ?g = "numgcd ?sa" ``` chaieb@23264 ` 1205` ``` let ?rsa = "reducecoeff ?sa" ``` chaieb@23264 ` 1206` ``` let ?r = "Inum bs ?rsa" ``` chaieb@23264 ` 1207` ``` have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) ``` chaieb@23264 ` 1208` ``` {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} ``` chaieb@23264 ` 1209` ``` with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) ``` chaieb@23264 ` 1210` ``` hence gp: "real ?g > 0" by simp ``` chaieb@23264 ` 1211` ``` have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff) ``` chaieb@23264 ` 1212` ``` with sa have "Inum bs a \ 0 = (real ?g * ?r \ real ?g * 0)" by simp ``` chaieb@23264 ` 1213` ``` also have "\ = (?r \ 0)" using gp ``` chaieb@23264 ` 1214` ``` by (simp only: mult_le_cancel_left) simp ``` chaieb@23264 ` 1215` ``` finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} ``` chaieb@23264 ` 1216` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1217` ```next ``` chaieb@23264 ` 1218` ``` case (8 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp ``` chaieb@23264 ` 1219` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` chaieb@23264 ` 1220` ``` moreover {assume H:"\ (\ v. ?sa = C v)" ``` chaieb@23264 ` 1221` ``` let ?g = "numgcd ?sa" ``` chaieb@23264 ` 1222` ``` let ?rsa = "reducecoeff ?sa" ``` chaieb@23264 ` 1223` ``` let ?r = "Inum bs ?rsa" ``` chaieb@23264 ` 1224` ``` have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) ``` chaieb@23264 ` 1225` ``` {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} ``` chaieb@23264 ` 1226` ``` with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) ``` chaieb@23264 ` 1227` ``` hence gp: "real ?g > 0" by simp ``` chaieb@23264 ` 1228` ``` have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff) ``` chaieb@23264 ` 1229` ``` with sa have "Inum bs a > 0 = (real ?g * ?r > real ?g * 0)" by simp ``` chaieb@23264 ` 1230` ``` also have "\ = (?r > 0)" using gp ``` chaieb@23264 ` 1231` ``` by (simp only: mult_less_cancel_left) simp ``` chaieb@23264 ` 1232` ``` finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} ``` chaieb@23264 ` 1233` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1234` ```next ``` chaieb@23264 ` 1235` ``` case (9 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp ``` chaieb@23264 ` 1236` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` chaieb@23264 ` 1237` ``` moreover {assume H:"\ (\ v. ?sa = C v)" ``` chaieb@23264 ` 1238` ``` let ?g = "numgcd ?sa" ``` chaieb@23264 ` 1239` ``` let ?rsa = "reducecoeff ?sa" ``` chaieb@23264 ` 1240` ``` let ?r = "Inum bs ?rsa" ``` chaieb@23264 ` 1241` ``` have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) ``` chaieb@23264 ` 1242` ``` {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} ``` chaieb@23264 ` 1243` ``` with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) ``` chaieb@23264 ` 1244` ``` hence gp: "real ?g > 0" by simp ``` chaieb@23264 ` 1245` ``` have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff) ``` chaieb@23264 ` 1246` ``` with sa have "Inum bs a \ 0 = (real ?g * ?r \ real ?g * 0)" by simp ``` chaieb@23264 ` 1247` ``` also have "\ = (?r \ 0)" using gp ``` chaieb@23264 ` 1248` ``` by (simp only: mult_le_cancel_left) simp ``` chaieb@23264 ` 1249` ``` finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} ``` chaieb@23264 ` 1250` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1251` ```next ``` chaieb@23264 ` 1252` ``` case (10 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp ``` chaieb@23264 ` 1253` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` chaieb@23264 ` 1254` ``` moreover {assume H:"\ (\ v. ?sa = C v)" ``` chaieb@23264 ` 1255` ``` let ?g = "numgcd ?sa" ``` chaieb@23264 ` 1256` ``` let ?rsa = "reducecoeff ?sa" ``` chaieb@23264 ` 1257` ``` let ?r = "Inum bs ?rsa" ``` chaieb@23264 ` 1258` ``` have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) ``` chaieb@23264 ` 1259` ``` {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} ``` chaieb@23264 ` 1260` ``` with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) ``` chaieb@23264 ` 1261` ``` hence gp: "real ?g > 0" by simp ``` chaieb@23264 ` 1262` ``` have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff) ``` chaieb@23264 ` 1263` ``` with sa have "Inum bs a = 0 = (real ?g * ?r = 0)" by simp ``` chaieb@23264 ` 1264` ``` also have "\ = (?r = 0)" using gp ``` wenzelm@51369 ` 1265` ``` by simp ``` chaieb@23264 ` 1266` ``` finally have ?case using H by (cases "?sa" , simp_all add: Let_def)} ``` chaieb@23264 ` 1267` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1268` ```next ``` chaieb@23264 ` 1269` ``` case (11 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp ``` chaieb@23264 ` 1270` ``` {fix v assume "?sa = C v" hence ?case using sa by simp } ``` chaieb@23264 ` 1271` ``` moreover {assume H:"\ (\ v. ?sa = C v)" ``` chaieb@23264 ` 1272` ``` let ?g = "numgcd ?sa" ``` chaieb@23264 ` 1273` ``` let ?rsa = "reducecoeff ?sa" ``` chaieb@23264 ` 1274` ``` let ?r = "Inum bs ?rsa" ``` chaieb@23264 ` 1275` ``` have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz) ``` chaieb@23264 ` 1276` ``` {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto} ``` chaieb@23264 ` 1277` ``` with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto) ``` chaieb@23264 ` 1278` ``` hence gp: "real ?g > 0" by simp ``` chaieb@23264 ` 1279` ``` have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff) ``` chaieb@23264 ` 1280` ``` with sa have "Inum bs a \ 0 = (real ?g * ?r \ 0)" by simp ``` chaieb@23264 ` 1281` ``` also have "\ = (?r \ 0)" using gp ``` wenzelm@51369 ` 1282` ``` by simp ``` wenzelm@51369 ` 1283` ``` finally have ?case using H by (cases "?sa") (simp_all add: Let_def) } ``` chaieb@23264 ` 1284` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1285` ```next ``` chaieb@23264 ` 1286` ``` case (12 i a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp ``` chaieb@23264 ` 1287` ``` have "i=0 \ (abs i = 1 \ check_int a) \ (i\0 \ ((abs i \ 1) \ (\ check_int a)))" by auto ``` chaieb@23264 ` 1288` ``` {assume "i=0" hence ?case using "12.hyps" by (simp add: rdvd_left_0_eq Let_def)} ``` chaieb@23264 ` 1289` ``` moreover ``` chaieb@23264 ` 1290` ``` {assume ai1: "abs i = 1" and ai: "check_int a" ``` chaieb@23264 ` 1291` ``` hence "i=1 \ i= - 1" by arith ``` chaieb@23264 ` 1292` ``` moreover {assume i1: "i = 1" ``` chaieb@23264 ` 1293` ``` from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]] ``` chaieb@23264 ` 1294` ``` have ?case using i1 ai by simp } ``` chaieb@23264 ` 1295` ``` moreover {assume i1: "i = - 1" ``` chaieb@23264 ` 1296` ``` from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]] ``` wenzelm@32960 ` 1297` ``` rdvd_abs1[where d="- 1" and t="Inum bs a"] ``` chaieb@23264 ` 1298` ``` have ?case using i1 ai by simp } ``` chaieb@23264 ` 1299` ``` ultimately have ?case by blast} ``` chaieb@23264 ` 1300` ``` moreover ``` chaieb@23264 ` 1301` ``` {assume inz: "i\0" and cond: "(abs i \ 1) \ (\ check_int a)" ``` chaieb@23264 ` 1302` ``` {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond ``` wenzelm@32960 ` 1303` ``` by (cases "abs i = 1", auto simp add: int_rdvd_iff) } ``` chaieb@23264 ` 1304` ``` moreover {assume H:"\ (\ v. ?sa = C v)" ``` chaieb@23264 ` 1305` ``` hence th: "simpfm (Dvd i a) = Dvd (fst (simpdvd i ?sa)) (snd (simpdvd i ?sa))" using inz cond by (cases ?sa, auto simp add: Let_def split_def) ``` chaieb@23264 ` 1306` ``` from simpnum_nz have nz:"nozerocoeff ?sa" by simp ``` chaieb@23264 ` 1307` ``` from simpdvd [OF nz inz] th have ?case using sa by simp} ``` chaieb@23264 ` 1308` ``` ultimately have ?case by blast} ``` chaieb@23264 ` 1309` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1310` ```next ``` chaieb@23264 ` 1311` ``` case (13 i a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp ``` chaieb@23264 ` 1312` ``` have "i=0 \ (abs i = 1 \ check_int a) \ (i\0 \ ((abs i \ 1) \ (\ check_int a)))" by auto ``` chaieb@23264 ` 1313` ``` {assume "i=0" hence ?case using "13.hyps" by (simp add: rdvd_left_0_eq Let_def)} ``` chaieb@23264 ` 1314` ``` moreover ``` chaieb@23264 ` 1315` ``` {assume ai1: "abs i = 1" and ai: "check_int a" ``` chaieb@23264 ` 1316` ``` hence "i=1 \ i= - 1" by arith ``` chaieb@23264 ` 1317` ``` moreover {assume i1: "i = 1" ``` chaieb@23264 ` 1318` ``` from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]] ``` chaieb@23264 ` 1319` ``` have ?case using i1 ai by simp } ``` chaieb@23264 ` 1320` ``` moreover {assume i1: "i = - 1" ``` chaieb@23264 ` 1321` ``` from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]] ``` wenzelm@32960 ` 1322` ``` rdvd_abs1[where d="- 1" and t="Inum bs a"] ``` chaieb@23264 ` 1323` ``` have ?case using i1 ai by simp } ``` chaieb@23264 ` 1324` ``` ultimately have ?case by blast} ``` chaieb@23264 ` 1325` ``` moreover ``` chaieb@23264 ` 1326` ``` {assume inz: "i\0" and cond: "(abs i \ 1) \ (\ check_int a)" ``` chaieb@23264 ` 1327` ``` {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond ``` wenzelm@32960 ` 1328` ``` by (cases "abs i = 1", auto simp add: int_rdvd_iff) } ``` chaieb@23264 ` 1329` ``` moreover {assume H:"\ (\ v. ?sa = C v)" ``` chaieb@23264 ` 1330` ``` hence th: "simpfm (NDvd i a) = NDvd (fst (simpdvd i ?sa)) (snd (simpdvd i ?sa))" using inz cond ``` wenzelm@32960 ` 1331` ``` by (cases ?sa, auto simp add: Let_def split_def) ``` chaieb@23264 ` 1332` ``` from simpnum_nz have nz:"nozerocoeff ?sa" by simp ``` chaieb@23264 ` 1333` ``` from simpdvd [OF nz inz] th have ?case using sa by simp} ``` chaieb@23264 ` 1334` ``` ultimately have ?case by blast} ``` chaieb@23264 ` 1335` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1336` ```qed (induct p rule: simpfm.induct, simp_all) ``` chaieb@23264 ` 1337` chaieb@23264 ` 1338` ```lemma simpdvd_numbound0: "numbound0 t \ numbound0 (snd (simpdvd d t))" ``` chaieb@23264 ` 1339` ``` by (simp add: simpdvd_def Let_def split_def reducecoeffh_numbound0) ``` chaieb@23264 ` 1340` chaieb@23264 ` 1341` ```lemma simpfm_bound0[simp]: "bound0 p \ bound0 (simpfm p)" ``` chaieb@23264 ` 1342` ```proof(induct p rule: simpfm.induct) ``` chaieb@23264 ` 1343` ``` case (6 a) hence nb: "numbound0 a" by simp ``` chaieb@23264 ` 1344` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` chaieb@23264 ` 1345` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0) ``` chaieb@23264 ` 1346` ```next ``` chaieb@23264 ` 1347` ``` case (7 a) hence nb: "numbound0 a" by simp ``` chaieb@23264 ` 1348` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` chaieb@23264 ` 1349` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0) ``` chaieb@23264 ` 1350` ```next ``` chaieb@23264 ` 1351` ``` case (8 a) hence nb: "numbound0 a" by simp ``` chaieb@23264 ` 1352` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` chaieb@23264 ` 1353` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0) ``` chaieb@23264 ` 1354` ```next ``` chaieb@23264 ` 1355` ``` case (9 a) hence nb: "numbound0 a" by simp ``` chaieb@23264 ` 1356` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` chaieb@23264 ` 1357` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0) ``` chaieb@23264 ` 1358` ```next ``` chaieb@23264 ` 1359` ``` case (10 a) hence nb: "numbound0 a" by simp ``` chaieb@23264 ` 1360` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` chaieb@23264 ` 1361` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0) ``` chaieb@23264 ` 1362` ```next ``` chaieb@23264 ` 1363` ``` case (11 a) hence nb: "numbound0 a" by simp ``` chaieb@23264 ` 1364` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` chaieb@23264 ` 1365` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0) ``` chaieb@23264 ` 1366` ```next ``` chaieb@23264 ` 1367` ``` case (12 i a) hence nb: "numbound0 a" by simp ``` chaieb@23264 ` 1368` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` chaieb@23264 ` 1369` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0 simpdvd_numbound0 split_def) ``` chaieb@23264 ` 1370` ```next ``` chaieb@23264 ` 1371` ``` case (13 i a) hence nb: "numbound0 a" by simp ``` chaieb@23264 ` 1372` ``` hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) ``` chaieb@23264 ` 1373` ``` thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0 simpdvd_numbound0 split_def) ``` chaieb@23264 ` 1374` ```qed(auto simp add: disj_def imp_def iff_def conj_def) ``` chaieb@23264 ` 1375` chaieb@23264 ` 1376` ```lemma simpfm_qf[simp]: "qfree p \ qfree (simpfm p)" ``` chaieb@23264 ` 1377` ```by (induct p rule: simpfm.induct, auto simp add: Let_def) ``` chaieb@23264 ` 1378` ```(case_tac "simpnum a",auto simp add: split_def Let_def)+ ``` chaieb@23264 ` 1379` chaieb@23264 ` 1380` chaieb@23264 ` 1381` ``` (* Generic quantifier elimination *) ``` chaieb@23264 ` 1382` haftmann@35416 ` 1383` ```definition list_conj :: "fm list \ fm" where ``` chaieb@23264 ` 1384` ``` "list_conj ps \ foldr conj ps T" ``` chaieb@23264 ` 1385` ```lemma list_conj: "Ifm bs (list_conj ps) = (\p\ set ps. Ifm bs p)" ``` chaieb@23264 ` 1386` ``` by (induct ps, auto simp add: list_conj_def) ``` chaieb@23264 ` 1387` ```lemma list_conj_qf: " \p\ set ps. qfree p \ qfree (list_conj ps)" ``` chaieb@23264 ` 1388` ``` by (induct ps, auto simp add: list_conj_def) ``` chaieb@23264 ` 1389` ```lemma list_conj_nb: " \p\ set ps. bound0 p \ bound0 (list_conj ps)" ``` chaieb@23264 ` 1390` ``` by (induct ps, auto simp add: list_conj_def) ``` haftmann@35416 ` 1391` ```definition CJNB :: "(fm \ fm) \ fm \ fm" where ``` haftmann@29788 ` 1392` ``` "CJNB f p \ (let cjs = conjuncts p ; (yes,no) = List.partition bound0 cjs ``` chaieb@23264 ` 1393` ``` in conj (decr (list_conj yes)) (f (list_conj no)))" ``` chaieb@23264 ` 1394` chaieb@23264 ` 1395` ```lemma CJNB_qe: ``` chaieb@23264 ` 1396` ``` assumes qe: "\ bs p. qfree p \ qfree (qe p) \ (Ifm bs (qe p) = Ifm bs (E p))" ``` chaieb@23264 ` 1397` ``` shows "\ bs p. qfree p \ qfree (CJNB qe p) \ (Ifm bs ((CJNB qe p)) = Ifm bs (E p))" ``` chaieb@23264 ` 1398` ```proof(clarify) ``` chaieb@23264 ` 1399` ``` fix bs p ``` chaieb@23264 ` 1400` ``` assume qfp: "qfree p" ``` chaieb@23264 ` 1401` ``` let ?cjs = "conjuncts p" ``` haftmann@29788 ` 1402` ``` let ?yes = "fst (List.partition bound0 ?cjs)" ``` haftmann@29788 ` 1403` ``` let ?no = "snd (List.partition bound0 ?cjs)" ``` chaieb@23264 ` 1404` ``` let ?cno = "list_conj ?no" ``` chaieb@23264 ` 1405` ``` let ?cyes = "list_conj ?yes" ``` haftmann@29788 ` 1406` ``` have part: "List.partition bound0 ?cjs = (?yes,?no)" by simp ``` chaieb@23264 ` 1407` ``` from partition_P[OF part] have "\ q\ set ?yes. bound0 q" by blast ``` chaieb@23264 ` 1408` ``` hence yes_nb: "bound0 ?cyes" by (simp add: list_conj_nb) ``` chaieb@23264 ` 1409` ``` hence yes_qf: "qfree (decr ?cyes )" by (simp add: decr_qf) ``` chaieb@23264 ` 1410` ``` from conjuncts_qf[OF qfp] partition_set[OF part] ``` chaieb@23264 ` 1411` ``` have " \q\ set ?no. qfree q" by auto ``` chaieb@23264 ` 1412` ``` hence no_qf: "qfree ?cno"by (simp add: list_conj_qf) ``` chaieb@23264 ` 1413` ``` with qe have cno_qf:"qfree (qe ?cno )" ``` chaieb@23264 ` 1414` ``` and noE: "Ifm bs (qe ?cno) = Ifm bs (E ?cno)" by blast+ ``` chaieb@23264 ` 1415` ``` from cno_qf yes_qf have qf: "qfree (CJNB qe p)" ``` wenzelm@51369 ` 1416` ``` by (simp add: CJNB_def Let_def split_def) ``` chaieb@23264 ` 1417` ``` {fix bs ``` chaieb@23264 ` 1418` ``` from conjuncts have "Ifm bs p = (\q\ set ?cjs. Ifm bs q)" by blast ``` chaieb@23264 ` 1419` ``` also have "\ = ((\q\ set ?yes. Ifm bs q) \ (\q\ set ?no. Ifm bs q))" ``` chaieb@23264 ` 1420` ``` using partition_set[OF part] by auto ``` chaieb@23264 ` 1421` ``` finally have "Ifm bs p = ((Ifm bs ?cyes) \ (Ifm bs ?cno))" using list_conj by simp} ``` chaieb@23264 ` 1422` ``` hence "Ifm bs (E p) = (\x. (Ifm (x#bs) ?cyes) \ (Ifm (x#bs) ?cno))" by simp ``` wenzelm@26932 ` 1423` ``` also fix y have "\ = (\x. (Ifm (y#bs) ?cyes) \ (Ifm (x#bs) ?cno))" ``` chaieb@23264 ` 1424` ``` using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast ``` chaieb@23264 ` 1425` ``` also have "\ = (Ifm bs (decr ?cyes) \ Ifm bs (E ?cno))" ``` hoelzl@33639 ` 1426` ``` by (auto simp add: decr[OF yes_nb] simp del: partition_filter_conv) ``` chaieb@23264 ` 1427` ``` also have "\ = (Ifm bs (conj (decr ?cyes) (qe ?cno)))" ``` chaieb@23264 ` 1428` ``` using qe[rule_format, OF no_qf] by auto ``` chaieb@23264 ` 1429` ``` finally have "Ifm bs (E p) = Ifm bs (CJNB qe p)" ``` chaieb@23264 ` 1430` ``` by (simp add: Let_def CJNB_def split_def) ``` chaieb@23264 ` 1431` ``` with qf show "qfree (CJNB qe p) \ Ifm bs (CJNB qe p) = Ifm bs (E p)" by blast ``` chaieb@23264 ` 1432` ```qed ``` chaieb@23264 ` 1433` krauss@41839 ` 1434` ```function (sequential) qelim :: "fm \ (fm \ fm) \ fm" where ``` chaieb@23264 ` 1435` ``` "qelim (E p) = (\ qe. DJ (CJNB qe) (qelim p qe))" ``` krauss@41839 ` 1436` ```| "qelim (A p) = (\ qe. not (qe ((qelim (NOT p) qe))))" ``` krauss@41839 ` 1437` ```| "qelim (NOT p) = (\ qe. not (qelim p qe))" ``` krauss@41839 ` 1438` ```| "qelim (And p q) = (\ qe. conj (qelim p qe) (qelim q qe))" ``` krauss@41839 ` 1439` ```| "qelim (Or p q) = (\ qe. disj (qelim p qe) (qelim q qe))" ``` krauss@41839 ` 1440` ```| "qelim (Imp p q) = (\ qe. disj (qelim (NOT p) qe) (qelim q qe))" ``` krauss@41839 ` 1441` ```| "qelim (Iff p q) = (\ qe. iff (qelim p qe) (qelim q qe))" ``` krauss@41839 ` 1442` ```| "qelim p = (\ y. simpfm p)" ``` krauss@41839 ` 1443` ```by pat_completeness auto ``` krauss@41839 ` 1444` ```termination by (relation "measure fmsize") auto ``` chaieb@23264 ` 1445` chaieb@23264 ` 1446` ```lemma qelim_ci: ``` chaieb@23264 ` 1447` ``` assumes qe_inv: "\ bs p. qfree p \ qfree (qe p) \ (Ifm bs (qe p) = Ifm bs (E p))" ``` chaieb@23264 ` 1448` ``` shows "\ bs. qfree (qelim p qe) \ (Ifm bs (qelim p qe) = Ifm bs p)" ``` wenzelm@41807 ` 1449` ``` using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]] ``` wenzelm@41807 ` 1450` ``` by (induct p rule: qelim.induct) (auto simp del: simpfm.simps) ``` chaieb@23264 ` 1451` chaieb@23264 ` 1452` chaieb@23316 ` 1453` ```text {* The @{text "\"} Part *} ``` chaieb@23316 ` 1454` ```text{* Linearity for fm where Bound 0 ranges over @{text "\"} *} ``` krauss@41839 ` 1455` krauss@41839 ` 1456` ```function zsplit0 :: "num \ int \ num" (* splits the bounded from the unbounded part*) where ``` chaieb@23264 ` 1457` ``` "zsplit0 (C c) = (0,C c)" ``` krauss@41839 ` 1458` ```| "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))" ``` krauss@41839 ` 1459` ```| "zsplit0 (CN n c a) = zsplit0 (Add (Mul c (Bound n)) a)" ``` krauss@41839 ` 1460` ```| "zsplit0 (CF c a b) = zsplit0 (Add (Mul c (Floor a)) b)" ``` krauss@41839 ` 1461` ```| "zsplit0 (Neg a) = (let (i',a') = zsplit0 a in (-i', Neg a'))" ``` krauss@41839 ` 1462` ```| "zsplit0 (Add a b) = (let (ia,a') = zsplit0 a ; ``` chaieb@23264 ` 1463` ``` (ib,b') = zsplit0 b ``` chaieb@23264 ` 1464` ``` in (ia+ib, Add a' b'))" ``` krauss@41839 ` 1465` ```| "zsplit0 (Sub a b) = (let (ia,a') = zsplit0 a ; ``` chaieb@23264 ` 1466` ``` (ib,b') = zsplit0 b ``` chaieb@23264 ` 1467` ``` in (ia-ib, Sub a' b'))" ``` krauss@41839 ` 1468` ```| "zsplit0 (Mul i a) = (let (i',a') = zsplit0 a in (i*i', Mul i a'))" ``` krauss@41839 ` 1469` ```| "zsplit0 (Floor a) = (let (i',a') = zsplit0 a in (i',Floor a'))" ``` krauss@41839 ` 1470` ```by pat_completeness auto ``` krauss@41839 ` 1471` ```termination by (relation "measure num_size") auto ``` chaieb@23264 ` 1472` chaieb@23264 ` 1473` ```lemma zsplit0_I: ``` chaieb@23264 ` 1474` ``` shows "\ n a. zsplit0 t = (n,a) \ (Inum ((real (x::int)) #bs) (CN 0 n a) = Inum (real x #bs) t) \ numbound0 a" ``` chaieb@23264 ` 1475` ``` (is "\ n a. ?S t = (n,a) \ (?I x (CN 0 n a) = ?I x t) \ ?N a") ``` chaieb@23264 ` 1476` ```proof(induct t rule: zsplit0.induct) ``` chaieb@23264 ` 1477` ``` case (1 c n a) thus ?case by auto ``` chaieb@23264 ` 1478` ```next ``` chaieb@23264 ` 1479` ``` case (2 m n a) thus ?case by (cases "m=0") auto ``` chaieb@23264 ` 1480` ```next ``` chaieb@23264 ` 1481` ``` case (3 n i a n a') thus ?case by auto ``` chaieb@23264 ` 1482` ```next ``` chaieb@23264 ` 1483` ``` case (4 c a b n a') thus ?case by auto ``` chaieb@23264 ` 1484` ```next ``` chaieb@23264 ` 1485` ``` case (5 t n a) ``` chaieb@23264 ` 1486` ``` let ?nt = "fst (zsplit0 t)" ``` chaieb@23264 ` 1487` ``` let ?at = "snd (zsplit0 t)" ``` wenzelm@41807 ` 1488` ``` have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \ n=-?nt" using 5 ``` chaieb@23264 ` 1489` ``` by (simp add: Let_def split_def) ``` wenzelm@41891 ` 1490` ``` from abj 5 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast ``` chaieb@23264 ` 1491` ``` from th2[simplified] th[simplified] show ?case by simp ``` chaieb@23264 ` 1492` ```next ``` chaieb@23264 ` 1493` ``` case (6 s t n a) ``` chaieb@23264 ` 1494` ``` let ?ns = "fst (zsplit0 s)" ``` chaieb@23264 ` 1495` ``` let ?as = "snd (zsplit0 s)" ``` chaieb@23264 ` 1496` ``` let ?nt = "fst (zsplit0 t)" ``` chaieb@23264 ` 1497` ``` let ?at = "snd (zsplit0 t)" ``` chaieb@23264 ` 1498` ``` have abjs: "zsplit0 s = (?ns,?as)" by simp ``` chaieb@23264 ` 1499` ``` moreover have abjt: "zsplit0 t = (?nt,?at)" by simp ``` wenzelm@41891 ` 1500` ``` ultimately have th: "a=Add ?as ?at \ n=?ns + ?nt" using 6 ``` chaieb@23264 ` 1501` ``` by (simp add: Let_def split_def) ``` chaieb@23264 ` 1502` ``` from abjs[symmetric] have bluddy: "\ x y. (x,y) = zsplit0 s" by blast ``` wenzelm@41891 ` 1503` ``` from 6 have "(\ x y. (x,y) = zsplit0 s) \ (\xa xb. zsplit0 t = (xa, xb) \ Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \ numbound0 xb)" by blast (*FIXME*) ``` chaieb@23264 ` 1504` ``` with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast ``` wenzelm@41891 ` 1505` ``` from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \ ?N ?as" by blast ``` chaieb@23264 ` 1506` ``` from th3[simplified] th2[simplified] th[simplified] show ?case ``` webertj@49962 ` 1507` ``` by (simp add: distrib_right) ``` chaieb@23264 ` 1508` ```next ``` chaieb@23264 ` 1509` ``` case (7 s t n a) ``` chaieb@23264 ` 1510` ``` let ?ns = "fst (zsplit0 s)" ``` chaieb@23264 ` 1511` ``` let ?as = "snd (zsplit0 s)" ``` chaieb@23264 ` 1512` ``` let ?nt = "fst (zsplit0 t)" ``` chaieb@23264 ` 1513` ``` let ?at = "snd (zsplit0 t)" ``` chaieb@23264 ` 1514` ``` have abjs: "zsplit0 s = (?ns,?as)" by simp ``` chaieb@23264 ` 1515` ``` moreover have abjt: "zsplit0 t = (?nt,?at)" by simp ``` wenzelm@41891 ` 1516` ``` ultimately have th: "a=Sub ?as ?at \ n=?ns - ?nt" using 7 ``` chaieb@23264 ` 1517` ``` by (simp add: Let_def split_def) ``` chaieb@23264 ` 1518` ``` from abjs[symmetric] have bluddy: "\ x y. (x,y) = zsplit0 s" by blast ``` wenzelm@41891 ` 1519` ``` from 7 have "(\ x y. (x,y) = zsplit0 s) \ (\xa xb. zsplit0 t = (xa, xb) \ Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \ numbound0 xb)" by blast (*FIXME*) ``` chaieb@23264 ` 1520` ``` with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast ``` wenzelm@41891 ` 1521` ``` from abjs 7 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \ ?N ?as" by blast ``` chaieb@23264 ` 1522` ``` from th3[simplified] th2[simplified] th[simplified] show ?case ``` chaieb@23264 ` 1523` ``` by (simp add: left_diff_distrib) ``` chaieb@23264 ` 1524` ```next ``` chaieb@23264 ` 1525` ``` case (8 i t n a) ``` chaieb@23264 ` 1526` ``` let ?nt = "fst (zsplit0 t)" ``` chaieb@23264 ` 1527` ``` let ?at = "snd (zsplit0 t)" ``` wenzelm@41891 ` 1528` ``` have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \ n=i*?nt" using 8 ``` chaieb@23264 ` 1529` ``` by (simp add: Let_def split_def) ``` wenzelm@41891 ` 1530` ``` from abj 8 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast ``` wenzelm@41891 ` 1531` ``` hence "?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp ``` webertj@49962 ` 1532` ``` also have "\ = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left) ``` chaieb@23264 ` 1533` ``` finally show ?case using th th2 by simp ``` chaieb@23264 ` 1534` ```next ``` chaieb@23264 ` 1535` ``` case (9 t n a) ``` chaieb@23264 ` 1536` ``` let ?nt = "fst (zsplit0 t)" ``` chaieb@23264 ` 1537` ``` let ?at = "snd (zsplit0 t)" ``` wenzelm@41891 ` 1538` ``` have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a= Floor ?at \ n=?nt" using 9 ``` chaieb@23264 ` 1539` ``` by (simp add: Let_def split_def) ``` wenzelm@41891 ` 1540` ``` from abj 9 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?N ?at" by blast ``` chaieb@23264 ` 1541` ``` hence na: "?N a" using th by simp ``` chaieb@23264 ` 1542` ``` have th': "(real ?nt)*(real x) = real (?nt * x)" by simp ``` chaieb@23264 ` 1543` ``` have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp ``` chaieb@23264 ` 1544` ``` also have "\ = real (floor ((real ?nt)* real(x) + ?I x ?at))" by simp ``` chaieb@23264 ` 1545` ``` also have "\ = real (floor (?I x ?at + real (?nt* x)))" by (simp add: add_ac) ``` chaieb@23264 ` 1546` ``` also have "\ = real (floor (?I x ?at) + (?nt* x))" ``` chaieb@23264 ` 1547` ``` using floor_add[where x="?I x ?at" and a="?nt* x"] by simp ``` chaieb@23264 ` 1548` ``` also have "\ = real (?nt)*(real x) + real (floor (?I x ?at))" by (simp add: add_ac) ``` chaieb@23264 ` 1549` ``` finally have "?I x (Floor t) = ?I x (CN 0 n a)" using th by simp ``` chaieb@23264 ` 1550` ``` with na show ?case by simp ``` chaieb@23264 ` 1551` ```qed ``` chaieb@23264 ` 1552` chaieb@23264 ` 1553` ```consts ``` chaieb@23264 ` 1554` ``` iszlfm :: "fm \ real list \ bool" (* Linearity test for fm *) ``` chaieb@23264 ` 1555` ``` zlfm :: "fm \ fm" (* Linearity transformation for fm *) ``` chaieb@23264 ` 1556` ```recdef iszlfm "measure size" ``` chaieb@23264 ` 1557` ``` "iszlfm (And p q) = (\ bs. iszlfm p bs \ iszlfm q bs)" ``` chaieb@23264 ` 1558` ``` "iszlfm (Or p q) = (\ bs. iszlfm p bs \ iszlfm q bs)" ``` chaieb@23264 ` 1559` ``` "iszlfm (Eq (CN 0 c e)) = (\ bs. c>0 \ numbound0 e \ isint e bs)" ``` chaieb@23264 ` 1560` ``` "iszlfm (NEq (CN 0 c e)) = (\ bs. c>0 \ numbound0 e \ isint e bs)" ``` chaieb@23264 ` 1561` ``` "iszlfm (Lt (CN 0 c e)) = (\ bs. c>0 \ numbound0 e \ isint e bs)" ``` chaieb@23264 ` 1562` ``` "iszlfm (Le (CN 0 c e)) = (\ bs. c>0 \ numbound0 e \ isint e bs)" ``` chaieb@23264 ` 1563` ``` "iszlfm (Gt (CN 0 c e)) = (\ bs. c>0 \ numbound0 e \ isint e bs)" ``` chaieb@23264 ` 1564` ``` "iszlfm (Ge (CN 0 c e)) = (\ bs. c>0 \ numbound0 e \ isint e bs)" ``` chaieb@23264 ` 1565` ``` "iszlfm (Dvd i (CN 0 c e)) = ``` chaieb@23264 ` 1566` ``` (\ bs. c>0 \ i>0 \ numbound0 e \ isint e bs)" ``` chaieb@23264 ` 1567` ``` "iszlfm (NDvd i (CN 0 c e))= ``` chaieb@23264 ` 1568` ``` (\ bs. c>0 \ i>0 \ numbound0 e \ isint e bs)" ``` chaieb@23264 ` 1569` ``` "iszlfm p = (\ bs. isatom p \ (bound0 p))" ``` chaieb@23264 ` 1570` chaieb@23264 ` 1571` ```lemma zlin_qfree: "iszlfm p bs \ qfree p" ``` chaieb@23264 ` 1572` ``` by (induct p rule: iszlfm.induct) auto ``` chaieb@23264 ` 1573` chaieb@23264 ` 1574` ```lemma iszlfm_gen: ``` chaieb@23264 ` 1575` ``` assumes lp: "iszlfm p (x#bs)" ``` chaieb@23264 ` 1576` ``` shows "\ y. iszlfm p (y#bs)" ``` chaieb@23264 ` 1577` ```proof ``` chaieb@23264 ` 1578` ``` fix y ``` chaieb@23264 ` 1579` ``` show "iszlfm p (y#bs)" ``` chaieb@23264 ` 1580` ``` using lp ``` chaieb@23264 ` 1581` ``` by(induct p rule: iszlfm.induct, simp_all add: numbound0_gen[rule_format, where x="x" and y="y"]) ``` chaieb@23264 ` 1582` ```qed ``` chaieb@23264 ` 1583` chaieb@23264 ` 1584` ```lemma conj_zl[simp]: "iszlfm p bs \ iszlfm q bs \ iszlfm (conj p q) bs" ``` chaieb@23264 ` 1585` ``` using conj_def by (cases p,auto) ``` chaieb@23264 ` 1586` ```lemma disj_zl[simp]: "iszlfm p bs \ iszlfm q bs \ iszlfm (disj p q) bs" ``` chaieb@23264 ` 1587` ``` using disj_def by (cases p,auto) ``` chaieb@23264 ` 1588` chaieb@23264 ` 1589` ```recdef zlfm "measure fmsize" ``` chaieb@23264 ` 1590` ``` "zlfm (And p q) = conj (zlfm p) (zlfm q)" ``` chaieb@23264 ` 1591` ``` "zlfm (Or p q) = disj (zlfm p) (zlfm q)" ``` chaieb@23264 ` 1592` ``` "zlfm (Imp p q) = disj (zlfm (NOT p)) (zlfm q)" ``` chaieb@23264 ` 1593` ``` "zlfm (Iff p q) = disj (conj (zlfm p) (zlfm q)) (conj (zlfm (NOT p)) (zlfm (NOT q)))" ``` chaieb@23264 ` 1594` ``` "zlfm (Lt a) = (let (c,r) = zsplit0 a in ``` chaieb@23264 ` 1595` ``` if c=0 then Lt r else ``` chaieb@23264 ` 1596` ``` if c>0 then Or (Lt (CN 0 c (Neg (Floor (Neg r))))) (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Lt (Add (Floor (Neg r)) r))) ``` chaieb@23264 ` 1597` ``` else Or (Gt (CN 0 (-c) (Floor(Neg r)))) (And (Eq(CN 0 (-c) (Floor(Neg r)))) (Lt (Add (Floor (Neg r)) r))))" ``` chaieb@23264 ` 1598` ``` "zlfm (Le a) = (let (c,r) = zsplit0 a in ``` chaieb@23264 ` 1599` ``` if c=0 then Le r else ``` chaieb@23264 ` 1600` ``` if c>0 then Or (Le (CN 0 c (Neg (Floor (Neg r))))) (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Lt (Add (Floor (Neg r)) r))) ``` chaieb@23264 ` 1601` ``` else Or (Ge (CN 0 (-c) (Floor(Neg r)))) (And (Eq(CN 0 (-c) (Floor(Neg r)))) (Lt (Add (Floor (Neg r)) r))))" ``` chaieb@23264 ` 1602` ``` "zlfm (Gt a) = (let (c,r) = zsplit0 a in ``` chaieb@23264 ` 1603` ``` if c=0 then Gt r else ``` chaieb@23264 ` 1604` ``` if c>0 then Or (Gt (CN 0 c (Floor r))) (And (Eq (CN 0 c (Floor r))) (Lt (Sub (Floor r) r))) ``` chaieb@23264 ` 1605` ``` else Or (Lt (CN 0 (-c) (Neg (Floor r)))) (And (Eq(CN 0 (-c) (Neg (Floor r)))) (Lt (Sub (Floor r) r))))" ``` chaieb@23264 ` 1606` ``` "zlfm (Ge a) = (let (c,r) = zsplit0 a in ``` chaieb@23264 ` 1607` ``` if c=0 then Ge r else ``` chaieb@23264 ` 1608` ``` if c>0 then Or (Ge (CN 0 c (Floor r))) (And (Eq (CN 0 c (Floor r))) (Lt (Sub (Floor r) r))) ``` chaieb@23264 ` 1609` ``` else Or (Le (CN 0 (-c) (Neg (Floor r)))) (And (Eq(CN 0 (-c) (Neg (Floor r)))) (Lt (Sub (Floor r) r))))" ``` chaieb@23264 ` 1610` ``` "zlfm (Eq a) = (let (c,r) = zsplit0 a in ``` chaieb@23264 ` 1611` ``` if c=0 then Eq r else ``` chaieb@23264 ` 1612` ``` if c>0 then (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Eq (Add (Floor (Neg r)) r))) ``` chaieb@23264 ` 1613` ``` else (And (Eq (CN 0 (-c) (Floor (Neg r)))) (Eq (Add (Floor (Neg r)) r))))" ``` chaieb@23264 ` 1614` ``` "zlfm (NEq a) = (let (c,r) = zsplit0 a in ``` chaieb@23264 ` 1615` ``` if c=0 then NEq r else ``` chaieb@23264 ` 1616` ``` if c>0 then (Or (NEq (CN 0 c (Neg (Floor (Neg r))))) (NEq (Add (Floor (Neg r)) r))) ``` chaieb@23264 ` 1617` ``` else (Or (NEq (CN 0 (-c) (Floor (Neg r)))) (NEq (Add (Floor (Neg r)) r))))" ``` chaieb@23264 ` 1618` ``` "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a) ``` chaieb@23264 ` 1619` ``` else (let (c,r) = zsplit0 a in ``` chaieb@23264 ` 1620` ``` if c=0 then Dvd (abs i) r else ``` chaieb@23264 ` 1621` ``` if c>0 then And (Eq (Sub (Floor r) r)) (Dvd (abs i) (CN 0 c (Floor r))) ``` chaieb@23264 ` 1622` ``` else And (Eq (Sub (Floor r) r)) (Dvd (abs i) (CN 0 (-c) (Neg (Floor r))))))" ``` chaieb@23264 ` 1623` ``` "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a) ``` chaieb@23264 ` 1624` ``` else (let (c,r) = zsplit0 a in ``` chaieb@23264 ` 1625` ``` if c=0 then NDvd (abs i) r else ``` chaieb@23264 ` 1626` ``` if c>0 then Or (NEq (Sub (Floor r) r)) (NDvd (abs i) (CN 0 c (Floor r))) ``` chaieb@23264 ` 1627` ``` else Or (NEq (Sub (Floor r) r)) (NDvd (abs i) (CN 0 (-c) (Neg (Floor r))))))" ``` chaieb@23264 ` 1628` ``` "zlfm (NOT (And p q)) = disj (zlfm (NOT p)) (zlfm (NOT q))" ``` chaieb@23264 ` 1629` ``` "zlfm (NOT (Or p q)) = conj (zlfm (NOT p)) (zlfm (NOT q))" ``` chaieb@23264 ` 1630` ``` "zlfm (NOT (Imp p q)) = conj (zlfm p) (zlfm (NOT q))" ``` chaieb@23264 ` 1631` ``` "zlfm (NOT (Iff p q)) = disj (conj(zlfm p) (zlfm(NOT q))) (conj (zlfm(NOT p)) (zlfm q))" ``` chaieb@23264 ` 1632` ``` "zlfm (NOT (NOT p)) = zlfm p" ``` chaieb@23264 ` 1633` ``` "zlfm (NOT T) = F" ``` chaieb@23264 ` 1634` ``` "zlfm (NOT F) = T" ``` chaieb@23264 ` 1635` ``` "zlfm (NOT (Lt a)) = zlfm (Ge a)" ``` chaieb@23264 ` 1636` ``` "zlfm (NOT (Le a)) = zlfm (Gt a)" ``` chaieb@23264 ` 1637` ``` "zlfm (NOT (Gt a)) = zlfm (Le a)" ``` chaieb@23264 ` 1638` ``` "zlfm (NOT (Ge a)) = zlfm (Lt a)" ``` chaieb@23264 ` 1639` ``` "zlfm (NOT (Eq a)) = zlfm (NEq a)" ``` chaieb@23264 ` 1640` ``` "zlfm (NOT (NEq a)) = zlfm (Eq a)" ``` chaieb@23264 ` 1641` ``` "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)" ``` chaieb@23264 ` 1642` ``` "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)" ``` chaieb@23264 ` 1643` ``` "zlfm p = p" (hints simp add: fmsize_pos) ``` chaieb@23264 ` 1644` chaieb@23264 ` 1645` ```lemma split_int_less_real: ``` chaieb@23264 ` 1646` ``` "(real (a::int) < b) = (a < floor b \ (a = floor b \ real (floor b) < b))" ``` chaieb@23264 ` 1647` ```proof( auto) ``` chaieb@23264 ` 1648` ``` assume alb: "real a < b" and agb: "\ a < floor b" ``` chaieb@23264 ` 1649` ``` from agb have "floor b \ a" by simp hence th: "b < real a + 1" by (simp only: floor_le_eq) ``` chaieb@23264 ` 1650` ``` from floor_eq[OF alb th] show "a= floor b" by simp ``` chaieb@23264 ` 1651` ```next ``` chaieb@23264 ` 1652` ``` assume alb: "a < floor b" ``` chaieb@23264 ` 1653` ``` hence "real a < real (floor b)" by simp ``` chaieb@23264 ` 1654` ``` moreover have "real (floor b) \ b" by simp ultimately show "real a < b" by arith ``` chaieb@23264 ` 1655` ```qed ``` chaieb@23264 ` 1656` chaieb@23264 ` 1657` ```lemma split_int_less_real': ``` chaieb@23264 ` 1658` ``` "(real (a::int) + b < 0) = (real a - real (floor(-b)) < 0 \ (real a - real (floor (-b)) = 0 \ real (floor (-b)) + b < 0))" ``` chaieb@23264 ` 1659` ```proof- ``` chaieb@23264 ` 1660` ``` have "(real a + b <0) = (real a < -b)" by arith ``` chaieb@23264 ` 1661` ``` with split_int_less_real[where a="a" and b="-b"] show ?thesis by arith ``` chaieb@23264 ` 1662` ```qed ``` chaieb@23264 ` 1663` chaieb@23264 ` 1664` ```lemma split_int_gt_real': ``` chaieb@23264 ` 1665` ``` "(real (a::int) + b > 0) = (real a + real (floor b) > 0 \ (real a + real (floor b) = 0 \ real (floor b) - b < 0))" ``` chaieb@23264 ` 1666` ```proof- ``` chaieb@23264 ` 1667` ``` have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith ``` nipkow@41849 ` 1668` ``` show ?thesis using myless[of _ "real (floor b)"] ``` chaieb@23264 ` 1669` ``` by (simp only:th split_int_less_real'[where a="-a" and b="-b"]) ``` wenzelm@51369 ` 1670` ``` (simp add: algebra_simps,arith) ``` chaieb@23264 ` 1671` ```qed ``` chaieb@23264 ` 1672` chaieb@23264 ` 1673` ```lemma split_int_le_real: ``` chaieb@23264 ` 1674` ``` "(real (a::int) \ b) = (a \ floor b \ (a = floor b \ real (floor b) < b))" ``` chaieb@23264 ` 1675` ```proof( auto) ``` chaieb@23264 ` 1676` ``` assume alb: "real a \ b" and agb: "\ a \ floor b" ``` huffman@30097 ` 1677` ``` from alb have "floor (real a) \ floor b " by (simp only: floor_mono) ``` chaieb@23264 ` 1678` ``` hence "a \ floor b" by simp with agb show "False" by simp ``` chaieb@23264 ` 1679` ```next ``` chaieb@23264 ` 1680` ``` assume alb: "a \ floor b" ``` huffman@30097 ` 1681` ``` hence "real a \ real (floor b)" by (simp only: floor_mono) ``` chaieb@23264 ` 1682` ``` also have "\\ b" by simp finally show "real a \ b" . ``` chaieb@23264 ` 1683` ```qed ``` chaieb@23264 ` 1684` chaieb@23264 ` 1685` ```lemma split_int_le_real': ``` chaieb@23264 ` 1686` ``` "(real (a::int) + b \ 0) = (real a - real (floor(-b)) \ 0 \ (real a - real (floor (-b)) = 0 \ real (floor (-b)) + b < 0))" ``` chaieb@23264 ` 1687` ```proof- ``` chaieb@23264 ` 1688` ``` have "(real a + b \0) = (real a \ -b)" by arith ``` chaieb@23264 ` 1689` ``` with split_int_le_real[where a="a" and b="-b"] show ?thesis by arith ``` chaieb@23264 ` 1690` ```qed ``` chaieb@23264 ` 1691` chaieb@23264 ` 1692` ```lemma split_int_ge_real': ``` chaieb@23264 ` 1693` ``` "(real (a::int) + b \ 0) = (real a + real (floor b) \ 0 \ (real a + real (floor b) = 0 \ real (floor b) - b < 0))" ``` chaieb@23264 ` 1694` ```proof- ``` chaieb@23264 ` 1695` ``` have th: "(real a + b \0) = (real (-a) + (-b) \ 0)" by arith ``` chaieb@23264 ` 1696` ``` show ?thesis by (simp only: th split_int_le_real'[where a="-a" and b="-b"]) ``` wenzelm@51369 ` 1697` ``` (simp add: algebra_simps ,arith) ``` chaieb@23264 ` 1698` ```qed ``` chaieb@23264 ` 1699` chaieb@23264 ` 1700` ```lemma split_int_eq_real: "(real (a::int) = b) = ( a = floor b \ b = real (floor b))" (is "?l = ?r") ``` chaieb@23264 ` 1701` ```by auto ``` chaieb@23264 ` 1702` chaieb@23264 ` 1703` ```lemma split_int_eq_real': "(real (a::int) + b = 0) = ( a - floor (-b) = 0 \ real (floor (-b)) + b = 0)" (is "?l = ?r") ``` chaieb@23264 ` 1704` ```proof- ``` chaieb@23264 ` 1705` ``` have "?l = (real a = -b)" by arith ``` chaieb@23264 ` 1706` ``` with split_int_eq_real[where a="a" and b="-b"] show ?thesis by simp arith ``` chaieb@23264 ` 1707` ```qed ``` chaieb@23264 ` 1708` chaieb@23264 ` 1709` ```lemma zlfm_I: ``` chaieb@23264 ` 1710` ``` assumes qfp: "qfree p" ``` chaieb@23264 ` 1711` ``` shows "(Ifm (real i #bs) (zlfm p) = Ifm (real i# bs) p) \ iszlfm (zlfm p) (real (i::int) #bs)" ``` chaieb@23264 ` 1712` ``` (is "(?I (?l p) = ?I p) \ ?L (?l p)") ``` chaieb@23264 ` 1713` ```using qfp ``` chaieb@23264 ` 1714` ```proof(induct p rule: zlfm.induct) ``` chaieb@23264 ` 1715` ``` case (5 a) ``` chaieb@23264 ` 1716` ``` let ?c = "fst (zsplit0 a)" ``` chaieb@23264 ` 1717` ``` let ?r = "snd (zsplit0 a)" ``` chaieb@23264 ` 1718` ``` have spl: "zsplit0 a = (?c,?r)" by simp ``` chaieb@23264 ` 1719` ``` from zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1720` ``` have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto ``` chaieb@23264 ` 1721` ``` let ?N = "\ t. Inum (real i#bs) t" ``` chaieb@23264 ` 1722` ``` have "?c = 0 \ (?c >0 \ ?c\0) \ (?c<0 \ ?c\0)" by arith ``` chaieb@23264 ` 1723` ``` moreover ``` chaieb@23264 ` 1724` ``` {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1725` ``` by (cases "?r", simp_all add: Let_def split_def,case_tac "nat", simp_all)} ``` chaieb@23264 ` 1726` ``` moreover ``` chaieb@23264 ` 1727` ``` {assume cp: "?c > 0" and cnz: "?c\0" hence l: "?L (?l (Lt a))" ``` chaieb@23264 ` 1728` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1729` ``` have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def) ``` haftmann@37887 ` 1730` ``` also have "\ = (?I (?l (Lt a)))" apply (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) by (simp add: Ia cp cnz Let_def split_def diff_minus) ``` chaieb@23264 ` 1731` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1732` ``` moreover ``` chaieb@23264 ` 1733` ``` {assume cn: "?c < 0" and cnz: "?c\0" hence l: "?L (?l (Lt a))" ``` chaieb@23264 ` 1734` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1735` ``` have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def) ``` wenzelm@51369 ` 1736` ``` also from cn cnz have "\ = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith) ``` chaieb@23264 ` 1737` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1738` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1739` ```next ``` chaieb@23264 ` 1740` ``` case (6 a) ``` chaieb@23264 ` 1741` ``` let ?c = "fst (zsplit0 a)" ``` chaieb@23264 ` 1742` ``` let ?r = "snd (zsplit0 a)" ``` chaieb@23264 ` 1743` ``` have spl: "zsplit0 a = (?c,?r)" by simp ``` chaieb@23264 ` 1744` ``` from zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1745` ``` have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto ``` chaieb@23264 ` 1746` ``` let ?N = "\ t. Inum (real i#bs) t" ``` chaieb@23264 ` 1747` ``` have "?c = 0 \ (?c >0 \ ?c\0) \ (?c<0 \ ?c\0)" by arith ``` chaieb@23264 ` 1748` ``` moreover ``` chaieb@23264 ` 1749` ``` {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1750` ``` by (cases "?r", simp_all add: Let_def split_def, case_tac "nat",simp_all)} ``` chaieb@23264 ` 1751` ``` moreover ``` chaieb@23264 ` 1752` ``` {assume cp: "?c > 0" and cnz: "?c\0" hence l: "?L (?l (Le a))" ``` chaieb@23264 ` 1753` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1754` ``` have "?I (Le a) = (real (?c * i) + (?N ?r) \ 0)" using Ia by (simp add: Let_def split_def) ``` haftmann@37887 ` 1755` ``` also have "\ = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus) ``` chaieb@23264 ` 1756` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1757` ``` moreover ``` chaieb@23264 ` 1758` ``` {assume cn: "?c < 0" and cnz: "?c\0" hence l: "?L (?l (Le a))" ``` chaieb@23264 ` 1759` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1760` ``` have "?I (Le a) = (real (?c * i) + (?N ?r) \ 0)" using Ia by (simp add: Let_def split_def) ``` haftmann@37887 ` 1761` ``` also from cn cnz have "\ = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac ,arith) ``` chaieb@23264 ` 1762` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1763` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1764` ```next ``` chaieb@23264 ` 1765` ``` case (7 a) ``` chaieb@23264 ` 1766` ``` let ?c = "fst (zsplit0 a)" ``` chaieb@23264 ` 1767` ``` let ?r = "snd (zsplit0 a)" ``` chaieb@23264 ` 1768` ``` have spl: "zsplit0 a = (?c,?r)" by simp ``` chaieb@23264 ` 1769` ``` from zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1770` ``` have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto ``` chaieb@23264 ` 1771` ``` let ?N = "\ t. Inum (real i#bs) t" ``` chaieb@23264 ` 1772` ``` have "?c = 0 \ (?c >0 \ ?c\0) \ (?c<0 \ ?c\0)" by arith ``` chaieb@23264 ` 1773` ``` moreover ``` chaieb@23264 ` 1774` ``` {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1775` ``` by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)} ``` chaieb@23264 ` 1776` ``` moreover ``` chaieb@23264 ` 1777` ``` {assume cp: "?c > 0" and cnz: "?c\0" hence l: "?L (?l (Gt a))" ``` chaieb@23264 ` 1778` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1779` ``` have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def) ``` haftmann@37887 ` 1780` ``` also have "\ = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus) ``` chaieb@23264 ` 1781` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1782` ``` moreover ``` chaieb@23264 ` 1783` ``` {assume cn: "?c < 0" and cnz: "?c\0" hence l: "?L (?l (Gt a))" ``` chaieb@23264 ` 1784` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1785` ``` have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def) ``` haftmann@37887 ` 1786` ``` also from cn cnz have "\ = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac, arith) ``` chaieb@23264 ` 1787` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1788` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1789` ```next ``` chaieb@23264 ` 1790` ``` case (8 a) ``` chaieb@23264 ` 1791` ``` let ?c = "fst (zsplit0 a)" ``` chaieb@23264 ` 1792` ``` let ?r = "snd (zsplit0 a)" ``` chaieb@23264 ` 1793` ``` have spl: "zsplit0 a = (?c,?r)" by simp ``` chaieb@23264 ` 1794` ``` from zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1795` ``` have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto ``` chaieb@23264 ` 1796` ``` let ?N = "\ t. Inum (real i#bs) t" ``` chaieb@23264 ` 1797` ``` have "?c = 0 \ (?c >0 \ ?c\0) \ (?c<0 \ ?c\0)" by arith ``` chaieb@23264 ` 1798` ``` moreover ``` chaieb@23264 ` 1799` ``` {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1800` ``` by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)} ``` chaieb@23264 ` 1801` ``` moreover ``` chaieb@23264 ` 1802` ``` {assume cp: "?c > 0" and cnz: "?c\0" hence l: "?L (?l (Ge a))" ``` chaieb@23264 ` 1803` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1804` ``` have "?I (Ge a) = (real (?c * i) + (?N ?r) \ 0)" using Ia by (simp add: Let_def split_def) ``` haftmann@37887 ` 1805` ``` also have "\ = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus) ``` chaieb@23264 ` 1806` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1807` ``` moreover ``` chaieb@23264 ` 1808` ``` {assume cn: "?c < 0" and cnz: "?c\0" hence l: "?L (?l (Ge a))" ``` chaieb@23264 ` 1809` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1810` ``` have "?I (Ge a) = (real (?c * i) + (?N ?r) \ 0)" using Ia by (simp add: Let_def split_def) ``` haftmann@37887 ` 1811` ``` also from cn cnz have "\ = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac, arith) ``` chaieb@23264 ` 1812` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1813` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1814` ```next ``` chaieb@23264 ` 1815` ``` case (9 a) ``` chaieb@23264 ` 1816` ``` let ?c = "fst (zsplit0 a)" ``` chaieb@23264 ` 1817` ``` let ?r = "snd (zsplit0 a)" ``` chaieb@23264 ` 1818` ``` have spl: "zsplit0 a = (?c,?r)" by simp ``` chaieb@23264 ` 1819` ``` from zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1820` ``` have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto ``` chaieb@23264 ` 1821` ``` let ?N = "\ t. Inum (real i#bs) t" ``` chaieb@23264 ` 1822` ``` have "?c = 0 \ (?c >0 \ ?c\0) \ (?c<0 \ ?c\0)" by arith ``` chaieb@23264 ` 1823` ``` moreover ``` chaieb@23264 ` 1824` ``` {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1825` ``` by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)} ``` chaieb@23264 ` 1826` ``` moreover ``` chaieb@23264 ` 1827` ``` {assume cp: "?c > 0" and cnz: "?c\0" hence l: "?L (?l (Eq a))" ``` chaieb@23264 ` 1828` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1829` ``` have "?I (Eq a) = (real (?c * i) + (?N ?r) = 0)" using Ia by (simp add: Let_def split_def) ``` chaieb@23264 ` 1830` ``` also have "\ = (?I (?l (Eq a)))" using cp cnz by (simp only: split_int_eq_real'[where a="?c*i" and b="?N ?r"]) (simp add: Let_def split_def Ia real_of_int_mult[symmetric] del: real_of_int_mult) ``` chaieb@23264 ` 1831` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1832` ``` moreover ``` chaieb@23264 ` 1833` ``` {assume cn: "?c < 0" and cnz: "?c\0" hence l: "?L (?l (Eq a))" ``` chaieb@23264 ` 1834` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1835` ``` have "?I (Eq a) = (real (?c * i) + (?N ?r) = 0)" using Ia by (simp add: Let_def split_def) ``` chaieb@23264 ` 1836` ``` also from cn cnz have "\ = (?I (?l (Eq a)))" by (simp only: split_int_eq_real'[where a="?c*i" and b="?N ?r"]) (simp add: Let_def split_def Ia real_of_int_mult[symmetric] del: real_of_int_mult,arith) ``` chaieb@23264 ` 1837` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1838` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1839` ```next ``` chaieb@23264 ` 1840` ``` case (10 a) ``` chaieb@23264 ` 1841` ``` let ?c = "fst (zsplit0 a)" ``` chaieb@23264 ` 1842` ``` let ?r = "snd (zsplit0 a)" ``` chaieb@23264 ` 1843` ``` have spl: "zsplit0 a = (?c,?r)" by simp ``` chaieb@23264 ` 1844` ``` from zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1845` ``` have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto ``` chaieb@23264 ` 1846` ``` let ?N = "\ t. Inum (real i#bs) t" ``` chaieb@23264 ` 1847` ``` have "?c = 0 \ (?c >0 \ ?c\0) \ (?c<0 \ ?c\0)" by arith ``` chaieb@23264 ` 1848` ``` moreover ``` chaieb@23264 ` 1849` ``` {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1850` ``` by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)} ``` chaieb@23264 ` 1851` ``` moreover ``` chaieb@23264 ` 1852` ``` {assume cp: "?c > 0" and cnz: "?c\0" hence l: "?L (?l (NEq a))" ``` chaieb@23264 ` 1853` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1854` ``` have "?I (NEq a) = (real (?c * i) + (?N ?r) \ 0)" using Ia by (simp add: Let_def split_def) ``` chaieb@23264 ` 1855` ``` also have "\ = (?I (?l (NEq a)))" using cp cnz by (simp only: split_int_eq_real'[where a="?c*i" and b="?N ?r"]) (simp add: Let_def split_def Ia real_of_int_mult[symmetric] del: real_of_int_mult) ``` chaieb@23264 ` 1856` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1857` ``` moreover ``` chaieb@23264 ` 1858` ``` {assume cn: "?c < 0" and cnz: "?c\0" hence l: "?L (?l (NEq a))" ``` chaieb@23264 ` 1859` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1860` ``` have "?I (NEq a) = (real (?c * i) + (?N ?r) \ 0)" using Ia by (simp add: Let_def split_def) ``` chaieb@23264 ` 1861` ``` also from cn cnz have "\ = (?I (?l (NEq a)))" by (simp only: split_int_eq_real'[where a="?c*i" and b="?N ?r"]) (simp add: Let_def split_def Ia real_of_int_mult[symmetric] del: real_of_int_mult,arith) ``` chaieb@23264 ` 1862` ``` finally have ?case using l by simp} ``` chaieb@23264 ` 1863` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1864` ```next ``` chaieb@23264 ` 1865` ``` case (11 j a) ``` chaieb@23264 ` 1866` ``` let ?c = "fst (zsplit0 a)" ``` chaieb@23264 ` 1867` ``` let ?r = "snd (zsplit0 a)" ``` chaieb@23264 ` 1868` ``` have spl: "zsplit0 a = (?c,?r)" by simp ``` chaieb@23264 ` 1869` ``` from zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1870` ``` have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto ``` chaieb@23264 ` 1871` ``` let ?N = "\ t. Inum (real i#bs) t" ``` chaieb@23264 ` 1872` ``` have "j=0 \ (j\0 \ ?c = 0) \ (j\0 \ ?c >0 \ ?c\0) \ (j\ 0 \ ?c<0 \ ?c\0)" by arith ``` chaieb@23264 ` 1873` ``` moreover ``` wenzelm@41891 ` 1874` ``` { assume j: "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) ``` wenzelm@41891 ` 1875` ``` hence ?case using 11 j by (simp del: zlfm.simps add: rdvd_left_0_eq)} ``` chaieb@23264 ` 1876` ``` moreover ``` chaieb@23264 ` 1877` ``` {assume "?c=0" and "j\0" hence ?case ``` chaieb@23264 ` 1878` ``` using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"] ``` chaieb@23264 ` 1879` ``` by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)} ``` chaieb@23264 ` 1880` ``` moreover ``` chaieb@23264 ` 1881` ``` {assume cp: "?c > 0" and cnz: "?c\0" and jnz: "j\0" hence l: "?L (?l (Dvd j a))" ``` chaieb@23264 ` 1882` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1883` ``` have "?I (Dvd j a) = (real j rdvd (real (?c * i) + (?N ?r)))" ``` chaieb@23264 ` 1884` ``` using Ia by (simp add: Let_def split_def) ``` chaieb@23264 ` 1885` ``` also have "\ = (real (abs j) rdvd real (?c*i) + (?N ?r))" ``` chaieb@23264 ` 1886` ``` by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp ``` chaieb@23264 ` 1887` ``` also have "\ = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \ ``` chaieb@23264 ` 1888` ``` (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r))))" ``` chaieb@23264 ` 1889` ``` by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac) ``` chaieb@23264 ` 1890` ``` also have "\ = (?I (?l (Dvd j a)))" using cp cnz jnz ``` chaieb@23264 ` 1891` ``` by (simp add: Let_def split_def int_rdvd_iff[symmetric] ``` wenzelm@32960 ` 1892` ``` del: real_of_int_mult) (auto simp add: add_ac) ``` chaieb@23264 ` 1893` ``` finally have ?case using l jnz by simp } ``` chaieb@23264 ` 1894` ``` moreover ``` chaieb@23264 ` 1895` ``` {assume cn: "?c < 0" and cnz: "?c\0" and jnz: "j\0" hence l: "?L (?l (Dvd j a))" ``` chaieb@23264 ` 1896` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1897` ``` have "?I (Dvd j a) = (real j rdvd (real (?c * i) + (?N ?r)))" ``` chaieb@23264 ` 1898` ``` using Ia by (simp add: Let_def split_def) ``` chaieb@23264 ` 1899` ``` also have "\ = (real (abs j) rdvd real (?c*i) + (?N ?r))" ``` chaieb@23264 ` 1900` ``` by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp ``` chaieb@23264 ` 1901` ``` also have "\ = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \ ``` chaieb@23264 ` 1902` ``` (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r))))" ``` chaieb@23264 ` 1903` ``` by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac) ``` chaieb@23264 ` 1904` ``` also have "\ = (?I (?l (Dvd j a)))" using cn cnz jnz ``` chaieb@23264 ` 1905` ``` using rdvd_minus [where d="abs j" and t="real (?c*i + floor (?N ?r))", simplified, symmetric] ``` chaieb@23264 ` 1906` ``` by (simp add: Let_def split_def int_rdvd_iff[symmetric] ``` wenzelm@32960 ` 1907` ``` del: real_of_int_mult) (auto simp add: add_ac) ``` chaieb@23264 ` 1908` ``` finally have ?case using l jnz by blast } ``` chaieb@23264 ` 1909` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1910` ```next ``` chaieb@23264 ` 1911` ``` case (12 j a) ``` chaieb@23264 ` 1912` ``` let ?c = "fst (zsplit0 a)" ``` chaieb@23264 ` 1913` ``` let ?r = "snd (zsplit0 a)" ``` chaieb@23264 ` 1914` ``` have spl: "zsplit0 a = (?c,?r)" by simp ``` chaieb@23264 ` 1915` ``` from zsplit0_I[OF spl, where x="i" and bs="bs"] ``` chaieb@23264 ` 1916` ``` have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto ``` chaieb@23264 ` 1917` ``` let ?N = "\ t. Inum (real i#bs) t" ``` chaieb@23264 ` 1918` ``` have "j=0 \ (j\0 \ ?c = 0) \ (j\0 \ ?c >0 \ ?c\0) \ (j\ 0 \ ?c<0 \ ?c\0)" by arith ``` chaieb@23264 ` 1919` ``` moreover ``` wenzelm@41891 ` 1920` ``` {assume j: "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) ``` wenzelm@41891 ` 1921` ``` hence ?case using 12 j by (simp del: zlfm.simps add: rdvd_left_0_eq)} ``` chaieb@23264 ` 1922` ``` moreover ``` chaieb@23264 ` 1923` ``` {assume "?c=0" and "j\0" hence ?case ``` chaieb@23264 ` 1924` ``` using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"] ``` chaieb@23264 ` 1925` ``` by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)} ``` chaieb@23264 ` 1926` ``` moreover ``` chaieb@23264 ` 1927` ``` {assume cp: "?c > 0" and cnz: "?c\0" and jnz: "j\0" hence l: "?L (?l (NDvd j a))" ``` chaieb@23264 ` 1928` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1929` ``` have "?I (NDvd j a) = (\ (real j rdvd (real (?c * i) + (?N ?r))))" ``` chaieb@23264 ` 1930` ``` using Ia by (simp add: Let_def split_def) ``` chaieb@23264 ` 1931` ``` also have "\ = (\ (real (abs j) rdvd real (?c*i) + (?N ?r)))" ``` chaieb@23264 ` 1932` ``` by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp ``` chaieb@23264 ` 1933` ``` also have "\ = (\ ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \ ``` chaieb@23264 ` 1934` ``` (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r)))))" ``` chaieb@23264 ` 1935` ``` by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac) ``` chaieb@23264 ` 1936` ``` also have "\ = (?I (?l (NDvd j a)))" using cp cnz jnz ``` chaieb@23264 ` 1937` ``` by (simp add: Let_def split_def int_rdvd_iff[symmetric] ``` wenzelm@32960 ` 1938` ``` del: real_of_int_mult) (auto simp add: add_ac) ``` chaieb@23264 ` 1939` ``` finally have ?case using l jnz by simp } ``` chaieb@23264 ` 1940` ``` moreover ``` chaieb@23264 ` 1941` ``` {assume cn: "?c < 0" and cnz: "?c\0" and jnz: "j\0" hence l: "?L (?l (NDvd j a))" ``` chaieb@23264 ` 1942` ``` by (simp add: nb Let_def split_def isint_Floor isint_neg) ``` chaieb@23264 ` 1943` ``` have "?I (NDvd j a) = (\ (real j rdvd (real (?c * i) + (?N ?r))))" ``` chaieb@23264 ` 1944` ``` using Ia by (simp add: Let_def split_def) ``` chaieb@23264 ` 1945` ``` also have "\ = (\ (real (abs j) rdvd real (?c*i) + (?N ?r)))" ``` chaieb@23264 ` 1946` ``` by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp ``` chaieb@23264 ` 1947` ``` also have "\ = (\ ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \ ``` chaieb@23264 ` 1948` ``` (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r)))))" ``` chaieb@23264 ` 1949` ``` by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac) ``` chaieb@23264 ` 1950` ``` also have "\ = (?I (?l (NDvd j a)))" using cn cnz jnz ``` chaieb@23264 ` 1951` ``` using rdvd_minus [where d="abs j" and t="real (?c*i + floor (?N ?r))", simplified, symmetric] ``` chaieb@23264 ` 1952` ``` by (simp add: Let_def split_def int_rdvd_iff[symmetric] ``` wenzelm@32960 ` 1953` ``` del: real_of_int_mult) (auto simp add: add_ac) ``` chaieb@23264 ` 1954` ``` finally have ?case using l jnz by blast } ``` chaieb@23264 ` 1955` ``` ultimately show ?case by blast ``` chaieb@23264 ` 1956` ```qed auto ``` chaieb@23264 ` 1957` chaieb@23316 ` 1958` ```text{* plusinf : Virtual substitution of @{text "+\"} ``` chaieb@23316 ` 1959` ``` minusinf: Virtual substitution of @{text "-\"} ``` chaieb@23316 ` 1960` ``` @{text "\"} Compute lcm @{text "d| Dvd d c*x+t \ p"} ``` wenzelm@50252 ` 1961` ``` @{text "d_\"} checks if a given l divides all the ds above*} ``` chaieb@23316 ` 1962` krauss@41839 ` 1963` ```fun minusinf:: "fm \ fm" where ``` chaieb@23264 ` 1964` ``` "minusinf (And p q) = conj (minusinf p) (minusinf q)" ``` krauss@41839 ` 1965` ```| "minusinf (Or p q) = disj (minusinf p) (minusinf q)" ``` krauss@41839 ` 1966` ```| "minusinf (Eq (CN 0 c e)) = F" ``` krauss@41839 ` 1967` ```| "minusinf (NEq (CN 0 c e)) = T" ``` krauss@41839 ` 1968` ```| "minusinf (Lt (CN 0 c e)) = T" ``` krauss@41839 ` 1969` ```| "minusinf (Le (CN 0 c e)) = T" ``` krauss@41839 ` 1970` ```| "minusinf (Gt (CN 0 c e)) = F" ``` krauss@41839 ` 1971` ```| "minusinf (Ge (CN 0 c e)) = F" ``` krauss@41839 ` 1972` ```| "minusinf p = p" ``` chaieb@23264 ` 1973` chaieb@23264 ` 1974` ```lemma minusinf_qfree: "qfree p \ qfree (minusinf p)" ``` chaieb@23264 ` 1975` ``` by (induct p rule: minusinf.induct, auto) ``` chaieb@23264 ` 1976` krauss@41839 ` 1977` ```fun plusinf:: "fm \ fm" where ``` chaieb@23264 ` 1978` ``` "plusinf (And p q) = conj (plusinf p) (plusinf q)" ``` krauss@41839 ` 1979` ```| "plusinf (Or p q) = disj (plusinf p) (plusinf q)" ``` krauss@41839 ` 1980` ```| "plusinf (Eq (CN 0 c e)) = F" ``` krauss@41839 ` 1981` ```| "plusinf (NEq (CN 0 c e)) = T" ``` krauss@41839 ` 1982` ```| "plusinf (Lt (CN 0 c e)) = F" ``` krauss@41839 ` 1983` ```| "plusinf (Le (CN 0 c e)) = F" ``` krauss@41839 ` 1984` ```| "plusinf (Gt (CN 0 c e)) = T" ``` krauss@41839 ` 1985` ```| "plusinf (Ge (CN 0 c e)) = T" ``` krauss@41839 ` 1986` ```| "plusinf p = p" ``` krauss@41839 ` 1987` krauss@41839 ` 1988` ```fun \ :: "fm \ int" where ``` huffman@31706 ` 1989` ``` "\ (And p q) = lcm (\ p) (\ q)" ``` krauss@41839 ` 1990` ```| "\ (Or p q) = lcm (\ p) (\ q)" ``` krauss@41839 ` 1991` ```| "\ (Dvd i (CN 0 c e)) = i" ``` krauss@41839 ` 1992` ```| "\ (NDvd i (CN 0 c e)) = i" ``` krauss@41839 ` 1993` ```| "\ p = 1" ``` krauss@41839 ` 1994` wenzelm@50252 ` 1995` ```fun d_\ :: "fm \ int \ bool" where ``` wenzelm@50252 ` 1996` ``` "d_\ (And p q) = (\ d. d_\ p d \ d_\ q d)" ``` wenzelm@50252 ` 1997` ```| "d_\ (Or p q) = (\ d. d_\ p d \ d_\ q d)" ``` wenzelm@50252 ` 1998` ```| "d_\ (Dvd i (CN 0 c e)) = (\ d. i dvd d)" ``` wenzelm@50252 ` 1999` ```| "d_\ (NDvd i (CN 0 c e)) = (\ d. i dvd d)" ``` wenzelm@50252 ` 2000` ```| "d_\ p = (\ d. True)" ``` chaieb@23264 ` 2001` chaieb@23264 ` 2002` ```lemma delta_mono: ``` chaieb@23264 ` 2003` ``` assumes lin: "iszlfm p bs" ``` chaieb@23264 ` 2004` ``` and d: "d dvd d'" ``` wenzelm@50252 ` 2005` ``` and ad: "d_\ p d" ``` wenzelm@50252 ` 2006` ``` shows "d_\ p d'" ``` chaieb@23264 ` 2007` ``` using lin ad d ``` chaieb@23264 ` 2008` ```proof(induct p rule: iszlfm.induct) ``` chaieb@23264 ` 2009` ``` case (9 i c e) thus ?case using d ``` nipkow@30042 ` 2010` ``` by (simp add: dvd_trans[of "i" "d" "d'"]) ``` chaieb@23264 ` 2011` ```next ``` chaieb@23264 ` 2012` ``` case (10 i c e) thus ?case using d ``` nipkow@30042 ` 2013` ``` by (simp add: dvd_trans[of "i" "d" "d'"]) ``` chaieb@23264 ` 2014` ```qed simp_all ``` chaieb@23264 ` 2015` chaieb@23264 ` 2016` ```lemma \ : assumes lin:"iszlfm p bs" ``` wenzelm@50252 ` 2017` ``` shows "d_\ p (\ p) \ \ p >0" ``` chaieb@23264 ` 2018` ```using lin ``` chaieb@23264 ` 2019` ```proof (induct p rule: iszlfm.induct) ``` chaieb@23264 ` 2020` ``` case (1 p q) ``` chaieb@23264 ` 2021` ``` let ?d = "\ (And p q)" ``` wenzelm@41891 ` 2022` ``` from 1 lcm_pos_int have dp: "?d >0" by simp ``` wenzelm@41891 ` 2023` ``` have d1: "\ p dvd \ (And p q)" using 1 by simp ``` wenzelm@50252 ` 2024` ``` hence th: "d_\ p ?d" ``` wenzelm@41891 ` 2025` ``` using delta_mono 1 by (simp only: iszlfm.simps) blast ``` wenzelm@41891 ` 2026` ``` have "\ q dvd \ (And p q)" using 1 by simp ``` wenzelm@50252 ` 2027` ``` hence th': "d_\ q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast ``` chaieb@23997 ` 2028` ``` from th th' dp show ?case by simp ``` chaieb@23264 ` 2029` ```next ``` chaieb@23264 ` 2030` ``` case (2 p q) ``` chaieb@23264 ` 2031` ``` let ?d = "\ (And p q)" ``` wenzelm@41891 ` 2032` ``` from 2 lcm_pos_int have dp: "?d >0" by simp ``` wenzelm@41891 ` 2033` ``` have "\ p dvd \ (And p q)" using 2 by simp ``` wenzelm@50252 ` 2034` ``` hence th: "d_\ p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast ``` wenzelm@41891 ` 2035` ``` have "\ q dvd \ (And p q)" using 2 by simp ``` wenzelm@50252 ` 2036` ``` hence th': "d_\ q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast ``` nipkow@31730 ` 2037` ``` from th th' dp show ?case by simp ``` chaieb@23264 ` 2038` ```qed simp_all ``` chaieb@23264 ` 2039` chaieb@23264 ` 2040` chaieb@23264 ` 2041` ```lemma minusinf_inf: ``` chaieb@23264 ` 2042` ``` assumes linp: "iszlfm p (a # bs)" ``` chaieb@23264 ` 2043` ``` shows "\ (z::int). \ x < z. Ifm ((real x)#bs) (minusinf p) = Ifm ((real x)#bs) p" ``` chaieb@23264 ` 2044` ``` (is "?P p" is "\ (z::int). \ x < z. ?I x (?M p) = ?I x p") ``` chaieb@23264 ` 2045` ```using linp ``` chaieb@23264 ` 2046` ```proof (induct p rule: minusinf.induct) ``` chaieb@23264 ` 2047` ``` case (1 f g) ``` wenzelm@41891 ` 2048` ``` then have "?P f" by simp ``` chaieb@23264 ` 2049` ``` then obtain z1 where z1_def: "\ x < z1. ?I x (?M f) = ?I x f" by blast ``` wenzelm@41891 ` 2050` ``` with 1 have "?P g" by simp ``` chaieb@23264 ` 2051` ``` then obtain z2 where z2_def: "\ x < z2. ?I x (?M g) = ?I x g" by blast ``` chaieb@23264 ` 2052` ``` let ?z = "min z1 z2" ``` chaieb@23264 ` 2053` ``` from z1_def z2_def have "\ x < ?z. ?I x (?M (And f g)) = ?I x (And f g)" by simp ``` chaieb@23264 ` 2054` ``` thus ?case by blast ``` chaieb@23264 ` 2055` ```next ``` wenzelm@41891 ` 2056` ``` case (2 f g) ``` wenzelm@41891 ` 2057` ``` then have "?P f" by simp ``` chaieb@23264 ` 2058` ``` then obtain z1 where z1_def: "\ x < z1. ?I x (?M f) = ?I x f" by blast ``` wenzelm@41891 ` 2059` ``` with 2 have "?P g" by simp ``` chaieb@23264 ` 2060` ``` then obtain z2 where z2_def: "\ x < z2. ?I x (?M g) = ?I x g" by blast ``` chaieb@23264 ` 2061` ``` let ?z = "min z1 z2" ``` chaieb@23264 ` 2062` ``` from z1_def z2_def have "\ x < ?z. ?I x (?M (Or f g)) = ?I x (Or f g)" by simp ``` chaieb@23264 ` 2063` ``` thus ?case by blast ``` chaieb@23264 ` 2064` ```next ``` chaieb@23264 ` 2065` ``` case (3 c e) ``` wenzelm@41891 ` 2066` ``` then have "c > 0" by simp ``` wenzelm@41891 ` 2067` ``` hence rcpos: "real c > 0" by simp ``` wenzelm@41891 ` 2068` ``` from 3 have nbe: "numbound0 e" by simp ``` wenzelm@26932 ` 2069` ``` fix y ``` chaieb@23264 ` 2070` ``` have "\ x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Eq (CN 0 c e))) = ?I x (Eq (CN 0 c e))" ``` chaieb@23264 ` 2071` ``` proof (simp add: less_floor_eq , rule allI, rule impI) ``` wenzelm@51369 ` 2072` ``` fix x :: int ``` wenzelm@51369 ` 2073` ``` assume A: "real x + 1 \ - (Inum (y # bs) e / real c)" ``` chaieb@23264 ` 2074` ``` hence th1:"real x < - (Inum (y # bs) e / real c)" by simp ``` chaieb@23264 ` 2075` ``` with rcpos have "(real c)*(real x) < (real c)*(- (Inum (y # bs) e / real c))" ``` huffman@36778 ` 2076` ``` by (simp only: mult_strict_left_mono [OF th1 rcpos]) ``` chaieb@23264 ` 2077` ``` hence "real c * real x + Inum (y # bs) e \ 0"using rcpos by simp ``` chaieb@23264 ` 2078` ``` thus "real c * real x + Inum (real x # bs) e \ 0" ``` chaieb@23264 ` 2079` ``` using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] by simp ``` chaieb@23264 ` 2080` ``` qed ``` chaieb@23264 ` 2081` ``` thus ?case by blast ``` chaieb@23264 ` 2082` ```next ``` chaieb@23264 ` 2083` ``` case (4 c e) ``` wenzelm@41891 ` 2084` ``` then have "c > 0" by simp hence rcpos: "real c > 0" by simp ``` wenzelm@41891 ` 2085` ``` from 4 have nbe: "numbound0 e" by simp ``` wenzelm@26932 ` 2086` ``` fix y ``` chaieb@23264 ` 2087` ``` have "\ x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (NEq (CN 0 c e))) = ?I x (NEq (CN 0 c e))" ``` chaieb@23264 ` 2088` ``` proof (simp add: less_floor_eq , rule allI, rule impI) ``` wenzelm@51369 ` 2089` ``` fix x :: int ``` wenzelm@51369 ` 2090` ``` assume A: "real x + 1 \ - (Inum (y # bs) e / real c)" ``` chaieb@23264 ` 2091` ``` hence th1:"real x < - (Inum (y # bs) e / real c)" by simp ``` chaieb@23264 ` 2092` ``` with rcpos have "(real c)*(real x) < (real c)*(- (Inum (y # bs) e / real c))" ``` huffman@36778 ` 2093` ``` by (simp only: mult_strict_left_mono [OF th1 rcpos]) ``` chaieb@23264 ` 2094` ``` hence "real c * real x + Inum (y # bs) e \ 0"using rcpos by simp ``` chaieb@23264 ` 2095` ``` thus "real c * real x + Inum (real x # bs) e \ 0" ``` chaieb@23264 ` 2096` ``` using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] by simp ``` chaieb@23264 ` 2097` ``` qed ``` chaieb@23264 ` 2098` ``` thus ?case by blast ``` chaieb@23264 ` 2099` ```next ``` chaieb@23264 ` 2100` ``` case (5 c e) ``` wenzelm@41891 ` 2101` ``` then have "c > 0" by simp hence rcpos: "real c > 0" by simp ``` wenzelm@41891 ` 2102` ``` from 5 have nbe: "numbound0 e" by simp ``` wenzelm@26932 ` 2103` ``` fix y ``` chaieb@23264 ` 2104` ``` have "\ x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Lt (CN 0 c e))) = ?I x (Lt (CN 0 c e))" ``` chaieb@23264 ` 2105` ``` proof (simp add: less_floor_eq , rule allI, rule impI) ``` wenzelm@51369 ` 2106` ``` fix x :: int ``` wenzelm@51369 ` 2107` ``` assume A: "real x + 1 \ - (Inum (y # bs) e / real c)" ``` chaieb@23264 ` 2108` ``` hence th1:"real x < - (Inum (y # bs) e / real c)" by simp ``` chaieb@23264 ` 2109` ``` with rcpos have "(real c)*(real x) < (real c)*(- (Inum (y # bs) e / real c))" ``` huffman@36778 ` 2110` ``` by (simp only: mult_strict_left_mono [OF th1 rcpos]) ``` chaieb@23264 ` 2111` ``` thus "real c * real x + Inum (real x # bs) e < 0" ``` chaieb@23264 ` 2112` ``` using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp ``` chaieb@23264 ` 2113` ``` qed ``` chaieb@23264 ` 2114` ``` thus ?case by blast ``` chaieb@23264 ` 2115` ```next ``` chaieb@23264 ` 2116` ``` case (6 c e) ``` wenzelm@41891 ` 2117` ``` then have "c > 0" by simp hence rcpos: "real c > 0" by simp ``` wenzelm@41891 ` 2118` ``` from 6 have nbe: "numbound0 e" by simp ``` wenzelm@26932 ` 2119` ``` fix y ``` chaieb@23264 ` 2120` ``` have "\ x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Le (CN 0 c e))) = ?I x (Le (CN 0 c e))" ``` chaieb@23264 ` 2121` ``` proof (simp add: less_floor_eq , rule allI, rule impI) ``` wenzelm@51369 ` 2122` ``` fix x :: int ``` wenzelm@51369 ` 2123` ``` assume A: "real x + 1 \ - (Inum (y # bs) e / real c)" ``` chaieb@23264 ` 2124` ``` hence th1:"real x < - (Inum (y # bs) e / real c)" by simp ``` chaieb@23264 ` 2125` ``` with rcpos have "(real c)*(real x) < (real c)*(- (Inum (y # bs) e / real c))" ``` huffman@36778 ` 2126` ``` by (simp only: mult_strict_left_mono [OF th1 rcpos]) ``` chaieb@23264 ` 2127` ``` thus "real c * real x + Inum (real x # bs) e \ 0" ``` chaieb@23264 ` 2128` ``` using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp ``` chaieb@23264 ` 2129` ``` qed ``` chaieb@23264 ` 2130` ``` thus ?case by blast ``` chaieb@23264 ` 2131` ```next ``` chaieb@23264 ` 2132` ``` case (7 c e) ``` wenzelm@41891 ` 2133` ``` then have "c > 0" by simp hence rcpos: "real c > 0" by simp ``` wenzelm@41891 ` 2134` ``` from 7 have nbe: "numbound0 e" by simp ``` wenzelm@26932