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