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