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